English
For a > 0, log(1 + a^{-1}) has a series expansion in powers of (2a+1)^{-1}, namely ∑_{k≥0} 2/(2k+1) (2a+1)^{-(2k+1)}.
Русский
Для a > 0 логарифм log(1 + a^{-1}) имеет разложение по степенным членам в степени (2a+1)^{-1}: ∑ 2/(2k+1) (2a+1)^{-(2k+1)}.
LaTeX
$$$\sum_{k=0}^{\infty} 2 \frac{1}{2k+1} \left(\frac{1}{2a+1}\right)^{2k+1} = \log(1 + a^{-1}), \quad a > 0$$$
Lean4
/-- Expansion of `log (1 + a⁻¹)` as a series in powers of `1 / (2 * a + 1)`. -/
theorem hasSum_log_one_add_inv {a : ℝ} (h : 0 < a) :
HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹)) :=
by
have h₁ : |1 / (2 * a + 1)| < 1 := by
rw [abs_of_pos, div_lt_one]
· linarith
· linarith
· exact div_pos one_pos (by linarith)
convert hasSum_log_sub_log_of_abs_lt_one h₁ using 1
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
have h₃ := h.ne'
rw [← log_div]
· congr
simp [field]
ring
· field_simp
positivity
· simp [field, h₃]
