This file proves $\log(n+1) \le H_n \le 1 + \log(n)$ for all natural numbers $n$.

theorem log_add_one_le_harmonic (n : ℕ) : (↑(n + 1)).log ≤ ↑(harmonic n)

theorem harmonic_le_one_add_log (n : ℕ) : ↑(harmonic n) ≤ 1 + (↑n).log

theorem log_le_harmonic_floor (y : ℝ) (hy : 0 ≤ y) : y.log ≤ ↑(harmonic ⌊y⌋₊)

theorem harmonic_floor_le_one_add_log (y : ℝ) (hy : 1 ≤ y) : ↑(harmonic ⌊y⌋₊) ≤ 1 + y.log