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 function fderiv 𝕜 f is measurable;
measurable_fderiv_apply_const: for a fixed vector y, the function fun x ↦ fderiv 𝕜 f x y is measurable;
measurable_deriv: the function deriv f is measurable (for f : 𝕜 → 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