# Quadratic variation of local martingales #

source
theorem ProbabilityTheory.IsLocalMartingale.isLocalSubmartingale_sq_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hX : IsLocalMartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
IsLocalSubmartingale (fun (t : ι) (ω : Ω) => ‖X t ω‖ ^ 2) 𝓕 P
source
noncomputable def ProbabilityTheory.quadraticVariation {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hX : IsLocalMartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) :
ι → Ω → ℝ

The quadratic variation of a local martingale, defined as the predictable part of the Doob-Meyer decomposition of its squared norm.

Equations

- ProbabilityTheory.quadraticVariation hX hX_cadlag = ProbabilityTheory.IsLocalSubmartingale.predictablePart (fun (t : ι) (ω : Ω) => ‖X t ω‖ ^ 2) ⋯ ⋯

Instances For