Smoothness of Posterior Cumulant Energy

Proved

FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulantEnergy_posterior_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement establishes smooth dependence of posterior cumulant energy on the localization parameters.

Let $\mu$ be a compactly supported isotropic probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ . For any $d\in\mathbb{N}$ and $u$ in that space, the function

q\longmapsto \operatorname{cumulantEnergy}(\mu_{q_1,q_2},d,u)

is $C^\infty$ on the full parameter space:

\operatorname{ContDiff}(\mathbb{R},\infty,q\mapsto \operatorname{cumulantEnergy}(\mu_{q_1,q_2},d,u)).

This is a technical regularity result used when applying generator and integral identities to posterior energy.

Original Lean declaration header

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

theorem contDiff_cumulantEnergy_posterior (hiso : KLS.Isotropic μ) (d : ℕ)
    (u : EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ ∞ (fun q : Param n =>
      cumulantEnergy (compactPosterior μ hc q.1 q.2 :
        Measure (EuclideanSpace ℝ (Fin n))) d u)

Module navigation

Module: KLS/BKL/Localization/Energy/Regularity.

Definition modules: KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Localization/Coefficients, KLS/Isotropic, Probability/Posterior/CompactDomain.

Supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, contDiff_cumulant_posterior, cumulantEnergy_eq_energyForm, contDiff_posteriorCovariance_joint.

Next: continuous_generator_of_contDiff_three.

Source excerpt, lines 26–30 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Energy_Regularity

open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Probability.Diffusion
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)

Formal statement

theorem FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulantEnergy_posterior_readable (hiso : KLS.Isotropic μ) (d : ℕ)
    (u : EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ ∞ (fun q : Param n =>
      cumulantEnergy (compactPosterior μ hc q.1 q.2 :
        Measure (EuclideanSpace ℝ (Fin n))) d u) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 5.2, p. 24. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Energy/Regularity.lean#L26-L88 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Energy.Regularity`, declaration `FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulantEnergy_posterior`; the repository is private at upload time).

View graph