Harmonic numbers grow like log n

Statement

Let $H_n = \sum_{k=1}^{n} \frac{1}{k}$ be the harmonic numbers. Then the limit $\lim_{n \to \infty} (H_n - \ln n)$ exists, and it lies in $[0, 1]$. In particular, $H_n \sim \ln n$ as $n \to \infty$.

Remarks

Let $a_n = H_n - \ln n$. Since $\ln(n + 1) - \ln n = \int_n^{n+1} \frac{dt}{t}$ lies between $\frac{1}{n+1}$ and $\frac{1}{n}$, the sequence $a_n$ decreases. Also $a_n \ge H_n - \ln(n + 1) \ge 0$. The monotone convergence theorem gives the limit. It is the Euler–Mascheroni constant $\gamma$. The symbol $\sim$ is asymptotic equivalence. Mathlib states the limit as Real.tendsto_harmonic_sub_log.

Explanations

L1 human

The sum $1 + 1/2 + \cdots + 1/n$ is close to the area under $1/x$ from $1$ to $n$, which is $\ln n$. The error tends to a constant.