Prove2Me

Legendre Transform As A Supremum Over An Open Convex Set

Proved
FunctionalInequalities.Analysis.legendre_eq_interior_sup_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a measure-free representation formula for the Legendre transform.

Let EE be a real inner-product normed additive group and let K⊆EK\subseteq E be open and convex with 0∈K0\in K. Let ψ:E→R‾\psi:E\to\overline{\mathbb R} satisfy:

  1. For every x∈Ex\in E, ψ(tx)→ψ(x)\psi(tx)\to\psi(x) as t→1t\to1 from below.
  2. If x∉K‾x\notin\overline K, then ψ(x)=+∞\psi(x)=+\infty.

Then, for every y∈Ey\in E,

ψ∗(y)=sup⁡x∈K(⟨x,y⟩−ψ(x)).\psi^*(y)=\sup_{x\in K}\bigl(\langle x,y\rangle-\psi(x)\bigr).

The formula identifies the full Legendre transform with the supremum of affine terms restricted to the original open set.

Original Lean declaration header

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

theorem legendre_eq_interior_sup
    {K : Set E} (hK : IsOpen K) (hKconv : Convex ℝ K) (h0 : (0 : E) ∈ K)
    (ψ : E → EReal)
    (hrad : ∀ x, Tendsto (fun t : ℝ => ψ (t • x)) (𝓝[<] 1) (𝓝 (ψ x)))
    (hoff : ∀ x ∉ closure K, ψ x = ⊤) (y : E) :
    legendre ψ y = ⨆ x ∈ K, (inner ℝ x y : EReal) - ψ x

Module navigation

Module: Analysis/Convex/Legendre.

Previous: lowerTruncate_convexification · Next: legendre_norm.

Source excerpt, lines 255–260 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Legendre

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
open Filter Set
open scoped Topology
Formal statement

theorem FunctionalInequalities.Analysis.legendre_eq_interior_sup_readable
    {K : Set E} (hK : IsOpen K) (hKconv : Convex ℝ K) (h0 : (0 : E) ∈ K)
    (ψ : E → EReal)
    (hrad : ∀ x, Tendsto (fun t : ℝ => ψ (t • x)) (𝓝[<] 1) (𝓝 (ψ x)))
    (hoff : ∀ x ∉ closure K, ψ x = ⊤) (y : E) :
    legendre ψ y = ⨆ x ∈ K, (inner ℝ x y : EReal) - ψ x := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Legendre.lean#L252-L293 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Legendre`, declaration `FunctionalInequalities.Analysis.legendre_eq_interior_sup`; the repository is private at upload time).

View graph