theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_aux_scale_rpow_le {Cscale x ε : ℝ} (hC : 1 ≤ Cscale) (hx : Cscale ≤ x) (hε : 0 < ε) : (Cscale * x) ^ (ε / 2) ≤ x ^ ε

Only the auxiliary SW scale is enlarged; the physical scale is unchanged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kClean_eventually_tau_le (k : ℕ) {Cscale δ : ℝ} (hC : 1 ≤ Cscale) (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (n : ℕ), 0 < n → ↑n ≤ Cscale * x → ↑((fouvryTau k) n) ≤ x ^ δ

Fixed multiplicative ranges cost only a uniform threshold.