Conditional Pythagoras for Square-Integrable Martingales

This lemma gives the conditional Pythagorean identity for an $L^2$ martingale.

Let $P$ be a probability measure, let $\mathcal F$ be a filtration, and let $M_t:\Omega\to\mathbb R$ be a martingale with respect to $\mathcal F$ and $P$. For times $s\le t$, assume $M_s,M_t\in L^2(P)$. Then, almost everywhere with respect to $P$,

The conditional expectations are represented by condExp, and the equality is an almost-everywhere equality. This identity is a general tool for analyzing squared increments of square-integrable martingales.

Original Lean declaration header

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

lemma condExp_sq_increment_of_martingale
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
    {M : ℝ → Ω → ℝ}
    (hmart : MeasureTheory.Martingale M ℱ P)
    {s t : ℝ} (hMs : MeasureTheory.MemLp (M s) 2 P) (hMt : MeasureTheory.MemLp (M t) 2 P)
    (hst : s ≤ t) :
    P[(fun ω => (M t ω - M s ω) ^ 2) | ℱ s]
      =ᵐ[P] fun ω => (P[(fun ω => (M t ω) ^ 2) | ℱ s]) ω - (M s ω) ^ 2

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionConvergence.

Previous: tendsto_eLpNorm_one_sq_sub · Next: integral_factor_increment_sq.

Source excerpt, lines 301–309 · Frozen source 408915f.