Raw Cumulant Expansion of a Centered Gradient Quadratic Form

Proved

FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_centeredGradient_zero_of_compact_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the raw expansion underlying Equation (74) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited as part of the spatial step of Lemma 4.3.

Let $E$ be finite-dimensional, let $\mu$ be a probability measure on $E$ with compact support, let $M:E\to E$ be continuous linear, let $m\in\mathbb N$ , and let $h:\operatorname{Fin}(m)\to E$ . Define

v(z)=\nabla\Lambda_\mu(z)-\nabla\Lambda_\mu(0),

where $\Lambda_\mu=\operatorname{logLaplace}(\mu)$ . Then

D^m\langle v(z),Mv(z)\rangle\big|_{z=0}[h] =\sum_{q\,:\,\exists i,\ q(i)=\mathrm{true}\ \wedge\ \exists i,\ q(i)=\mathrm{false}}\left\langle \kappa_{|q|+1}(h_q,\cdot),M\kappa_{m-|q|+1}(h_{\neg q},\cdot)\right\rangle,

where selected forms the ordered sublists $h_q$ and $h_{\neg q}$ , and the sum ranges over Boolean masks selecting both at least one direction and at least one complementary direction.

This is a deterministic raw Leibniz expansion; it contains no stochastic-process or cumulant-evolution assertion.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem iteratedFDeriv_inner_centeredGradient_zero_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (M : E →L[ℝ] E) (m : ℕ) (h : Fin m → E) :
    iteratedFDeriv ℝ m (fun z : E =>
        ⟪gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0,
          M (gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0)⟫) 0 h =
      ∑ q ∈ (Finset.univ.filter fun q : Fin m → Bool => (∃ i, q i = true) ∧ (∃ i, q i = false)),
        ⟪cumulantVector (μ : Measure E) (selected h q),
          M (cumulantVector (μ : Measure E) (selected h (fun i => !(q i))))⟫

Module navigation

Module: Analysis/BakryEmery/Cumulant/Leibniz.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, Analysis/BakryEmery/Cumulant/Local, Analysis/IteratedDerivative/Bilinear.

Supporting theorems: directional_centeredGradient_logLaplace_zero_of_compact, directional_bilinear.

Previous: directional_centeredGradient_logLaplace_zero_of_compact · Next: iteratedFDeriv_inner_centeredGradient_zero_grouped_of_compact.

Source excerpt, lines 61–68 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Leibniz

open MeasureTheory
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_centeredGradient_zero_of_compact_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (M : E →L[ℝ] E) (m : ℕ) (h : Fin m → E) :
    iteratedFDeriv ℝ m (fun z : E =>
        ⟪gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0,
          M (gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0)⟫) 0 h =
      ∑ q ∈ (Finset.univ.filter fun q : Fin m → Bool => (∃ i, q i = true) ∧ (∃ i, q i = false)),
        ⟪cumulantVector (μ : Measure E) (selected h q),
          M (cumulantVector (μ : Measure E) (selected h (fun i => !(q i))))⟫ := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Theorem 4.1, p. 18; Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Equations (72) and (74), pp. 20–21 (spatial step of the proof of Lemma 4.3). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Leibniz.lean#L60-L146 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Leibniz`, declaration `FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_centeredGradient_zero_of_compact`; the repository is private at upload time).

View graph