Localizing sequences of stopping times #
structure
ProbabilityTheory.IsPreLocalizingSequence
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[TopologicalSpace ι]
[OrderTopology ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(τ : ℕ → Ω → WithTop ι)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
A pre-localizing sequence is a sequence of stopping times that tends almost surely to infinity.
- isStoppingTime (n : ℕ) : MeasureTheory.IsStoppingTime 𝓕 (τ n)
- tendsto_top : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ℕ) => τ x ω) Filter.atTop (nhds ⊤)
Instances For
structure
ProbabilityTheory.IsLocalizingSequence
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[TopologicalSpace ι]
[OrderTopology ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(τ : ℕ → Ω → WithTop ι)
(P : MeasureTheory.Measure Ω := by volume_tac)
extends ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P :
A localizing sequence is a sequence of stopping times that is almost surely increasing and tends almost surely to infinity.
- tendsto_top : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ℕ) => τ x ω) Filter.atTop (nhds ⊤)
Instances For
theorem
ProbabilityTheory.isLocalizingSequence_const_top
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
[Preorder ι]
[TopologicalSpace ι]
[OrderTopology ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
:
IsLocalizingSequence 𝓕 (fun (x : ℕ) (x_1 : Ω) => ⊤) P
theorem
ProbabilityTheory.IsLocalizingSequence.min
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
{τ σ : ℕ → Ω → WithTop ι}
(hτ : IsLocalizingSequence 𝓕 τ P)
(hσ : IsLocalizingSequence 𝓕 σ P)
:
IsLocalizingSequence 𝓕 (τ ⊓ σ) P
theorem
ProbabilityTheory.measure_iInter_of_ae_antitone
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
[Countable ι]
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{s : ι → Set Ω}
(hs : ∀ᵐ (ω : Ω) ∂P, Antitone fun (x : ι) => s x ω)
(hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) P)
(hfin : ∃ (i : ι), P (s i) ≠ ⊤)
:
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_aux'
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[SecondCountableTopology ι]
[MeasureTheory.IsFiniteMeasure P]
{τ : ℕ → Ω → WithTop ι}
{σ : ℕ → ℕ → Ω → WithTop ι}
(hτ : IsLocalizingSequence 𝓕 τ P)
(hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P)
:
∃ (T : ℕ → ι),
Filter.Tendsto T Filter.atTop Filter.atTop ∧ ∀ (n : ℕ), ∃ (k : ℕ), P {ω : Ω | σ n k ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
Auxliary defintion for isPreLocalizingSequence_of_isLocalizingSequence which constructs a
strictly increasing sequence from a given sequence.
Equations
- ProbabilityTheory.mkStrictMonoAux x 0 = x 0
- ProbabilityTheory.mkStrictMonoAux x n.succ = max (x (n + 1)) (ProbabilityTheory.mkStrictMonoAux x n) + 1
Instances For
theorem
ProbabilityTheory.isPreLocalizingSequence_of_isLocalizingSequence_aux
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[SecondCountableTopology ι]
[MeasureTheory.IsFiniteMeasure P]
{τ : ℕ → Ω → WithTop ι}
{σ : ℕ → ℕ → Ω → WithTop ι}
(hτ : IsLocalizingSequence 𝓕 τ P)
(hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P)
:
∃ (nk : ℕ → ℕ),
StrictMono nk ∧ ∃ (T : ℕ → ι),
Filter.Tendsto T Filter.atTop Filter.atTop ∧ ∀ (n : ℕ), P {ω : Ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[𝓕.HasUsualConditions 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 ι]
[𝓕.HasUsualConditions P]
{p : (ι → E) → Prop}
(hpX : ∀ᵐ (ω : Ω) ∂P, p fun (x : ι) => X x ω)
:
IsLocalizingSequence 𝓕 (LocalizingSequenceOfProp X p) P