Differentiability From Unique Convex Subgradient

Proved

FunctionalInequalities.Analysis.hasFDerivAt_of_convexOn_of_unique_subgradient_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an auxiliary differentiability criterion for convex functions.

Let $E$ be a finite-dimensional real inner-product space and let $u:E\to\mathbb R$ be convex. Fix $x,g\in E$ . Assume $g$ is a subgradient at $x$ :

u(x)+\langle g,y-x\rangle\le u(y)\quad\text{for all }y,

and assume it is unique: every $q$ satisfying the same supporting inequality equals $g$ . Then $u$ has a Fréchet derivative at $x$ , represented through the inner product by $g$ :

\operatorname{HasFDerivAt}(u,\operatorname{toDual}(g),x).

The result is used to pass from pointwise uniqueness of subgradients to continuous differentiability.

Original Lean declaration header

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

private lemma hasFDerivAt_of_convexOn_of_unique_subgradient {u : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (x g : E)
    (hg : ∀ y, u x + ⟪g, y - x⟫ ≤ u y)
    (huniq : ∀ q, (∀ y, u x + ⟪q, y - x⟫ ≤ u y) → q = g) :
    HasFDerivAt u ((InnerProductSpace.toDual ℝ E) g) x

Module navigation

Module: Analysis/Convex/Subgradient.

Supporting theorems: exists_subgradient_slope_le_inner_add.

Previous: ConvexOn.ae_differentiableAt_of_isOpen · Next: support_of_max.

Source excerpt, lines 656–660 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient

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

Formal statement

 lemma FunctionalInequalities.Analysis.hasFDerivAt_of_convexOn_of_unique_subgradient_readable {u : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (x g : E)
    (hg : ∀ y, u x + ⟪g, y - x⟫ ≤ u y)
    (huniq : ∀ q, (∀ y, u x + ⟪q, y - x⟫ ≤ u y) → q = g) :
    HasFDerivAt u ((InnerProductSpace.toDual ℝ E) g) x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Subgradient.lean#L656-L833 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Subgradient`, declaration `_private.FunctionalInequalities.Analysis.Convex.Subgradient.0.FunctionalInequalities.Analysis.hasFDerivAt_of_convexOn_of_unique_subgradient`; the repository is private at upload time).

View graph