Derivative is measurable #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that the derivative of any function with complete codomain is a measurable function. Namely, we prove:
measurable_set_of_differentiable_at: the set{x | differentiable_at 𝕜 f x}is measurable;measurable_fderiv: the functionfderiv 𝕜 fis measurable;measurable_fderiv_apply_const: for a fixed vectory, the functionλ x, fderiv 𝕜 f x yis measurable;measurable_deriv: the functionderiv fis measurable (forf : 𝕜 → F).
We also show the same results for the right derivative on the real line
(see measurable_deriv_within_Ici and ``measurable_deriv_within_Ioi`), following the same
proof strategy.
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.
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.
Equations
- fderiv_measurable_aux.B f K r s ε = ⋃ (L : E →L[𝕜] F) (H : L ∈ K), fderiv_measurable_aux.A f L r ε ∩ fderiv_measurable_aux.A f L s ε
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.
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.
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.
Equations
- right_deriv_measurable_aux.B f K r s ε = ⋃ (L : F) (H : L ∈ K), right_deriv_measurable_aux.A f L r ε ∩ right_deriv_measurable_aux.A f L s ε
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.
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.