chore(analysis/complex/basic): add times_cont_diff.real_of_complex (#…

…5073)

Also rename `has_deriv_at_real_of_complex` to `has_deriv_at.real_of_complex`.

src/analysis/complex/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.calculus.deriv
+import analysis.calculus.times_cont_diff
 import analysis.normed_space.finite_dimension
 
 /-!
@@ -24,7 +24,7 @@ it defines functions:
 They are bundled versions of the real part, the imaginary part, and the embedding of `ℝ` in `ℂ`,
 as continuous `ℝ`-linear maps.
 
-`has_deriv_at_real_of_complex` expresses that, if a function on `ℂ` is differentiable (over `ℂ`),
+`has_deriv_at.real_of_complex` expresses that, if a function on `ℂ` is differentiable (over `ℂ`),
 then its restriction to `ℝ` is differentiable over `ℝ`, with derivative the real part of the
 complex derivative.
 -/
@@ -158,16 +158,10 @@ section real_deriv_of_complex
 open complex
 variables {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}
 
-/--
-A preliminary lemma for `has_deriv_at_real_of_complex`,
-which we only separate out to keep the maximum compile time per declaration low.
--/
-lemma has_deriv_at_real_of_complex_aux (h : has_deriv_at e e' z) :
-  has_deriv_at (⇑continuous_linear_map.re ∘ λ {z : ℝ}, e (continuous_linear_map.of_real z))
-    (((continuous_linear_map.re.comp
-       ((continuous_linear_map.smul_right (1 : ℂ →L[ℂ] ℂ) e').restrict_scalars ℝ)).comp
-         continuous_linear_map.of_real) (1 : ℝ))
-    z :=
+/-- If a complex function is differentiable at a real point, then the induced real function is also
+differentiable at this point, with a derivative equal to the real part of the complex derivative. -/
+theorem has_deriv_at.real_of_complex (h : has_deriv_at e e' z) :
+  has_deriv_at (λx:ℝ, (e x).re) e'.re z :=
 begin
   have A : has_fderiv_at continuous_linear_map.of_real continuous_linear_map.of_real z :=
     continuous_linear_map.of_real.has_fderiv_at,
@@ -176,17 +170,23 @@ begin
     (has_deriv_at_iff_has_fderiv_at.1 h).restrict_scalars ℝ,
   have C : has_fderiv_at continuous_linear_map.re continuous_linear_map.re
     (e (continuous_linear_map.of_real z)) := continuous_linear_map.re.has_fderiv_at,
-  exact has_fderiv_at_iff_has_deriv_at.1 (C.comp z (B.comp z A)),
+  simpa using has_fderiv_at_iff_has_deriv_at.1 (C.comp z (B.comp z A)),
 end
 
-/-- If a complex function is differentiable at a real point, then the induced real function is also
-differentiable at this point, with a derivative equal to the real part of the complex derivative. -/
-theorem has_deriv_at_real_of_complex (h : has_deriv_at e e' z) :
-  has_deriv_at (λx:ℝ, (e x).re) e'.re z :=
+theorem times_cont_diff_at.real_of_complex {n : with_top ℕ} (h : times_cont_diff_at ℂ n e z) :
+  times_cont_diff_at ℝ n (λ x : ℝ, (e x).re) z :=
 begin
-  rw (show (λx:ℝ, (e x).re) = (continuous_linear_map.re : ℂ → ℝ) ∘ e ∘ (continuous_linear_map.of_real : ℝ → ℂ),
-    by { ext x, refl }),
-  simpa using has_deriv_at_real_of_complex_aux h,
+  have A : times_cont_diff_at ℝ n continuous_linear_map.of_real z,
+    from continuous_linear_map.of_real.times_cont_diff.times_cont_diff_at,
+  have B : times_cont_diff_at ℝ n e z := h.restrict_scalars ℝ,
+  have C : times_cont_diff_at ℝ n continuous_linear_map.re (e z),
+    from continuous_linear_map.re.times_cont_diff.times_cont_diff_at,
+  exact C.comp z (B.comp z A)
 end
 
+theorem times_cont_diff.real_of_complex {n : with_top ℕ} (h : times_cont_diff ℂ n e) :
+  times_cont_diff ℝ n (λ x : ℝ, (e x).re) :=
+times_cont_diff_iff_times_cont_diff_at.2 $ λ x,
+  h.times_cont_diff_at.real_of_complex
+
 end real_deriv_of_complex

src/analysis/special_functions/exp_log.lean

@@ -119,7 +119,7 @@ namespace real
 variables {x y z : ℝ}
 
 lemma has_deriv_at_exp (x : ℝ) : has_deriv_at exp (exp x) x :=
-has_deriv_at_real_of_complex (complex.has_deriv_at_exp x)
+(complex.has_deriv_at_exp x).real_of_complex
 
 lemma differentiable_exp : differentiable ℝ exp :=
 λx, (has_deriv_at_exp x).differentiable_at

src/analysis/special_functions/trigonometric.lean

@@ -307,7 +307,7 @@ namespace real
 variables {x y z : ℝ}
 
 lemma has_deriv_at_sin (x : ℝ) : has_deriv_at sin (cos x) x :=
-has_deriv_at_real_of_complex (complex.has_deriv_at_sin x)
+(complex.has_deriv_at_sin x).real_of_complex
 
 lemma differentiable_sin : differentiable ℝ sin :=
 λx, (has_deriv_at_sin x).differentiable_at
@@ -324,7 +324,7 @@ differentiable_sin.continuous
 lemma measurable_sin : measurable sin := continuous_sin.measurable
 
 lemma has_deriv_at_cos (x : ℝ) : has_deriv_at cos (-sin x) x :=
-(has_deriv_at_real_of_complex (complex.has_deriv_at_cos x) : _)
+(complex.has_deriv_at_cos x).real_of_complex
 
 lemma differentiable_cos : differentiable ℝ cos :=
 λx, (has_deriv_at_cos x).differentiable_at
@@ -346,7 +346,7 @@ lemma continuous_on_cos {s} : continuous_on cos s := continuous_cos.continuous_o
 lemma measurable_cos : measurable cos := continuous_cos.measurable
 
 lemma has_deriv_at_sinh (x : ℝ) : has_deriv_at sinh (cosh x) x :=
-has_deriv_at_real_of_complex (complex.has_deriv_at_sinh x)
+(complex.has_deriv_at_sinh x).real_of_complex
 
 lemma differentiable_sinh : differentiable ℝ sinh :=
 λx, (has_deriv_at_sinh x).differentiable_at
@@ -363,7 +363,7 @@ differentiable_sinh.continuous
 lemma measurable_sinh : measurable sinh := continuous_sinh.measurable
 
 lemma has_deriv_at_cosh (x : ℝ) : has_deriv_at cosh (sinh x) x :=
-has_deriv_at_real_of_complex (complex.has_deriv_at_cosh x)
+(complex.has_deriv_at_cosh x).real_of_complex
 
 lemma differentiable_cosh : differentiable ℝ cosh :=
 λx, (has_deriv_at_cosh x).differentiable_at
@@ -1990,7 +1990,7 @@ end
 lemma has_deriv_at_tan {x : ℝ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) :
   has_deriv_at tan (1 / (cos x)^2) x :=
 begin
-  convert has_deriv_at_real_of_complex (complex.has_deriv_at_tan (by { convert h, norm_cast } )),
+  convert (complex.has_deriv_at_tan (by { convert h, norm_cast } )).real_of_complex,
   rw ← complex.of_real_re (1/((cos x)^2)),
   simp,
 end