Real Representative Normalization

Proved

FunctionalInequalities.Probability.MomentMeasure.real_legendre_normalization_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a normalization lemma for a finite real representative of a Legendre transform.

Let $E$ be a real inner-product space with Borel measurable structure, let $dx$ be a measure, let $q:E\to\overline{\mathbb{R}}$ , and let $\psi:E\to\mathbb{R}$ . Assume

q^*(x)=\psi(x)\quad\text{in }\overline{\mathbb{R}}\text{ for every }x,

and

\operatorname{mass}_{dx}(q^*)=1.

Then $e^{-\psi}$ is Bochner integrable with respect to $dx$ , its integral is one, and the weighted measure weightedMeasure dx (fun x => (ψ x : EReal)) is a probability measure:

\int e^{-\psi(x)}\,dx=1.

The declaration converts the finite extended-real conjugate mass into real integrability and probability normalization.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem real_legendre_normalization
    (dx : Measure E) (q : E → EReal) (ψ : E → ℝ)
    (hψ : ∀ x, legendre q x = (ψ x : EReal))
    (hmass : mass dx (legendre q) = 1) :
    Integrable (fun x => Real.exp (-ψ x)) dx ∧
    (∫ x, Real.exp (-ψ x) ∂dx) = 1 ∧
    IsProbabilityMeasure (weightedMeasure dx (fun x => (ψ x : EReal)))

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

Definition modules: Probability/MomentMeasure/Basic, Analysis/Convex/Legendre.

Previous: log_sub_ge_of_integral_limits.

Source excerpt, lines 268–274 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_ConjugateMass

open MeasureTheory Set Metric
open FunctionalInequalities.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Probability.MomentMeasure.real_legendre_normalization_readable
    (dx : Measure E) (q : E → EReal) (ψ : E → ℝ)
    (hψ : ∀ x, legendre q x = (ψ x : EReal))
    (hmass : mass dx (legendre q) = 1) :
    Integrable (fun x => Real.exp (-ψ x)) dx ∧
    (∫ x, Real.exp (-ψ x) ∂dx) = 1 ∧
    IsProbabilityMeasure (weightedMeasure dx (fun x => (ψ x : EReal))) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/ConjugateMass.lean#L264-L304 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.ConjugateMass`, declaration `FunctionalInequalities.Probability.MomentMeasure.real_legendre_normalization`; the repository is private at upload time).

View graph