theorem MeasureTheory.StronglyAdapted.isStronglyProgressive_of_rightContinuous {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} {mΩ : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] {X : ι → Ω → β} {𝓕 : Filtration ι mΩ} (h : StronglyAdapted 𝓕 X) (hu_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) :
def MeasureTheory.AEStronglyAdapted {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] [TopologicalSpace E] (X : ι → Ω → E) (𝓕 : Filtration ι mΩ) (P : Measure Ω) :
A stochastic process is a.e. strongly adapted if it is undistinguishable from a strongly adapted process.
Equations
- MeasureTheory.AEStronglyAdapted X 𝓕 P = ∃ (Y : ι → Ω → E), MeasureTheory.StronglyAdapted 𝓕 Y ∧ X ≡ᵐ[P] Y
Instances For
theorem MeasureTheory.AEStronglyAdapted.congr {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] (hX : AEStronglyAdapted X 𝓕 P) (h : X ≡ᵐ[P] Y) :
AEStronglyAdapted Y 𝓕 P
theorem MeasureTheory.StronglyAdapted.aestronglyAdapted {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] (hX : StronglyAdapted 𝓕 X) :
AEStronglyAdapted X 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.const {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {P : Measure Ω} [TopologicalSpace E] {c : E} :
AEStronglyAdapted (fun (x : ι) (x_1 : Ω) => c) 𝓕 P
noncomputable def MeasureTheory.AEStronglyAdapted.mk {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {P : Measure Ω} [TopologicalSpace E] (X : ι → Ω → E) (hX : AEStronglyAdapted X 𝓕 P) :
ι → Ω → E
Given a hX : AEStronglyAdapted process X, hX.mk X is a strongly adapted process
that is indistinguishable from X.
Equations
Instances For
theorem MeasureTheory.AEStronglyAdapted.stronglyAdapted_mk {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] (hX : AEStronglyAdapted X 𝓕 P) :
StronglyAdapted 𝓕 (mk X hX)
theorem MeasureTheory.AEStronglyAdapted.indist_mk {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] (hX : AEStronglyAdapted X 𝓕 P) :
theorem MeasureTheory.Continuous.comp_stronglyAdapted {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] {F : Type u_7} [TopologicalSpace F] {g : E → F} (hg : Continuous g) (hX : StronglyAdapted 𝓕 X) :
StronglyAdapted 𝓕 fun (t : ι) => g ∘ X t
theorem MeasureTheory.Continuous.comp_aestronglyAdapted {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] {F : Type u_7} [TopologicalSpace F] {g : E → F} (hg : Continuous g) (hX : AEStronglyAdapted X 𝓕 P) :
AEStronglyAdapted (fun (t : ι) => g ∘ X t) 𝓕 P
theorem MeasureTheory.StronglyAdapted.prodMk {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] {F : Type u_7} [TopologicalSpace F] {Y : ι → Ω → F} (hX : StronglyAdapted 𝓕 X) (hY : StronglyAdapted 𝓕 Y) :
StronglyAdapted 𝓕 fun (t : ι) (ω : Ω) => (X t ω, Y t ω)
theorem MeasureTheory.AEStronglyAdapted.prodMk {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] {F : Type u_7} [TopologicalSpace F] {Y : ι → Ω → F} (hX : AEStronglyAdapted X 𝓕 P) (hY : AEStronglyAdapted Y 𝓕 P) :
AEStronglyAdapted (fun (t : ι) (ω : Ω) => (X t ω, Y t ω)) 𝓕 P
theorem MeasureTheory.StronglyAdapted.const_smul {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] {R : Type u_7} [SMul R E] [ContinuousConstSMul R E] {c : R} (hX : StronglyAdapted 𝓕 X) :
StronglyAdapted 𝓕 (c • X)
theorem MeasureTheory.StronglyAdapted.const_vadd {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [TopologicalSpace E] {R : Type u_7} [VAdd R E] [ContinuousConstVAdd R E] {c : R} (hX : StronglyAdapted 𝓕 X) :
StronglyAdapted 𝓕 (c +ᵥ X)
theorem MeasureTheory.AEStronglyAdapted.const_smul {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] {R : Type u_7} [SMul R E] [ContinuousConstSMul R E] {c : R} (hX : AEStronglyAdapted X 𝓕 P) :
AEStronglyAdapted (c • X) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.const_vadd {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] {R : Type u_7} [VAdd R E] [ContinuousConstVAdd R E] {c : R} (hX : AEStronglyAdapted X 𝓕 P) :
AEStronglyAdapted (c +ᵥ X) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.mul {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [Mul E] [ContinuousMul E] (hX : AEStronglyAdapted X 𝓕 P) (hY : AEStronglyAdapted Y 𝓕 P) :
AEStronglyAdapted (X * Y) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.add {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [Add E] [ContinuousAdd E] (hX : AEStronglyAdapted X 𝓕 P) (hY : AEStronglyAdapted Y 𝓕 P) :
AEStronglyAdapted (X + Y) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.inv {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [Group E] [ContinuousInv E] (hX : AEStronglyAdapted X 𝓕 P) :
AEStronglyAdapted X⁻¹ 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.neg {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [AddGroup E] [ContinuousNeg E] (hX : AEStronglyAdapted X 𝓕 P) :
AEStronglyAdapted (-X) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.div' {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [Div E] [ContinuousDiv E] (hX : AEStronglyAdapted X 𝓕 P) (hY : AEStronglyAdapted Y 𝓕 P) :
AEStronglyAdapted (X / Y) 𝓕 P
theorem MeasureTheory.AEStronglyAdapted.sub {Ω : Type u_4} {ι : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} [Preorder ι] {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} {P : Measure Ω} [TopologicalSpace E] [Sub E] [ContinuousSub E] (hX : AEStronglyAdapted X 𝓕 P) (hY : AEStronglyAdapted Y 𝓕 P) :
AEStronglyAdapted (X - Y) 𝓕 P