Commit 2024-03-01 13:29 57e3f1d7

feat: explicit logarithmic bounds on the harmonic numbers (#9984) Prove $\log(n+1) \le H_n \le 1 + \log(n)$ for all natural numbers $n$. There is an existing proof that $H_n$ is not an integer which uses p-adics. Since the new result uses some heavy machinery that is disjoint from the existing proof, the file is split into three parts to keep the dependencies lighter. See zulip