Local properties of processes #
This file defines local and stable properties of stochastic processes with respect to a filtration. This is notably useful for local martingales.
Main definitions #
IsPreLocalizingSequence: A pre-localizing sequence is a sequence of stopping times which tends almost surely to infinity.IsLocalizingSequence: A localizing sequence is a pre-localizing sequence which is almost surely non-decreasing.Locally: A stochastic processXis said to satisfy a propertyplocally with respect to a filtration𝓕if there exists a localizing sequence(τ n)such that for alln, the stopped processX^{τ n} I_{τ n > ⊥}satisfiesp.IsStable: A property of stochastic processes is said to be stable if it is preserved under taking the stopped processX^{τ} I_{τ > ⊥}by a stopping timeτ.
Main results #
IsStable.isStable_locally: If a propertypis stable, then the property "satisfiesplocally" is also stable.IsPreLocalizingSequence.isLocalizingSequence_biInf: Given a pre-localizing sequence(τ n), the sequence⊓ j ≥ n, τ jis a localizing sequence.IsStable.locally_of_isPreLocalizingSequence: If a propertypis stable, then to prove thatXsatisfiesplocally, one can replace the localizing sequence in the definition of "locally" by a pre-localizing sequence.IsStable.locally_locally: For stable properties, locally is idempotent.IsStable.locally_induction: Ifqis a stable property, andpimplies locallyq, then locallypimplies locallyq.
Tags #
localizing sequence, local property, stable property
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
def
ProbabilityTheory.Locally
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(p : (ι → Ω → E) → Prop)
(𝓕 : MeasureTheory.Filtration ι mΩ)
(X : ι → Ω → E)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
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 fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i) satisfies p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ProbabilityTheory.Locally.localSeq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally p 𝓕 X P)
:
A localizing sequence, witness of the local property of the stochastic process.
Equations
- hX.localSeq = Exists.choose hX
Instances For
theorem
ProbabilityTheory.Locally.isLocalizingSequence_localSeq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally p 𝓕 X P)
:
IsLocalizingSequence 𝓕 hX.localSeq P
theorem
ProbabilityTheory.Locally.stoppedProcess_localSeq
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally p 𝓕 X P)
(n : ℕ)
:
theorem
ProbabilityTheory.Locally.of_prop
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hpq : ∀ (X : ι → Ω → E), p X → q X)
(hpX : Locally p 𝓕 X P)
:
Locally q 𝓕 X P
theorem
ProbabilityTheory.Locally.of_and
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P)
:
theorem
ProbabilityTheory.Locally.left
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P)
:
Locally p 𝓕 X P
theorem
ProbabilityTheory.Locally.right
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 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]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(p : (ι → Ω → E) → 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.IsStable.and
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[Zero E]
(hp : IsStable 𝓕 p)
(hq : IsStable 𝓕 q)
:
theorem
ProbabilityTheory.IsStable.locally
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[Zero E]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
:
theorem
ProbabilityTheory.IsStable.locally_and_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[Zero E]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
(hq : IsStable 𝓕 q)
:
theorem
ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[DenselyOrdered ι]
[FirstCountableTopology ι]
[NoMaxOrder ι]
{τ : ℕ → Ω → WithTop ι}
[𝓕.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]
[DenselyOrdered ι]
[FirstCountableTopology ι]
[NoMaxOrder ι]
{τ : ℕ → Ω → 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.IsLocalizingSequence.isPrelocalizingSequence_inf_extraction
{ι : 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
@[simp]
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]
[DenselyOrdered ι]
[NoMaxOrder ι]
[Zero E]
[𝓕.IsRightContinuous]
(hp : IsStable 𝓕 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]
[DenselyOrdered ι]
[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]
[DenselyOrdered ι]
[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.