# 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.
• [Pertti Mattila, Geometry of sets and measures in Euclidean spaces, Theorem 7.3][Federer1996]