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
thenf
is ae differentiable in the direction ofv
. SeeLipschitzWith.ae_lineDifferentiableAt
. - Step 2: the line derivative
LineDeriv ℝ f x v
is ae linear inv
. Morrey proves this by a duality argument, integrating against a smooth compactly supported functiong
, passing the derivative tog
by integration by parts, and using the linearity of the derivative ofg
. SeeLipschitzWith.ae_lineDeriv_sum_eq
. - Step 3: consider a countable dense set
s
of directions. Almost everywhere, the functionf
is line-differentiable in all these directions and the line derivative is linear. Approximating any direction by a direction ins
and using the fact thatf
is Lipschitz to control the error, it follows thatf
is Fréchet-differentiable at these points. SeeLipschitzWith.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.