Sum over values of auxiliary function gets arbitrary big, justification Let $f : \mathbb N_{>0} \to \mathbb R_{\ge 0}$ be a function satisfying $\sum_{n=1}^{\infty} 2^{-f(n)} = \infty$ (like $f(n) = \log n$). Define
$$
 F(n) = \left\lfloor \log_2\left( \sum_{i=1}^n 2^{-f(i)} \right)\right\rfloor.
$$
Why do we have $\sum_{F(n) = m} 2^{-f(n)} \ge 2^m - 1$?
 A: Since $2^{-f(n)} > 0$, we know that $F$ is non-decreasing. Also, since $\sum 2^{-f(n)} = +\infty$, $F$ is unbounded.
If $F$ attains the value $m$, then there is a smallest value $a$ with $F(a) = m$, and a smallest value $b$ with $F(b) \geqslant m+1$. Then we have by definition of $F$
$$\sum_{n = 1}^{a-1} 2^{-f(n)} < 2^m\quad\text{and}\quad \sum_{n = 1}^b 2^{-f(n)} \geqslant 2^{m+1}.$$
It then follows that
$$\sum_{F(n) = m} 2^{-f(n)} = \sum_{n = a}^{b-1} 2^{-f(n)} > 2^{m+1} - 2^{-f(b)} - 2^m = 2^m - 2^{-f(b)} \geqslant 2^m - 1,$$
since $2^{-f(b)} \leqslant 1.$
If $F$ does not attain the value $m$, then we have
$$\sum_{F(n) = m} 2^{-f(n)} = 0,$$
so we need to see that $m \leqslant 0$ to have $2^m - 1 \leqslant 0$.
Now suppose that $m > 0$ and $b$ is the smallest positive integer with $F(b) > m$. Then we have
$$\sum_{n = 1}^b 2^{-f(n)} \geqslant 2^{m+1} \geqslant 4,$$
so in particular $b \geqslant 4$, and
$$2^{m+1} > \sum_{n = 1}^{b-1} 2^{-f(n)} = \sum_{n = 1}^b 2^{-f(n)} - 2^{-f(b)} \geqslant 2^{m+1}-1 \geqslant 2^m,$$
so we have $F(b-1) = m$, and $F$ does not skip the value $m$, as desired.
A: $F(n)=m$ means that
$$
2^m\le\sum_{k=1}^n2^{-f(k)}\lt2^{m+1}\tag{1}
$$
Let $n_m$ be the smallest $n$ so that $F(n)=m$. Then
$$
\sum_{k=1}^{n_m-1}2^{-f(k)}\lt2^m\tag{2}
$$
Since $f(k)\ge0$, we have $2^{-f(k)}\le1$. Therefore, since
$$
\sum_{k=1}^{n_{m+1}}2^{-f(k)}\ge2^{m+1}\tag{3}
$$
we have
$$
\sum_{k=1}^{n_{m+1}-1}2^{-f(k)}\ge2^{m+1}-1\tag{4}
$$
Therefore, subtracting $(2)$ from $(4)$, we get
$$
\begin{align}
\sum_{F(k)=m}2^{-f(k)}
&=\sum_{k=1}^{n_{m+1}-1}2^{-f(k)}-\sum_{k=1}^{n_m-1}2^{-f(k)}\\[6pt]
&\gt2^m-1\tag{5}
\end{align}
$$
