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

theorem harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

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