theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_log_rpow_eventually (a : ℝ) {s : ℝ} (hs : 0 < s) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ a ≤ ↑N ^ s

Fixed logarithmic powers are eventually dominated uniformly in the scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_log_cutoff_eventually (K : ℕ) (C : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (d : ℕ), ↑d ≤ Real.log ↑N ^ K → d ≤ SieveTheory.LiuWeight.panModulusCutoff N C

Every fixed logarithmic modulus range lies inside the genuine BV cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_large_log_bound (B : ℕ) {N d : ℕ} (hN : 3 ≤ N) (hl : 1 ≤ Real.log ↑N) (hpow : Real.log ↑N ^ (B + 1) ≤ ↑N) (hd : 0 < d) (hlarge : Real.log ↑N ^ (B + 1) ≤ ↑d) (S : Finset ℕ) (hS : S ⊆ Finset.range (N + 1)) (h b : ℕ) : |betaCoprimeAPDiscrepancy S primeSWBeta d h b| ≤ (2 + 2 * SieveTheory.Richert1969.richertReciprocalTotientConstant) * ↑N / Real.log ↑N ^ B

The large-modulus envelope is uniformly logarithmically small, including d>N.