Localizing sequences of stopping times #
theorem
ProbabilityTheory.isLocalizingSequence_of_isPreLocalizingSequence
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
[NoMaxOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{τ : ℕ → Ω → WithTop ι}
(h𝓕 : 𝓕.IsRightContinuous)
(hτ : IsPreLocalizingSequence 𝓕 τ P)
:
IsLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) => ⨅ (j : ℕ), ⨅ (_ : j ≥ i), τ j ω) P
theorem
ProbabilityTheory.isPreLocalizingSequence_of_isLocalizingSequence
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[SecondCountableTopology ι]
[MeasureTheory.IsFiniteMeasure P]
[NoMaxOrder ι]
{τ : ℕ → Ω → WithTop ι}
{σ : ℕ → ℕ → Ω → WithTop ι}
(hτ : IsLocalizingSequence 𝓕 τ P)
(hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P)
:
∃ (nk : ℕ → ℕ), StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun (i : ℕ) (ω : Ω) => min (τ i ω) (σ i (nk i) ω)) P
noncomputable def
ProbabilityTheory.LocalizingSequenceOfProp
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
(X : ι → Ω → E)
(p : (ι → E) → Prop)
:
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 ⊥
Instances For
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)
:
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