A few more lemmas needed by Mandelbrot computations

Author: girving

Series/Analysis/ContDiff.lean

@@ -38,6 +38,9 @@ variable {E : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 variable {G : Type} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
+lemma hasDerivAt_const_mul {x : 𝕜} (c : 𝕜) : HasDerivAt (fun (x : 𝕜) => c * x) c x := by
+  simpa only [mul_one] using (hasDerivAt_id' x).const_mul c
+
 lemma iteratedDeriv_const {n : ℕ} {x : 𝕜} {c : F} :
     iteratedDeriv n (fun _ ↦ c) x = if n = 0 then c else 0 := by
   induction' n with n h generalizing c

Series/Misc/Sqrt.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
 
 /-!
 # The principle branch of the complex square root
@@ -43,3 +44,10 @@ lemma ContDiffAt.csqrt (m : z ∈ slitPlane) {n : WithTop ℕ∞} : ContDiffAt 
 /-- In the right halfplane, `sqrt (z ^ 2) = z` -/
 lemma Complex.sqrt_sq (r : 0 < z.re) : (z ^ 2).sqrt = z := by
   simp only [Complex.sqrt_eq_cpow, Complex.sq_cpow_two_inv r]
+
+lemma HasDerivAt.csqrt {f : ℂ → ℂ} {f' z : ℂ} (m : f z ∈ Complex.slitPlane)
+    (df : HasDerivAt f f' z) : HasDerivAt (fun z : ℂ ↦ (f z).sqrt) (f' / (2 * (f z).sqrt)) z := by
+  simp only [Complex.sqrt_eq_cpow]
+  apply (HasDerivAt.cpow_const (c := 2⁻¹) df m).congr_deriv
+  field_simp
+  norm_num [Complex.cpow_neg, div_eq_inv_mul]

Series/Series/Shift.lean

@@ -68,3 +68,9 @@ lemma series_coeff_shift {f : 𝕜 → 𝕜} {m n k : ℕ} (fc : ContDiffAt 𝕜
     split_ifs with ni
     · simp only [approx_zero]
     · exact c.2
+
+/-- Series shift nicely approximates `z ^ n` -/
+@[approx] lemma Series.approx_one_shift (n : ℕ) :
+    approx ((1 : Series α) <<< n) (fun z : 𝕜 ↦ z ^ n) := by
+  simpa only [mul_one] using Series.approx_shift (𝕜 := 𝕜)
+    (f := (1 : Series α)) (f' := fun z ↦ 1) approx_one n