feat(analysis/calculus): assorted simple lemmas (#10975)

Various lemmas from the formalization of the Cauchy integral formula (#10000 and some later developments on top of it).
Also add `@[measurability]` attrs to theorems like `measurable_fderiv`.

src/analysis/calculus/deriv.lean

@@ -1060,6 +1060,12 @@ theorem has_deriv_at_filter.scomp
   has_deriv_at_filter (g₁ ∘ h) (h' • g₁') x L :=
 by simpa using ((hg.restrict_scalars 𝕜).comp x hh hL).has_deriv_at_filter
 
+theorem has_deriv_within_at.scomp_has_deriv_at
+  (hg : has_deriv_within_at g₁ g₁' s' (h x))
+  (hh : has_deriv_at h h' x) (hs : ∀ x, h x ∈ s') :
+  has_deriv_at (g₁ ∘ h) (h' • g₁') x :=
+hg.scomp x hh $ tendsto_inf.2 ⟨hh.continuous_at, tendsto_principal.2 $ eventually_of_forall hs⟩
+
 theorem has_deriv_within_at.scomp
   (hg : has_deriv_within_at g₁ g₁' t' (h x))
   (hh : has_deriv_within_at h h' s x) (hst : maps_to h s t') :

src/analysis/calculus/fderiv.lean

@@ -451,6 +451,14 @@ lemma differentiable_on.has_fderiv_at (h : differentiable_on 𝕜 f s) (hs : s 
   has_fderiv_at f (fderiv 𝕜 f x) x :=
 ((h x (mem_of_mem_nhds hs)).differentiable_at hs).has_fderiv_at
 
+lemma differentiable_on.differentiable_at (h : differentiable_on 𝕜 f s) (hs : s ∈ 𝓝 x) :
+  differentiable_at 𝕜 f x :=
+(h.has_fderiv_at hs).differentiable_at
+
+lemma differentiable_on.eventually_differentiable_at (h : differentiable_on 𝕜 f s) (hs : s ∈ 𝓝 x) :
+  ∀ᶠ y in 𝓝 x, differentiable_at 𝕜 f y :=
+(eventually_eventually_nhds.2 hs).mono $ λ y, h.differentiable_at
+
 lemma has_fderiv_at.fderiv (h : has_fderiv_at f f' x) : fderiv 𝕜 f x = f' :=
 by { ext, rw h.unique h.differentiable_at.has_fderiv_at }
 

src/analysis/calculus/fderiv_measurable.lean

@@ -389,7 +389,7 @@ begin
   simp
 end
 
-lemma measurable_fderiv : measurable (fderiv 𝕜 f) :=
+@[measurability] lemma measurable_fderiv : measurable (fderiv 𝕜 f) :=
 begin
   refine measurable_of_is_closed (λ s hs, _),
   have : fderiv 𝕜 f ⁻¹' s = {x | differentiable_at 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪
@@ -400,14 +400,14 @@ begin
     ((measurable_set.const _).inter (measurable_set_of_differentiable_at _ _).compl)
 end
 
-lemma measurable_fderiv_apply_const [measurable_space F] [borel_space F] (y : E) :
+@[measurability] lemma measurable_fderiv_apply_const [measurable_space F] [borel_space F] (y : E) :
   measurable (λ x, fderiv 𝕜 f x y) :=
 (continuous_linear_map.measurable_apply y).comp (measurable_fderiv 𝕜 f)
 
 variable {𝕜}
 
-lemma measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜] [measurable_space F]
-  [borel_space F] (f : 𝕜 → F) : measurable (deriv f) :=
+@[measurability] lemma measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜]
+  [measurable_space F] [borel_space F] (f : 𝕜 → F) : measurable (deriv f) :=
 by simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1
 
 lemma ae_measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜] [measurable_space F]

src/analysis/calculus/mean_value.lean

@@ -694,6 +694,20 @@ theorem lipschitz_on_with_of_nnnorm_deriv_le {C : ℝ≥0}
 hs.lipschitz_on_with_of_nnnorm_has_deriv_within_le
 (λ x hx, (hf x hx).has_deriv_at.has_deriv_within_at) bound
 
+/-- The mean value theorem set in dimension 1: if the derivative of a function is bounded by `C`,
+then the function is `C`-Lipschitz.  Version with `deriv` and `lipschitz_with`. -/
+theorem _root_.lipschitz_with_of_nnnorm_deriv_le {C : ℝ≥0} (hf : differentiable 𝕜 f)
+  (bound : ∀ x, ∥deriv f x∥₊ ≤ C) : lipschitz_with C f :=
+lipschitz_on_univ.1 $ convex_univ.lipschitz_on_with_of_nnnorm_deriv_le (λ x hx, hf x)
+  (λ x hx, bound x)
+
+/-- If `f : 𝕜 → G`, `𝕜 = R` or `𝕜 = ℂ`, is differentiable everywhere and its derivative equal zero,
+then it is a constant function. -/
+theorem _root_.is_const_of_deriv_eq_zero (hf : differentiable 𝕜 f) (hf' : ∀ x, deriv f x = 0)
+  (x y : 𝕜) :
+  f x = f y :=
+is_const_of_fderiv_eq_zero hf (λ z, by { ext, simp [← deriv_fderiv, hf'] }) _ _
+
 end convex
 
 end