Samplinglib mathematical lesson

The compensated finite-grid quadratic-variation error has an exact L² norm

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2.integral_quadraticVariationError_sq · theorem · Teaching coverage

Read this first

Mathematical statement

Let B be a real pre-Brownian process and t₀≤⋯≤tₙ a deterministic grid. If Q is the sum over cells of the squared Brownian increment minus the cell length, then E[Q²] is exactly twice the sum of the squared cell lengths.

\[\mathbb E\left[\left(\sum_{i=0}^{n-1}((B_{t_{i+1}}-B_{t_i})^2-(t_{i+1}-t_i))\right)^2\right]=2\sum_{i=0}^{n-1}(t_{i+1}-t_i)^2\]

Lean statement · integral_quadraticVariationError_sq

The theorem quantifies over every finite monotone NNReal-time grid and keeps the IsPreBrownianReal process assumption explicit.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem integral_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, (quadraticVariationError B times omega) ^ 2 ∂mu =
      2 * ∑ i : Fin n,
        (((times i.succ - times i.castSucc : ℝ≥0) : ℝ) ^ 2)

Exact module and namespace context

Proof roadmap

1Center one squared increment
The Gaussian second and fourth moments give mean zero and second moment 2Δt² for each squared increment after subtracting its time length.
2Use independence across grid cells
Independent Brownian increments remain independent after applying the measurable centered-square map, so distinct centered summands are orthogonal in L².
3Add the cell variances
Because every summand is square-integrable and centered, the variance of their finite sum is the sum of their variances. Substituting the one-cell identity produces the exact factor 2.

Full assumptions and notation

All objects and hypotheses

B satisfies Samplinglib's real pre-Brownian contract under the measure μ.
The deterministic grid has n cells and is monotone in nonnegative real time.
No strict time inequalities, positive horizon, filtration usual conditions, or pathwise boundedness are required.

Mathematical proof

1. Center one squared increment

The Gaussian second and fourth moments give mean zero and second moment 2Δt² for each squared increment after subtracting its time length.

\[\mathbb E[((\Delta B_i)^2-\Delta t_i)^2]=2(\Delta t_i)^2\]

Corresponding Lean step

Reuse integral_centered_increment_sq_eq_zero, centered_increment_sq_memLp_two, and integral_centered_increment_sq_sq.

2. Use independence across grid cells

Independent Brownian increments remain independent after applying the measurable centered-square map, so distinct centered summands are orthogonal in L².

\[i\ne j\Longrightarrow \mathbb E[Y_iY_j]=0\]

Corresponding Lean step

Use iIndepFun_centeredSquaredIncrement and the finite-sum variance theorem.

3. Add the cell variances

Because every summand is square-integrable and centered, the variance of their finite sum is the sum of their variances. Substituting the one-cell identity produces the exact factor 2.

\[\operatorname{Var}(\sum_iY_i)=\sum_i\operatorname{Var}(Y_i)=2\sum_i(\Delta t_i)^2\]

Corresponding Lean step

Apply ProbabilityTheory.IndepFun.variance_sum, rewrite variance by the zero mean, and simplify the finite sum.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · integral_quadraticVariationError_sq

The proof packages the Gaussian fourth-moment calculation into a one-cell variance, transports independence through the centered-square map, and invokes finite-sum variance additivity.

Download module (.lean)

theorem integral_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, (quadraticVariationError B times omega) ^ 2 ∂mu =
      2 * ∑ i : Fin n,
        (((times i.succ - times i.castSucc : ℝ≥0) : ℝ) ^ 2) := by
  let _ : IsProbabilityMeasure mu := hB.isGaussianProcess.isProbabilityMeasure
  let Y : Fin n → Omega → ℝ := fun i => centeredSquaredIncrement B times i
  have hYmem : ∀ i, MemLp (Y i) 2 mu := fun i => by
    change MemLp
      (fun omega =>
        (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
          ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)) 2 mu
    simpa only using
      centered_increment_sq_memLp_two hB _ _
  have hYind : Set.Pairwise (↑(Finset.univ : Finset (Fin n)) : Set (Fin n))
      (fun i j => Y i ⟂ᵢ[mu] Y j) := by
    intro i _ j _ hij
    exact (iIndepFun_centeredSquaredIncrement hB hmono).indepFun hij
  have hvar := ProbabilityTheory.IndepFun.variance_sum
    (s := Finset.univ) (X := Y) (fun i _ => hYmem i) hYind
  have hsumMem : MemLp (∑ i : Fin n, Y i) 2 mu :=
    memLp_finsetSum' Finset.univ (fun i _ => hYmem i)
  have hmean : ∫ omega, (∑ i : Fin n, Y i) omega ∂mu = 0 := by
    calc
      ∫ omega, (∑ i : Fin n, Y i) omega ∂mu =
          ∫ omega, ∑ i ∈ (Finset.univ : Finset (Fin n)), Y i omega ∂mu := by
            congr 1
            funext omega
            simp only [Finset.sum_apply]
      _ = ∑ i ∈ (Finset.univ : Finset (Fin n)), ∫ omega, Y i omega ∂mu := by
        rw [integral_finsetSum]
        intro i _
        exact (hYmem i).integrable (by norm_num)
      _ = 0 := by
        apply Finset.sum_eq_zero
        intro i _
        simpa [Y, centeredSquaredIncrement] using
          integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero hsumMem.aemeasurable hmean] at hvar
  change ∫ omega, (∑ i : Fin n, centeredSquaredIncrement B times i omega) ^ 2 ∂mu = _
  change ∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu = _
  rw [show (∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu) =
      ∑ i : Fin n, Var[Y i; mu] by
    simpa only [Finset.sum_apply] using hvar]
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro i _
  have hYiMean : ∫ omega, Y i omega ∂mu = 0 := by
    simpa [Y, centeredSquaredIncrement] using
      integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero (hYmem i).aemeasurable hYiMean]
  simpa [Y, centeredSquaredIncrement] using
    integral_centered_increment_sq_sq hB (grid_cell_le hmono i)

Exact module and namespace context

Scope and omitted-condition boundaries

This theorem is the finite-grid identity only. Its scalar dyadic Tendsto consumer is formalized separately; bounded predictable weights, vector cross-variation, Taylor localization, stochastic integration, and a complete Ito formula remain separate obligations.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.IndepFun.variance_sum
variance_of_integral_eq_zero
integral_finsetSum
memLp_finsetSum'

Mathematical sources

Sinho Chewi, Log-Concave Sampling, 2026-08-09, Section 3.1 — Quadratic variation and the finite-grid compensated squared-increment calculation.
Samplinglib compiled finite-grid L² theorem — Exact assumptions, finite-grid identity, and reusable helper chain.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.