Convexity of the Real Legendre Epigraph

This proves convexity of the real epigraph of the Legendre transform.

Let $E$ be a real inner-product space and let $\varphi:E\to\overline{\mathbb R}$ be arbitrary, with EReal allowing the values $\pm\infty$. Define the Legendre transform by legendre. Then

is convex.

The statement is measure-free and applies without convexity, properness, or finiteness assumptions on $\varphi$. It is basic infrastructure for later properties of conjugates and biconjugates.

Original Lean declaration header

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

theorem convex_epigraph_legendre (φ : E → EReal) :
    Convex ℝ {p : E × ℝ | legendre φ p.1 ≤ (p.2 : EReal)}

Module navigation

Module: Analysis/Convex/Legendre.

Next: legendre_ne_bot_iff.

Source excerpt, lines 151–152 · Frozen source 408915f.