Regular potentials under linear isometries

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Isometry

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

bkl2026functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

If V is a RegularPotential on a finite-dimensional inner-product space $E$ and $L:E\simeq F$ is a real linear isometry, RegularPotential.comp_isometry states that $y\mapsto V(L^{-1}y)$ is a regular potential on $F$ with the same constants $a,b$ . The conclusion preserves the temperate-growth and pointwise Hessian bounds exactly under the isometry.

Original module imports

import FunctionalInequalities.KLS.LogConcave.Regular.Basic
import FunctionalInequalities.Probability.Transport
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import FunctionalInequalities.KLS.Isotropic
import FunctionalInequalities.Poincare.SmoothTest.Transport
import FunctionalInequalities.KLS.LogConcave.Poincare

Original declaration excerpt

Shown in the original module context. Body omitted.

theorem RegularPotential.comp_isometry {V : E → ℝ} {a b : ℝ} (hV : KLS.RegularPotential V a b)
    (L : E ≃ₗᵢ[ℝ] F) :
    KLS.RegularPotential (fun y => V (L.symm y)) a b

Module navigation

Direct project imports: KLS/LogConcave/Regular/Basic, Probability/Transport, KLS/Isotropic, Poincare/SmoothTest/Transport, KLS/LogConcave/Poincare.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.Regular.Isometry · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Isotropic
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_SmoothTest_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Poincare

open MeasureTheory
open scoped ContDiff
namespace FunctionalInequalities
namespace KLS
universe u v
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {F : Type v} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [CompleteSpace F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] in
/-- **Regular potentials are preserved by linear isometries** `L : E ≃ F`, with the same constants `a, b`. -/
theorem RegularPotential.comp_isometry {V : E → ℝ} {a b : ℝ} (hV : KLS.RegularPotential V a b)
    (L : E ≃ₗᵢ[ℝ] F) :
    KLS.RegularPotential (fun y => V (L.symm y)) a b := by
  have hV2 : ContDiff ℝ 2 V := hV.temperate.1.of_le (WithTop.coe_le_coe.mpr le_top)
  refine ⟨hV.temperate.comp L.symm.toContinuousLinearEquiv.hasTemperateGrowth, hV.pos, ?_, ?_⟩
  · intro y w
    have hh := Analysis.BakryEmery.bilinearIteratedFDerivTwo_comp_clm hV2 (L.symm : F →L[ℝ] E) y w w
    simp only [LinearIsometryEquiv.coe_coe''] at hh
    rw [hh]
    simpa only [LinearIsometryEquiv.norm_map] using hV.lower (L.symm y) (L.symm w)
  · intro y w
    have hh := Analysis.BakryEmery.bilinearIteratedFDerivTwo_comp_clm hV2 (L.symm : F →L[ℝ] E) y w w
    simp only [LinearIsometryEquiv.coe_coe''] at hh
    rw [hh]
    simpa only [LinearIsometryEquiv.norm_map] using hV.upper (L.symm y) (L.symm w)
end KLS
end FunctionalInequalities

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), item E12. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Regular/Isometry.lean#L31-L47 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Regular.Isometry`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Isometry`; the repository is private at upload time).

View graph