Local properties of processes #
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 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
@[simp]
theorem
ProbabilityTheory.stoppedProcess_const_top
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
{X : ι → Ω → E}
[OrderBot ι]
:
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 ι]
{𝓕 : 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
{ι : 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)
:
theorem
ProbabilityTheory.Locally.stoppedProcess
{ι : 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.of_and_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.of_and_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Ω}
[OrderBot ι]
[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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{p : (ι → Ω → E) → Prop}
[OrderBot ι]
[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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[OrderBot ι]
[Zero E]
[TopologicalSpace ι]
[OrderTopology ι]
(hp : IsStable 𝓕 p)
(hq : IsStable 𝓕 q)
:
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.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.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
theorem
ProbabilityTheory.locally_locally
{ι : 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]
(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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
{p q : (ι → Ω → E) → Prop}
[SecondCountableTopology ι]
[MeasureTheory.IsFiniteMeasure P]
[DenselyOrdered ι]
[NoMaxOrder ι]
[Zero E]
(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.
noncomputable def
ProbabilityTheory.LocalizingSequence_of_prop
{ι : 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.LocalizingSequence_of_prop 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 Ω}
[LinearOrder ι]
[OrderBot ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
[𝓕.HasUsualConditions P]
(τ : Ω → WithTop ι)
(c : WithTop ι)
(hτ : τ =ᵐ[P] Function.const Ω c)
:
theorem
ProbabilityTheory.isLocalizingSequence_ae
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
(𝓕 : MeasureTheory.Filtration ι mΩ)
(P : MeasureTheory.Measure Ω)
[𝓕.HasUsualConditions P]
{p : (ι → E) → Prop}
(hpX : ∀ᵐ (ω : Ω) ∂P, p fun (x : ι) => X x ω)
:
theorem
ProbabilityTheory.locally_of_ae
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup 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
theorem
ProbabilityTheory.Locally.rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace E]
(hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) 𝓕 X P)
:
∀ᵐ (ω : Ω) ∂P, Function.RightContinuous fun (x : ι) => X x ω
theorem
ProbabilityTheory.locally_rightContinuous_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace E]
:
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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace 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_left_limit_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace E]
:
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 ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace E]
(hX : Locally (fun (X : ι → Ω → E) => ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) 𝓕 X P)
:
theorem
ProbabilityTheory.locally_isCadlag_iff
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
{X : ι → Ω → E}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[𝓕.HasUsualConditions P]
[NormedSpace ℝ E]
[CompleteSpace E]
:
theorem
ProbabilityTheory.isStable_rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
IsStable 𝓕 fun (X : ι → Ω → E) => ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω
theorem
ProbabilityTheory.isStable_left_limit
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
IsStable 𝓕 fun (X : ι → Ω → E) =>
∀ (ω : Ω) (x : ι), ∃ (l : E), Filter.Tendsto (fun (x : ι) => X x ω) (nhdsWithin x (Set.Iio x)) (nhds l)
theorem
ProbabilityTheory.isStable_isCadlag
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[LinearOrder ι]
[OrderBot ι]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[TopologicalSpace ι]
[OrderTopology ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
:
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]
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasureTheory.IsFiniteMeasure P]
{𝓕 : MeasureTheory.Filtration ι mΩ}
[𝓕.HasUsualConditions P]
{X : ι → Ω → E}
: