hasSum_log_one_add — Mathlib

English

For a ≥ 0, log(1 + a) equals the series with terms 2/(2k+1) (a/(a+2))^{2k+1}.

Русский

Для a ≥ 0 логарифм log(1 + a) равен сумме со степенями a/(a+2): log(1 + a) = ∑ 2/(2k+1) (a/(a+2))^{2k+1}.

LaTeX

$$$\sum_{k=0}^{\infty} 2 \frac{1}{2k+1} \left(\frac{a}{a+2}\right)^{2k+1} = \log(1 + a), \quad a \ge 0$$$

Lean4

/-- Expansion of `log (1 + a)` as a series in powers of `a / (a + 2)`. -/
theorem hasSum_log_one_add {a : ℝ} (h : 0 ≤ a) :
    HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a)) :=
  by
  obtain (rfl | ha0) := eq_or_ne a 0
  · simp [hasSum_zero]
  · convert hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
    all_goals simp [field, add_comm]

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