Strictly Convex Subgradients Lie In Interior

Proved

FunctionalInequalities.Analysis.subgradient_mem_interior_of_strictConvexOn_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves interior membership for subgradients of a strictly convex function.

Let $E$ be a finite-dimensional real inner-product space and let $u:E\to\mathbb R$ be strictly convex. Let $K\subseteq E$ be convex with nonempty interior. Assume every subgradient of $u$ belongs to $K$ :

\forall x,p,\quad \bigl[\forall y,\ u(x)+\langle p,y-x\rangle\le u(y)\bigr]\Rightarrow p\in K.

Then every such subgradient lies in the interior:

\forall x,p,\quad \bigl[\forall y,\ u(x)+\langle p,y-x\rangle\le u(y)\bigr]\Rightarrow p\in\operatorname{int}K.

This strengthens closed-range containment and is used when deriving local density bounds.

Original Lean declaration header

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

theorem subgradient_mem_interior_of_strictConvexOn {u : E → ℝ}
    (hstrict : StrictConvexOn ℝ univ u) {K : Set E} (hKc : Convex ℝ K)
    (hKint : (interior K).Nonempty)
    (hK : ∀ x p : E, (∀ y, u x + ⟪p, y - x⟫ ≤ u y) → p ∈ K)
    {x p : E} (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) : p ∈ interior K

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: exists_subgradient_slope_le_inner_add.

Previous: strictConvexOn_of_contact_eq · Next: exists_exposed_contact_of_lt.

Source excerpt, lines 1162–1166 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

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

Formal statement


theorem FunctionalInequalities.Analysis.subgradient_mem_interior_of_strictConvexOn_readable {u : E → ℝ}
    (hstrict : StrictConvexOn ℝ univ u) {K : Set E} (hKc : Convex ℝ K)
    (hKint : (interior K).Nonempty)
    (hK : ∀ x p : E, (∀ y, u x + ⟪p, y - x⟫ ≤ u y) → p ∈ K)
    {x p : E} (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) : p ∈ interior K := by sorry

Source

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

View graph