Derivative is measurable #
In this file we prove that the derivative of any function with complete codomain is a measurable function. Namely, we prove:
measurableSet_of_differentiableAt
: the set{x | DifferentiableAt π f x}
is measurable;measurable_fderiv
: the functionfderiv π f
is measurable;measurable_fderiv_apply_const
: for a fixed vectory
, the functionfun x β¦ fderiv π f x y
is measurable;measurable_deriv
: the functionderiv f
is measurable (forf : π β F
).
We also show the same results for the right derivative on the real line
(see measurable_derivWithin_Ici
and measurable_derivWithin_Ioi
), following the same
proof strategy.
We also prove measurability statements for functions depending on a parameter: for f : Ξ± β E β F
,
we show the measurability of (p : Ξ± Γ E) β¦ fderiv π (f p.1) p.2
. This requires additional
assumptions. We give versions of the above statements (appending with_param
to their names) when
f
is continuous and E
is locally compact.
Implementation #
We give a proof that avoids second-countability issues, by expressing the differentiability set
as a function of open sets in the following way. Define A (L, r, Ξ΅)
to be the set of points
where, on a ball of radius roughly r
around x
, the function is uniformly approximated by the
linear map L
, up to Ξ΅ r
. It is an open set.
Let also B (L, r, s, Ξ΅) = A (L, r, Ξ΅) β© A (L, s, Ξ΅)
: we require that at two possibly different
scales r
and s
, the function is well approximated by the linear map L
. It is also open.
We claim that the differentiability set of f
is exactly
D = β Ξ΅ > 0, β Ξ΄ > 0, β r, s < Ξ΄, β L, B (L, r, s, Ξ΅)
.
In other words, for any Ξ΅ > 0
, we require that there is a size Ξ΄
such that, for any two scales
below this size, the function is well approximated by a linear map, common to the two scales.
The set β L, B (L, r, s, Ξ΅)
is open, as a union of open sets. Converting the intersections and
unions to countable ones (using real numbers of the form 2 ^ (-n)
), it follows that the
differentiability set is measurable.
To prove the claim, there are two inclusions. One is trivial: if the function is differentiable
at x
, then x
belongs to D
(just take L
to be the derivative, and use that the
differentiability exactly says that the map is well approximated by L
). This is proved in
mem_A_of_differentiable
and differentiable_set_subset_D
.
For the other direction, the difficulty is that L
in the union may depend on Ξ΅, r, s
. The key
point is that, in fact, it doesn't depend too much on them. First, if x
belongs both to
A (L, r, Ξ΅)
and A (L', r, Ξ΅)
, then L
and L'
have to be close on a shell, and thus
βL - L'β
is bounded by Ξ΅
(see norm_sub_le_of_mem_A
). Assume now x β D
. If one has two maps
L
and L'
such that x
belongs to A (L, r, Ξ΅)
and to A (L', r', Ξ΅')
, one deduces that L
is
close to L'
by arguing as follows. Consider another scale s
smaller than r
and r'
. Take a
linear map Lβ
that approximates f
around x
both at scales r
and s
w.r.t. Ξ΅
(it exists as
x
belongs to D
). Take also Lβ
that approximates f
around x
both at scales r'
and s
w.r.t. Ξ΅'
. Then Lβ
is close to L
(as they are close on a shell of radius r
), and Lβ
is
close to Lβ
(as they are close on a shell of radius s
), and L'
is close to Lβ
(as they are
close on a shell of radius r'
). It follows that L
is close to L'
, as we claimed.
It follows that the different approximating linear maps that show up form a Cauchy sequence when
Ξ΅
tends to 0
. When the target space is complete, this sequence converges, to a limit f'
.
With the same kind of arguments, one checks that f
is differentiable with derivative f'
.
To show that the derivative itself is measurable, add in the definition of B
and D
a set
K
of continuous linear maps to which L
should belong. Then, when K
is complete, the set D K
is exactly the set of points where f
is differentiable with a derivative in K
.
Tags #
derivative, measurable function, Borel Ο-algebra
The set A f L r Ξ΅
is the set of points x
around which the function f
is well approximated
at scale r
by the linear map L
, up to an error Ξ΅
. We tweak the definition to make sure that
this is an open set.
Instances For
The set B f K r s Ξ΅
is the set of points x
around which there exists a continuous linear map
L
belonging to K
(a given set of continuous linear maps) that approximates well the
function f
(up to an error Ξ΅
), simultaneously at scales r
and s
.
Instances For
The set D f K
is a complicated set constructed using countable intersections and unions. Its
main use is that, when K
is complete, it is exactly the set of points where f
is differentiable,
with a derivative in K
.
Instances For
Easy inclusion: a differentiability point with derivative in K
belongs to D f K
.
Harder inclusion: at a point in D f K
, the function f
has a derivative, in K
.
The set of differentiability points of a function, with derivative in a given complete set, is Borel-measurable.
The set of differentiability points of a function taking values in a complete space is Borel-measurable.
The set A f L r Ξ΅
is the set of points x
around which the function f
is well approximated
at scale r
by the linear map h β¦ h β’ L
, up to an error Ξ΅
. We tweak the definition to
make sure that this is open on the right.
Instances For
The set B f K r s Ξ΅
is the set of points x
around which there exists a vector
L
belonging to K
(a given set of vectors) such that h β’ L
approximates well f (x + h)
(up to an error Ξ΅
), simultaneously at scales r
and s
.
Instances For
The set D f K
is a complicated set constructed using countable intersections and unions. Its
main use is that, when K
is complete, it is exactly the set of points where f
is differentiable,
with a derivative in K
.
Instances For
Easy inclusion: a differentiability point with derivative in K
belongs to D f K
.
Harder inclusion: at a point in D f K
, the function f
has a derivative, in K
.
The set of right differentiability points of a function, with derivative in a given complete set, is Borel-measurable.
The set of right differentiability points of a function taking values in a complete space is Borel-measurable.
The set of right differentiability points of a function taking values in a complete space is Borel-measurable.
The set of differentiability points of a continuous function depending on a parameter taking values in a complete space is Borel-measurable.