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 : ℕ) : Real.log ↑(n + 1) ≤ ↑(harmonic n)

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

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

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