Log-Concavity of a Normalized Convex Potential Weight

Proved

FunctionalInequalities.KLS.LogConcave.rpow_mul_rpow_le_of_convexOn_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves the pointwise log-concavity inequality for a normalized exponential weight.

Let $V$ be a real inner-product space, let $W:V\to\mathbb R$ be convex on all of $V$ , and let $Z>0$ . For $x,y\in V$ and $0<t<1$ ,

\left(\frac{e^{-W(x)}}{Z}\right)^t \left(\frac{e^{-W(y)}}{Z}\right)^{1-t} \le \frac{e^{-W(tx+(1-t)y)}}{Z}.

The powers are real powers Real.rpow, and the positivity assumption on $Z$ is explicit. This is the density-level inequality used to show that exponential tilts by convex potentials are log-concave.

Original Lean declaration header

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

theorem rpow_mul_rpow_le_of_convexOn {W : V → ℝ} (hconv : ConvexOn ℝ Set.univ W) {Z : ℝ}
    (hZ : 0 < Z) (x y : V) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    (Real.exp (-W x) / Z) ^ t * (Real.exp (-W y) / Z) ^ (1 - t) ≤
      Real.exp (-W (t • x + (1 - t) • y)) / Z

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Previous: integral_exp_neg_pos_of_eq_tilted · Next: isBorellDensity_of_eq_tilted.

Source excerpt, lines 77–80 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {ν : MeasureTheory.ProbabilityMeasure V}
omit [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.rpow_mul_rpow_le_of_convexOn_readable {W : V → ℝ} (hconv : ConvexOn ℝ Set.univ W) {Z : ℝ}
    (hZ : 0 < Z) (x y : V) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    (Real.exp (-W x) / Z) ^ t * (Real.exp (-W y) / Z) ^ (1 - t) ≤
      Real.exp (-W (t • x + (1 - t) • y)) / Z := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/Tilted.lean#L74-L117 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.Tilted`, declaration `FunctionalInequalities.KLS.LogConcave.rpow_mul_rpow_le_of_convexOn`; the repository is private at upload time).

View graph