Iterated derivatives of analytic functions with power factors

This file contains lemmas about the iterated derivative of a function that factors as a power of (· - z₀) times an analytic function.

theorem iteratedDeriv_mul_pow_sub_of_analytic {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] {k t : ℕ} {z₀ : 𝕜} {R R₁ : 𝕜 → 𝕜} (hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z) (hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) : ∃ (R₂ : 𝕜 → 𝕜), (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧ ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t).factorial / ↑t.factorial * R₁ z + (z - z₀) * R₂ z)

If a function R : 𝕜 → 𝕜 factors as R z = (z - z₀) ^ (k + t) * R₁ z, where R₁ is analytic everywhere, then there exists an everywhere analytic function R₂ : 𝕜 → 𝕜 such that the k-th iterated derivative of R is given by iteratedDeriv k R z = (z - z₀) ^ t * ((k + t)! / t ! * R₁ z + (z - z₀) * R₂ z).