theorem MeasureTheory.isStoppingTime_piecewise_top {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {τ : Ω → WithTop ι} {A : Set Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} [DecidablePred fun (x : Ω) => x ∈ A] (hτ : IsStoppingTime 𝓕 τ) (hA : MeasurableSet A) : IsStoppingTime 𝓕 (A.piecewise τ fun (x : Ω) => ⊤)

@[instance_reducible]

def MeasureTheory.leftMeasurableSpace {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι mΩ) (τ : Ω → WithTop ι) : MeasurableSpace Ω

The measurable space of the strict past before τ.

Equations

• MeasureTheory.leftMeasurableSpace 𝓕 τ = ↑𝓕 ⊥ ⊔ MeasurableSpace.generateFrom {s : Set Ω | ∃ (A : Set Ω) (t : ι), MeasurableSet A ∧ s = A ∩ {ω : Ω | ↑t < τ ω}}

def MeasureTheory.IsPredictableTime {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι mΩ) (τ : Ω → WithTop ι) : Prop

A predictable time is a random time whose graph is a predictable set.

Equations

• MeasureTheory.IsPredictableTime 𝓕 τ = MeasurableSet (ProbabilityTheory.stochIco τ fun (x : Ω) => ⊤)

theorem MeasureTheory.IsPredictableTime.isStoppingTime {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {τ : Ω → WithTop ι} [Preorder ι] {𝓕 : Filtration ι mΩ} [OrderBot ι] (hτ : IsPredictableTime 𝓕 τ) : IsStoppingTime 𝓕 τ

A predictable time is a stopping time.

structure MeasureTheory.IsAccessibleTime {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι mΩ) (τ : Ω → WithTop ι) : Prop

An accessible time is a stopping time whose graph is contained in the union of the graphs a sequence of predictable times.

• isStoppingTime : IsStoppingTime 𝓕 τ
• stochIco_subset : ∃ (σ : ℕ → Ω → WithTop ι), (∀ (n : ℕ), IsPredictableTime 𝓕 (σ n)) ∧ ProbabilityTheory.stochGraph τ ⊆ ⋃ (n : ℕ), ProbabilityTheory.stochGraph (σ n)

structure MeasureTheory.IsInacessibleTime {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] [Preorder ι] [OrderBot ι] (𝓕 : Filtration ι mΩ) (τ : Ω → WithTop ι) (P : Measure Ω) : Prop

An inaccessible time is a stopping time τ such that for any predictable time σ, P(σ = τ < ⊤) = 0.

• isStoppingTime : IsStoppingTime 𝓕 τ
• measure_eq_lt_top_eq_zero (σ : Ω → WithTop ι) : IsPredictableTime 𝓕 σ → P {ω : Ω | τ ω = σ ω ∧ σ ω < ⊤} = 0

theorem MeasureTheory.Set.iInter_prod {α : Type u_3} {β : Type u_4} {ι : Type u_5} {s : Set α} {t : ι → Set β} [hι : Nonempty ι] : (⋂ (i : ι), t i) ×ˢ s = ⋂ (i : ι), t i ×ˢ s

theorem MeasureTheory.IsPredictableTime.const {ι : Type u_1} {Ω : Type u_2} [mΩ : MeasurableSpace Ω] [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] (𝓕 : Filtration ι mΩ) (t : WithTop ι) : IsPredictableTime 𝓕 fun (x : Ω) => t

A constant time is predictable.

theorem MeasureTheory.IsStoppingTime.measurableSet_lt_top {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {τ : Ω → WithTop ι} [LinearOrder ι] [OrderBot ι] {𝓕 : Filtration ι mΩ} (hτ : IsStoppingTime 𝓕 τ) [TopologicalSpace ι] [OrderTopology ι] [TopologicalSpace.SeparableSpace ι] : MeasurableSet {ω : Ω | τ ω < ⊤}

theorem MeasureTheory.IsStoppingTime.decompositon {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {τ : Ω → WithTop ι} [LinearOrder ι] [OrderBot ι] {𝓕 : Filtration ι mΩ} {P : Measure Ω} [(ω : Ω) → (s : Set Ω) → Decidable (ω ∈ s)] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [IsFiniteMeasure P] (hτ : IsStoppingTime 𝓕 τ) : ∃ (A : Set Ω), MeasurableSet A ∧ A ⊆ {ω : Ω | τ ω < ⊤} ∧ IsAccessibleTime 𝓕 (A.piecewise τ fun (x : Ω) => ⊤) ∧ IsInacessibleTime 𝓕 (Aᶜ.piecewise τ fun (x : Ω) => ⊤) P

For a stopping time τ, there exists a set A that is 𝓕 τ-measurable and such that τ_A is accessible while τ_Aᶜ is inaccessible, where τ_A is the stopping time which coincides with τ over A and is infinite elsewhere.