Unique Centered Generator Preimage

Proved

FunctionalInequalities.KLS.LogConcave.existsUnique_centered_adjointComp_eq_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the existence-and-uniqueness part of Lemma 2.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 7.

Let $V$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure, and let $\nu$ be a log-concave probability measure with nonempty interior support. Assume that $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ for a $C^2$ function $U:V\to\mathbb R$ . Let $C\in[0,\infty)$ satisfy $C_P(\nu)\le C$ . For every centered $g\in L^2(\nu)$ , there exists exactly one element $u$ in the domain of the adjoint composition of the closed weighted operator such that $u$ is centered and its adjoint composition equals $g$ :

\exists!\,u\in D(\bar T^\dagger\bar T),\qquad \int u\,d\nu=0\quad\text{and}\quad \bar T^\dagger\bar T u=g.

The uniqueness is among domain elements satisfying both displayed conditions.

This provides the centered inverse of the generator for subsequent operator-domain constructions.

Formalization Note: L2.mean expresses centering, and equality of the adjoint composition is equality in the $L^2(\nu)$ space. The Poincaré comparison is between the ENNReal intrinsic constant and the coercion of $C\in\mathrm{NNReal}$ .

Original Lean declaration header

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

theorem existsUnique_centered_adjointComp_eq {C : NNReal}
    (hC : Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
    (g : Lp ℝ 2 (ν : Measure V)) (hg : L2.mean ν g = 0) :
    ∃! u : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain,
      L2.mean ν (u : Lp ℝ 2 (ν : Measure V)) = 0 ∧
        adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u = g

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Inverse.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, L2/MeanVariance, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Poincare/LocalSlope/Basic.

Supporting theorems: eq_of_adjointComp_eq, exists_adjointComp_eq_of_gap, closedWeightedOperator_id_gap_of_literature_le, orthogonal_ker_iff_mean_eq_zero.

Previous: orthogonal_ker_iff_mean_eq_zero · Next: centered_adjointComp_bounds.

Source excerpt, lines 105–110 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Inverse

open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.Semigroup.Generated
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
include hνU hU

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.existsUnique_centered_adjointComp_eq_readable {C : NNReal}
    (hC : Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
    (g : Lp ℝ 2 (ν : Measure V)) (hg : L2.mean ν g = 0) :
    ∃! u : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain,
      L2.mean ν (u : Lp ℝ 2 (ν : Measure V)) = 0 ∧
        adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u = g := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 2.1, p. 7. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Inverse.lean#L101-L160 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Inverse`, declaration `FunctionalInequalities.KLS.LogConcave.existsUnique_centered_adjointComp_eq`; the repository is private at upload time).

View graph