Normalized Supremum Witness

This formalizes the variational-existence part of Proposition 12 of Cordero–Klartag (arXiv:1304.0630v1), in a limit-based form.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $dx$ be an additive Haar measure, and let $\mu$ be a probability measure. Assume:

1. Every linear subspace $V\subseteq E$ with $\mu(V^c)=0$ is all of $E$.
2. The identity map on $E$ is integrable with respect to $\mu$.
3. The barycenter vanishes: $\int x\,d\mu=0$.

Then there exist $S\in\mathbb{R}$ and a function $\psi:E\to\overline{\mathbb{R}}$ such that $\psi$ is a convex potential, is potential-integrable with respect to $\mu$, is nonnegative, and satisfies $\psi(0)=0$. Its conjugate mass is finite and strictly positive, and

$$(S:\overline{\mathbb{R}})\le I_{dx,\mu}(\psi),$$

where variationalFunctional is $I_{dx,\mu}$. Moreover, every competitor $\eta$ that is convex, potential-integrable, nonnegative, and satisfies $\eta(0)=0$ obeys

$$I_{dx,\mu}(\eta)\le S.$$

This statement supplies a normalized potential whose value reaches the supremum level up to the displayed lower bound and is used to obtain an actual variational maximizer.

Original Lean declaration header

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

theorem exists_limit_ge_normalized_supremum (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirstMoment : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ (S : ℝ) (ψ : E → EReal), ConvexPotential ψ ∧ PotentialIntegrable ψ μ ∧
      (∀ x, 0 ≤ ψ x) ∧ ψ 0 = 0 ∧ 0 < mass dx (legendre ψ) ∧ mass dx (legendre ψ) ≠ ⊤ ∧
      (S : EReal) ≤ variationalFunctional dx μ ψ ∧
      ∀ η : E → EReal, ConvexPotential η → PotentialIntegrable η μ →
        (∀ x, 0 ≤ η x) → η 0 = 0 → variationalFunctional dx μ η ≤ (S : EReal)

Module navigation

Module: KLS/CEK/VariationalMaximum.

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

Supporting theorems: exists_normalized_maximizing_sequence, exists_integral_bound_of_eventual_functional_lower, exists_subseq_integral_bounds_of_convex_epigraph, log_sub_ge_of_integral_limits, zero_mem_interior_convexHull_support_of_integral_eq_zero.

Previous: exists_normalized_maximizing_sequence · Next: exists_variational_maximum.

Source excerpt, lines 88–96 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_VariationalMaximum

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_limit_ge_normalized_supremum_readable (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirstMoment : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ (S : ℝ) (ψ : E → EReal), ConvexPotential ψ ∧ PotentialIntegrable ψ μ ∧
      (∀ x, 0 ≤ ψ x) ∧ ψ 0 = 0 ∧ 0 < mass dx (legendre ψ) ∧ mass dx (legendre ψ) ≠ ⊤ ∧
      (S : EReal) ≤ variationalFunctional dx μ ψ ∧
      ∀ η : E → EReal, ConvexPotential η → PotentialIntegrable η μ →
        (∀ x, 0 ≤ η x) → η 0 = 0 → variationalFunctional dx μ η ≤ (S : EReal) := by sorry