Continuous Convex Tilt Gives a Borell Density

Proved

FunctionalInequalities.KLS.LogConcave.isBorellDensity_of_eq_tilted_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the density description of a continuous convex tilt.

Let $V$ be a real inner-product normed space with Borel measurable structure, let $\nu$ be a probability measure, let $m$ be a measure, and let $W:V\to\mathbb R$ . Assume:

$\nu=m.\mathrm{tilted}(-W)$ ;
$W$ is continuous;
$W$ is convex on all of $V$ .

Then $\nu$ is a Borell density with respect to $m$ whose density is

x\longmapsto \frac{e^{-W(x)}}{\int_V e^{-W(y)}\,dm(y)}.

In particular, the density is measurable, nonnegative, upper semicontinuous, and log-concave. This is the density-theoretic interface between tilted measures and log-concave laws.

Original Lean declaration header

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

theorem isBorellDensity_of_eq_tilted {m : Measure V} {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) (hW : Continuous W)
    (hconv : ConvexOn ℝ Set.univ W) :
    IsBorellDensity (ν : Measure V) m (fun x => Real.exp (-W x) / ∫ y, Real.exp (-W y) ∂m)

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Definition modules: KLS/LogConcave/Density/BorellRepresentation/Basic.

Supporting theorems: integral_exp_neg_pos_of_eq_tilted, rpow_mul_rpow_le_of_convexOn.

Previous: rpow_mul_rpow_le_of_convexOn · Next: interior_support_nonempty_of_eq_tilted.

Source excerpt, lines 122–125 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

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

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.isBorellDensity_of_eq_tilted_readable {m : Measure V} {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) (hW : Continuous W)
    (hconv : ConvexOn ℝ Set.univ W) :
    IsBorellDensity (ν : Measure V) m (fun x => Real.exp (-W x) / ∫ y, Real.exp (-W y) ∂m) := by sorry

Source

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

View graph