Scaled Legendre Density Exponential Bound

This is a technical density estimate for a nonnegative extended-real Legendre transform.

Let $E$ be a real inner-product normed additive group, let $\phi:E\to\overline{\mathbb R}$, and let $c,C,M,a\in\mathbb R$. Assume:

1. $0\le C$.
2. $1\le a$ and $M\le a$.
3. For every $y\in E$, the Legendre transform $\phi^*(y)$ is nonnegative and satisfies

Then, for every $y\in E$, the density associated with density and the scaled point $ay$ obeys

This provides a reusable exponential envelope after scaling, without finite-dimensionality or measurability assumptions in the statement.

Formalization Note The density and bound are $[0,\infty]$-valued (ENNReal); the exponent is an ordinary real number.

Original Lean declaration header

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

theorem density_scaled_le_exp (φ : E → EReal) {c C M a : ℝ}
    (hC : 0 ≤ C) (ha : 1 ≤ a) (hMa : M ≤ a)
    (hlower : ∀ y, 0 ≤ legendre φ y ∧ ((c * ‖y‖ - C * M : ℝ) : EReal) ≤ legendre φ y)
    (y : E) : density (legendre φ) (a • y) ≤ ENNReal.ofReal (Real.exp (C - c * ‖y‖))

Module navigation

Module: Probability/MomentMeasure/Coercivity.

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

Previous: exists_uniform_legendre_lower · Next: exists_uniform_mass_bound.

Source excerpt, lines 103–106 · Frozen source 408915f.