Positive Normalizing Integral for a Probability Tilt

Proved

FunctionalInequalities.KLS.LogConcave.integral_exp_neg_pos_of_eq_tilted_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a positivity statement for a tilted probability law.

Let $V$ be a measurable space, let $\nu$ be a probability measure on $V$ , let $m$ be a measure on $V$ , and let $W:V\to\mathbb R$ . Assume that $\nu=m.\mathrm{tilted}(-W)$ as measures. Then the normalizing integral is strictly positive:

0<\int_V e^{-W(x)}\,dm(x).

The result is a basic normalization fact used when identifying densities of tilted probability measures; it does not require norm, inner-product, finite-dimensional, or Borel-space structure.

Original Lean declaration header

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

theorem integral_exp_neg_pos_of_eq_tilted {m : Measure V} {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) :
    0 < ∫ x, Real.exp (-W x) ∂m

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Supporting theorems: integrable_exp_neg_of_eq_tilted.

Previous: integrable_exp_neg_of_eq_tilted · Next: rpow_mul_rpow_le_of_convexOn.

Source excerpt, lines 49–51 · 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 [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [BorelSpace V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.integral_exp_neg_pos_of_eq_tilted_readable {m : Measure V} {W : V → ℝ}
    (hνW : (ν : Measure V) = m.tilted (-W)) :
    0 < ∫ x, Real.exp (-W x) ∂m := by sorry

Source

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

View graph