Affine subtraction from an extended-real potential

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Affine

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $f:E\to\overline{\mathbb{R}}$ , $a\in E$ , $b\in\mathbb{R}$ , and $x\in E$ , affineSubtract f a b x is $f(x)-(\langle a,x\rangle+b)$ , with the affine function coerced into the extended reals. The module records pointwise transformation properties of Legendre transforms, epigraph convexity, and normalization under such affine shifts.

Original module imports

import FunctionalInequalities.Analysis.Convex.Legendre
import FunctionalInequalities.Analysis.Convex.SupportingPlane

Original declaration excerpt

Shown in the original module context.

def affineSubtract (f : E → EReal) (a : E) (b : ℝ) (x : E) : EReal :=
  f x - ((inner ℝ a x + b : ℝ) : EReal)

Module navigation

Direct project imports: Analysis/Convex/Legendre, Analysis/Convex/SupportingPlane.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Legendre
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SupportingPlane

noncomputable section
namespace FunctionalInequalities
namespace Analysis
section
open scoped ENNReal
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- Subtract the actual affine function `inner a x + b`. -/
def affineSubtract (f : E → EReal) (a : E) (b : ℝ) (x : E) : EReal :=
  f x - ((inner ℝ a x + b : ℝ) : EReal)
end
end Analysis
end FunctionalInequalities

Source

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

View graph