Characterization of Finite-Above Legendre Values

Proved

FunctionalInequalities.Analysis.legendre_ne_bot_iff_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This characterizes when a Legendre transform value is not negative infinity.

Let $\phi:E\to\overline{\mathbb R}$ and $y\in E$ . Then

\operatorname{Leg}(\phi)(y)\neq-\infty \quad\Longleftrightarrow\quad \exists x\in E,\ \phi(x)\neq+\infty.

Thus the conjugate avoids $-\infty$ exactly when the effective domain of $\phi$ is nonempty. No convexity, measurability, or finiteness assumptions are imposed on the input.

Original Lean declaration header

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

theorem legendre_ne_bot_iff (φ : E → EReal) (y : E) :
    legendre φ y ≠ ⊥ ↔ ∃ x, φ x ≠ ⊤

Module navigation

Module: Analysis/Convex/Legendre.

Previous: convex_epigraph_legendre · Next: lowerTruncate_convexification.

Source excerpt, lines 182–183 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Legendre

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

Formal statement


theorem FunctionalInequalities.Analysis.legendre_ne_bot_iff_readable (φ : E → EReal) (y : E) :
    legendre φ y ≠ ⊥ ↔ ∃ x, φ x ≠ ⊤ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Legendre.lean#L180-L204 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Legendre`, declaration `FunctionalInequalities.Analysis.legendre_ne_bot_iff`; the repository is private at upload time).

View graph