Quadratic variation of local martingales #
theorem
ProbabilityTheory.IsLocalMartingale.isLocalSubmartingale_sq_norm
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[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
noncomputable def
ProbabilityTheory.quadraticVariation
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[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) ⋯ ⋯