Sum of the Reciprocals of the Triangular Numbers

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

theorem Theorems100.inverse_triangle_sum (n : Nat) : Eq ((Finset.range n).sum fun (k : Nat) => HDiv.hDiv 2 (HMul.hMul k.cast (HAdd.hAdd k.cast 1))) (ite (Eq n 0) 0 (HSub.hSub 2 (HDiv.hDiv 2 n.cast)))

Sum of the Reciprocals of the Triangular Numbers