hardy_k_ratio_bounded

lemma hardy_k_ratio_bounded (ε : ℝ) (hε : 0 < ε) :    Filter.IsBoundedUnder (· ≤ ·) Filter.atTop (fun (n : ℕ) => (n : ℝ) / (hardy_k ε n : ℝ)) := by  -- We know `hardy_k ε n = max 1 (floor (ε * n))`. Eventually `floor (ε * n) >= 1`, so `hardy_k = floor`.  have h_eventually_floor : ∀ᶠ n in Filter.atTop, hardy_k ε n = Nat.floor (ε * n) := by    simp +zetaDelta at *;    exact ⟨ ⌈ε⁻¹⌉₊ + 1, fun n hn => max_eq_right <| Nat.floor_pos.mpr <| by nlinarith [ Nat.le_ceil ( ε⁻¹ ), show ( n : ℝ ) ≥ ⌈ε⁻¹⌉₊ + 1 by exact_mod_cast hn, mul_inv_cancel₀ hε.ne' ] ⟩;  -- We already proved `n / floor` is bounded in `k_n_properties`.  have h_bounded_floor : Filter.IsBoundedUnder (· ≤ ·) Filter.atTop (fun n : ℕ => (n : ℝ) / (Nat.floor (ε * n)) : ℕ → ℝ) := by    exact k_n_properties ε hε |>.1;  obtain ⟨ C, hC ⟩ := h_bounded_floor;  refine' ⟨ Max.max C 1, Filter.eventually_atTop.mpr _ ⟩;  obtain ⟨ N, hN ⟩ := Filter.eventually_atTop.mp hC; obtain ⟨ M, hM ⟩ := Filter.eventually_atTop.mp h_eventually_floor; use Max.max N M; intros n hn; aesop;