English
For |x| < 1, log(1+x) - log(1-x) equals the sum over k≥0 of 2/(2k+1) x^{2k+1}.
Русский
Для |x| < 1 log(1+x) - log(1-x) совпадает с суммой по k≥0: 2/(2k+1) x^{2k+1}.
LaTeX
$$$\sum_{k=0}^{\infty} \dfrac{2}{2k+1} x^{2k+1} = \log(1+x) - \log(1-x), \quad |x|<1$$$
Lean4
/-- Power series expansion of `log(1 + x) - log(1 - x)` for `|x| < 1`. -/
theorem hasSum_log_sub_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) :
HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x)) :=
by
set term := fun n : ℕ => -1 * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + x ^ (n + 1) / (n + 1)
have h_term_eq_goal : term ∘ (2 * ·) = fun k : ℕ => 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1) :=
by
ext n
dsimp only [term, (· ∘ ·)]
rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
push_cast
ring_nf
rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]
· have h₁ := (hasSum_pow_div_log_of_abs_lt_one (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
convert h₁.add (hasSum_pow_div_log_of_abs_lt_one h) using 1
ring_nf
· intro m hm
rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm
dsimp [term]
rw [Even.neg_pow hm, neg_one_mul, neg_add_cancel]
