Leibniz's rule at a zero of a power

The n-th derivative of z ↦ (z - a) ^ n • h z at a is n! • h a: in Leibniz's rule every other term differentiates (z - a) ^ n fewer than n times and so vanishes at a. If an analytic function f factors as f z = (z - a) ^ n • h z (for instance through AnalyticOnNhd.exists_eq_prod_pow_smul), this recovers its first possibly nonzero derivative at a from the value of the quotient h.

More generally, multiplying by (z - a) ^ p shifts the Taylor coefficients at a up by p without changing them.

Main results

• TauCeti.iteratedDeriv_pow_sub_smul_self: the identity above.
• TauCeti.inv_factorial_smul_iteratedDeriv_pow_sub_smul: the (p + i)-th Taylor coefficient of z ↦ (z - a) ^ p • h z at a is the i-th Taylor coefficient of h.

theorem TauCeti.iteratedDeriv_pow_sub_smul_self {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : 𝕜} {h : 𝕜 → E} {n : ℕ} (hh : ContDiffAt 𝕜 (↑n) h a) : iteratedDeriv n (fun (z : 𝕜) => (z - a) ^ n • h z) a = n.factorial • h a

The n-th derivative of z ↦ (z - a) ^ n • h z at a is n! • h a: in Leibniz's rule every other term differentiates (z - a) ^ n fewer than n times and so vanishes at a.

theorem TauCeti.inv_factorial_smul_iteratedDeriv_pow_sub_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : 𝕜} [CharZero 𝕜] (p i : ℕ) {h : 𝕜 → E} (hh : ContDiffAt 𝕜 (↑p + ↑i) h a) : (↑(p + i).factorial)⁻¹ • iteratedDeriv (p + i) (fun (z : 𝕜) => (z - a) ^ p • h z) a = (↑i.factorial)⁻¹ • iteratedDeriv i h a

Taylor-shift invariance. Multiplying h by (z - a) ^ p shifts its Taylor coefficients at a up by p without changing them: the (p + i)-th Taylor coefficient at a of z ↦ (z - a) ^ p • h z is the i-th Taylor coefficient of h. In Leibniz's rule only the term that differentiates (z - a) ^ p exactly p times survives at a.