Legendre Transform of the Norm

Proved

FunctionalInequalities.Analysis.legendre_norm_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This computes the extended-real Legendre transform of the norm.

For every $y$ in a real inner-product space,

\operatorname{Leg}\bigl(x\mapsto\|x\|\bigr)(y) = \begin{cases} 0,&\|y\|\leq1,\\ +\infty,&\|y\|>1. \end{cases}

The equality is in EReal. Thus the conjugate of the norm is the indicator of the closed unit ball, with value $0$ on the ball and $+\infty$ outside.

Original Lean declaration header

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

theorem legendre_norm (y : E) :
    legendre (fun x : E => (‖x‖ : EReal)) y = if ‖y‖ ≤ 1 then 0 else ⊤

Module navigation

Module: Analysis/Convex/Legendre.

Supporting theorems: legendre_ne_bot_iff.

Previous: legendre_eq_interior_sup.

Source excerpt, lines 311–312 · 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_norm_readable (y : E) :
    legendre (fun x : E => (‖x‖ : EReal)) y = if ‖y‖ ≤ 1 then 0 else ⊤ := by sorry

Source

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

View graph