Invariance of Normalized Tilts Under Positive Rescaling

Proved

FunctionalInequalities.Probability.tilted_smul_pos_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement proves that normalized tilting is unchanged by a positive rescaling of the base measure.

Let $A$ be a measurable space, let $μ$ be a measure on $A$ , let $f:A\to\mathbb R$ , and let $c>0$ . Using the definition Measure.tilted, the normalized tilt of $(\operatorname{ENNReal.ofReal}(c)\,\bullet\,μ)$ equals the normalized tilt of $μ$ :

(\operatorname{ENNReal.ofReal}(c)\,\bullet\,μ).\operatorname{tilted}(f) = μ.\operatorname{tilted}(f).

This algebraic invariance isolates the normalization property of tilted measures and does not require probability or finiteness assumptions on $μ$ .

Original Lean declaration header

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

theorem Probability.tilted_smul_pos {A : Type*} [MeasurableSpace A] (μ : Measure A)
    (f : A → ℝ) {c : ℝ} (hc : 0 < c) :
    (ENNReal.ofReal c • μ).tilted f = μ.tilted f

Module navigation

Module: Probability/Transport.

Next: Covariance.operator_map_continuousLinearEquiv.

Source excerpt, lines 55–57 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport

open MeasureTheory Filter Topology InnerProductSpace
variable {A B : Type*}

Formal statement


theorem FunctionalInequalities.Probability.tilted_smul_pos_readable {A : Type*} [MeasurableSpace A] (μ : Measure A)
    (f : A → ℝ) {c : ℝ} (hc : 0 < c) :
    (ENNReal.ofReal c • μ).tilted f = μ.tilted f := by sorry

Source

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

View graph