BrunTitchmarsh.IsBigO.nat_Top_of_atTop

theorem IsBigO.nat_Top_of_atTop (f g : ℕ → ℝ) (h : f =O[Filter.atTop] g)    (h0 : ∀ n, g n = 0 → f n = 0) : f =O[⊤] g := by  simp only [Asymptotics.isBigO_top, Real.norm_eq_abs]  rw [Asymptotics.isBigO_atTop_iff_eventually_exists] at h  simp only [ge_iff_le, Real.norm_eq_abs, Filter.eventually_atTop] at h  obtain ⟨N, hN⟩ := h  specialize hN N le_rfl  obtain ⟨c, hc⟩ := hN  let C := Finset.max' (insert c ((Finset.range N).image (fun n ↦ |f n| * |g n|⁻¹))) (by simp)  refine ⟨C, fun n ↦ ?_⟩  by_cases hn : N ≤ n  · calc |f n| ≤ c * |g n| := hc n hn      _ ≤ C * |g n| := by        gcongr        apply Finset.le_max'        simp  · by_cases hg : g n = 0    · simp [hg, h0]    rw [← mul_inv_le_iff₀]    · apply Finset.le_max'      simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range]      exact .inr ⟨n, by omega, rfl⟩    · simp [hg]