hasSum_taylorSeries_neg_log — Mathlib

English

For |z|<1, the series ∑ z^n/n converges to −log(1−z).

Русский

Для |z|<1 ряд ∑ z^n/n сходится к −log(1−z).

LaTeX

$$$\\sum_{n=1}^{\\infty} \\frac{z^{n}}{n} = -\\log(1 - z) \\quad (|z|<1)$$$

Lean4

/-- The series `∑ z^n/n` converges to `-log (1-z)` on the open unit disk. -/
theorem hasSum_taylorSeries_neg_log {z : ℂ} (hz : ‖z‖ < 1) : HasSum (fun n : ℕ ↦ z ^ n / n) (-log (1 - z)) :=
  by
  conv => enter [1, n]; rw [← neg_neg (z ^ n / n)]
  refine HasSum.neg ?_
  convert hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz) using 2 with n
  rcases n.eq_zero_or_pos with rfl | hn
  · simp
  simp [field, pow_add, ← mul_pow]

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