Prove $\sum\limits_{n \le k/2} \frac 1 n < \log k$ for Pólya's inequality In Introduction to Analytic Number Theory, theorem 8.21, Apostol's proves Pólya's inequality. The last step of the proof requires showing:
$\sum\limits_{n \le k/2} \frac 1 n < log \; k$
my proof of the theorem shows that we need $k > 1$. Is this a standard inequality? What is an easy way to prove it? I have to code it into a theorem prover!
Here is the proof of the book:



Let's write $H_m = \sum\limits_{n=1}^m \frac{1}{n}$. Then we need to show:
$(1) \; k = 2m + 1 \implies H_m < \log(2m + 1)$ and $(2) \; k = 2m + 2 \implies H_m < \log(2m + 2)$
It's enough to prove $H_m < \log(2m + 1)$.
We have $\log(2m + 1) = \log(2 + \frac{1}{m}) + \log m = \log 2 + \log m + \log(1 + \frac{1}{2m})$.
From, for example, Approximating Euler's constant by Hirschhorn (we actually need a weaker result than theirs, but it's the only reference I found) we have $H_m < \log m + \gamma + \frac{1}{2m}$. So we need $\gamma + \frac{1}{2m} \leqslant \log2 + \log(1 + \frac{1}{2m})$ or $\log 2 - \gamma + \log(1 + \frac{1}{2m}) - \frac{1}{2m} \geqslant 0$.
Derivative of left side is $\frac{1}{2m^2}\cdot\left(\frac{1}{-1 + 1 / 2m} + 1\right) > 0$, so if the inequality holds for some $m$, it holds for all greater $m$. From wolfram, it holds for $m = 2$. For $m = 1$, we can manually check $H_1 = 1$ and $\log(3) > \log(e) > 1$.
(I would like to see some proof involving less calculations, but as I commented we at least need to somehow get $\gamma < 1$)
