Quadratic variation of locally square-integrable martingales #
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Ω}
[MeasureTheory.SigmaFiniteFiltration P 𝓕]
(hX_sq : IsLocallySquareIntegrable X 𝓕 P)
(hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω)
:
ι → Ω → ℝ
The quadratic variation of a locally square-integrable martingale, defined as the predictable part of the Doob-Meyer decomposition of its squared norm.
Equations
- ProbabilityTheory.quadraticVariation hX_sq hX_cadlag = ProbabilityTheory.IsLocalSubmartingale.predictablePart (fun (t : ι) (ω : Ω) => ‖X t ω‖ ^ 2) ⋯ ⋯