Prove2Me

Convexity of the Truncated Conjugate

Proved
FunctionalInequalities.Analysis.convexOn_truncatedConjugate_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves convexity of the truncated conjugate.

Let EE be a finite-dimensional real inner-product space and let u:E→Ru:E\to\mathbb R be continuous. For every M≥0M\ge0, the function p↦truncatedConjugate⁡(u,M,p)p\mapsto\operatorname{truncatedConjugate}(u,M,p) is convex on all of EE:

ConvexOn⁡R(E,truncatedConjugate⁡(u,M)).\operatorname{ConvexOn}_{\mathbb R}(E,\operatorname{truncatedConjugate}(u,M)).

The declaration is convexOn_truncatedConjugate_readable. The statement concerns the supremum restricted to the closed ball of radius MM and makes no claim about strict convexity or differentiability.

Original Lean declaration header

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

theorem convexOn_truncatedConjugate {u : E → ℝ} (hu : Continuous u) {M : ℝ} (hM : 0 ≤ M) :
    ConvexOn ℝ univ (truncatedConjugate u M)

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: exists_truncatedConjugate_eq.

Previous: exists_truncatedConjugate_eq · Next: truncatedConjugate_centered_spec.

Source excerpt, lines 1309–1310 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

open Set Metric
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.convexOn_truncatedConjugate_readable {u : E → ℝ} (hu : Continuous u) {M : ℝ} (hM : 0 ≤ M) :
    ConvexOn ℝ univ (truncatedConjugate u M) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Caffarelli.lean#L1308-L1327 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Caffarelli`, declaration `FunctionalInequalities.Analysis.convexOn_truncatedConjugate`; the repository is private at upload time).

View graph