Local properties of processes #
theorem
ProbabilityTheory.locally_and_of_isStable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[Zero E]
[TopologicalSpace ι]
[LinearOrder ι]
[OrderBot ι]
[OrderTopology ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
(hp : IsStable 𝓕 p)
(hpX : p X)
(hqX : 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}
[𝓕.IsComplete 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.IsRightContinuous fun (x : ι) => X x ω) 𝓕 X P)
:
∀ᵐ (ω : Ω) ∂P, Function.IsRightContinuous 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.IsRightContinuous 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]
[𝓕.IsComplete P]
:
Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.IsRightContinuous fun (x : ι) => X x ω) 𝓕 X P ↔ ∀ᵐ (ω : Ω) ∂P, Function.IsRightContinuous 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]
[𝓕.IsComplete 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]
[𝓕.IsComplete 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Ω}
[𝓕.IsComplete P]
[𝓕.IsRightContinuous]
{X : ι → Ω → E}
:
theorem
ProbabilityTheory.rightContinuous_indicator
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
{X : ι → Ω → E}
[TopologicalSpace ι]
(hC : ∀ (ω : Ω), Function.IsRightContinuous fun (x : ι) => X x ω)
(s : Set Ω)
(ω : Ω)
:
Function.IsRightContinuous 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.isStronglyProgressive_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.IsStronglyProgressive 𝓕 X)
{τ : Ω → WithTop ι}
(hτ : MeasureTheory.IsStoppingTime 𝓕 τ)
:
theorem
ProbabilityTheory.isStable_isStronglyProgressive
{ι : 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.IsStronglyProgressive 𝓕 x
The class of strongly progressive processes is stable.