Second-Moment Recursion for Partial Sums

Proved

LevyStochCalc.Brownian.Ito.SimplePredictable.integral_partialSum_sq_succ_readable

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

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

This theorem gives the one-step second-moment recursion for partial sums of a simple predictable Brownian integral.

Let $G$ be a simple predictable integrand with strongly measurable coefficients, let $W$ be a Brownian motion with Brownian filtration $\mathcal F$ , and assume:

$C\ge0$ ;
every coefficient satisfies $|\xi_i(\omega)|\le C$ ;
$k<N$ , where $N$ is the number of tiles.

If $S_k=\texttt{G.partialSum}(W,k)$ , $\xi_k$ is the $k$ th coefficient, and $\tau_k,\tau_{k+1}$ are the corresponding partition times, then

\int S_{k+1}^2\,dP =\int S_k^2\,dP+(\tau_{k+1}-\tau_k)\int \xi_k^2\,dP.

The result is the basic variance recursion for elementary Brownian integrals.

Original Lean declaration header

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

theorem integral_partialSum_sq_succ {k : ℕ} (hk : k < G.N) :
    ∫ ω, (G.partialSum W (k + 1) ω) ^ 2 ∂P
      = (∫ ω, (G.partialSum W k ω) ^ 2 ∂P)
        + (∫ ω, (G.ξ ⟨k, hk⟩ ω) ^ 2 ∂P)
          * (G.partition (⟨k, hk⟩ : Fin G.N).succ
            - G.partition (⟨k, hk⟩ : Fin G.N).castSucc)

Module navigation

Module: LevyStochCalc/Brownian/ItoFourthMomentPartialSums.

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

Supporting theorems: stronglyMeasurable_partialSum, integral_add_mul_increment_sq.

Previous: integral_add_mul_increment_pow_four · Next: integral_partialSum_pow_four_succ.

Source excerpt, lines 234–239 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFourthMomentPartialSums

/-
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/Brownian/ItoFourthMomentPartialSums.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
variable {T : ℝ} (G : LevyStochCalc.Brownian.Ito.SimplePredictable Ω T)
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
variable (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration W ℱ)
  (h_adapt : ∀ i : Fin G.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
    (ℱ (G.partition i.castSucc)) (G.ξ i))
  {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (i : Fin G.N) (ω : Ω), |G.ξ i ω| ≤ C)
include hℱ h_adapt hC0 hC

Formal statement


theorem LevyStochCalc.Brownian.Ito.SimplePredictable.integral_partialSum_sq_succ_readable {k : ℕ} (hk : k < G.N) :
    ∫ ω, (G.partialSum W (k + 1) ω) ^ 2 ∂P
      = (∫ ω, (G.partialSum W k ω) ^ 2 ∂P)
        + (∫ ω, (G.ξ ⟨k, hk⟩ ω) ^ 2 ∂P)
          * (G.partition (⟨k, hk⟩ : Fin G.N).succ
            - G.partition (⟨k, hk⟩ : Fin G.N).castSucc) := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoFourthMomentPartialSums.lean#L232-L250 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoFourthMomentPartialSums`, declaration `LevyStochCalc.Brownian.Ito.SimplePredictable.integral_partialSum_sq_succ`; 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