Open Slopes With Interior Truncated Maximizers

Proved

FunctionalInequalities.Analysis.isOpen_setOf_truncatedConjugate_maximizer_lt_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves openness of a set of admissible slopes for the truncated conjugate.

Let $E$ be a finite-dimensional real inner-product space, let $u:E\to\mathbb R$ be continuous, and let $M\in\mathbb R$ satisfy $0\le M$ . Define the set of slopes $p$ such that every maximizer $x$ in the closed ball $\overline B(0,M)$ of truncatedConjugate satisfies $\|x\|<M$ :

\left\{p:\forall x\in\overline B(0,M),\quad u_M^*(p)=\langle p,x\rangle-u(x)\Rightarrow\|x\|<M\right\}.

This set is open.

The result is a technical topological ingredient for identifying subgradient images of the truncated conjugate.

Original Lean declaration header

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

theorem isOpen_setOf_truncatedConjugate_maximizer_lt {u : E → ℝ} (hu : Continuous u) {M : ℝ}
    (hM : 0 ≤ M) :
    IsOpen {p : E | ∀ x ∈ closedBall (0 : E) M,
      truncatedConjugate u M p = ⟪p, x⟫ - u x → ‖x‖ < M}

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: convexOn_truncatedConjugate.

Previous: truncatedConjugate_centered_spec · Next: n7_subgradient_eq_maximizer.

Source excerpt, lines 1552–1555 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

open Set Metric
open scoped RealInnerProductSpace Topology
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.isOpen_setOf_truncatedConjugate_maximizer_lt_readable {u : E → ℝ} (hu : Continuous u) {M : ℝ}
    (hM : 0 ≤ M) :
    IsOpen {p : E | ∀ x ∈ closedBall (0 : E) M,
      truncatedConjugate u M p = ⟪p, x⟫ - u x → ‖x‖ < M} := by sorry

Source

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

View graph