Uniform Linear Lower Bound For Legendre Transforms

This is a coercivity-support statement for moment potentials.

Let $E$ be finite-dimensional with a real inner product and Borel measurable structure, and let $\mu$ be a finite measure. Assume that $0$ lies in the interior of the convex hull of $\operatorname{supp}(\mu)$. Then there exist constants $c,C>0$ such that every $\phi:E\to\overline{\mathbb R}$ satisfying

1. $\phi\ge0$ pointwise;
2. $\phi(0)=0$;
3. ConvexPotential φ;
4. PotentialIntegrable φ μ;

has, for every $y\in E$,

The constants are chosen independently of the particular potential and provide a uniform linear lower bound for its Legendre transform.

Original Lean declaration header

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

theorem exists_uniform_legendre_lower (μ : Measure E) [IsFiniteMeasure μ]
    (h0 : (0 : E) ∈ interior (convexHull ℝ μ.support)) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ φ : E → EReal,
      (∀ x, 0 ≤ φ x) → φ 0 = 0 → ConvexPotential φ → PotentialIntegrable φ μ →
      ∀ y, 0 ≤ legendre φ y ∧
        ((c * ‖y‖ - C * (∫ x, (φ x).toReal ∂μ) : ℝ) : EReal) ≤ legendre φ y

Module navigation

Module: Probability/MomentMeasure/Coercivity.

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

Supporting theorems: affineMaximum_coercive, exists_pos_le_mul_lintegral_toReal_of_convex_epigraph.

Next: density_scaled_le_exp.

Source excerpt, lines 53–58 · Frozen source 408915f.