The aim of this post is to show how to work one's way with the Coq proof assistant, for something as simple as the proof that the harmonic series diverges, that is

$$\sum_{k=1}^{\infty} \frac{1}{k} = \infty$$

This proof is based on the idea that the sum can be split in chunks of size $2^n$, each of the chunks being bigger than $1/2$.

The proof is on GitHub, in particular in the files Summing.v and Harmonic.v.

## Variant of the sum notation

A general notation about sums first. I will use a variant of the sum notation: $$\sum_{k}^{(n)} u_k$$ means the sum up to $n-1$, starting at zero. It would usually be written as $\sum_{k=0}^{n-1} u_k$.

## Preliminary results on sums

Some preliminary results first.

An estimate of the sum from an estimate of the sequence:

$$\forall u, N, l,\quad (\forall k < N,\quad u_{k} ≥ l) \implies \forall n ≤ N,\quad \sum_{k}^{(n)}u_{k} ≥ n \ l$$

We now use that to bound sums of decreasing sequences:

$$\forall u, (\forall n1, n1,\quad n1 ≤ n2 \implies u_{n_2} ≤ u_{n_1}) \implies \forall n\quad \sum_{k}^{(n)} u_{k} ≥ n \ u_{n-1}$$

We now use that a sum can be broken down in sub sums:

$$\forall u, n, m, \quad \sum_{k}^{(n+m)} u_k = \sum_{k}^{(n)} u_k + \sum_{k}^{(m)} u_{k+n}$$

The sum respects order of sequences:

$$\forall u, v,\quad (\forall n, \quad u_n ≤ v_n) \implies \forall N\quad \sum_{k}^{(N)} u_k ≤ \sum_{k}^{(N)} v_k$$

Finally, we compute the sum of a constant sequence:

$$\forall C,m,n,\quad \sum_{k}^{(n)} C = nC$$

## Decomposition in chunks

A result about decomposition by chunks. The $n$th chunk is defined as $$C_n(u) := \sum_{k}^{(2^n)} u_{k+2^n}$$

The lemma about chunk decomposition says that

$$\forall u, n,\quad \sum_{k}^{(2^n)} u_k = \sum_{k}^{(n)} C_k(u) + u_0$$

## The harmonic series

All the sequences start at zero, so we define it as

$$H_n := \frac{1}{n+1}$$

Here we have to be very careful. Indeed, the $n$ on the left is a natural number, but the one on the right is a real number. So we use in fact the injection of natural numbers into real numbers. I will denote this injection by $ι$, so the correct definition is in fact $$H_n = \frac{1}{ι(n + 1)}$$

We will need that the harmonic sequence is decreasing: $$\forall n1,n2,\quad n_1 ≤ n_2 \implies u_{n_2} ≤ u_{n_1}$$

## Technical Lemmas

And now we need a couple of boring technical lemmas, some of which have to do with the injection $ι$.

First, the power defined on natural and real numbers is the same:

$$\forall x,m,\quad x = ι(m) \implies \forall n, \quad x^n = ι(m^n)$$

Now we need a result about the injection $ι$, and the minus operation on natural numbers.

$$\forall n, \quad ι(2 \times 2^n - 1) +1 = 2\times 2^n$$

Why is that not obvious?

That is for two reasons. The first is that the power operation is not the same on natural and real number. The second reason is that the subtraction is completely different on natural and real numbers. Indeed, on natural numbers, the following equality is true: $$1-2 = 0$$ In particular, it is not true that $(n - 1) + 1 = n$. Indeed, $(0-1)+1= 0+1 = 1$. In our case, it works because $2\times2^n ≥ 1$, a fact that has to be proved during the proof.

We also need a Lemma showing that $\frac{1}{2} = \frac{2^n}{2^{n+1}}$ for any natural number $n$.

We can do some work now!

## The proof

First show that all the chunks are greater than one half.

$$\forall n,\quad \frac{1}{2} ≤ C_n(H)$$

Now we show that the sum of harmonic terms up to $2^n$ is greater than the sum of constant one halves:

$$\forall n,\quad \sum_{k}^{(n)} \frac{1}{2} ≤ \sum_{k}^{(n)} C_n(H)$$

And now the final theorem

$$\forall n,\quad \sum_{k}^{(2^n)} u_k ≥ \frac{n}{2} + 1$$

Again, in the equation above, the correct expression is $ι(n)/2 + 1$.