Gaussian fourth moment and elementary Itô-integral sums
DefinitionKLSModular_LevyStochCalc_Brownian_ItoFourthMomentIncrementsVendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. gaussianFourthMoment is the real fourth moment ; for a simple predictable integrand and Brownian motion under a probability measure , SimplePredictable.term G W i ω is its -th coefficient times the corresponding Brownian increment, and SimplePredictable.partialSum G W k ω sums these terms for . SimplePredictable.varClock G W c k records , with terms beyond the partition length contributing zero.
Original module imports
import LevyStochCalc.Brownian.ItoAlgebra
Original declaration excerpt
Shown in the original module context.
noncomputable def gaussianFourthMoment : ℝ :=
∫ x : ℝ, x ^ 4 ∂(gaussianReal 0 1)
Module navigation
Direct project imports: LevyStochCalc/Brownian/ItoAlgebra.
Theorems in source order:
integral_pow_gaussianReal_zerointegral_mul_increment_powstronglyMeasurable_partialSumvarClock_mono
Project result: The KLS conjecture.
Original module · LevyStochCalc.Brownian.ItoFourthMomentIncrements · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoAlgebra
/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoFourthMomentIncrements.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
/-- The fourth moment of the standard real Gaussian distribution. -/
noncomputable def gaussianFourthMoment : ℝ :=
∫ x : ℝ, x ^ 4 ∂(gaussianReal 0 1)
namespace SimplePredictable
variable {T : ℝ} (G : SimplePredictable Ω T)
{P : Measure Ω} [IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
/-- The `i`-th summand of the elementary integral, indexed by a natural number. -/
noncomputable def term (i : ℕ) (ω : Ω) : ℝ :=
if h : i < G.N then
G.ξ ⟨i, h⟩ ω * (W.W (G.partition (⟨i, h⟩ : Fin G.N).succ) ω
- W.W (G.partition (⟨i, h⟩ : Fin G.N).castSucc) ω)
else 0
/-- The partial sums of the elementary integral. -/
noncomputable def partialSum (k : ℕ) (ω : Ω) : ℝ := ∑ i ∈ Finset.range k, G.term W i ω
/-- The variance budget of the first `k` tiles for a per-tile coefficient bound `c`:
`∑_{j < k} c_j² (τ_{j+1} − τ_j)`. -/
noncomputable def varClock (c : Fin G.N → ℝ) (k : ℕ) : ℝ :=
∑ j ∈ Finset.range k, if h : j < G.N then
c ⟨j, h⟩ ^ 2 * (G.partition (⟨j, h⟩ : Fin G.N).succ
- G.partition (⟨j, h⟩ : Fin G.N).castSucc) else 0
end SimplePredictable
end Ito
end Brownian
end LevyStochCalc