Polynomial Bound On Legendre Mass

This is a uniform polynomial bound for conjugate mass in the coercivity argument.

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

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

satisfies

The constant is selected before $\phi$, and the estimate is polynomial in the maximum of the real integral and $1$.

Original Lean declaration header

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

theorem exists_uniform_mass_bound (dx μ : Measure E) [dx.IsAddHaarMeasure] [IsFiniteMeasure μ]
    (h0 : (0 : E) ∈ interior (convexHull ℝ μ.support)) :
    ∃ A : ℝ, 0 < A ∧ ∀ φ : E → EReal,
      (∀ x, 0 ≤ φ x) → φ 0 = 0 → ConvexPotential φ → PotentialIntegrable φ μ →
      mass dx (legendre φ) ≤ ENNReal.ofReal
        (A * (max (∫ x, (φ x).toReal ∂μ) 1) ^ Module.finrank ℝ E)

Module navigation

Module: Probability/MomentMeasure/Coercivity.

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

Supporting theorems: density_scaled_le_exp, exists_uniform_legendre_lower, integrable_exp_sub_norm.

Previous: density_scaled_le_exp · Next: exists_coercivity_of_centered_probability.

Source excerpt, lines 137–142 · Frozen source 408915f.