Legendre Maximizer and Dual Gradient

Proved

FunctionalInequalities.Analysis.exists_legendre_maximizer_with_gradient_identity_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an attainment statement for the Legendre transform.

Let $E$ be a finite-dimensional real inner-product normed space, let $\phi:E\to\overline{\mathbb R}$ be a ProperPotential and lower semicontinuous, and let $y$ belong to the interior of $\{q:\phi^*(q)\ne+\infty\}$ . Then there exists $z\in E$ such that

\langle z,y\rangle-\phi(z)=\phi^*(y).

Moreover, if $q\mapsto(\phi^*(q))_{\mathrm{toReal}}$ is differentiable at $y$ , then

z=\nabla\big((\phi^*)_{\mathrm{toReal}}\big)(y).

Thus every interior point of the finite Legendre domain has a primal maximizer, with the stated gradient identification under the additional differentiability implication.

Original Lean declaration header

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

theorem exists_legendre_maximizer_with_gradient_identity
    (φ : E → EReal) (hφ : ProperPotential φ)
    (hlsc : LowerSemicontinuous φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤}) :
    ∃ z : E,
      (inner ℝ z y : EReal) - φ z = legendre φ y ∧
      (DifferentiableAt ℝ (fun q : E => (legendre φ q).toReal) y →
        z = gradient (fun q : E => (legendre φ q).toReal) y)

Module navigation

Module: Analysis/Convex/LegendreVariation/Attainment.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: conjugate_maximizer_eq_gradient, exists_finite_maximum_of_upperSemicontinuous_linear_decay, tiltedObjective_data.

Previous: tiltedObjective_data.

Source excerpt, lines 337–344 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_LegendreVariation_Attainment

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

Formal statement


theorem FunctionalInequalities.Analysis.exists_legendre_maximizer_with_gradient_identity_readable
    (φ : E → EReal) (hφ : ProperPotential φ)
    (hlsc : LowerSemicontinuous φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤}) :
    ∃ z : E,
      (inner ℝ z y : EReal) - φ z = legendre φ y ∧
      (DifferentiableAt ℝ (fun q : E => (legendre φ q).toReal) y →
        z = gradient (fun q : E => (legendre φ q).toReal) y) := by sorry

Source

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

View graph