Affine Transformation Rule for Regular Potential Laws

Proved

FunctionalInequalities.KLS.RegularPotential.law_comp_affine_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the affine stability statement for regular log-concave measures in Section 2, equation (12), of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a finite-dimensional complete real inner-product space with its Borel measurable structure. Let $V:E\to\mathbb R$ and suppose RegularPotential V a b holds for real constants $a,b$ . Let $L:E\simeq_L E$ be a continuous linear equivalence and let $c\in E$ . The law RegularPotential.comp_affine hV L c of the potential $x\mapsto V(Lx+c)$ is the pushforward of the original law under $y\mapsto L^{-1}(y-c)$ :

\operatorname{law}(V\circ(L\,\cdot+c)) = \operatorname{map}\bigl(y\mapsto L^{-1}(y-c)\bigr)\bigl(\operatorname{law}(V)\bigr).

The result is a reusable change-of-variables identity for centering and affine normalization of regular laws.

Original Lean declaration header

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

theorem RegularPotential.law_comp_affine
    (L : E ≃L[ℝ] E) (c : E) :
    ((RegularPotential.comp_affine hV L c).law : Measure E) =
      (hV.law : Measure E).map (fun y => L.symm (y - c))

Module navigation

Module: KLS/LogConcave/Regular/Affine.

Definition modules: KLS/LogConcave/Regular/Basic.

Supporting theorems: Probability.tilted_smul_pos.

Source excerpt, lines 71–74 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Affine

open MeasureTheory
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable {V : E → ℝ} {a b : ℝ} (hV : FunctionalInequalities.KLS.RegularPotential V a b)
include hV

Formal statement


theorem FunctionalInequalities.KLS.RegularPotential.law_comp_affine_readable
    (L : E ≃L[ℝ] E) (c : E) :
    ((RegularPotential.comp_affine hV L c).law : Measure E) =
      (hV.law : Measure E).map (fun y => L.symm (y - c)) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Section 2, (12), p. 5 (unnumbered). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Regular/Affine.lean#L68-L88 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Regular.Affine`, declaration `FunctionalInequalities.KLS.RegularPotential.law_comp_affine`; the repository is private at upload time).

View graph