Documentation

Mathlib.Analysis.Calculus.Rademacher

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.

References #

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) :

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 (∑ 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} [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[] ), vs, 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 : EF} (hf : LipschitzWith C f) {s : Set E} (hs : Metric.sphere 0 1 closure s) {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} [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 sDifferentiableWithinAt 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 sDifferentiableWithinAt 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 : EF} (hf : LipschitzOnWith C f s) :
∀ᵐ (x : E) ∂μ, x sDifferentiableWithinAt 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 : EF} (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 : EF} (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.