Convexity of a Real Legendre Representative

Proved

FunctionalInequalities.Analysis.real_convexOn_legendre_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This transfers convexity of the extended-real Legendre epigraph to a real representative.

Let $E$ be a real inner-product space, let $q:E\to\overline{\mathbb R}$ , and let $\psi:E\to\mathbb R$ . Assume that for every $x\in E$ ,

\operatorname{Leg}(q)(x)=\psi(x)

where the right-hand side is coerced to EReal. Then $\psi$ is convex on all of $E$ :

\psi(a x+b y)\leq a\psi(x)+b\psi(y)

whenever $a,b\geq0$ and $a+b=1$ . No finite-dimensional, measurability, or bounded-domain hypothesis is required.

Original Lean declaration header

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

theorem real_convexOn_legendre
    (q : E → EReal) (ψ : E → ℝ)
    (hψ : ∀ x, legendre q x = (ψ x : EReal)) :
    ConvexOn ℝ (univ : Set E) ψ

Module navigation

Module: Analysis/Convex/BoundedConjugate.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: convex_epigraph_legendre.

Previous: legendre_le_of_real_lower_bound · Next: lipschitzWith_real_legendre.

Source excerpt, lines 158–161 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_BoundedConjugate

open MeasureTheory Set Metric
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.real_convexOn_legendre_readable
    (q : E → EReal) (ψ : E → ℝ)
    (hψ : ∀ x, legendre q x = (ψ x : EReal)) :
    ConvexOn ℝ (univ : Set E) ψ := by sorry

Source

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

View graph