theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_eventually_const_mul_rpow_le (C p q : ℝ) (hpq : p < q) : ∀ᶠ (N : ℝ) in Filter.atTop, C * N ^ p ≤ N ^ q

A fixed coefficient is absorbed by a strictly positive exponent gap.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_eventually_power_endpoints (K ε α : ℝ) (hK : 1 ≤ K) (hε : 0 < ε) (hεα : ε < α) : ∀ᶠ (N : ℝ) in Filter.atTop, (4 * N) ^ ε ≤ N ^ α / 2 ∧ N ^ (1 / 10) ≤ (N / K) ^ (1 / 10 + ε / 10)

The lower and upper power endpoints are admitted at one global threshold.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9Scale_eventually_local_global (K ε α : ℝ) (hK : 1 ≤ K) (hε : 0 < ε) (hεα : ε < α) (_hα : α ≤ 1 / 10) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ (x T : ℝ), N / K ≤ x → x ≤ 4 * N → N ^ α / 2 ≤ T → T ≤ N ^ (1 / 10) → have ν := Real.log T / Real.log x; 1 < x ∧ 1 ≤ T ∧ T = x ^ ν ∧ ε ≤ ν ∧ ν ≤ 1 / 10 + ε / 10 ∧ N ≤ K * x

Uniform local/global scale bridge. The cutoff precedes both moving parameters. No conclusion about well-factorability or a curved summation region is asserted.