logTaylor — Mathlib

English

Let log denote the complex logarithm. The nth Taylor polynomial of log about the point 1 is the function z ↦ ∑_{j=1}^n (-1)^{j+1} z^j / j from the complex numbers to themselves.

Русский

Пусть log обозначает комплексный логарифм. n-й полином Тейлора log в точке 1 задается как функция z ↦ ∑_{j=1}^n (-1)^{j+1} z^j / j из ℂ в ℂ.

LaTeX

$$$\logTaylor_n(z) = \displaystyle \sum_{j=1}^{n} \frac{(-1)^{j+1}}{j} z^{j}$$$

Lean4

/-- The `n`th Taylor polynomial of `log` at `1`, as a function `ℂ → ℂ` -/
noncomputable def logTaylor (n : ℕ) : ℂ → ℂ := fun z ↦ ∑ j ∈ Finset.range n, (-1) ^ (j + 1) * z ^ j / j

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