Theorems · Theorem · real analysis

Real.hasSum_log_sub_log_of_abs_lt_one

∀ {x : ℝ}, |x| < 1 → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (Real.log (1 + x) - Real.log (1 - x))

Power series expansion of log(1 + x) - log(1 - x) for |x| < 1.

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Deriv

Cited by

1 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound