Sum of the Reciprocals of the Triangular Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Theorem 42 from the 100 Theorems List.

We interpret “triangular numbers” as naturals of the form $\frac{k(k+1)}{2}$ for natural k. We prove that the sum of the reciprocals of the first n triangular numbers is $2 - \frac2n$.

Tags #

discrete_sum

source

theorem theorem_100.inverse_triangle_sum (n : ℕ) :

(finset.range n).sum (λ (k : ℕ), 2 / (↑k * (↑k + 1))) = ite (n = 0) 0 (2 - 2 / ↑n)

Sum of the Reciprocals of the Triangular Numbers