integral_div_log_asymptotic

lemma integral_div_log_asymptotic : ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1:ℝ)) ∧    ∀ᶠ (x : ℝ) in atTop, ∫ t in Set.Icc 2 x, 1 / (log t) = (1 + c x) * x / (log x) := by  obtain ⟨c, hc⟩ := inv_div_log_asy  use fun x => ((∫ (t : ℝ) in Set.Icc 2 x, 1 / log t ^ 2) - 2 / log 2) * log x / x  constructor  · simp_rw [mul_div_assoc, mul_comm]    apply isLittleO_mul_iff_isLittleO_div _|>.mpr    · simp_rw [one_div_div]      apply IsLittleO.sub      · apply IsBigO.trans_isLittleO (g := (fun x ↦ x / log x ^ 2))        · rw [isBigO_iff]          use c          filter_upwards [eventually_ge_atTop 2, hc] with x hx hc          simp only [norm_eq_abs]          rwa [abs_of_nonneg, abs_of_nonneg]          · bound          · apply setIntegral_nonneg measurableSet_Icc fun t ht ↦ (by bound)        apply isLittleO_of_tendsto        · simp        apply tendsto_log_atTop.inv_tendsto_atTop.congr'        filter_upwards [eventually_ne_atTop 0] with x hx        simp only [Pi.inv_apply]        field      apply isLittleO_mul_iff_isLittleO_div _|>.mp      · conv => arg 2; ext; rw [mul_comm]        apply IsLittleO.const_mul_left isLittleO_log_id_atTop      · filter_upwards [eventually_ge_atTop 2] with x hx        simp; grind    filter_upwards [eventually_ge_atTop 2] with x hx    simp    grind  · filter_upwards [eventually_ge_atTop 4] with x hx    rw [integral_log_inv_pialt x hx]    field [show log x ≠ 0 by simp; grind]