theorem HarmonicSumAsymptotics.abs_harmonic_sub_log_sub_euler (n : ℕ) (hn : 1 ≤ n) : |↑(harmonic n) - Real.log ↑n - Real.eulerMascheroniConstant| ≤ 1 / ↑n

theorem HarmonicSumAsymptotics.log_sub_log_floor_le (x : ℝ) (hx : 1 ≤ x) : Real.log x - Real.log ↑⌊x⌋₊ ≤ 1 / ↑⌊x⌋₊

theorem HarmonicSumAsymptotics.harmonic_floor_eq_log_add_euler_mascheroni_add_bigO : (fun (x : ℝ) => ↑(harmonic ⌊x⌋₊) - Real.log x - Real.eulerMascheroniConstant) =O[Filter.atTop] fun (x : ℝ) => x⁻¹

theorem HarmonicSumAsymptotics.euler_mascheroni_eq_lim_harmonic_sub_log : Filter.Tendsto (fun (n : ℕ) => ↑(harmonic n) - Real.log ↑n) Filter.atTop (nhds Real.eulerMascheroniConstant)