feat(Analysis/Analytic): add AnalyticAt properties for iterated dslope

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -374,3 +374,32 @@ theorem AnalyticOnNhd.map_codiscreteWithin {U : Set 𝕜} {f : 𝕜 → E}
   fun _ hs ↦ mem_map.1 (preimage_mem_codiscreteWithin hfU h₂f hs)
 
 end PreimgCodiscrete
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+private lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s)
+    (hs : s ≠ z₀) : AnalyticAt 𝕜 (_root_.dslope f z₀) s := by
+  have h_inv : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹) s :=
+    (analyticAt_id.sub analyticAt_const).inv (sub_ne_zero.mpr hs)
+  have h_quot : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹ • (f z - f z₀)) s :=
+    h_inv.smul (hf.sub analyticAt_const)
+  have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] _root_.dslope f z₀ := by
+    filter_upwards [isOpen_ne.mem_nhds hs] with z hz
+    exact (_root_.dslope_of_ne f hz).symm
+  exact h_quot.congr h_eq
+
+/-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/
+lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) :
+    AnalyticAt 𝕜 (_root_.dslope f z₀) s := by
+  by_cases hs : s = z₀
+  · subst hs
+    obtain ⟨p, hp⟩ := hf
+    exact ⟨_, hp.has_fpower_series_dslope_fslope⟩
+  · exact hf.dslope_of_ne hs
+
+/-- If `f` is analytic at `s`, then the `n`-th iterated `dslope` of `f` at `z₀`
+is analytic at `s`. -/
+lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
+    AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s :=
+  Function.Iterate.rec _ hf (fun _ hf ↦ hf.dslope) n