Almost-Everywhere Differentiability of Convex Functions

This statement gives almost-everywhere differentiability of a convex function on an open set.

Let $E$ be a finite-dimensional real normed space with its Borel measurable structure, let $\mu$ be an additive Haar measure on $E$, and let $U\subseteq E$ be open. If $f:E\to\mathbb R$ is convex on $U$, then

Equivalently, the exceptional set of points in $U$ where differentiability fails is $\mu$-null. This technical result supports almost-everywhere arguments involving subgradients of convex functions.

Original Lean declaration header

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

theorem ConvexOn.ae_differentiableAt_of_isOpen {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [μ.IsAddHaarMeasure]
    {U : Set E} (hU : IsOpen U) {f : E → ℝ} (hf : ConvexOn ℝ U f) :
    ∀ᵐ x ∂μ, x ∈ U → DifferentiableAt ℝ f x

Module navigation

Module: Analysis/Convex/Subgradient.

Previous: exists_subgradient_slope_le_inner_add · Next: hasFDerivAt_of_convexOn_of_unique_subgradient.

Source excerpt, lines 569–573 · Frozen source 408915f.