Simple-Level Compensated Square Martingale

This proves that the compensated square of a simple Brownian integral is a martingale. Let $P$ be a probability measure, let $W$ be a Brownian motion with Brownian filtration $\mathcal F$, let $T>0$, and let $G$ be a simple predictable integrand on horizon $T$. Assume every coefficient $G.\xi(i)$ is strongly measurable with respect to $\mathcal F_{G.\mathrm{partition}(i)}$. Then the process

is a martingale with respect to $\mathcal F$ and $P$. The compensator uses the interval $[0,t]$, which is empty when $t<0$.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

lemma martingale_simpleIntegral_sq_sub_compensator
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
    {T : ℝ} (hT : 0 < T) (G : SimplePredictable Ω T)
    (h_adapt : ∀ i : Fin G.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ (G.partition i.castSucc)) (G.ξ i)) :
    MeasureTheory.Martingale
      (fun t ω => (simpleIntegral W G t ω) ^ 2
        - ∫ u in Set.Icc (0 : ℝ) t, (G.eval u ω) ^ 2 ∂volume)
      ℱ P

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionCompensator.

Definition modules: LevyStochCalc/Brownian/ItoSimpleIntegrand, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Construction.

Supporting theorems: condExp_sq_increment_of_martingale, setIntegral_eval_sq_Icc_clamped, simpleIntegral_sub_sq_bochner_clamped_weighted.

Previous: setIntegral_eval_sq_Icc_clamped.

Source excerpt, lines 329–339 · Frozen source 408915f.