Extended-real convex potentials and Legendre transforms

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Legendre

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a real inner-product space $E$ and $\varphi:E\to\overline{\mathbb{R}}$ , ConvexPotential φ means that $\varphi$ never equals $-\infty$ and that its real epigraph is convex, while ProperPotential φ additionally requires at least one finite value. legendre φ y is the extended-real supremum $\sup_x(\langle x,y\rangle-\varphi(x))$ , and lowerTruncate φ M is $\max(\varphi(x),-M)$ pointwise; the module includes order, convexity, semicontinuity, and truncation auxiliary results.

Original module imports

import Mathlib.Analysis.Convex.Topology
import Mathlib.Analysis.InnerProductSpace.Continuous
import Mathlib.Data.EReal.Operations
import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Topology.Instances.EReal.Lemmas
import Mathlib.Analysis.Normed.Module.Convex

Original declaration excerpt

Shown in the original module context.

def ConvexPotential (φ : E → EReal) : Prop :=
  (∀ x, φ x ≠ ⊥) ∧ Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)}

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Convex.Legendre · Frozen source 408915f.

Definition code

import Mathlib.Analysis.Convex.Topology
import Mathlib.Analysis.InnerProductSpace.Continuous
import Mathlib.Data.EReal.Operations
import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Topology.Instances.EReal.Lemmas
import Mathlib.Analysis.Normed.Module.Convex

noncomputable section
namespace FunctionalInequalities
namespace Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- Convexity of an extended-real potential, expressed through its real epigraph. -/
def ConvexPotential (φ : E → EReal) : Prop :=
  (∀ x, φ x ≠ ⊥) ∧ Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)}
/-- The actual extended-real Legendre transform; no selected maximizers are assumed. -/
def legendre (φ : E → EReal) (y : E) : EReal :=
  ⨆ x : E, (inner ℝ x y : EReal) - φ x
/-- A finite-value witness as well as exclusion of `-∞`, rather than a desired conclusion. -/
def ProperPotential (φ : E → EReal) : Prop :=
  (∀ x, φ x ≠ ⊥) ∧ ∃ x, φ x ≠ ⊤
/-- The actual lower truncation in CEK equation (61). -/
def lowerTruncate (φ : E → EReal) (M : ℝ) : E → EReal :=
  fun x => max (φ x) ((-M : ℝ) : EReal)
end Analysis
end FunctionalInequalities

Source

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

View graph