Localizing sequences of stopping times

The lemmas of this section with a name ending in ' are versions of the Mathlib lemmas of the same name without the hypothesis DenselyOrdered ι. They use IsStoppingTime.biInf'.

theorem ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf' {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [FirstCountableTopology ι] {τ : ℕ → Ω → WithTop ι} [𝓕.IsRightContinuous] (hτ : IsPreLocalizingSequence 𝓕 τ P) : IsLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) => ⨅ (j : ℕ), ⨅ (_ : j ≥ i), τ j ω) P

theorem ProbabilityTheory.isLocalizingSequence_of_isPreLocalizingSequence {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [FirstCountableTopology ι] {τ : ℕ → Ω → WithTop ι} (h𝓕 : 𝓕.IsRightContinuous) (hτ : IsPreLocalizingSequence 𝓕 τ P) : IsLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) => ⨅ (j : ℕ), ⨅ (_ : j ≥ i), τ j ω) P

theorem ProbabilityTheory.IsStable.locally_of_isPreLocalizingSequence' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] [FirstCountableTopology ι] {τ : ℕ → Ω → WithTop ι} (hp : IsStable 𝓕 p) [𝓕.IsRightContinuous] (hτ : IsPreLocalizingSequence 𝓕 τ P) (hpτ : ∀ (n : ℕ), p (MeasureTheory.stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ n ω}.indicator (X i)) (τ n))) : Locally p 𝓕 X P

A process X satisfies a stable property p locally if there exists a pre-localizing sequence τ for which the stopped processes of fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i) satisfy p.

theorem ProbabilityTheory.IsStable.exists_monotone_localSeq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] [FirstCountableTopology ι] [𝓕.IsRightContinuous] (hp : IsStable 𝓕 p) (hX : Locally p 𝓕 X P) : ∃ (τ : ℕ → Ω → WithTop ι), IsLocalizingSequence 𝓕 τ P ∧ (∀ (ω : Ω), Monotone fun (x : ℕ) => τ x ω) ∧ ∀ (n : ℕ), p (MeasureTheory.stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ n ω}.indicator (X i)) (τ n))

A stable property which holds locally holds along a localizing sequence which is monotone everywhere, and not only almost surely.

theorem ProbabilityTheory.IsStable.locally_locally_iff' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] [NoMaxOrder ι] [Zero E] [𝓕.IsRightContinuous] (hp : IsStable 𝓕 p) : Locally (fun (Y : ι → Ω → E) => Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P

A stable property holding locally is idempotent.

theorem ProbabilityTheory.IsStable.locally_induction' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] [NoMaxOrder ι] [Zero E] [𝓕.IsRightContinuous] (hq : IsStable 𝓕 q) (hpq : ∀ (Y : ι → Ω → E), p Y → Locally q 𝓕 Y P) (hpX : Locally p 𝓕 X P) : Locally q 𝓕 X P

If q is a stable property and p implies q locally, then p locally implies q locally.

theorem ProbabilityTheory.IsStable.locally_induction₂' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] [NoMaxOrder ι] [Zero E] {r : (ι → Ω → E) → Prop} [𝓕.IsRightContinuous] (hrpq : ∀ (Y : ι → Ω → E), r Y → p Y → Locally q 𝓕 Y P) (hr : IsStable 𝓕 r) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q) (hrX : Locally r 𝓕 X P) (hpX : Locally p 𝓕 X P) : Locally q 𝓕 X P

If p, q, r are stable properties and r and p implies locally q, then r locally and p locally imply q locally.

noncomputable def ProbabilityTheory.LocalizingSequenceOfProp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] (X : ι → Ω → E) (p : (ι → E) → Prop) : ℕ → Ω → WithTop ι

Given a property on paths which holds almost surely for a stochastic process, we construct a localizing sequence by setting the stopping time to be ∞ whenever the property holds.

Equations

• ProbabilityTheory.LocalizingSequenceOfProp X p = Function.const ℕ fun (ω : Ω) => if p fun (x : ι) => X x ω then ⊤ else ⊥

theorem ProbabilityTheory.isStoppingTime_ae_const {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsComplete P] (τ : Ω → WithTop ι) (c : WithTop ι) (hτ : τ =ᵐ[P] Function.const Ω c) : MeasureTheory.IsStoppingTime 𝓕 τ

theorem ProbabilityTheory.isLocalizingSequence_localizingSequenceOfProp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace ι] [OrderTopology ι] [𝓕.IsComplete P] {p : (ι → E) → Prop} (hpX : ∀ᵐ (ω : Ω) ∂P, p fun (x : ι) => X x ω) : IsLocalizingSequence 𝓕 (LocalizingSequenceOfProp X p) P