Prove2Me

Subgradients Lie In Closed Convex Gradient Range

Proved
FunctionalInequalities.Analysis.subgradient_mem_of_ae_gradient_mem_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves containment of every subgradient in a closed convex range of the almost-everywhere gradient.

Let EE be a finite-dimensional real inner-product space with its Borel measurable structure. Let u:E→Ru:E\to\mathbb R be Lipschitz and convex. Let K⊆EK\subseteq E be closed and convex, and assume

∇u(x)∈Kfor almost every x with respect to volume.\nabla u(x)\in K\quad\text{for almost every }x\text{ with respect to volume}.

If x,p∈Ex,p\in E satisfy

u(x)+⟨p,y−x⟩≤u(y)for all y∈E,u(x)+\langle p,y-x\rangle\le u(y)\quad\text{for all }y\in E,

then

p∈K.p\in K.

This is a support-and-closure principle used to control subgradient images.

Original Lean declaration header

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

theorem subgradient_mem_of_ae_gradient_mem [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    {K : Set E} (hK : IsClosed K) (hKc : Convex ℝ K)
    (hae : ∀ᵐ x ∂(volume : Measure E), gradient u x ∈ K)
    {x p : E} (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) : p ∈ K

Module navigation

Module: Analysis/Convex/Subgradient.

Previous: contDiff_one_of_convexOn_of_differentiable · Next: exists_subgradient_slope_le_inner_add.

Source excerpt, lines 150–154 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient

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

theorem FunctionalInequalities.Analysis.subgradient_mem_of_ae_gradient_mem_readable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    {K : Set E} (hK : IsClosed K) (hKc : Convex ℝ K)
    (hae : ∀ᵐ x ∂(volume : Measure E), gradient u x ∈ K)
    {x p : E} (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) : p ∈ K := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Subgradient.lean#L145-L186 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Subgradient`, declaration `FunctionalInequalities.Analysis.subgradient_mem_of_ae_gradient_mem`; the repository is private at upload time).

View graph