theorem
MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
{𝓕 : Filtration ι mΩ}
[NoMaxOrder ι]
{τ : Ω → WithTop ι}
(h𝓕 : 𝓕.IsRightContinuous)
(hτ : ∀ (i : ι), MeasurableSet {ω : Ω | τ ω < ↑i})
:
IsStoppingTime 𝓕 τ
theorem
MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous'
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
{𝓕 : Filtration ι mΩ}
{τ : Ω → WithTop ι}
(h𝓕 : 𝓕.IsRightContinuous)
(hτ1 : ∀ (i : ι), ¬IsMax i → MeasurableSet {ω : Ω | τ ω < ↑i})
(hτ2 : ∀ (i : ι), IsMax i → MeasurableSet {ω : Ω | τ ω ≤ ↑i})
:
IsStoppingTime 𝓕 τ
theorem
MeasureTheory.IsStoppingTime.iInf
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
[NoMaxOrder ι]
{𝓕 : Filtration ι mΩ}
{τ : ℕ → Ω → WithTop ι}
(s : Set ℕ)
(h𝓕 : 𝓕.IsRightContinuous)
(hτ : ∀ (n : ℕ), IsStoppingTime 𝓕 (τ n))
:
IsStoppingTime 𝓕 fun (ω : Ω) => ⨅ n ∈ s, τ n ω
theorem
MeasureTheory.stoppedProcess_min_eq_stoppedProcess
{ι : Type u_4}
{Ω : Type u_5}
{E : Type u_6}
[Nonempty ι]
[LinearOrder ι]
(X : ι → Ω → E)
(τ : Ω → WithTop ι)
{i j : ι}
(hij : i ≤ j)
: