theorem AnalyticNumberTheory.LargeSieve.PanQuotientBounds.eventually_nat_div_quarter : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (a : ℕ), 1 ≤ a → ↑a ≤ ↑N ^ (2 / 3) → ↑N ^ (1 / 4) ≤ ↑(N / a)

theorem AnalyticNumberTheory.LargeSieve.PanQuotientBounds.eventually_quotient_parameters (b : ℝ) (M : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (a : ℕ), 1 ≤ a → ↑a ≤ ↑N ^ (2 / 3) → M ≤ N / a ∧ 0 < Real.log ↑N ∧ 0 < Real.log ↑(N / a) ∧ Real.log ↑N ≤ 4 * Real.log ↑(N / a) ∧ 4 ^ b ≤ Real.log ↑(N / a)