English
Let n be a natural number and z a complex number. The derivative of the (n+1)-st truncated Taylor polynomial of the logarithm at z equals the finite sum ∑_{j=0}^{n-1} (-1)^j z^j.
Русский
Пусть n — натуральное число и z — комплексное число. Производная (n+1)-й усечённой тейлоровской полиномы логарифма в точке z равна конечной сумме ∑_{j=0}^{n-1} (-1)^j z^j.
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\mathrm{logTaylor}(n+1; z) \ = \ \\sum_{j=0}^{n-1} (-1)^j z^j$$$
Lean4
theorem hasDerivAt_logTaylor (n : ℕ) (z : ℂ) :
HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z := by
induction n with
| zero => simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]
| succ n ih =>
rw [logTaylor_succ]
simp only [Nat.cast_add, Nat.cast_one, Finset.sum_range_succ]
refine HasDerivAt.add ih ?_
simp only [mul_div_assoc]
have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z :=
by
simp_rw [div_eq_mul_inv]
convert HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
simp [field]
convert HasDerivAt.const_mul _ this using 2
ring
