Local properties of processes #
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 of 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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[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
{ι : 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}
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally p 𝓕 X 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}
[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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P)
:
theorem
ProbabilityTheory.Locally.of_and_left
{ι : 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}
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
(hX : Locally (fun (Y : ι → Ω → E) => p Y ∧ q Y) 𝓕 X P)
:
Locally p 𝓕 X P
theorem
ProbabilityTheory.Locally.of_and_right
{ι : 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}
[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 ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[Zero E]
(p q : (ι → Ω → E) → Prop)
(hp : IsStable 𝓕 p)
(hq : IsStable 𝓕 q)
:
theorem
ProbabilityTheory.IsStable.isStable_locally
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{p : (ι → Ω → E) → Prop}
[Zero E]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
:
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]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
(hq : IsStable 𝓕 q)
:
theorem
ProbabilityTheory.locally_and_of_isStable
{ι : 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]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
(hpX : p X)
(hqX : Locally q 𝓕 X P)
:
theorem
ProbabilityTheory.locally_of_isPreLocalizingSequence
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
[NoMaxOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[Zero E]
{τ : ℕ → Ω → WithTop ι}
(hp : IsStable 𝓕 p)
(h𝓕 : 𝓕.IsRightContinuous)
(hτ : IsPreLocalizingSequence 𝓕 τ P)
(hpτ : ∀ (n : ℕ), p (MeasureTheory.stoppedProcess (fun (i : ι) => {ω : Ω | ⊥ < τ n ω}.indicator (X i)) (τ n)))
:
Locally p 𝓕 X P
A stable property holds locally p for X if there exists a pre-localizing sequence τ for
which the stopped process of fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i) satisfies p.
theorem
ProbabilityTheory.locally_locally
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NoMaxOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p : (ι → Ω → E) → Prop}
[SecondCountableTopology ι]
[DenselyOrdered ι]
[Zero E]
[MeasureTheory.IsFiniteMeasure P]
(h𝓕 : 𝓕.IsRightContinuous)
(hp : IsStable 𝓕 p)
:
A stable property holding locally is idempotent.
theorem
ProbabilityTheory.locally_induction
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NoMaxOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[SecondCountableTopology ι]
[DenselyOrdered ι]
[Zero E]
[MeasureTheory.IsFiniteMeasure P]
(h𝓕 : 𝓕.IsRightContinuous)
(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.
theorem
ProbabilityTheory.locally_induction₂
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[NoMaxOrder ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[SecondCountableTopology ι]
[DenselyOrdered ι]
[Zero E]
[MeasureTheory.IsFiniteMeasure P]
{r : (ι → Ω → E) → Prop}
(h𝓕 : 𝓕.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
theorem
ProbabilityTheory.locally_of_ae
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[𝓕.HasUsualConditions P]
{p : (ι → E) → Prop}
(hpX : ∀ᵐ (ω : Ω) ∂P, p fun (x : ι) => X x ω)
(hp₀ : p 0)
:
Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), p fun (x : ι) => X x ω) 𝓕 X P
If the filtration satisfies the usual conditions, then a property of the paths of a process that holds almost surely holds locally.
theorem
ProbabilityTheory.Locally.rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
(hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) 𝓕 X P)
:
∀ᵐ (ω : Ω) ∂P, Function.RightContinuous fun (x : ι) => X x ω
theorem
ProbabilityTheory.Locally.left_limit
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
(hX :
Locally
(fun (X : ι → Ω → E) =>
∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l))
𝓕 X P)
:
∀ᵐ (ω : Ω) ∂P, ∀ (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)
theorem
ProbabilityTheory.Locally.isCadlag
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
(hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P)
:
theorem
ProbabilityTheory.isStable_rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace E]
:
IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω
The processes with right-continuous paths are a stable class.
theorem
ProbabilityTheory.isStable_left_limit
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace E]
:
IsStable 𝓕 fun (X : ι → Ω → E) =>
∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)
The processes with left limits are a stable class.
theorem
ProbabilityTheory.isStable_isCadlag
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace E]
:
The càdlàg processes are a stable class.
theorem
ProbabilityTheory.locally_rightContinuous_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
[𝓕.HasUsualConditions P]
:
Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, Function.RightContinuous fun (x : ι) => X x ω
theorem
ProbabilityTheory.locally_left_limit_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
[𝓕.HasUsualConditions P]
:
Locally
(fun (X : ι → Ω → E) =>
∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l))
𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, ∀ (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)
theorem
ProbabilityTheory.locally_isCadlag_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[Zero E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace E]
[𝓕.HasUsualConditions P]
:
theorem
ProbabilityTheory.locally_isCadlag_iff_locally_ae
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[ConditionallyCompleteLinearOrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
[DenselyOrdered ι]
[NoMaxOrder ι]
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure P]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[𝓕.HasUsualConditions P]
{X : ι → Ω → E}
:
theorem
ProbabilityTheory.rightContinuous_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
{X : ι → Ω → E}
[TopologicalSpace ι]
(hC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
(s : Set Ω)
(ω : Ω)
:
Function.RightContinuous fun (t : ι) => s.indicator (X t) ω
theorem
ProbabilityTheory.stronglyAdapted_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[NormedAddCommGroup E]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
(hX : MeasureTheory.StronglyAdapted 𝓕 X)
{τ : Ω → WithTop ι}
(hτ : MeasureTheory.IsStoppingTime 𝓕 τ)
:
theorem
ProbabilityTheory.progMeasurable_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[NormedAddCommGroup E]
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[OrderBot ι]
[MeasurableSpace ι]
(hX : MeasureTheory.ProgMeasurable 𝓕 X)
{τ : Ω → WithTop ι}
(hτ : MeasureTheory.IsStoppingTime 𝓕 τ)
:
theorem
ProbabilityTheory.isStable_progMeasurable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[NormedAddCommGroup E]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[SecondCountableTopology ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
[OrderBot ι]
[OrderTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
:
IsStable 𝓕 fun (x : ι → Ω → E) => MeasureTheory.ProgMeasurable 𝓕 x
The class of progressively measurable processes is stable.