Existence of an Epsilon-Normalized Convex Competitor

This formalizes the reduction step in the proof of Proposition 12 of Cordero–Erausquin–Klartag (arXiv:1304.0630v1).

Let $dx$ be an additive Haar measure and let $\mu$ be a probability measure on a finite-dimensional real inner-product space. Assume:

1. $\mu$ is not concentrated on any proper linear subspace;
2. the identity map is $\mu$-integrable;
3. $\mu$ is centered, $\int x\,d\mu(x)=0$;
4. $f$ is potential-integrable;
5. $\varepsilon>0$.

Then there exists $\psi:E\to\overline{\mathbb R}$ such that $\psi$ is a convex potential, is potential-integrable, and

$$\psi(x)\geq0,\qquad \psi(0)=0,$$

and its variational value satisfies

$$\mathcal V_{dx,\mu}(f) \leq \mathcal V_{dx,\mu}(\psi)+\varepsilon.$$

This provides an epsilon-close normalized convex competitor for variational arguments.

Original Lean declaration header

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

theorem exists_normalized_competitor (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)
    (f : E → EReal) (hf : PotentialIntegrable f μ) (ε : ℝ) (hε : 0 < ε) :
    ∃ ψ : E → EReal, ConvexPotential ψ ∧ PotentialIntegrable ψ μ ∧
      (∀ x, 0 ≤ ψ x) ∧ ψ 0 = 0 ∧
      variationalFunctional dx μ f ≤ variationalFunctional dx μ ψ + (ε : EReal)

Module navigation

Module: KLS/CEK/Competitors.

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

Selected supporting theorems: exists_nonnegative_origin_zero_affine, legendre_affineSubtract, affineSubtract_potentialIntegrable, exists_convexified_lowerTruncate_variational_le_add, integral_affineSubtract.

Next: exists_uniform_functional_upper.

Source excerpt, lines 32–38 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_Competitors

open FunctionalInequalities.Analysis
open FunctionalInequalities.Probability.MomentMeasure
open MeasureTheory Filter Set
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.KLS.CEK.exists_normalized_competitor_readable (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)
    (f : E → EReal) (hf : PotentialIntegrable f μ) (ε : ℝ) (hε : 0 < ε) :
    ∃ ψ : E → EReal, ConvexPotential ψ ∧ PotentialIntegrable ψ μ ∧
      (∀ x, 0 ≤ ψ x) ∧ ψ 0 = 0 ∧
      variationalFunctional dx μ f ≤ variationalFunctional dx μ ψ + (ε : EReal) := by sorry