source
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 𝓕 τ
source
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 𝓕 τ
source
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 ω
source
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) :
stoppedProcess X (fun (ω : Ω) => min (↑j) (τ ω)) i = stoppedProcess X τ i