second_smaller_terms

lemma second_smaller_terms (f : ℝ → ℝ) (hf : Tendsto f atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) :    ∀ᶠ x : ℝ in atTop,      (1 + δ) * (x / Real.log x) > (1 + f x) * (x / Real.log x) := by  have first_term := bound_f_second_term f hf δ hδ   simp only [_root_.add_lt_add_iff_left, eventually_atTop] at first_term  obtain ⟨p, hp⟩ := first_term  simp only [gt_iff_lt, eventually_atTop]  let a := max p 2  have ha: ∀ (b : ℝ), a ≤ b → 1 + δ > 1 + f ( b) := by    intro b hb    have a_ge_p: p <= a := by simp [a]    specialize hp b (by linarith)    linarith  use a  intro b hb  specialize ha b hb  have rhs_nonzero:  b / log ( b) > 0 := by    simp only [sup_le_iff, a] at hb    obtain ⟨_, hb2⟩ := hb    have log_pos: Real.log (b) > 0 := by      refine (Real.log_pos_iff ?_).mpr ?_      · positivity      · linarith    positivity  rw [mul_lt_mul_iff_left₀]  · exact ha  · linarith