Composition Rule for Exponential Tilts

Proved

FunctionalInequalities.Analysis.BakryEmery.expTilt_tilted_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem relates an exponential tilt of a tilted measure to a single tilt with a modified potential.

Let $E$ be a real inner-product space, let $m$ be a measure on $E$ , and let $V:E\to\mathbb R$ . Assume that $x\mapsto e^{-V(x)}$ is integrable with respect to $m$ . For every $z\in E$ ,

\operatorname{expTilt}\bigl(m.\operatorname{tilted}(-V)\bigr)(z) =m.\operatorname{tilted}\bigl(-(V-\langle z,\cdot\rangle)\bigr).

The definitions expTilt and Measure.tilted are used exactly as stated; no finite-dimensional, completeness, Borel, or Haar-measure assumptions are required by the theorem. This identity is a basic algebraic rule for manipulating exponential tilts.

Original Lean declaration header

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

theorem expTilt_tilted {V : E → ℝ} (hV : Integrable (fun x => Real.exp ((-V) x)) m) (z : E) :
    expTilt (m.tilted (-V)) z = m.tilted (-fun y => V y - ⟪z, y⟫)

Module navigation

Module: Analysis/BakryEmery/Tilt/Basic.

Previous: gradient_sub_inner · Next: integrable_gradient_expTilt.

Source excerpt, lines 91–92 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Basic

open MeasureTheory FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace ContDiff
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable (m : MeasureTheory.Measure E) [m.IsAddHaarMeasure]
omit [CompleteSpace E] [FiniteDimensional ℝ E] [BorelSpace E] [m.IsAddHaarMeasure]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.expTilt_tilted_readable {V : E → ℝ} (hV : Integrable (fun x => Real.exp ((-V) x)) m) (z : E) :
    expTilt (m.tilted (-V)) z = m.tilted (-fun y => V y - ⟪z, y⟫) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/Basic.lean#L89-L104 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.expTilt_tilted`; the repository is private at upload time).

View graph