Frozen ordinary BV in the exact Wu modulus norm

The ordinary producer is the frozen, unconditional Richert (4.18) theorem. Its integral starts at 2 without an additive constant. Only its already proved Richert weight payment is specialized here; no BV analytic input is reproved.

theorem Wu2004MeanValue.wu_weighted_sum_eq_squarefree (S : Finset ℕ) (E : ℕ → ℝ) : ∑ d ∈ S, wuModulusWeight d * E d = MathlibNt.SieveTheory.Richert1969.threeOmegaErrorMass (Finset.filter Squarefree S) E

theorem Wu2004MeanValue.small_weighted_prime_prefix_log_saving (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ Q ≤ MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B, ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d ≤ C * ↑N / Real.log ↑N ^ A

Constants precede the endpoint and the modulus cutoff. The maximum is inside the weighted modulus sum and includes every reduced residue and every integer prime endpoint from 2 to N.