Legendre Transform Under Affine Subtraction

Proved

FunctionalInequalities.Analysis.legendre_affineSubtract_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the exact conjugation formula for subtracting an affine function.

Let $f:E\to\overline{\mathbb R}$ , $a,y\in E$ , and $b\in\mathbb R$ . For the definition affineSubtract f a b, namely

(\operatorname{affineSubtract} f\ a\ b)(x)=f(x)-\bigl(\langle a,x\rangle+b\bigr),

one has

\operatorname{Leg}(\operatorname{affineSubtract}(f,a,b))(y) = \operatorname{Leg}(f)(y+a)+b.

The equality is in EReal and remains valid with infinite input or conjugate values.

Original Lean declaration header

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

theorem legendre_affineSubtract (f : E → EReal) (a : E) (b : ℝ) (y : E) :
    legendre (affineSubtract f a b) y = legendre f (y + a) + (b : EReal)

Module navigation

Module: Analysis/Convex/Affine.

Definition modules: Analysis/Convex/Legendre.

Next: convex_epigraph_affineSubtract.

Source excerpt, lines 40–41 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Affine

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

Formal statement


theorem FunctionalInequalities.Analysis.legendre_affineSubtract_readable (f : E → EReal) (a : E) (b : ℝ) (y : E) :
    legendre (affineSubtract f a b) y = legendre f (y + a) + (b : EReal) := by sorry

Source

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

View graph