Second Moment of a Sum of Martingale Differences

Proved

LevyStochCalc.Probability.integral_sq_sum_of_condExp_eq_zero_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This theorem identifies the second moment of a finite sum of martingale differences with the sum of their second moments.

Let $P$ be a probability measure, let $(\mathcal G_k)_{k\in\mathbb N}$ be an increasing family of measurable spaces dominated by the ambient measurable space, and let $Y_k:\Omega\to\mathbb R$ . Assume every $Y_k$ is in $L^2(P)$ , is strongly measurable, and satisfies $\mathbb E[Y_k\mid\mathcal G_k]=0$ almost everywhere. For every $n\in\mathbb N$ ,

\int\left(\sum_{i<n}Y_i\right)^2dP =\sum_{i<n}\int Y_i^2\,dP.

This is the finite orthogonality identity used to control sums of centered stochastic increments.

Original Lean declaration header

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

theorem integral_sq_sum_of_condExp_eq_zero (n : ℕ) :
    ∫ ω, (∑ i ∈ Finset.range n, Y i ω) ^ 2 ∂P
      = ∑ i ∈ Finset.range n, ∫ ω, (Y i ω) ^ 2 ∂P

Module navigation

Module: LevyStochCalc/Probability/MartingaleDifference.

Supporting theorems: integral_sum_mul_of_condExp_eq_zero.

Previous: integral_sum_mul_of_condExp_eq_zero.

Source excerpt, lines 77–79 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Probability_MartingaleDifference

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Probability/MartingaleDifference.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory
variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
variable (𝒢 : ℕ → MeasurableSpace Ω) (h𝒢le : ∀ k, 𝒢 k ≤ mΩ) (h𝒢mono : Monotone 𝒢)
  (Y : ℕ → Ω → ℝ) (hY : ∀ k, MeasureTheory.MemLp (Y k) 2 P)
  (hYmeas : ∀ k, StronglyMeasurable[𝒢 (k + 1)] (Y k))
  (hYcond : ∀ k, P[Y k | 𝒢 k] =ᵐ[P] 0)
include h𝒢le h𝒢mono hY hYmeas hYcond

Formal statement


theorem LevyStochCalc.Probability.integral_sq_sum_of_condExp_eq_zero_readable (n : ℕ) :
    ∫ ω, (∑ i ∈ Finset.range n, Y i ω) ^ 2 ∂P
      = ∑ i ∈ Finset.range n, ∫ ω, (Y i ω) ^ 2 ∂P := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Probability/MartingaleDifference.lean#L74-L112 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Probability.MartingaleDifference`, declaration `LevyStochCalc.Probability.integral_sq_sum_of_condExp_eq_zero`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph