Finite affine maximum

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_AffineMaximum

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a nonempty finite set $s\subset E$ , a real function $a:E\to\mathbb{R}$ , and $y\in E$ , affineMaximum s hs a y is the genuine finite maximum of $\langle x,y\rangle-a(x)$ over $x\in s$ . The bundle also contains geometric auxiliary results controlling these maxima and comparing them with the extended-real Legendre transform.

Original module imports

import FunctionalInequalities.Analysis.Convex.Legendre
import Mathlib.Analysis.Normed.Affine.Convex

Original declaration excerpt

Shown in the original module context.

def affineMaximum (s : Finset E) (hs : s.Nonempty) (a : E → ℝ) (y : E) : ℝ :=
  s.sup' hs (fun x => inner ℝ x y - a x)

Module navigation

Direct project imports: Analysis/Convex/Legendre.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Legendre
import Mathlib.Analysis.Normed.Affine.Convex

noncomputable section
open Filter Set
open scoped Topology
namespace FunctionalInequalities
namespace Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- A genuine finite maximum of the affine summands of a conjugate. -/
def affineMaximum (s : Finset E) (hs : s.Nonempty) (a : E → ℝ) (y : E) : ℝ :=
  s.sup' hs (fun x => inner ℝ x y - a x)
end Analysis
end FunctionalInequalities

Source

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

View graph