Supporting Affine Minorant at the Origin

Proved

FunctionalInequalities.Analysis.exists_supporting_affine_at_zero_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

corderoklartag2015functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes a stronger pointwise supporting-plane statement related to Proposition 12 of Cordero–Erausquin–Klartag (CorderoKlartag2015).

Let $E$ be finite-dimensional, let $f:E\to\overline{\mathbb R}$ be a ConvexPotential, and assume $0$ lies in the interior of $\{x:f(x)\ne+\infty\}$ . Then there exists $a\in E$ such that, for every $x\in E$ ,

\langle a,x\rangle+(f(0))_{\mathrm{toReal}}\le f(x),

where the affine expression is embedded into the extended reals. This is a pointwise supporting affine minorant and is not the variational maximizer assertion of the cited proposition.

Original Lean declaration header

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

theorem exists_supporting_affine_at_zero [FiniteDimensional ℝ E]
    (f : E → EReal) (hf : ConvexPotential f)
    (h0 : (0 : E) ∈ interior {x | f x ≠ ⊤}) :
    ∃ a : E, ∀ x, ((inner ℝ a x + (f 0).toReal : ℝ) : EReal) ≤ f x

Module navigation

Module: Analysis/Convex/SupportingPlane.

Definition modules: Analysis/Convex/Legendre.

Source excerpt, lines 76–79 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SupportingPlane

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.exists_supporting_affine_at_zero_readable [FiniteDimensional ℝ E]
    (f : E → EReal) (hf : ConvexPotential f)
    (h0 : (0 : E) ∈ interior {x | f x ≠ ⊤}) :
    ∃ a : E, ∀ x, ((inner ℝ a x + (f 0).toReal : ℝ) : EReal) ≤ f x := by sorry

Source

Source: Cordero-Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), Proposition 12. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/SupportingPlane.lean#L74-L183 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.SupportingPlane`, declaration `FunctionalInequalities.Analysis.exists_supporting_affine_at_zero`; the repository is private at upload time).

View graph