Eventual Affine-Maximum Lower Bound for Legendre Transforms

This formalizes equation (60) of Cordero-Erausquin–Klartag, Moment measures (arXiv:1304.0630v1).

Let $E$ be a real inner-product normed space, let $\phi_j:E\to\overline{\mathbb R}$ be a sequence of extended-real functions, and let $\psi:E\to\overline{\mathbb R}$. Let $s\subset E$ be a nonempty finite set. Assume every $\psi(x)$ for $x\in s$ is neither $+\infty$ nor $-\infty$, and that $\phi_j(x)\to\psi(x)$ at each $x\in s$. For $\varepsilon>0$, eventually in $j$ and for every $y\in E$,

where the left side is embedded into EReal and $(\phi_j)^*$ is legendre (φ j).

The statement provides a bound uniform in the dual point $y$, obtained from pointwise convergence at finitely many vertices. It is a geometric approximation tool for Legendre transforms.

Original Lean declaration header

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

theorem eventually_affineMaximum_sub_le_legendre
    (φ : ℕ → E → EReal) (ψ : E → EReal) (s : Finset E) (hs : s.Nonempty)
    (hfin : ∀ x ∈ s, ψ x ≠ ⊤ ∧ ψ x ≠ ⊥)
    (hlim : ∀ x ∈ s, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x)))
    {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ j in atTop, ∀ y : E,
      ((affineMaximum s hs (fun x => (ψ x).toReal) y - ε : ℝ) : EReal) ≤
        legendre (φ j) y

Module navigation

Module: Analysis/Convex/AffineMaximum.

Definition modules: Analysis/Convex/Legendre.

Previous: affineMaximum_coercive.

Source excerpt, lines 102–109 · Frozen source 408915f.