# 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.ae_lineDifferentiableAt {E : Type u_1} [] [] [] [] {C : NNReal} {f : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) (v : E) :
∀ᵐ (p : E) ∂μ,
theorem LipschitzWith.memℒp_lineDeriv {E : Type u_1} [] [] [] {C : NNReal} {f : E} {μ : } (hf : ) (v : E) :
MeasureTheory.Memℒp (fun (x : E) => lineDeriv f x v) μ
theorem LipschitzWith.locallyIntegrable_lineDeriv {E : Type u_1} [] [] [] [] {C : NNReal} {f : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) (v : E) :

### 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} [] [] [] [] {C : NNReal} {f : E} {g : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) (hg : ) (v : E) :
Filter.Tendsto (fun (t : ) => ∫ (x : E), t⁻¹ (f (x + t v) - f x) * g xμ) (nhdsWithin 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} [] [] [] [] {C : NNReal} {f : E} {g : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) (h'f : ) (hg : ) (v : E) :
Filter.Tendsto (fun (t : ) => ∫ (x : E), t⁻¹ (f (x + t v) - f x) * g xμ) (nhdsWithin 0 ()) (nhds (∫ (x : E), lineDeriv f x v * g xμ))
theorem LipschitzWith.integral_lineDeriv_mul_eq {E : Type u_1} [] [] [] [] {C : NNReal} {D : NNReal} {f : E} {g : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) (hg : ) (h'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} [] [] [] [] {C : NNReal} {f : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) {ι : Type u_3} (s : ) (a : ι) (v : ιE) :
∀ᵐ (x : E) ∂μ, lineDeriv f x (is, a i v i) = is, 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} [] [] [] [] {C : NNReal} {f : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) {s : Set E} (hs : s.Countable) :
∀ᵐ (x : E) ∂μ, ∃ (L : ), vs, HasLineDerivAt f (L v) x v
theorem LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure {E : Type u_1} [] [] {F : Type u_2} [] {C : NNReal} {f : EF} (hf : ) {s : Set E} (hs : ) {L : E →L[] F} {x : E} (hL : vs, HasLineDerivAt f (L v) x v) :

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} [] [] [] [] {C : NNReal} {f : E} {μ : } [μ.IsAddHaarMeasure] (hf : ) :
∀ᵐ (x : E) ∂μ,

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} [] [] [] [] {C : NNReal} {f : E} {s : Set E} {μ : } [μ.IsAddHaarMeasure] (hf : ) :
∀ᵐ (x : E) ∂μ, x s

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} [] [] [] [] {C : NNReal} {μ : } [μ.IsAddHaarMeasure] {ι : Type u_3} [] {f : Eι} {s : Set E} (hf : ) :
∀ᵐ (x : E) ∂μ, x s

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} [] [] [] [] {F : Type u_2} [] {C : NNReal} {s : Set E} {μ : } [μ.IsAddHaarMeasure] [] {f : EF} (hf : ) :
∀ᵐ (x : E) ∂μ, x s

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} [] [] [] [] {F : Type u_2} [] {C : NNReal} {s : Set E} {μ : } [μ.IsAddHaarMeasure] [] {f : EF} (hf : ) (hs : ) :
∀ᵐ (x : E) ∂μ.restrict s,

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} [] [] [] [] {F : Type u_2} [] {C : NNReal} {μ : } [μ.IsAddHaarMeasure] [] {f : EF} (h : ) :
∀ᵐ (x : E) ∂μ,

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