Rademacher's theorem for locally Lipschitz and convex functions

Mathlib proves Rademacher's theorem for a function between finite-dimensional real normed spaces that is Lipschitz on a set (LipschitzOnWith.ae_differentiableWithinAt_of_mem). This file localises it: a function that is only locally Lipschitz on a set s is differentiable within s at almost every point of s, and differentiable at almost every point of s when s is open.

A convex function on a convex set s of a finite-dimensional real normed space is locally Lipschitz on the interior of s (ConvexOn.locallyLipschitzOn_interior), and the frontier of a convex set is Haar-null (Convex.addHaar_frontier). Together these give the classical fact that a real convex function is differentiable at almost every point of its (convex) domain, with no assumption that the domain be open or have nonempty interior: when the interior is empty the domain lies in a proper affine subspace and is itself null.

Main statements

• LocallyLipschitzOn.ae_differentiableWithinAt_of_mem and LocallyLipschitzOn.ae_differentiableAt_of_mem — Rademacher's theorem for locally Lipschitz functions;
• Convex.ae_mem_interior — almost every point of a convex set is an interior point;
• ConvexOn.ae_differentiableAt_of_mem — a convex function is differentiable at almost every point of its domain.

References

• H. Rademacher, Über partielle und totale Differenzierbarkeit von Funktionen mehrerer Variabeln und über die Transformation der Doppelintegrale, Math. Ann. 79 (1919), 340--359;
• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, Theorem 25.5.

theorem LocallyLipschitzOn.ae_differentiableWithinAt_of_mem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} (hf : LocallyLipschitzOn s f) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Rademacher's theorem for locally Lipschitz functions: a function between finite-dimensional real normed spaces which is locally Lipschitz on a set is differentiable within that set at almost every point of it.

theorem LocallyLipschitzOn.ae_differentiableAt_of_mem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} (hf : LocallyLipschitzOn s f) (hs : IsOpen s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableAt ℝ f x

Rademacher's theorem for locally Lipschitz functions on an open set: a function between finite-dimensional real normed spaces which is locally Lipschitz on an open set is differentiable at almost every point of it.

theorem ConvexOn.ae_differentiableAt_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} {f : E → ℝ} (hf : ConvexOn ℝ s f) : ∀ᵐ (x : E) ∂μ, x ∈ interior s → DifferentiableAt ℝ f x

A real convex function on a finite-dimensional real normed space is differentiable at almost every interior point of its domain.

theorem ConvexOn.ae_differentiableAt_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} {f : E → ℝ} (hf : ConvexOn ℝ s f) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableAt ℝ f x

A real convex function on a finite-dimensional real normed space is differentiable at almost every point of its domain.