Aux.sum_inv_le_log

theorem sum_inv_le_log (n : ℕ) (hn : 1 ≤ n) :    ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ ≤ 1 + Real.log ↑n :=  by  rw [← Finset.sum_erase_add (Icc 1 n) _ (by simp [hn] : 1 ∈ Icc 1 n), add_comm]  gcongr  · norm_num  simp only [Icc_erase_left]  calc    ∑ d ∈ Ico 2 (n + 1), (d : ℝ)⁻¹ = ∑ d ∈ Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_    _ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹  := ?_    _ = Real.log ↑n := ?_  · congr; norm_num;  · apply @AntitoneOn.sum_le_integral_Ico 2 (n + 1) fun x : ℝ => (x - 1)⁻¹    · linarith [hn]    apply inv_sub_antitoneOn_Icc; norm_num  rw [intervalIntegral.integral_comp_sub_right _ 1, integral_inv]  · norm_num  norm_num; simp[hn, show (0:ℝ) < 1 by norm_num]