Uniform Upper Bound For Admissible CEK Competitors

This is the finite-range reduction statement from the proof of Proposition 12 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), although no paper item directly cites this declaration.

Let $E$ be finite-dimensional with an additive Haar measure $dx$, and let $\mu$ be a probability measure. Assume:

1. Every linear subspace with full $\mu$-measure equals $E$.
2. The identity map is $\mu$-integrable.
3. $\int x\,d\mu(x)=0$.

Then there exists $U\in\mathbb R$ such that every $f:E\to\overline{\mathbb R}$ with PotentialIntegrable f μ satisfies

No convexity, nonnegativity, normalization, or finiteness of the conjugate mass is required of the competitor beyond PotentialIntegrable.

Original Lean declaration header

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

theorem exists_uniform_functional_upper (dx μ : Measure E) [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirst : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ U : ℝ, ∀ f : E → EReal, PotentialIntegrable f μ →
      variationalFunctional dx μ f ≤ (U : EReal)

Module navigation

Module: KLS/CEK/Competitors.

Definition modules: Probability/MomentMeasure/Basic.

Supporting theorems: exists_normalized_competitor, exists_coercivity_of_centered_probability, real_coercivity_le_uniform.

Previous: exists_normalized_competitor.

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