feat(analysis/calculus/fderiv_measurable): the right derivative is me…

…asurable (#14527)

We already know that the full Fréchet derivative is measurable. In this PR, we follow the same proof to show that the right derivative of a function defined on the real line is also measurable (the target space may be any complete vector space).

src/analysis/calculus/deriv.lean

@@ -225,15 +225,28 @@ theorem unique_diff_within_at.eq_deriv (s : set 𝕜) (H : unique_diff_within_at
   (h : has_deriv_within_at f f' s x) (h₁ : has_deriv_within_at f f₁' s x) : f' = f₁' :=
 smul_right_one_eq_iff.mp $ unique_diff_within_at.eq H h h₁
 
+theorem has_deriv_at_filter_iff_is_o :
+  has_deriv_at_filter f f' x L ↔ (λ x' : 𝕜, f x' - f x - (x' - x) • f') =o[L] (λ x', x' - x) :=
+iff.rfl
+
 theorem has_deriv_at_filter_iff_tendsto :
   has_deriv_at_filter f f' x L ↔
   tendsto (λ x' : 𝕜, ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) L (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
+theorem has_deriv_within_at_iff_is_o :
+  has_deriv_within_at f f' s x
+    ↔ (λ x' : 𝕜, f x' - f x - (x' - x) • f') =o[𝓝[s] x] (λ x', x' - x) :=
+iff.rfl
+
 theorem has_deriv_within_at_iff_tendsto : has_deriv_within_at f f' s x ↔
   tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝[s] x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
+theorem has_deriv_at_iff_is_o :
+  has_deriv_at f f' x ↔ (λ x' : 𝕜, f x' - f x - (x' - x) • f') =o[𝓝 x] (λ x', x' - x) :=
+iff.rfl
+
 theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔
   tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝 x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
@@ -430,6 +443,34 @@ lemma deriv_within_of_open (hs : is_open s) (hx : x ∈ s) :
   deriv_within f s x = deriv f x :=
 by { unfold deriv_within, rw fderiv_within_of_open hs hx, refl }
 
+lemma deriv_mem_iff {f : 𝕜 → F} {s : set F} {x : 𝕜} :
+  deriv f x ∈ s ↔ (differentiable_at 𝕜 f x ∧ deriv f x ∈ s) ∨
+    (¬differentiable_at 𝕜 f x ∧ (0 : F) ∈ s) :=
+by by_cases hx : differentiable_at 𝕜 f x; simp [deriv_zero_of_not_differentiable_at, *]
+
+lemma deriv_within_mem_iff {f : 𝕜 → F} {t : set 𝕜} {s : set F} {x : 𝕜} :
+  deriv_within f t x ∈ s ↔ (differentiable_within_at 𝕜 f t x ∧ deriv_within f t x ∈ s) ∨
+    (¬differentiable_within_at 𝕜 f t x ∧ (0 : F) ∈ s) :=
+by by_cases hx : differentiable_within_at 𝕜 f t x;
+  simp [deriv_within_zero_of_not_differentiable_within_at, *]
+
+lemma differentiable_within_at_Ioi_iff_Ici [partial_order 𝕜] :
+  differentiable_within_at 𝕜 f (Ioi x) x ↔ differentiable_within_at 𝕜 f (Ici x) x :=
+⟨λ h, h.has_deriv_within_at.Ici_of_Ioi.differentiable_within_at,
+λ h, h.has_deriv_within_at.Ioi_of_Ici.differentiable_within_at⟩
+
+lemma deriv_within_Ioi_eq_Ici {E : Type*} [normed_group E] [normed_space ℝ E] (f : ℝ → E) (x : ℝ) :
+  deriv_within f (Ioi x) x = deriv_within f (Ici x) x :=
+begin
+  by_cases H : differentiable_within_at ℝ f (Ioi x) x,
+  { have A := H.has_deriv_within_at.Ici_of_Ioi,
+    have B := (differentiable_within_at_Ioi_iff_Ici.1 H).has_deriv_within_at,
+    simpa using (unique_diff_on_Ici x).eq le_rfl A B },
+  { rw [deriv_within_zero_of_not_differentiable_within_at H,
+      deriv_within_zero_of_not_differentiable_within_at],
+    rwa differentiable_within_at_Ioi_iff_Ici at H }
+end
+
 section congr
 /-! ### Congruence properties of derivatives -/
 

src/analysis/calculus/fderiv.lean

@@ -611,18 +611,14 @@ end
 
 lemma fderiv_mem_iff {f : E → F} {s : set (E →L[𝕜] F)} {x : E} :
   fderiv 𝕜 f x ∈ s ↔ (differentiable_at 𝕜 f x ∧ fderiv 𝕜 f x ∈ s) ∨
-    (0 : E →L[𝕜] F) ∈ s ∧ ¬differentiable_at 𝕜 f x :=
-begin
-  split,
-  { intro hfx,
-    by_cases hx : differentiable_at 𝕜 f x,
-    { exact or.inl ⟨hx, hfx⟩ },
-    { rw [fderiv_zero_of_not_differentiable_at hx] at hfx,
-      exact or.inr ⟨hfx, hx⟩ } },
-  { rintro (⟨hf, hf'⟩|⟨h₀, hx⟩),
-    { exact hf' },
-    { rwa [fderiv_zero_of_not_differentiable_at hx] } }
-end
+    (¬differentiable_at 𝕜 f x ∧ (0 : E →L[𝕜] F) ∈ s) :=
+by by_cases hx : differentiable_at 𝕜 f x; simp [fderiv_zero_of_not_differentiable_at, *]
+
+lemma fderiv_within_mem_iff {f : E → F} {t : set E} {s : set (E →L[𝕜] F)} {x : E} :
+  fderiv_within 𝕜 f t x ∈ s ↔ (differentiable_within_at 𝕜 f t x ∧ fderiv_within 𝕜 f t x ∈ s) ∨
+    (¬differentiable_within_at 𝕜 f t x ∧ (0 : E →L[𝕜] F) ∈ s) :=
+by by_cases hx : differentiable_within_at 𝕜 f t x;
+  simp [fderiv_within_zero_of_not_differentiable_within_at, *]
 
 end fderiv_properties