Alternating harmonic series

TheoremThe alternating harmonic series sums to \(\log 2\)#✓fully proved

The partial sums \(\sum_{i=0}^{k-1} (-1)^i / (i + 1)\) of real numbers converge to \(\log 2\) as \(k \to \infty\).

theorem tendsto_sum_alternating_harmonic :
    Filter.Tendsto (fun k => ∑ i ∈ Finset.range k, (-1 : ℝ) ^ i / (↑i + 1)) Filter.atTop
      (𝓝 (Real.log 2))

TheoremThe alternating harmonic series is not absolutely summable#✓fully proved

The series of real numbers \(\sum_{n \ge 0} \left|(-1)^n / (n + 1)\right|\) is not summable.

The series of absolute values is the harmonic series \(\sum_{n \ge 0} 1 / (n + 1)\), which diverges. In particular the convergence of the alternating harmonic series to \(\log 2\) is only conditional.

theorem not_summable_abs_alternating_harmonic :
    ¬ Summable (fun n : ℕ => |(-1 : ℝ) ^ n / (↑n + 1)|)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.