English
For |z|<1, the Taylor series of log(1+z) around 0 converges to log(1+z): ∑_{n≥1} (-1)^{n+1} z^n / n = log(1+z).
Русский
При |z|<1 ряд Тейлора логарифма log(1+z) вокруг 0 сходится к log(1+z): ∑_{n≥1} (-1)^{n+1} z^n / n = log(1+z).
LaTeX
$$$\\sum_{n=1}^{\\infty} \\frac{(-1)^{n+1}}{n} z^{n} = \\log(1+z) \\quad (|z|<1)$$$
Lean4
/-- The Taylor series of the complex logarithm at `1` converges to the logarithm in the
open unit disk. -/
theorem hasSum_taylorSeries_log {z : ℂ} (hz : ‖z‖ < 1) :
HasSum (fun n : ℕ ↦ (-1) ^ (n + 1) * z ^ n / n) (log (1 + z)) :=
by
refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_
· refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_
intro n
simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]
rcases n.eq_zero_or_pos with rfl | hn
· simp
conv => enter [2]; rw [← div_one (‖z‖ ^ n)]
gcongr
norm_cast
· rw [← tendsto_sub_nhds_zero_iff]
conv => enter [1, x]; rw [← div_one (_ - _), ← logTaylor]
rw [← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim]
refine IsLittleO.trans_isBigO ?_ <| isBigO_const_one ℂ (1 : ℝ) atTop
have H : (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] (fun n : ℕ ↦ ‖z‖ ^ n) :=
by
have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖ ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ :=
by
rw [norm_sub_rev, norm_pow, norm_norm]
cases n with
| zero => simp [logTaylor_zero]
| succ n =>
refine (norm_log_sub_logTaylor_le n hz).trans ?_
rw [mul_comm, ← div_one ((max _ _) * _)]
gcongr
· exact le_max_right ..
· linarith
exact (isBigOWith_of_le' atTop this).isBigO
refine IsBigO.trans_isLittleO H ?_
convert isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz
exact (one_pow _).symm
