logTaylor_succ — Mathlib

English

For every n, the (n+1)st Taylor polynomial equals the nth polynomial plus the nth-term contribution of z^n with coefficient (-1)^{n+1}/n.

Русский

Для каждого n+1-й полином Тейлора равен n-му полиному плюс вклад очередного члена: (-1)^{n+1} z^n / n.

LaTeX

$$$\logTaylor(n+1)(z) = \logTaylor(n)(z) + \dfrac{(-1)^{n+1}}{n} z^n$$$

Lean4

theorem logTaylor_succ (n : ℕ) : logTaylor (n + 1) = logTaylor n + (fun z : ℂ ↦ (-1) ^ (n + 1) * z ^ n / n) :=
  by
  funext
  simpa only [logTaylor] using Finset.sum_range_succ ..

Похожие утверждения