English
Let n be a natural number and z with 1+z lying in the slit plane. Then the derivative of log(1+z) − logTaylor(n+1) z at z equals (-z)^n (1+z)^{-1}.
Русский
Пусть n — натуральное число и z таково, что 1+z лежит на разрезанной плоскости. Тогда производная по z у выражения log(1+z) − logTaylor(n+1) z равна (-z)^n (1+z)^{-1}.
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\bigl(\\log(1+z) - \\mathrm{logTaylor}(n+1)\\,z\\bigr) \ = \ (-z)^n\\,(1+z)^{-1}$$$
Lean4
theorem hasDerivAt_log_sub_logTaylor (n : ℕ) {z : ℂ} (hz : 1 + z ∈ slitPlane) :
HasDerivAt (fun z : ℂ ↦ log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z :=
by
convert ((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z) using 1
have hz' : -z ≠ 1 := by
intro H
rw [neg_eq_iff_eq_neg] at H
simp only [H, add_neg_cancel] at hz
exact slitPlane_ne_zero hz rfl
simp_rw [← mul_pow, neg_one_mul, geom_sum_eq hz', ← neg_add', div_neg, add_comm z]
simp [field]
