Fourth-Moment Bound by the Variance Clock

Proved

LevyStochCalc.Brownian.Ito.SimplePredictable.integral_partialSum_pow_four_le_varClock_readable

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

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

This theorem bounds the fourth moment of a partial elementary Brownian integral using per-tile variance budgets.

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

the coefficients are strongly measurable;
$C\ge0$ and $|\xi_i(\omega)|\le C$ ;
$|\xi_i(\omega)|\le c_i$ for a family $c_i$ ;
$k\le N$ .

Then

\int \bigl(G.\operatorname{partialSum}(W,k)\bigr)^4\,dP \le 6\,V_NV_k+\mathsf g_4 V_k^2,

where $V_r=\operatorname{varClock}(G,c,r)$ and $\mathsf g_4$ is gaussianFourthMoment. This is the sharper partial-sum fourth-moment estimate in terms of elapsed variance rather than a uniform time bound.

Original Lean declaration header

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

theorem integral_partialSum_pow_four_le_varClock {c : Fin G.N → ℝ}
    (hc : ∀ (i : Fin G.N) (ω : Ω), |G.ξ i ω| ≤ c i) :
    ∀ (k : ℕ) (_hk : k ≤ G.N),
      ∫ ω, (G.partialSum W k ω) ^ 4 ∂P
        ≤ 6 * (G.varClock c G.N * G.varClock c k)
          + gaussianFourthMoment * G.varClock c k ^ 2

Module navigation

Module: LevyStochCalc/Brownian/ItoFourthMomentPartialSums.

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

Supporting theorems: integral_partialSum_pow_four_succ, integral_partialSum_sq_le_varClock, varClock_mono.

Previous: integral_partialSum_sq_le_varClock.

Source excerpt, lines 464–469 · 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_pow_four_le_varClock_readable {c : Fin G.N → ℝ}
    (hc : ∀ (i : Fin G.N) (ω : Ω), |G.ξ i ω| ≤ c i) :
    ∀ (k : ℕ) (_hk : k ≤ G.N),
      ∫ ω, (G.partialSum W k ω) ^ 4 ∂P
        ≤ 6 * (G.varClock c G.N * G.varClock c k)
          + gaussianFourthMoment * G.varClock c k ^ 2 := by sorry

Source

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