Ball-truncated convex conjugate

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a real inner-product space $E$ , a real function $u:E\to\mathbb{R}$ , $M\in\mathbb{R}$ , and $p\in E$ , truncatedConjugate u M p is the supremum of $\langle p,x\rangle-u(x)$ over the closed ball $\{x:\|x\|\le M\}$ . It is the finite-ball truncation used in the weak Caffarelli strict-convexity development, which also contains geometric comparison lemmas.

Original module imports

import FunctionalInequalities.Analysis.Convex.Alexandrov
import FunctionalInequalities.Analysis.Convex.Normalization
import FunctionalInequalities.Analysis.Convex.Subgradient
import Mathlib.Analysis.LocallyConvex.Separation
import Mathlib.Analysis.Convex.Extrema
import Mathlib.Analysis.Convex.Continuous
import FunctionalInequalities.Analysis.Convex.Coercivity

Original declaration excerpt

Shown in the original module context.

def truncatedConjugate {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ)
    (M : ℝ) (p : E) : ℝ :=
  sSup ((fun x => ⟪p, x⟫ - u x) '' closedBall (0 : E) M)

Module navigation

Direct project imports: Analysis/Convex/Alexandrov, Analysis/Convex/Normalization, Analysis/Convex/Subgradient, Analysis/Convex/Coercivity.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Normalization
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient
import Mathlib.Analysis.LocallyConvex.Separation
import Mathlib.Analysis.Convex.Extrema
import Mathlib.Analysis.Convex.Continuous
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Coercivity

noncomputable section
open Set Metric
open scoped RealInnerProductSpace
section LT11F2TruncatedConjugate
open Set Metric
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Analysis
/-- The **ball-truncated conjugate** `p ↦ sup_{‖x‖ ≤ M} (⟪p, x⟫ − u x)` (weak Letwin route;
KLS500 `truncatedLegendrePotential`): a globally finite convex function that agrees with the Legendre
transform of `u` wherever the supremum is attained inside the ball. -/
def truncatedConjugate {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E → ℝ)
    (M : ℝ) (p : E) : ℝ :=
  sSup ((fun x => ⟪p, x⟫ - u x) '' closedBall (0 : E) M)
end Analysis
end FunctionalInequalities
end LT11F2TruncatedConjugate

Source

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

View graph