feat(analysis/special_functions): real derivs of complex.exp and `c…

…omplex.log` (#9422)

src/analysis/complex/basic.lean

@@ -124,6 +124,15 @@ le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
 calc 1 = ∥im_clm I∥ : by simp
    ... ≤ ∥im_clm∥ : unit_le_op_norm _ _ (by simp)
 
+lemma restrict_scalars_one_smul_right' {E : Type*} [normed_group E] [normed_space ℂ E] (x : E) :
+  continuous_linear_map.restrict_scalars ℝ ((1 : ℂ →L[ℂ] ℂ).smul_right x : ℂ →L[ℂ] E) =
+    re_clm.smul_right x + I • im_clm.smul_right x :=
+by { ext ⟨a, b⟩, simp [mk_eq_add_mul_I, add_smul, mul_smul, smul_comm I] }
+
+lemma restrict_scalars_one_smul_right (x : ℂ) :
+  continuous_linear_map.restrict_scalars ℝ ((1 : ℂ →L[ℂ] ℂ).smul_right x : ℂ →L[ℂ] ℂ) = x • 1 :=
+by { ext1 z, dsimp, apply mul_comm }
+
 /-- The complex-conjugation function from `ℂ` to itself is an isometric linear equivalence. -/
 def conj_lie : ℂ ≃ₗᵢ[ℝ] ℂ := ⟨conj_ae.to_linear_equiv, abs_conj⟩
 

src/analysis/complex/real_deriv.lean

@@ -79,6 +79,42 @@ theorem times_cont_diff.real_of_complex {n : with_top ℕ} (h : times_cont_diff
 times_cont_diff_iff_times_cont_diff_at.2 $ λ x,
   h.times_cont_diff_at.real_of_complex
 
+variables {E : Type*} [normed_group E] [normed_space ℂ E]
+
+lemma has_strict_deriv_at.complex_to_real_fderiv' {f : ℂ → E} {x : ℂ} {f' : E}
+  (h : has_strict_deriv_at f f' x) :
+  has_strict_fderiv_at f (re_clm.smul_right f' + I • im_clm.smul_right f') x :=
+by simpa only [complex.restrict_scalars_one_smul_right']
+  using h.has_strict_fderiv_at.restrict_scalars ℝ
+
+lemma has_deriv_at.complex_to_real_fderiv' {f : ℂ → E} {x : ℂ} {f' : E} (h : has_deriv_at f f' x) :
+  has_fderiv_at f (re_clm.smul_right f' + I • im_clm.smul_right f') x :=
+by simpa only [complex.restrict_scalars_one_smul_right']
+  using h.has_fderiv_at.restrict_scalars ℝ
+
+lemma has_deriv_within_at.complex_to_real_fderiv' {f : ℂ → E} {s : set ℂ} {x : ℂ} {f' : E}
+  (h : has_deriv_within_at f f' s x) :
+  has_fderiv_within_at f (re_clm.smul_right f' + I • im_clm.smul_right f') s x :=
+by simpa only [complex.restrict_scalars_one_smul_right']
+  using h.has_fderiv_within_at.restrict_scalars ℝ
+
+lemma has_strict_deriv_at.complex_to_real_fderiv {f : ℂ → ℂ} {f' x : ℂ}
+  (h : has_strict_deriv_at f f' x) :
+  has_strict_fderiv_at f (f' • (1 : ℂ →L[ℝ] ℂ)) x :=
+by simpa only [complex.restrict_scalars_one_smul_right]
+  using h.has_strict_fderiv_at.restrict_scalars ℝ
+
+lemma has_deriv_at.complex_to_real_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : has_deriv_at f f' x) :
+  has_fderiv_at f (f' • (1 : ℂ →L[ℝ] ℂ)) x :=
+by simpa only [complex.restrict_scalars_one_smul_right]
+  using h.has_fderiv_at.restrict_scalars ℝ
+
+lemma has_deriv_within_at.complex_to_real_fderiv {f : ℂ → ℂ} {s : set ℂ} {f' x : ℂ}
+  (h : has_deriv_within_at f f' s x) :
+  has_fderiv_within_at f (f' • (1 : ℂ →L[ℝ] ℂ)) s x :=
+by simpa only [complex.restrict_scalars_one_smul_right]
+  using h.has_fderiv_within_at.restrict_scalars ℝ
+
 end real_deriv_of_complex
 
 section conformality

src/analysis/special_functions/complex/log.lean

@@ -167,6 +167,10 @@ have h0 :  x ≠ 0, by { rintro rfl, simpa [lt_irrefl] using h },
 exp_local_homeomorph.has_strict_deriv_at_symm h h0 $
   by simpa [exp_log h0] using has_strict_deriv_at_exp (log x)
 
+lemma has_strict_fderiv_at_log_real {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) :
+  has_strict_fderiv_at log (x⁻¹ • (1 : ℂ →L[ℝ] ℂ)) x :=
+(has_strict_deriv_at_log h).complex_to_real_fderiv
+
 lemma times_cont_diff_at_log {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) {n : with_top ℕ} :
   times_cont_diff_at ℂ n log x :=
 exp_local_homeomorph.times_cont_diff_at_symm_deriv (exp_ne_zero $ log x) h
@@ -250,6 +254,12 @@ lemma has_strict_deriv_at.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : has_strict
   has_strict_deriv_at (λ t, log (f t)) (f' / f x) x :=
 by { rw div_eq_inv_mul, exact (has_strict_deriv_at_log h₂).comp x h₁ }
 
+lemma has_strict_deriv_at.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : has_strict_deriv_at f f' x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_strict_deriv_at (λ t, log (f t)) (f' / f x) x :=
+by simpa only [div_eq_inv_mul]
+  using (has_strict_fderiv_at_log_real h₂).comp_has_strict_deriv_at x h₁
+
 lemma has_fderiv_at.clog {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E}
   (h₁ : has_fderiv_at f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
   has_fderiv_at (λ t, log (f t)) ((f x)⁻¹ • f') x :=
@@ -260,6 +270,12 @@ lemma has_deriv_at.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : has_deriv_at f f'
   has_deriv_at (λ t, log (f t)) (f' / f x) x :=
 by { rw div_eq_inv_mul, exact (has_strict_deriv_at_log h₂).has_deriv_at.comp x h₁ }
 
+lemma has_deriv_at.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : has_deriv_at f f' x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_deriv_at (λ t, log (f t)) (f' / f x) x :=
+by simpa only [div_eq_inv_mul]
+  using (has_strict_fderiv_at_log_real h₂).has_fderiv_at.comp_has_deriv_at x h₁
+
 lemma differentiable_at.clog {f : E → ℂ} {x : E} (h₁ : differentiable_at ℂ f x)
   (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
   differentiable_at ℂ (λ t, log (f t)) x :=
@@ -276,6 +292,12 @@ lemma has_deriv_within_at.clog {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ}
 by { rw div_eq_inv_mul,
      exact (has_strict_deriv_at_log h₂).has_deriv_at.comp_has_deriv_within_at x h₁ }
 
+lemma has_deriv_within_at.clog_real {f : ℝ → ℂ} {s : set ℝ} {x : ℝ} {f' : ℂ}
+  (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_deriv_within_at (λ t, log (f t)) (f' / f x) s x :=
+by simpa only [div_eq_inv_mul]
+  using (has_strict_fderiv_at_log_real h₂).has_fderiv_at.comp_has_deriv_within_at x h₁
+
 lemma differentiable_within_at.clog {f : E → ℂ} {s : set E} {x : E}
   (h₁ : differentiable_within_at ℂ f s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
   differentiable_within_at ℂ (λ t, log (f t)) s x :=

src/analysis/special_functions/exp_log.lean

@@ -155,6 +155,10 @@ end
 lemma has_strict_deriv_at_exp (x : ℂ) : has_strict_deriv_at exp (exp x) x :=
 times_cont_diff_exp.times_cont_diff_at.has_strict_deriv_at' (has_deriv_at_exp x) le_rfl
 
+lemma has_strict_fderiv_at_exp_real (x : ℂ) :
+  has_strict_fderiv_at exp (exp x • (1 : ℂ →L[ℝ] ℂ)) x :=
+(has_strict_deriv_at_exp x).complex_to_real_fderiv
+
 lemma is_open_map_exp : is_open_map exp :=
 open_map_of_strict_deriv has_strict_deriv_at_exp exp_ne_zero
 
@@ -186,6 +190,25 @@ hc.has_deriv_at.cexp.deriv
 
 end
 
+section
+variables {f : ℝ → ℂ} {f' : ℂ} {x : ℝ} {s : set ℝ}
+
+open complex
+
+lemma has_strict_deriv_at.cexp_real (h : has_strict_deriv_at f f' x) :
+  has_strict_deriv_at (λ x, exp (f x)) (exp (f x) * f') x :=
+(has_strict_fderiv_at_exp_real (f x)).comp_has_strict_deriv_at x h
+
+lemma has_deriv_at.cexp_real (h : has_deriv_at f f' x) :
+  has_deriv_at (λ x, exp (f x)) (exp (f x) * f') x :=
+(has_strict_fderiv_at_exp_real (f x)).has_fderiv_at.comp_has_deriv_at x h
+
+lemma has_deriv_within_at.cexp_real (h : has_deriv_within_at f f' s x) :
+  has_deriv_within_at (λ x, exp (f x)) (exp (f x) * f') s x :=
+(has_strict_fderiv_at_exp_real (f x)).has_fderiv_at.comp_has_deriv_within_at x h
+
+end
+
 section
 
 variables {E : Type*} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ}