Successor Cumulant Energy Reindexing

Proved

FunctionalInequalities.KLS.BKL.cumulantEnergy_succ_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the reindexing identity for the next cumulant energy, corresponding to BKL equation (90).

Let $\nu$ be any measure on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ , let $r\in\mathbb N$ , and let $u$ be a direction. Set $\sigma=\operatorname{Cov}(\nu)^{-1/2}$ using inverseSqrt. Then

E_{r+1}^{\nu}(u)=\sum_{K:\,\mathrm{Fin}(r)\to\mathrm{Fin}(n)}\sum_{k:\,\mathrm{Fin}(n)} \kappa_{r+2}^{\nu}\!\left(u,\sigma e_{K(0)},\ldots,\sigma e_{K(r-1)},\sigma e_k\right)^2.

The finite sums are obtained by splitting the final index of a map from Fin (r+1) to Fin n. This is a combinatorial identity useful for comparing successive cumulant energies; no probability, isotropy, compactness, or invertibility assumptions are imposed.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL. Shown in its original module context. Proof omitted.

theorem cumulantEnergy_succ_eq (ν : Measure (EuclideanSpace ℝ (Fin n))) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    cumulantEnergy ν (r + 1) u =
      ∑ K : Fin r → Fin n, ∑ k : Fin n, cumulant ν (r + 1 + 1)
        (Fin.cons u (Fin.snoc (fun s => inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ (K s)))
          (inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ k)))) ^ 2

Module navigation

Module: KLS/BKL/Localization/NoiseBound.

Definition modules: KLS/BKL/CumulantEnergy/Basic, Probability/Covariance/Basic, Analysis/Operator/InverseSqrt, Analysis/BakryEmery/Cumulant/Basic.

Previous: cumulant_middle_sum · Next: sum_sq_conjugatedNoiseMatrix_mulVec_le.

Source excerpt, lines 99–103 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound

open MeasureTheory
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.KLS.BKL.cumulantEnergy_succ_eq_readable (ν : Measure (EuclideanSpace ℝ (Fin n))) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    cumulantEnergy ν (r + 1) u =
      ∑ K : Fin r → Fin n, ∑ k : Fin n, cumulant ν (r + 1 + 1)
        (Fin.cons u (Fin.snoc (fun s => inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ (K s)))
          (inverseSqrt (Covariance.operator ν) (EuclideanSpace.basisFun (Fin n) ℝ k)))) ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/NoiseBound.lean#L97-L180 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.NoiseBound`, declaration `FunctionalInequalities.KLS.BKL.cumulantEnergy_succ_eq`; the repository is private at upload time).

View graph