exists_k_n_of_mem_𝔓pos

lemma exists_k_n_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) : ∃ k n, p ∈ ℭ k n ∧ k ≤ n := by  obtain ⟨k, mp⟩ := exists_k_of_mem_𝔓pos h; use k  have dens'_pos : 0 < dens' k {p} := dens'_pos_of_mem_𝔓pos h mp  have dens'_le : dens' k {p} ≤ 2 ^ (-k : ℤ) := dens'_le_of_mem_𝔓pos h  have dens'_lt_top : dens' k {p} < ⊤ :=    dens'_le.trans_lt (ENNReal.zpow_lt_top (by simp) (by simp) _)  have dens'_toReal_pos : 0 < (dens' k {p}).toReal :=    ENNReal.toReal_pos dens'_pos.ne' dens'_lt_top.ne  -- 2 ^ (4 * a - n) < dens' k {p} ≤ 2 ^ (4 * a - n + 1)  -- 4 * a - n < log_2 dens' k {p} ≤ 4 * a - n + 1  -- -n < log_2 dens' k {p} - 4 * a ≤ -n + 1  -- n - 1 ≤ 4 * a - log_2 dens' k {p} < n  -- n ≤ 4 * a - log_2 dens' k {p} + 1 < n + 1  -- n = 4 * a + ⌊-log_2 dens' k {p}⌋ + 1  let v : ℝ := -Real.logb 2 (dens' k {p}).toReal  have klv : k ≤ v := by    rw [le_neg, Real.logb_le_iff_le_rpow one_lt_two dens'_toReal_pos,      show (2 : ℝ) = (2 : ℝ≥0∞).toReal by rfl, ENNReal.toReal_rpow,      ENNReal.toReal_le_toReal dens'_lt_top.ne (by simp)]    exact_mod_cast dens'_le  have klq : k ≤ ⌊v⌋₊ := Nat.le_floor klv  let n : ℕ := 4 * a + ⌊v⌋₊ + 1; use n; refine ⟨⟨mp, ?_⟩, by lia⟩  rw [show 4 * (a : ℤ) - (4 * a + ⌊v⌋₊ + 1 : ℕ) = (-⌊v⌋₊ - 1 : ℤ) by lia, sub_add_cancel, mem_Ioc,    ← ENNReal.ofReal_toReal dens'_lt_top.ne, ← ENNReal.rpow_intCast, ← ENNReal.rpow_intCast,    show (2 : ℝ≥0∞) = ENNReal.ofReal (2 : ℝ) by norm_cast,    ENNReal.ofReal_rpow_of_pos zero_lt_two, ENNReal.ofReal_rpow_of_pos zero_lt_two,    ENNReal.ofReal_lt_ofReal_iff dens'_toReal_pos, ENNReal.ofReal_le_ofReal_iff (by positivity),    ← Real.logb_le_iff_le_rpow one_lt_two dens'_toReal_pos,    ← Real.lt_logb_iff_rpow_lt one_lt_two dens'_toReal_pos,    Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub_left, neg_lt, le_neg]  constructor  · rw [add_comm]; exact_mod_cast Nat.lt_succ_floor _  · exact Nat.floor_le ((Nat.cast_nonneg' k).trans klv)