Differentiable Convex Functions Are C¹

Proved

FunctionalInequalities.Analysis.contDiff_one_of_convexOn_of_differentiable_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves the finite-dimensional regularity fact that a differentiable convex function is $C^1$ .

Let $E$ be a finite-dimensional real normed space and let $u:E\to\mathbb R$ . If $u$ is convex on all of $E$ and differentiable everywhere, then

u\in C^1(E),\qquad\text{that is,}\qquad \operatorname{ContDiff}_{\mathbb R}^{1}(u).

The declaration is contDiff_one_of_convexOn_of_differentiable_readable. No quantitative Lipschitz estimate for the derivative is included, and finite dimensionality is essential to the stated result.

Original Lean declaration header

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

theorem contDiff_one_of_convexOn_of_differentiable {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (hdiff : Differentiable ℝ u) :
    ContDiff ℝ 1 u

Module navigation

Module: Analysis/Convex/Subgradient.

Next: subgradient_mem_of_ae_gradient_mem.

Source excerpt, lines 32–35 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient

Formal statement


theorem FunctionalInequalities.Analysis.contDiff_one_of_convexOn_of_differentiable_readable {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (hdiff : Differentiable ℝ u) :
    ContDiff ℝ 1 u := by sorry

Source

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

View graph