1 Sum Formulas
This chapter contains classical summation formulas that serve as a demonstration of the Lean Blueprint workflow.
1.1 Sum of Natural Numbers
For all \(n \in \mathbb {N}\):
\[ \sum _{i=0}^{n} i = \frac{n(n+1)}{2} \]
Proof
By induction on \(n\). The base case \(n = 0\) is trivial since both sides equal \(0\). For the inductive step, assuming the formula holds for \(n\), we have:
\[ \sum _{i=0}^{n+1} i = \sum _{i=0}^{n} i + (n+1) = \frac{n(n+1)}{2} + (n+1) = \frac{(n+1)(n+2)}{2} \]
which is the formula for \(n+1\).
1.2 Sum of Squares
For all \(n \in \mathbb {N}\):
\[ \sum _{i=0}^{n} i^2 = \frac{n(n+1)(2n+1)}{6} \]
Proof
By induction on \(n\). The base case \(n = 0\) is trivial. For the inductive step, assuming the formula holds for \(n\):
\[ \sum _{i=0}^{n+1} i^2 = \sum _{i=0}^{n} i^2 + (n+1)^2 = \frac{n(n+1)(2n+1)}{6} + (n+1)^2 \]
Simplifying:
\[ = \frac{n(n+1)(2n+1) + 6(n+1)^2}{6} = \frac{(n+1)(2n^2 + n + 6n + 6)}{6} = \frac{(n+1)(n+2)(2n+3)}{6} \]
which is the formula for \(n+1\).