# mathlib3documentation

analysis.calculus.fderiv_measurable

# 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 function fderiv 𝕜 f is measurable;
• measurable_fderiv_apply_const: for a fixed vector y, the function λ 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_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

theorem continuous_linear_map.measurable_apply₂ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] [borel_space F] :
measurable (λ (p : (E →L[𝕜] F) × E), (p.fst) p.snd)
def fderiv_measurable_aux.A {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) (L : E →L[𝕜] F) (r ε : ) :
set E

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.

Equations
def fderiv_measurable_aux.B {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) (K : set (E →L[𝕜] F)) (r s ε : ) :
set E

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
def fderiv_measurable_aux.D {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) (K : set (E →L[𝕜] F)) :
set E

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.

Equations
theorem fderiv_measurable_aux.is_open_A {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (L : E →L[𝕜] F) (r ε : ) :
is_open r ε)
theorem fderiv_measurable_aux.is_open_B {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {K : set (E →L[𝕜] F)} {r s ε : } :
is_open r s ε)
theorem fderiv_measurable_aux.A_mono {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (L : E →L[𝕜] F) (r : ) {ε δ : } (h : ε δ) :
ε δ
theorem fderiv_measurable_aux.le_of_mem_A {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {r ε : } {L : E →L[𝕜] F} {x : E} (hx : x ε) {y z : E} (hy : y (r / 2)) (hz : z (r / 2)) :
f z - f y - L (z - y) ε * r
theorem fderiv_measurable_aux.mem_A_of_differentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {ε : } (hε : 0 < ε) {x : E} (hx : x) :
(R : ) (H : R > 0), (r : ), r R x (fderiv 𝕜 f x) r ε
theorem fderiv_measurable_aux.norm_sub_le_of_mem_A {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {c : 𝕜} (hc : 1 < c) {r ε : } (hε : 0 < ε) (hr : 0 < r) {x : E} {L₁ L₂ : E →L[𝕜] F} (h₁ : x r ε) (h₂ : x r ε) :
L₁ - L₂ 4 * c * ε
theorem fderiv_measurable_aux.differentiable_set_subset_D {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (K : set (E →L[𝕜] F)) :
{x : E | x f x K}

Easy inclusion: a differentiability point with derivative in K belongs to D f K.

theorem fderiv_measurable_aux.D_subset_differentiable_set {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {K : set (E →L[𝕜] F)} (hK : is_complete K) :
{x : E | x f x K}

Harder inclusion: at a point in D f K, the function f has a derivative, in K.

theorem fderiv_measurable_aux.differentiable_set_eq_D {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} (K : set (E →L[𝕜] F)) (hK : is_complete K) :
{x : E | x f x K} =
theorem measurable_set_of_differentiable_at_of_is_complete (𝕜 : Type u_1) {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) {K : set (E →L[𝕜] F)} (hK : is_complete K) :
measurable_set {x : E | x f x K}

The set of differentiability points of a function, with derivative in a given complete set, is Borel-measurable.

theorem measurable_set_of_differentiable_at (𝕜 : Type u_1) {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F)  :
measurable_set {x : E | x}

The set of differentiability points of a function taking values in a complete space is Borel-measurable.

@[measurability]
theorem measurable_fderiv (𝕜 : Type u_1) {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F)  :
@[measurability]
theorem measurable_fderiv_apply_const (𝕜 : Type u_1) {E : Type u_2} [ E] {F : Type u_3} [ F] (f : E F) [borel_space F] (y : E) :
measurable (λ (x : E), (fderiv 𝕜 f x) y)
@[measurability]
theorem measurable_deriv {𝕜 : Type u_1} {F : Type u_3} [ F] [borel_space F] (f : 𝕜 F) :
theorem strongly_measurable_deriv {𝕜 : Type u_1} {F : Type u_3} [ F] (f : 𝕜 F) :
theorem ae_measurable_deriv {𝕜 : Type u_1} {F : Type u_3} [ F] [borel_space F] (f : 𝕜 F) (μ : measure_theory.measure 𝕜) :
μ
theorem ae_strongly_measurable_deriv {𝕜 : Type u_1} {F : Type u_3} [ F] (f : 𝕜 F) (μ : measure_theory.measure 𝕜) :
def right_deriv_measurable_aux.A {F : Type u_1} [ F] (f : F) (L : F) (r ε : ) :

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.

Equations
def right_deriv_measurable_aux.B {F : Type u_1} [ F] (f : F) (K : set F) (r s ε : ) :

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
def right_deriv_measurable_aux.D {F : Type u_1} [ F] (f : F) (K : set F) :

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.

Equations
theorem right_deriv_measurable_aux.A_mem_nhds_within_Ioi {F : Type u_1} [ F] {f : F} {L : F} {r ε x : } (hx : x ε) :
ε (set.Ioi x)
theorem right_deriv_measurable_aux.B_mem_nhds_within_Ioi {F : Type u_1} [ F] {f : F} {K : set F} {r s ε x : } (hx : x s ε) :
s ε (set.Ioi x)
theorem right_deriv_measurable_aux.measurable_set_B {F : Type u_1} [ F] {f : F} {K : set F} {r s ε : } :
theorem right_deriv_measurable_aux.A_mono {F : Type u_1} [ F] {f : F} (L : F) (r : ) {ε δ : } (h : ε δ) :
ε δ
theorem right_deriv_measurable_aux.le_of_mem_A {F : Type u_1} [ F] {f : F} {r ε : } {L : F} {x : } (hx : x ε) {y z : } (hy : y (x + r / 2)) (hz : z (x + r / 2)) :
f z - f y - (z - y) L ε * r
theorem right_deriv_measurable_aux.mem_A_of_differentiable {F : Type u_1} [ F] {f : F} {ε : } (hε : 0 < ε) {x : } (hx : x) :
(R : ) (H : R > 0), (r : ), r R x (set.Ici x) x) r ε
theorem right_deriv_measurable_aux.norm_sub_le_of_mem_A {F : Type u_1} [ F] {f : F} {r x : } (hr : 0 < r) (ε : ) {L₁ L₂ : F} (h₁ : x ε) (h₂ : x ε) :
L₁ - L₂ 4 * ε
theorem right_deriv_measurable_aux.differentiable_set_subset_D {F : Type u_1} [ F] {f : F} (K : set F) :
{x : | x (set.Ici x) x K}

Easy inclusion: a differentiability point with derivative in K belongs to D f K.

theorem right_deriv_measurable_aux.D_subset_differentiable_set {F : Type u_1} [ F] {f : F} {K : set F} (hK : is_complete K) :
{x : | x (set.Ici x) x K}

Harder inclusion: at a point in D f K, the function f has a derivative, in K`.

theorem right_deriv_measurable_aux.differentiable_set_eq_D {F : Type u_1} [ F] {f : F} (K : set F) (hK : is_complete K) :
{x : | x (set.Ici x) x K} =
theorem measurable_set_of_differentiable_within_at_Ici_of_is_complete {F : Type u_1} [ F] (f : F) {K : set F} (hK : is_complete K) :
measurable_set {x : | x (set.Ici x) x K}

The set of right differentiability points of a function, with derivative in a given complete set, is Borel-measurable.

theorem measurable_set_of_differentiable_within_at_Ici {F : Type u_1} [ F] (f : F)  :

The set of right differentiability points of a function taking values in a complete space is Borel-measurable.

@[measurability]
theorem measurable_deriv_within_Ici {F : Type u_1} [ F] (f : F) [borel_space F] :
measurable (λ (x : ), (set.Ici x) x)
theorem ae_measurable_deriv_within_Ici {F : Type u_1} [ F] (f : F) [borel_space F]  :
ae_measurable (λ (x : ), (set.Ici x) x) μ
theorem measurable_set_of_differentiable_within_at_Ioi {F : Type u_1} [ F] (f : F)  :

The set of right differentiability points of a function taking values in a complete space is Borel-measurable.

@[measurability]
theorem measurable_deriv_within_Ioi {F : Type u_1} [ F] (f : F) [borel_space F] :
measurable (λ (x : ), (set.Ioi x) x)
theorem ae_measurable_deriv_within_Ioi {F : Type u_1} [ F] (f : F) [borel_space F]  :
ae_measurable (λ (x : ), (set.Ioi x) x) μ