Nullity of Two-Point Subgradient Slopes

Proved

FunctionalInequalities.Analysis.volume_subgradient_two_points_eq_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the Alexandrov null-set statement for repeated subgradients.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $u:E\to\mathbb R$ be Lipschitz and convex. Consider the set of slopes that are subgradients at two distinct points:

S=\left\{p:\exists x\ne y,\ \forall z,\ u(x)+\langle p,z-x\rangle\le u(z),\ \ u(y)+\langle p,z-y\rangle\le u(z)\right\}.

Then its volume is zero:

\operatorname{vol}(S)=0.

This is a measure-theoretic uniqueness statement for subgradients and is used in the push-forward Alexandrov identity.

Original Lean declaration header

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

theorem volume_subgradient_two_points_eq_zero [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u) :
    (volume : Measure E) {p : E | ∃ x y : E, x ≠ y ∧ (∀ z, u x + ⟪p, z - x⟫ ≤ u z) ∧
      (∀ z, u y + ⟪p, z - y⟫ ≤ u z)} = 0

Module navigation

Module: Analysis/Convex/Subgradient.

Supporting theorems: ConvexOn.ae_differentiableAt_of_isOpen, conjugate_maximizer_eq_gradient, convex_epigraph_legendre.

Previous: subgradientImage_subset_of_le · Next: eventually_abs_sub_quadratic_le_of_subgradient_expansion.

Source excerpt, lines 1113–1116 · 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.volume_subgradient_two_points_eq_zero_readable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u) :
    (volume : Measure E) {p : E | ∃ x y : E, x ≠ y ∧ (∀ z, u x + ⟪p, z - x⟫ ≤ u z) ∧
      (∀ z, u y + ⟪p, z - y⟫ ≤ u z)} = 0 := by sorry

Source

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

View graph