Closed-ball cap of an extended-real potential

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_BoundedConjugate

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For an extended-real potential $\varphi:E\to\overline{\mathbb{R}}$ and $L\in\mathbb{R}_{\ge0}$ , closedBallCap φ L equals $\varphi$ on the closed ball of radius $L$ centered at $0$ and equals $+\infty$ outside that ball. The surrounding results establish lower semicontinuity and bounded-domain consequences for the Legendre transform, including finiteness and Lipschitz bounds under the listed hypotheses.

Original module imports

import FunctionalInequalities.Analysis.Convex.Legendre
import Mathlib.Analysis.Normed.Module.Convex
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Topology.MetricSpace.Lipschitz
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Original declaration excerpt

Shown in the original module context.

noncomputable def closedBallCap (φ : E → EReal) (L : NNReal) : E → EReal := by
  classical
  exact fun x => if x ∈ closedBall (0 : E) (L : ℝ) then φ x else ⊤

Module navigation

Direct project imports: Analysis/Convex/Legendre.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Legendre
import Mathlib.Analysis.Normed.Module.Convex
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.Semicontinuity.Basic
import Mathlib.Topology.MetricSpace.Lipschitz
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

noncomputable section
namespace FunctionalInequalities
namespace Analysis
open MeasureTheory Set Metric
open scoped ENNReal Topology RealInnerProductSpace
open FunctionalInequalities
open FunctionalInequalities.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- Restrict an extended-real potential to the closed ball, assigning top outside. -/
noncomputable def closedBallCap (φ : E → EReal) (L : NNReal) : E → EReal := by
  classical
  exact fun x => if x ∈ closedBall (0 : E) (L : ℝ) then φ x else ⊤
end Analysis
end FunctionalInequalities

Source

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

View graph