k_n_properties

lemma k_n_properties (ε : ℝ) (hε : 0 < ε) :    Filter.IsBoundedUnder (· ≤ ·) Filter.atTop (fun (n : ℕ) => (n : ℝ) / Nat.floor (ε * n)) ∧    ∀ᶠ n in Filter.atTop, 0 < Nat.floor (ε * n) := by  constructor <;> norm_num [ Filter.IsBoundedUnder, Filter.IsBounded ];  · use 2 / ε;    exact ⟨ ⌈ε⁻¹ * 2⌉₊ + 1, fun n hn => by rw [ div_le_div_iff₀ ] <;> nlinarith [ Nat.le_ceil ( ε⁻¹ * 2 ), Nat.lt_of_ceil_lt hn, Nat.floor_le ( show 0 ≤ ε * ↑n by positivity ), Nat.lt_floor_add_one ( ε * ↑n ), mul_inv_cancel₀ ( ne_of_gt hε ), mul_div_cancel₀ ( 2 : ℝ ) hε.ne' ] ⟩;  · exact ⟨ 1 / ε + 1, fun x hx => Nat.floor_pos.2 <| by nlinarith [ mul_div_cancel₀ 1 hε.ne' ] ⟩