Rademacher's theorem: a Lipschitz function is differentiable almost everywhere

This file proves Rademacher's theorem: a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere with respect to the Lebesgue measure. This is the content of LipschitzWith.ae_differentiableAt. Versions for functions which are Lipschitz on sets are also given (see LipschitzOnWith.ae_differentiableWithinAt).

Implementation

There are many proofs of Rademacher's theorem. We follow the one by Morrey, which is not the most elementary but maybe the most elegant once necessary prerequisites are set up.

• Step 0: without loss of generality, one may assume that f is real-valued.
• Step 1: Since a one-dimensional Lipschitz function has bounded variation, it is differentiable almost everywhere. With a Fubini argument, it follows that given any vector v then f is ae differentiable in the direction of v. See LipschitzWith.ae_lineDifferentiableAt.
• Step 2: the line derivative LineDeriv ℝ f x v is ae linear in v. Morrey proves this by a duality argument, integrating against a smooth compactly supported function g, passing the derivative to g by integration by parts, and using the linearity of the derivative of g. See LipschitzWith.ae_lineDeriv_sum_eq.
• Step 3: consider a countable dense set s of directions. Almost everywhere, the function f is line-differentiable in all these directions and the line derivative is linear. Approximating any direction by a direction in s and using the fact that f is Lipschitz to control the error, it follows that f is Fréchet-differentiable at these points. See LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure.

References

• [Pertti Mattila, Geometry of sets and measures in Euclidean spaces, Theorem 7.3][Federer1996]

Step 1: A Lipschitz function is ae differentiable in any given direction

This follows from the one-dimensional result that a Lipschitz function on ℝ has bounded variation, and is therefore ae differentiable, together with a Fubini argument.

theorem LipschitzWith.memℒp_lineDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} (hf : LipschitzWith C f) (v : E) : MeasureTheory.Memℒp (fun (x : E) => lineDeriv ℝ f x v) ⊤ μ

theorem LipschitzWith.ae_lineDifferentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (v : E) : ∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v

theorem LipschitzWith.locallyIntegrable_lineDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (v : E) : MeasureTheory.LocallyIntegrable (fun (x : E) => lineDeriv ℝ f x v) μ

Step 2: the ae line derivative is linear

Surprisingly, this is the hardest step. We prove it using an elegant but slightly sophisticated argument by Morrey, with a distributional flavor: we integrate against a smooth function, and push the derivative to the smooth function by integration by parts. As the derivative of a smooth function is linear, this gives the result.

theorem LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (hg : MeasureTheory.Integrable g μ) (v : E) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

theorem LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (h'f : HasCompactSupport f) (hg : Continuous g) (v : E) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

theorem LipschitzWith.integral_lineDeriv_mul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {D : NNReal} {f : E → ℝ} {g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (hg : LipschitzWith D g) (h'g : HasCompactSupport g) (v : E) : ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ

Integration by parts formula for the line derivative of Lipschitz functions, assuming one of them is compactly supported.

theorem LipschitzWith.ae_lineDeriv_sum_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) {ι : Type u_3} (s : Finset ι) (a : ι → ℝ) (v : ι → E) : ∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)

The line derivative of a Lipschitz function is almost everywhere linear with respect to fixed coefficients.

Step 3: construct the derivative using the line derivatives along a basis

theorem LipschitzWith.ae_exists_fderiv_of_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) {s : Set E} (hs : s.Countable) : ∀ᵐ (x : E) ∂μ, ∃ (L : E →L[ℝ] ℝ), ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

theorem LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] {f : E → F} (hf : LipschitzWith C f) {s : Set E} (hs : Metric.sphere 0 1 ⊆ closure s) {L : E →L[ℝ] F} {x : E} (hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) : HasFDerivAt f L x

If a Lipschitz functions has line derivatives in a dense set of directions, all of them given by a single continuous linear map L, then it admits L as Fréchet derivative.

theorem LipschitzWith.ae_differentiableAt_of_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

A real-valued function on a finite-dimensional space which is Lipschitz is differentiable almost everywere. Superseded by LipschitzWith.ae_differentiableAt which works for functions taking value in any finite-dimensional space.

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

A real-valued function on a finite-dimensional space which is Lipschitz on a set is differentiable almost everywere in this set. Superseded by LipschitzOnWith.ae_differentiableWithinAt_of_mem which works for functions taking value in any finite-dimensional space.

theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ι : Type u_3} [Fintype ι] {f : E → ι → ℝ} {s : Set E} (hf : LipschitzOnWith C f s) : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

A function on a finite-dimensional space which is Lipschitz on a set and taking values in a product space is differentiable almost everywere in this set. Superseded by LipschitzOnWith.ae_differentiableWithinAt_of_mem which works for functions taking value in any finite-dimensional space.

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

Rademacher's theorem: a function between finite-dimensional real vector spaces which is Lipschitz on a set is differentiable almost everywere in this set.

theorem LipschitzOnWith.ae_differentiableWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F} (hf : LipschitzOnWith C f s) (hs : MeasurableSet s) : ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x

Rademacher's theorem: a function between finite-dimensional real vector spaces which is Lipschitz on a set is differentiable almost everywere in this set.

theorem LipschitzWith.ae_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : NNReal} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F} (h : LipschitzWith C f) : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Rademacher's theorem: a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.

theorem ae_differentiableAt_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ (fun (x : E) => ‖x‖) x

In a real finite-dimensional normed vector space, the norm is almost everywhere differentiable.

theorem dense_differentiableAt_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : Dense {x : E | DifferentiableAt ℝ (fun (x : E) => ‖x‖) x}

In a real finite-dimensional normed vector space, the set of points where the norm is differentiable at is dense.