Local properties of processes

structure ProbabilityTheory.IsLocalizingSequence {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] (𝓕 : MeasureTheory.Filtration ι mΩ) (τ : ℕ → Ω → WithTop ι) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop

A localizing sequence is a sequence of stopping times that is almost surely increasing and tends almost surely to infinity.

• isStoppingTime (n : ℕ) : MeasureTheory.IsStoppingTime 𝓕 (τ n)
• mono : ∀ᵐ (ω : Ω) ∂P, Monotone fun (x : ℕ) => τ x ω
• tendsto_top : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ℕ) => τ x ω) Filter.atTop Filter.atTop

theorem ProbabilityTheory.isLocalizingSequence_const_top {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : IsLocalizingSequence 𝓕 (fun (x : ℕ) (x_1 : Ω) => ⊤) P

@[simp]

theorem ProbabilityTheory.stoppedProcess_const_top {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {X : ι → Ω → E} : (MeasureTheory.stoppedProcess X fun (x : Ω) => ⊤) = X

def ProbabilityTheory.Locally {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [Zero E] (p : (ι → Ω → E) → Prop) (𝓕 : MeasureTheory.Filtration ι mΩ) (X : ι → Ω → E) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop

A stochastic process X is said to satisfy a property p locally with respect to a filtration 𝓕 if there exists a localizing sequence (τ_n) such that for all n, the stopped process of fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i) satisfies p.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Locally.localSeq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] (hX : Locally p 𝓕 X P) : ℕ → Ω → WithTop ι

A localizing sequence, witness of the local property of the stochastic process.

Equations

• hX.localSeq = Exists.choose hX

theorem ProbabilityTheory.Locally.IsLocalizingSequence {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] (hX : Locally p 𝓕 X P) : ProbabilityTheory.IsLocalizingSequence 𝓕 hX.localSeq P

theorem ProbabilityTheory.Locally.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] (hX : Locally p 𝓕 X P) (n : ℕ) : p (MeasureTheory.stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < hX.localSeq n ω}.indicator (X i)) (hX.localSeq n))

theorem ProbabilityTheory.locally_of_prop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] (hp : p X) : Locally p 𝓕 X P

theorem ProbabilityTheory.Locally.mono {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [Zero E] (hpq : ∀ (X : ι → Ω → E), p X → q X) (hpX : Locally p 𝓕 X P) : Locally q 𝓕 X P

def ProbabilityTheory.IsStable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [LinearOrder ι] [OrderBot ι] [Zero E] (p : (ι → Ω → E) → Prop) (𝓕 : MeasureTheory.Filtration ι mΩ) : Prop

A property of stochastic processes is said to be stable if it is preserved under taking the stopped process by a stopping time.

Equations

• ProbabilityTheory.IsStable p 𝓕 = ∀ (X : ι → Ω → E), p X → ∀ (τ : Ω → WithTop ι), MeasureTheory.IsStoppingTime 𝓕 τ → p fun (i : ι) => {ω : Ω | ⊥ < τ ω}.indicator (X i)

theorem ProbabilityTheory.locally_and {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [Zero E] (hp : IsStable p 𝓕) (hq : IsStable q 𝓕) : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P

theorem ProbabilityTheory.locally_locally {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop} [Zero E] (hp : IsStable p 𝓕) : Locally (fun (Y : ι → Ω → E) => Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P

theorem ProbabilityTheory.locally_induction {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder ι] [OrderBot ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop} [Zero E] (hpq : ∀ (Y : ι → Ω → E), p Y → Locally q 𝓕 Y P) (hq : IsStable q 𝓕) (hpX : Locally p 𝓕 X P) : Locally q 𝓕 X P

If p implies q locally, then p locally implies q locally.