feat(analysis/special_functions/exp_log): exp is infinitely smooth (#…

…5086)

* Prove that `complex.exp` and `real.exp` are infinitely smooth.
* Generalize lemmas about `exp ∘ f` to `f : E → ℂ` or `f : E → ℝ`
  instead of `f : ℂ → ℂ` or `f : ℝ → ℝ`.

src/analysis/special_functions/exp_log.lean

@@ -69,16 +69,23 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
 
+lemma times_cont_diff_exp : ∀ {n}, times_cont_diff ℂ n exp :=
+begin
+  refine times_cont_diff_all_iff_nat.2 (λ n, _),
+  induction n with n ihn,
+  { exact times_cont_diff_zero.2 continuous_exp },
+  { rw times_cont_diff_succ_iff_deriv,
+    use differentiable_exp,
+    rwa deriv_exp }
+end
+
 lemma measurable_exp : measurable exp := continuous_exp.measurable
 
 end complex
 
 section
 variables {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ}
 
-lemma measurable.cexp (hf : measurable f) : measurable (λ x, complex.exp (f x)) :=
-complex.measurable_exp.comp hf
-
 lemma has_deriv_at.cexp (hf : has_deriv_at f f' x) :
   has_deriv_at (λ x, complex.exp (f x)) (complex.exp (f x) * f') x :=
 (complex.has_deriv_at_exp (f x)).comp x hf
@@ -87,13 +94,41 @@ lemma has_deriv_within_at.cexp (hf : has_deriv_within_at f f' s x) :
   has_deriv_within_at (λ x, complex.exp (f x)) (complex.exp (f x) * f') s x :=
 (complex.has_deriv_at_exp (f x)).comp_has_deriv_within_at x hf
 
+lemma deriv_within_cexp (hf : differentiable_within_at ℂ f s x)
+  (hxs : unique_diff_within_at ℂ s x) :
+  deriv_within (λx, complex.exp (f x)) s x = complex.exp (f x) * (deriv_within f s x) :=
+hf.has_deriv_within_at.cexp.deriv_within hxs
+
+@[simp] lemma deriv_cexp (hc : differentiable_at ℂ f x) :
+  deriv (λx, complex.exp (f x)) x = complex.exp (f x) * (deriv f x) :=
+hc.has_deriv_at.cexp.deriv
+
+end
+
+section
+
+variables {E : Type*} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ}
+  {x : E} {s : set E}
+
+lemma measurable.cexp {α : Type*} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
+  measurable (λ x, complex.exp (f x)) :=
+complex.measurable_exp.comp hf
+
+lemma has_fderiv_within_at.cexp (hf : has_fderiv_within_at f f' s x) :
+  has_fderiv_within_at (λ x, complex.exp (f x)) (complex.exp (f x) • f') s x :=
+(complex.has_deriv_at_exp (f x)).comp_has_fderiv_within_at x hf
+
+lemma has_fderiv_at.cexp (hf : has_fderiv_at f f' x) :
+  has_fderiv_at (λ x, complex.exp (f x)) (complex.exp (f x) • f') x :=
+has_fderiv_within_at_univ.1 $ hf.has_fderiv_within_at.cexp
+
 lemma differentiable_within_at.cexp (hf : differentiable_within_at ℂ f s x) :
   differentiable_within_at ℂ (λ x, complex.exp (f x)) s x :=
-hf.has_deriv_within_at.cexp.differentiable_within_at
+hf.has_fderiv_within_at.cexp.differentiable_within_at
 
 @[simp] lemma differentiable_at.cexp (hc : differentiable_at ℂ f x) :
   differentiable_at ℂ (λx, complex.exp (f x)) x :=
-hc.has_deriv_at.cexp.differentiable_at
+hc.has_fderiv_at.cexp.differentiable_at
 
 lemma differentiable_on.cexp (hc : differentiable_on ℂ f s) :
   differentiable_on ℂ (λx, complex.exp (f x)) s :=
@@ -103,14 +138,21 @@ lemma differentiable_on.cexp (hc : differentiable_on ℂ f s) :
   differentiable ℂ (λx, complex.exp (f x)) :=
 λx, (hc x).cexp
 
-lemma deriv_within_cexp (hf : differentiable_within_at ℂ f s x)
-  (hxs : unique_diff_within_at ℂ s x) :
-  deriv_within (λx, complex.exp (f x)) s x = complex.exp (f x) * (deriv_within f s x) :=
-hf.has_deriv_within_at.cexp.deriv_within hxs
+lemma times_cont_diff.cexp {n} (h : times_cont_diff ℂ n f) :
+  times_cont_diff ℂ n (λ x, complex.exp (f x)) :=
+complex.times_cont_diff_exp.comp h
 
-@[simp] lemma deriv_cexp (hc : differentiable_at ℂ f x) :
-  deriv (λx, complex.exp (f x)) x = complex.exp (f x) * (deriv f x) :=
-hc.has_deriv_at.cexp.deriv
+lemma times_cont_diff_at.cexp {n} (hf : times_cont_diff_at ℂ n f x) :
+  times_cont_diff_at ℂ n (λ x, complex.exp (f x)) x :=
+complex.times_cont_diff_exp.times_cont_diff_at.comp x hf
+
+lemma times_cont_diff_on.cexp {n} (hf : times_cont_diff_on ℂ n f s) :
+  times_cont_diff_on ℂ n (λ x, complex.exp (f x)) s :=
+complex.times_cont_diff_exp.comp_times_cont_diff_on  hf
+
+lemma times_cont_diff_within_at.cexp {n} (hf : times_cont_diff_within_at ℂ n f s x) :
+  times_cont_diff_within_at ℂ n (λ x, complex.exp (f x)) s x :=
+complex.times_cont_diff_exp.times_cont_diff_at.comp_times_cont_diff_within_at x hf
 
 end
 
@@ -121,6 +163,9 @@ variables {x y z : ℝ}
 lemma has_deriv_at_exp (x : ℝ) : has_deriv_at exp (exp x) x :=
 (complex.has_deriv_at_exp x).real_of_complex
 
+lemma times_cont_diff_exp {n} : times_cont_diff ℝ n exp :=
+complex.times_cont_diff_exp.real_of_complex
+
 lemma differentiable_exp : differentiable ℝ exp :=
 λx, (has_deriv_at_exp x).differentiable_at
 
@@ -143,17 +188,11 @@ end real
 
 
 section
-/-! Register lemmas for the derivatives of the composition of `real.exp`, `real.cos`, `real.sin`,
-`real.cosh` and `real.sinh` with a differentiable function, for standalone use and use with
-`simp`. -/
+/-! Register lemmas for the derivatives of the composition of `real.exp` with a differentiable
+function, for standalone use and use with `simp`. -/
 
 variables {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ}
 
-/-! `real.exp`-/
-
-lemma measurable.exp (hf : measurable f) : measurable (λ x, real.exp (f x)) :=
-real.measurable_exp.comp hf
-
 lemma has_deriv_at.exp (hf : has_deriv_at f f' x) :
   has_deriv_at (λ x, real.exp (f x)) (real.exp (f x) * f') x :=
 (real.has_deriv_at_exp (f x)).comp x hf
@@ -162,13 +201,63 @@ lemma has_deriv_within_at.exp (hf : has_deriv_within_at f f' s x) :
   has_deriv_within_at (λ x, real.exp (f x)) (real.exp (f x) * f') s x :=
 (real.has_deriv_at_exp (f x)).comp_has_deriv_within_at x hf
 
+lemma deriv_within_exp (hf : differentiable_within_at ℝ f s x)
+  (hxs : unique_diff_within_at ℝ s x) :
+  deriv_within (λx, real.exp (f x)) s x = real.exp (f x) * (deriv_within f s x) :=
+hf.has_deriv_within_at.exp.deriv_within hxs
+
+@[simp] lemma deriv_exp (hc : differentiable_at ℝ f x) :
+  deriv (λx, real.exp (f x)) x = real.exp (f x) * (deriv f x) :=
+hc.has_deriv_at.exp.deriv
+
+end
+
+section
+/-! Register lemmas for the derivatives of the composition of `real.exp` with a differentiable
+function, for standalone use and use with `simp`. -/
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ}
+  {x : E} {s : set E}
+
+lemma measurable.exp {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
+  measurable (λ x, real.exp (f x)) :=
+real.measurable_exp.comp hf
+
+lemma times_cont_diff.exp {n} (hf : times_cont_diff ℝ n f) :
+  times_cont_diff ℝ n (λ x, real.exp (f x)) :=
+real.times_cont_diff_exp.comp hf
+
+lemma times_cont_diff_at.exp {n} (hf : times_cont_diff_at ℝ n f x) :
+  times_cont_diff_at ℝ n (λ x, real.exp (f x)) x :=
+real.times_cont_diff_exp.times_cont_diff_at.comp x hf
+
+lemma times_cont_diff_on.exp {n} (hf : times_cont_diff_on ℝ n f s) :
+  times_cont_diff_on ℝ n (λ x, real.exp (f x)) s :=
+real.times_cont_diff_exp.comp_times_cont_diff_on  hf
+
+lemma times_cont_diff_within_at.exp {n} (hf : times_cont_diff_within_at ℝ n f s x) :
+  times_cont_diff_within_at ℝ n (λ x, real.exp (f x)) s x :=
+real.times_cont_diff_exp.times_cont_diff_at.comp_times_cont_diff_within_at x hf
+
+lemma has_fderiv_within_at.exp (hf : has_fderiv_within_at f f' s x) :
+  has_fderiv_within_at (λ x, real.exp (f x)) (real.exp (f x) • f') s x :=
+begin
+  convert (has_deriv_at_iff_has_fderiv_at.1 $
+    real.has_deriv_at_exp (f x)).comp_has_fderiv_within_at x hf,
+  ext y, simp [mul_comm]
+end
+
+lemma has_fderiv_at.exp (hf : has_fderiv_at f f' x) :
+  has_fderiv_at (λ x, real.exp (f x)) (real.exp (f x) • f') x :=
+has_fderiv_within_at_univ.1 $ hf.has_fderiv_within_at.exp
+
 lemma differentiable_within_at.exp (hf : differentiable_within_at ℝ f s x) :
   differentiable_within_at ℝ (λ x, real.exp (f x)) s x :=
-hf.has_deriv_within_at.exp.differentiable_within_at
+hf.has_fderiv_within_at.exp.differentiable_within_at
 
 @[simp] lemma differentiable_at.exp (hc : differentiable_at ℝ f x) :
   differentiable_at ℝ (λx, real.exp (f x)) x :=
-hc.has_deriv_at.exp.differentiable_at
+hc.has_fderiv_at.exp.differentiable_at
 
 lemma differentiable_on.exp (hc : differentiable_on ℝ f s) :
   differentiable_on ℝ (λx, real.exp (f x)) s :=
@@ -178,14 +267,14 @@ lemma differentiable_on.exp (hc : differentiable_on ℝ f s) :
   differentiable ℝ (λx, real.exp (f x)) :=
 λx, (hc x).exp
 
-lemma deriv_within_exp (hf : differentiable_within_at ℝ f s x)
+lemma fderiv_within_exp (hf : differentiable_within_at ℝ f s x)
   (hxs : unique_diff_within_at ℝ s x) :
-  deriv_within (λx, real.exp (f x)) s x = real.exp (f x) * (deriv_within f s x) :=
-hf.has_deriv_within_at.exp.deriv_within hxs
+  fderiv_within ℝ (λx, real.exp (f x)) s x = real.exp (f x) • (fderiv_within ℝ f s x) :=
+hf.has_fderiv_within_at.exp.fderiv_within hxs
 
-@[simp] lemma deriv_exp (hc : differentiable_at ℝ f x) :
-  deriv (λx, real.exp (f x)) x = real.exp (f x) * (deriv f x) :=
-hc.has_deriv_at.exp.deriv
+@[simp] lemma fderiv_exp (hc : differentiable_at ℝ f x) :
+  fderiv ℝ (λx, real.exp (f x)) x = real.exp (f x) • (fderiv ℝ f x) :=
+hc.has_fderiv_at.exp.fderiv
 
 end