Tilt-Average Identity on the Generator Domain

Proved

FunctionalInequalities.KLS.LogConcave.tiltAverage_adjointComp_eq_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the tilted generator identity (48) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Equation (48), p. 14.

Let $V$ be finite-dimensional, let $\nu$ be a log-concave probability measure with nonempty interior support, and let $m$ be Haar measure. Assume $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ for a function $U\in C^1(V)$ , and assume all exponential moments are integrable:

\forall r\in\mathbb R,\qquad \int e^{r\|x\|}\,d\nu(x)<\infty.

For every $F$ in the domain of $A=\bar T^\dagger\bar T$ and every $z\in V$ , the tilt average of $AF$ equals the inner product of $z$ with the tilt average of $\bar TF$ :

F_{AF}(z)=\left\langle z,F_{\bar TF}(z)\right\rangle.

The representatives involved are the $L^2(\nu)$ classes of $AF$ and $\bar TF$ .

This identity is the domain-level form of the integration-by-parts relation used to derive Taylor-tensor recursions.

Formalization Note: The definition tiltAverage is applied to the $L^2$ representatives supplied by adjointComp and closedWeightedOperator; no pointwise regularity of $F$ is asserted.

Original Lean declaration header

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

theorem tiltAverage_adjointComp_eq (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : ContDiff ℝ 1 U)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (z : V) :
    tiltAverage (ν : Measure V)
        (⇑(adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) F)) z =
      ⟪z, tiltAverage (ν : Measure V)
        (⇑(hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
          ⟨(F : Lp ℝ 2 (ν : Measure V)), F.2.2⟩)) z⟫

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Tilt.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: integrable_expTilt_of_memLp, tiltAverage_neg_weightedLaplacian, tendsto_apply_of_tendsto_adjointComp, exists_seq_smooth_tendsto_adjointComp_of_localRegularity, toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal.

Source excerpt, lines 81–90 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Tilt

open MeasureTheory Filter Topology
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace ENNReal
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 → ℝ}

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.tiltAverage_adjointComp_eq_readable (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : ContDiff ℝ 1 U)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (z : V) :
    tiltAverage (ν : Measure V)
        (⇑(adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) F)) z =
      ⟪z, tiltAverage (ν : Measure V)
        (⇑(hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
          ⟨(F : Lp ℝ 2 (ν : Measure V)), F.2.2⟩)) z⟫ := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Equation (48), p. 14 (unnumbered). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Tilt.lean#L79-L109 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Tilt`, declaration `FunctionalInequalities.KLS.LogConcave.tiltAverage_adjointComp_eq`; the repository is private at upload time).

View graph