refactor(analysis/calculus/mean_value): use is_R_or_C in more lemmas (

#6022)

* use `is_R_or_C` in `convex.norm_image_sub_le*` lemmas;
* replace `strict_fderiv_of_cont_diff` with
  `has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at` and
  `has_strict_deriv_at_of_has_deriv_at_of_continuous_at`, slightly change assumptions;
* add `has_ftaylor_series_up_to_on.has_fderiv_at`,
  `has_ftaylor_series_up_to_on.eventually_has_fderiv_at`,
  `has_ftaylor_series_up_to_on.differentiable_at`;
* add `times_cont_diff_at.has_strict_deriv_at` and
  `times_cont_diff_at.has_strict_deriv_at'`;
* prove that `complex.exp` is strictly differentiable and is an open map;
* add `simp` lemma `interior_mem_nhds`.

src/analysis/calculus/mean_value.lean

@@ -15,7 +15,8 @@ In this file we prove the following facts:
 * `convex.norm_image_sub_le_of_norm_deriv_le` : if `f` is differentiable on a convex set `s`
   and the norm of its derivative is bounded by `C`, then `f` is Lipschitz continuous on `s` with
   constant `C`; also a variant in which what is bounded by `C` is the norm of the difference of the
-  derivative from a fixed linear map.
+  derivative from a fixed linear map. This lemma and its versions are formulated using `is_R_or_C`,
+  so they work both for real and complex derivatives.
 
 * `image_le_of*`, `image_norm_le_of_*` : several similar lemmas deducing `f x ≤ B x` or
   `∥f x∥ ≤ B x` from upper estimates on `f'` or `∥f'∥`, respectively. These lemmas differ by
@@ -462,15 +463,29 @@ end
 
 end
 
-/-! ### Vector-valued functions `f : E → F` -/
+/-!
+### Vector-valued functions `f : E → G`
+
+Theorems in this section work both for real and complex differentiable functions. We use assumptions
+`[is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 G]` to achieve this result. For the domain `E` we
+also assume `[normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]` to have a notion of a `convex` set. In both
+interesting cases `𝕜 = ℝ` and `𝕜 = ℂ` the assumption `[is_scalar_tower ℝ 𝕜 E]` is satisfied
+automatically. -/
+
+section
+
+variables {𝕜 G : Type*} [is_R_or_C 𝕜] [normed_space 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
+  [normed_group G] [normed_space 𝕜 G] {f : E → G} {C : ℝ} {s : set E} {x y : E}
+  {f' : E → E →L[𝕜] G} {φ : E →L[𝕜] G}
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`, then
 the function is `C`-Lipschitz. Version with `has_fderiv_within`. -/
 theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le
-  {f : E → F} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ] F)}
   (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
 begin
+  letI : normed_space ℝ G := restrict_scalars.normed_space ℝ 𝕜 G,
+  letI : is_scalar_tower ℝ 𝕜 G := restrict_scalars.is_scalar_tower _ _ _,
   /- By composition with `t ↦ x + t • (y-x)`, we reduce to a statement for functions defined
   on `[0,1]`, for which it is proved in `norm_image_sub_le_of_norm_deriv_le_segment`.
   We just have to check the differentiability of the composition and bounds on its derivative,
@@ -487,22 +502,20 @@ begin
   rw this,
   have : f y = f (g 1), by { simp only [g], rw [one_smul, add_sub_cancel'_right] },
   rw this,
-  have D2: ∀ t ∈ Icc (0:ℝ) 1, has_deriv_within_at (f ∘ g)
-    ((f' (g t) : E → F) (y-x)) (Icc (0:ℝ) 1) t,
+  have D2: ∀ t ∈ Icc (0:ℝ) 1, has_deriv_within_at (f ∘ g) (f' (g t) (y - x)) (Icc 0 1) t,
   { intros t ht,
-    exact (hf (g t) $ segm ht).comp_has_deriv_within_at _
-      (Dg t).has_deriv_within_at segm },
+    have : has_fderiv_within_at f ((f' (g t)).restrict_scalars ℝ) s (g t),
+      from hf (g t) (segm ht),
+    exact this.comp_has_deriv_within_at _ (Dg t).has_deriv_within_at segm },
   apply norm_image_sub_le_of_norm_deriv_le_segment_01' D2,
-  assume t ht,
-  refine le_trans (le_op_norm _ _) (mul_le_mul_of_nonneg_right _ (norm_nonneg _)),
+  refine λ t ht, le_of_op_norm_le _ _ _,
   exact bound (g t) (segm $ Ico_subset_Icc_self ht)
 end
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `has_fderiv_within` and
 `lipschitz_on_with`. -/
 theorem convex.lipschitz_on_with_of_norm_has_fderiv_within_le
-  {f : E → F} {C : ℝ} {s : set E} {f' : E → (E →L[ℝ] F)}
   (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥ ≤ C)
   (hs : convex s) : lipschitz_on_with (nnreal.of_real C) f s :=
 begin
@@ -514,32 +527,32 @@ end
 
 /-- The mean value theorem on a convex set: if the derivative of a function within this set is
 bounded by `C`, then the function is `C`-Lipschitz. Version with `fderiv_within`. -/
-theorem convex.norm_image_sub_le_of_norm_fderiv_within_le {f : E → F} {C : ℝ} {s : set E} {x y : E}
-  (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥fderiv_within ℝ f s x∥ ≤ C)
+theorem convex.norm_image_sub_le_of_norm_fderiv_within_le
+  (hf : differentiable_on 𝕜 f s) (bound : ∀x∈s, ∥fderiv_within 𝕜 f s x∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
 hs.norm_image_sub_le_of_norm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at)
 bound xs ys
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv_within` and
 `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_fderiv_within_le {f : E → F} {C : ℝ} {s : set E}
-  (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥fderiv_within ℝ f s x∥ ≤ C)
+theorem convex.lipschitz_on_with_of_norm_fderiv_within_le
+  (hf : differentiable_on 𝕜 f s) (bound : ∀x∈s, ∥fderiv_within 𝕜 f s x∥ ≤ C)
   (hs : convex s) : lipschitz_on_with (nnreal.of_real C) f s:=
 hs.lipschitz_on_with_of_norm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at) bound
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`,
 then the function is `C`-Lipschitz. Version with `fderiv`. -/
-theorem convex.norm_image_sub_le_of_norm_fderiv_le {f : E → F} {C : ℝ} {s : set E} {x y : E}
-  (hf : ∀ x ∈ s, differentiable_at ℝ f x) (bound : ∀x∈s, ∥fderiv ℝ f x∥ ≤ C)
+theorem convex.norm_image_sub_le_of_norm_fderiv_le
+  (hf : ∀ x ∈ s, differentiable_at 𝕜 f x) (bound : ∀x∈s, ∥fderiv 𝕜 f x∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
 hs.norm_image_sub_le_of_norm_has_fderiv_within_le
 (λ x hx, (hf x hx).has_fderiv_at.has_fderiv_within_at) bound xs ys
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv` and `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_fderiv_le {f : E → F} {C : ℝ} {s : set E}
-  (hf : ∀ x ∈ s, differentiable_at ℝ f x) (bound : ∀x∈s, ∥fderiv ℝ f x∥ ≤ C)
+theorem convex.lipschitz_on_with_of_norm_fderiv_le
+  (hf : ∀ x ∈ s, differentiable_at 𝕜 f x) (bound : ∀x∈s, ∥fderiv 𝕜 f x∥ ≤ C)
   (hs : convex s) : lipschitz_on_with (nnreal.of_real C) f s :=
 hs.lipschitz_on_with_of_norm_has_fderiv_within_le
 (λ x hx, (hf x hx).has_fderiv_at.has_fderiv_within_at) bound
@@ -548,7 +561,6 @@ hs.lipschitz_on_with_of_norm_has_fderiv_within_le
 the derivative and a fixed linear map, rather than a bound on the derivative itself. Version with
 `has_fderiv_within`. -/
 theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le'
-  {f : E → F} {C : ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ] F)} {φ : E →L[ℝ] F}
   (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x - φ∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x - φ (y - x)∥ ≤ C * ∥y - x∥ :=
 begin
@@ -565,36 +577,37 @@ begin
 end
 
 /-- Variant of the mean value inequality on a convex set. Version with `fderiv_within`. -/
-theorem convex.norm_image_sub_le_of_norm_fderiv_within_le' {f : E → F} {C : ℝ} {s : set E} {x y : E}
-  {φ : E →L[ℝ] F} (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥fderiv_within ℝ f s x - φ∥ ≤ C)
+theorem convex.norm_image_sub_le_of_norm_fderiv_within_le'
+  (hf : differentiable_on 𝕜 f s) (bound : ∀x∈s, ∥fderiv_within 𝕜 f s x - φ∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x - φ (y - x)∥ ≤ C * ∥y - x∥ :=
 hs.norm_image_sub_le_of_norm_has_fderiv_within_le' (λ x hx, (hf x hx).has_fderiv_within_at)
 bound xs ys
 
 /-- Variant of the mean value inequality on a convex set. Version with `fderiv`. -/
-theorem convex.norm_image_sub_le_of_norm_fderiv_le' {f : E → F} {C : ℝ} {s : set E} {x y : E}
-  {φ : E →L[ℝ] F} (hf : ∀ x ∈ s, differentiable_at ℝ f x) (bound : ∀x∈s, ∥fderiv ℝ f x - φ∥ ≤ C)
+theorem convex.norm_image_sub_le_of_norm_fderiv_le'
+  (hf : ∀ x ∈ s, differentiable_at 𝕜 f x) (bound : ∀x∈s, ∥fderiv 𝕜 f x - φ∥ ≤ C)
   (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x - φ (y - x)∥ ≤ C * ∥y - x∥ :=
 hs.norm_image_sub_le_of_norm_has_fderiv_within_le'
 (λ x hx, (hf x hx).has_fderiv_at.has_fderiv_within_at) bound xs ys
 
 /-- If a function has zero Fréchet derivative at every point of a convex set,
 then it is a constant on this set. -/
-theorem convex.is_const_of_fderiv_within_eq_zero {s : set E} (hs : convex s)
-  {f : E → F} (hf : differentiable_on ℝ f s) (hf' : ∀ x ∈ s, fderiv_within ℝ f s x = 0)
-  {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
+theorem convex.is_const_of_fderiv_within_eq_zero (hs : convex s) (hf : differentiable_on 𝕜 f s)
+  (hf' : ∀ x ∈ s, fderiv_within 𝕜 f s x = 0) (hx : x ∈ s) (hy : y ∈ s) :
   f x = f y :=
-have bound : ∀ x ∈ s, ∥fderiv_within ℝ f s x∥ ≤ 0,
+have bound : ∀ x ∈ s, ∥fderiv_within 𝕜 f s x∥ ≤ 0,
   from λ x hx, by simp only [hf' x hx, norm_zero],
 by simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm]
   using hs.norm_image_sub_le_of_norm_fderiv_within_le hf bound hx hy
 
-theorem is_const_of_fderiv_eq_zero {f : E → F} (hf : differentiable ℝ f)
-  (hf' : ∀ x, fderiv ℝ f x = 0) (x y : E) :
+theorem is_const_of_fderiv_eq_zero (hf : differentiable 𝕜 f) (hf' : ∀ x, fderiv 𝕜 f x = 0)
+  (x y : E) :
   f x = f y :=
 convex_univ.is_const_of_fderiv_within_eq_zero hf.differentiable_on
   (λ x _, by rw fderiv_within_univ; exact hf' x) trivial trivial
 
+end
+
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
 bounded by `C`, then the function is `C`-Lipschitz. Version with `has_deriv_within`. -/
 theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le
@@ -1088,59 +1101,39 @@ make sense and are enough. Many formulations of the mean value inequality could
 balls over `ℝ` or `ℂ`. For now, we only include the ones that we need.
 -/
 
-variables {𝕜 : Type*} [is_R_or_C 𝕜]
-{G : Type*} [normed_group G] [normed_space 𝕜 G]
-{H : Type*} [normed_group H] [normed_space 𝕜 H]
-
-/-- Variant of the mean value inequality over `ℝ` or `ℂ`, on a ball, using a bound on the difference
-between the derivative and a fixed linear map, rather than a bound on the derivative itself.
-Version with `has_fderiv_within`. -/
-theorem is_R_or_C.norm_image_sub_le_of_norm_has_fderiv_within_le'
-  {f : G → H} {C : ℝ} {x y z : G} {r : ℝ} {f' : G → (G →L[𝕜] H)} {φ : G →L[𝕜] H}
-  (hf : ∀ x ∈ ball z r, has_fderiv_within_at f (f' x) (ball z r) x)
-  (bound : ∀ x ∈ ball z r, ∥f' x - φ∥ ≤ C) (xs : x ∈ ball z r) (ys : y ∈ ball z r) :
-  ∥f y - f x - φ (y - x)∥ ≤ C * ∥y - x∥ :=
-begin
-  letI : normed_space ℝ G := restrict_scalars.normed_space ℝ 𝕜 G,
-  letI : is_scalar_tower ℝ 𝕜 G := restrict_scalars.is_scalar_tower _ _ _,
-  letI : normed_space ℝ H := restrict_scalars.normed_space ℝ 𝕜 H,
-  letI : is_scalar_tower ℝ 𝕜 H := restrict_scalars.is_scalar_tower _ _ _,
-  change ∥f y - f x - (φ.restrict_scalars ℝ) (y - x)∥ ≤ C * ∥y - x∥,
-  have : ∀ x ∈ ball z r, has_fderiv_within_at f ((f' x).restrict_scalars ℝ) (ball z r) x := hf,
-  exact convex.norm_image_sub_le_of_norm_has_fderiv_within_le' this bound (convex_ball _ _) xs ys,
-end
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {G : Type*} [normed_group G] [normed_space 𝕜 G]
+  {H : Type*} [normed_group H] [normed_space 𝕜 H] {f : G → H} {f' : G → G →L[𝕜] H} {x : G}
 
 /-- Over the reals or the complexes, a continuously differentiable function is strictly
 differentiable. -/
-lemma strict_fderiv_of_cont_diff
-  {f : G → H} {s : set G}  {x : G} {f' : G → (G →L[𝕜] H)}
-  (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (hcont : continuous_on f' s) (hs : s ∈ 𝓝 x) :
+lemma has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at
+  (hder : ∀ᶠ y in 𝓝 x, has_fderiv_at f (f' y) y) (hcont : continuous_at f' x) :
   has_strict_fderiv_at f (f' x) x :=
 begin
 -- turn little-o definition of strict_fderiv into an epsilon-delta statement
-  apply is_o_iff_forall_is_O_with.mpr,
-  intros c hc,
-  refine is_O_with.of_bound (eventually_iff.mpr (mem_nhds_iff.mpr _)),
--- the correct ε is the modulus of continuity of f', shrunk to be inside s
-  rcases (metric.continuous_on_iff.mp hcont x (mem_of_nhds hs) c hc) with ⟨ε₁, H₁, hcont'⟩,
-  rcases (mem_nhds_iff.mp hs) with ⟨ε₂, H₂, hε₂⟩,
-  refine ⟨min ε₁ ε₂, lt_min H₁ H₂, _⟩,
--- mess with ε construction
-  set t := ball x (min ε₁ ε₂),
-  have hts : t ⊆ s := λ _ hy, hε₂ (ball_subset_ball (min_le_right ε₁ ε₂) hy),
-  have Hf : ∀ y ∈ t, has_fderiv_within_at f (f' y) t y :=
-    λ y yt, has_fderiv_within_at.mono (hf y (hts yt)) hts,
+  refine is_o_iff.mpr (λ c hc, metric.eventually_nhds_iff_ball.mpr _),
+-- the correct ε is the modulus of continuity of f'
+  rcases mem_nhds_iff.mp (inter_mem_sets hder (hcont $ ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩,
+  refine ⟨ε, ε0, _⟩,
 -- simplify formulas involving the product E × E
   rintros ⟨a, b⟩ h,
-  simp only [mem_set_of_eq, map_sub],
-  have hab : a ∈ t ∧ b ∈ t := by rwa [mem_ball, prod.dist_eq, max_lt_iff] at h,
+  rw [← ball_prod_same, prod_mk_mem_set_prod_eq] at h,
 -- exploit the choice of ε as the modulus of continuity of f'
-  have hf' : ∀ x' ∈ t, ∥f' x' - f' x∥ ≤ c,
-  { intros x' H',
-    refine le_of_lt (hcont' x' (hts H') _),
-    exact ball_subset_ball (min_le_left ε₁ ε₂) H' },
+  have hf' : ∀ x' ∈ ball x ε, ∥f' x' - f' x∥ ≤ c,
+  { intros x' H', rw ← dist_eq_norm, exact le_of_lt (hε H').2 },
 -- apply mean value theorem
-  simpa using is_R_or_C.norm_image_sub_le_of_norm_has_fderiv_within_le' Hf hf' hab.2 hab.1,
+  letI : normed_space ℝ G := restrict_scalars.normed_space ℝ 𝕜 G,
+  letI : is_scalar_tower ℝ 𝕜 G := restrict_scalars.is_scalar_tower _ _ _,
+  refine (convex_ball _ _).norm_image_sub_le_of_norm_has_fderiv_within_le' _ hf' h.2 h.1,
+  exact λ y hy, (hε hy).1.has_fderiv_within_at
 end
 
+/-- Over the reals or the complexes, a continuously differentiable function is strictly
+differentiable. -/
+lemma has_strict_deriv_at_of_has_deriv_at_of_continuous_at {f f' : 𝕜 → G} {x : 𝕜}
+  (hder : ∀ᶠ y in 𝓝 x, has_deriv_at f (f' y) y) (hcont : continuous_at f' x) :
+  has_strict_deriv_at f (f' x) x :=
+has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at (hder.mono (λ y hy, hy.has_fderiv_at)) $
+  (smul_rightL 1).continuous.continuous_at.comp hcont
+
 end is_R_or_C