# 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 #

### 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.

### 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.

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

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 #

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.

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.

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.

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.

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

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

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