smaller_terms

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