Prove2Me

Affine Subtraction Preserves Epigraph Convexity

Proved
FunctionalInequalities.Analysis.convex_epigraph_affineSubtract_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves preservation of real epigraph convexity under affine subtraction.

Let EE be a real inner-product space, let f:E→R‾f:E\to\overline{\mathbb R}, let a∈Ea\in E, and let b∈Rb\in\mathbb R. Assume the real epigraph

{(p,r)∈E×R:f(p)≤r}\{(p,r)\in E\times\mathbb R:f(p)\le r\}

is convex. Define affineSubtract by

affineSubtract⁡(f,a,b)(x)=f(x)−(⟨a,x⟩+b).\operatorname{affineSubtract}(f,a,b)(x)=f(x)-\bigl(\langle a,x\rangle+b\bigr).

Then its real epigraph is convex:

{(p,r):affineSubtract⁡(f,a,b)(p)≤r} is convex.\{(p,r):\operatorname{affineSubtract}(f,a,b)(p)\le r\}\text{ is convex}.

This is measure-free infrastructure for affine normalization of extended-real convex potentials.

Original Lean declaration header

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

theorem convex_epigraph_affineSubtract (f : E → EReal) (a : E) (b : ℝ)
    (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ (p.2 : EReal)}) :
    Convex ℝ {p : E × ℝ | affineSubtract f a b p.1 ≤ (p.2 : EReal)}

Module navigation

Module: Analysis/Convex/Affine.

Previous: legendre_affineSubtract · Next: exists_nonnegative_origin_zero_affine.

Source excerpt, lines 91–93 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Affine

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

theorem FunctionalInequalities.Analysis.convex_epigraph_affineSubtract_readable (f : E → EReal) (a : E) (b : ℝ)
    (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ (p.2 : EReal)}) :
    Convex ℝ {p : E × ℝ | affineSubtract f a b p.1 ≤ (p.2 : EReal)} := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Affine.lean#L90-L121 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Affine`, declaration `FunctionalInequalities.Analysis.convex_epigraph_affineSubtract`; the repository is private at upload time).

View graph