theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_small_prefix (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ d ∈ Finset.Icc 1 (SieveTheory.LiuWeight.panModulusCutoff N C), ∀ x ∈ Finset.Icc 2 N, ∀ b ∈ AnalyticNumberTheory.Sieve.unitResidues d, |AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError x d b| ≤ K * ↑N / Real.log ↑N ^ A

An individual genuine AP error is bounded by its term in unconditional BV.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWSum_Ioc (P : ℕ → Prop) [DecidablePred P] {u v : ℕ} (huv : u ≤ v) : primeSWSum (Finset.Ioc u v) P = primeSWSum (Finset.range (v + 1)) P - primeSWSum (Finset.range (u + 1)) P

Literal interval subtraction for an arbitrary fixed predicate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval_AP_eq_sub {u v : ℝ} (huv : u ≤ v) (d b : ℕ) : (primeSWSum (primeSWInterval u v) fun (n : ℕ) => n ≡ b [MOD d]) = ↑(SieveTheory.BombieriVinogradov.primesInAP ⌊v⌋₊ d b) - ↑(SieveTheory.BombieriVinogradov.primesInAP ⌊u⌋₊ d b)

No rounding correction is lost: the support is exactly the natural Ioc.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_primesInAP_mod (x d b : ℕ) : SieveTheory.BombieriVinogradov.primesInAP x d (b % d) = SieveTheory.BombieriVinogradov.primesInAP x d b

Canonicalization does not change the actual prime count.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_error_le_prefix {N x d b : ℕ} (hx : x ∈ Finset.Icc 2 N) (hd : 0 < d) (hb : b.Coprime d) : |AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPError x d b| ≤ AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d

Prefix maximal bounds apply to every integer representative of a reduced class.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_interval_li_bound {N : ℕ} {u v : ℝ} (huv : u ≤ v) (hu : ⌊u⌋₊ ∈ Finset.Icc 2 N) (hv : ⌊v⌋₊ ∈ Finset.Icc 2 N) {d b : ℕ} (hd : 0 < d) (hb : b.Coprime d) : |(primeSWSum (primeSWInterval u v) fun (n : ℕ) => n ≡ b [MOD d]) - (AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.logarithmicIntegral ↑⌊v⌋₊ - AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.logarithmicIntegral ↑⌊u⌋₊) / ↑d.totient| ≤ 2 * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d

The same unconditional BV constant controls every moving interval endpoint.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_tau_two_le (d : ℕ) : (fouvryTau 2) d ≤ d

There are at most d divisors of a positive modulus.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_interval_discrepancy_bound {N : ℕ} {u v : ℝ} (huv : u ≤ v) (hu : ⌊u⌋₊ ∈ Finset.Icc 2 N) (hv : ⌊v⌋₊ ∈ Finset.Icc 2 N) {d h b : ℕ} (hd : 0 < d) (hh : 0 < h) (hb : b.Coprime d) : |betaCoprimeAPDiscrepancy (primeSWInterval u v) primeSWBeta d h b| ≤ 2 * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d + 2 * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N 1 + ↑d + 2 * ↑((fouvryTau 2) h)

The normalization by the actual coprime mass differs from li by ordinary prime-counting error and explicitly retained prime-divisor losses.