Actual prime-count centering in Wu (2004), equation (5.7)

Both discrepancies use the same actual AP count. The main term here is the actual number of primes, not li. Their difference is the principal error summed over the modulus-dependent coprime source set, before taking absolute values. The balanced PNT estimate pays this filtered difference uniformly.

noncomputable def Wu2004MeanValue.primeCenteredAPSum (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) : ℝ

Equations

• Wu2004MeanValue.primeCenteredAPSum S f r d b = ∑ m ∈ S, if m.Coprime d then f m * (↑(Wu2004MeanValue.scaledPrimeCount (↑m * r m) d b m) - Wu2004MeanValue.realPrimeCount (r m) / ↑d.totient) else 0

theorem Wu2004MeanValue.primeCenteredAPSum_eq_inverse (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hS : ∀ m ∈ S, 0 < m) (hr : ∀ m ∈ S, 0 ≤ r m) : primeCenteredAPSum S f r d b = ∑ m ∈ S, if m.Coprime d then f m * (↑(AnalyticNumberTheory.Sieve.primesInAP ⌊r m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - realPrimeCount (r m) / ↑d.totient) else 0

theorem Wu2004MeanValue.primeCenteredAPSum_eq_actual_sub_principal (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hS : ∀ m ∈ S, 0 < m) : primeCenteredAPSum S f r d b = actualAPSum S f r d b - (∑ m ∈ S with m.Coprime d, f m * principalError (r m)) / ↑d.totient

theorem Wu2004MeanValue.primeCenteredAPSum_sub_actual_weighted (A eta F : ℝ) (hA : 0 < A) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (Q : ℕ) (S : ℕ → Finset ℕ) (f r : ℕ → ℕ → ℝ) (b : ℕ → ℕ), ↑Q ≤ x → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, 1 ≤ m ∧ ↑m ≤ x ^ (1 - eta)) → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, |f d m| ≤ F) → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, 2 ≤ r d m ∧ ↑m * r d m ≤ x) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |primeCenteredAPSum (S d) (f d) (r d) d (b d) - actualAPSum (S d) (f d) (r d) d (b d)| ≤ C * x / Real.log x ^ A

The two families may even be selected independently for each modulus. The coprimality mask is kept inside the prime-error sum.

theorem Wu2004MeanValue.weighted_primeCenteredAPSum_le_actual_add (A eta F : ℝ) (hA : 0 < A) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (Q : ℕ) (S : ℕ → Finset ℕ) (f r : ℕ → ℕ → ℝ) (b : ℕ → ℕ), ↑Q ≤ x → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, 1 ≤ m ∧ ↑m ≤ x ^ (1 - eta)) → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, |f d m| ≤ F) → (∀ d ∈ Finset.Icc 1 Q, ∀ m ∈ S d, 2 ≤ r d m ∧ ↑m * r d m ≤ x) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |primeCenteredAPSum (S d) (f d) (r d) d (b d)| ≤ ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum (S d) (f d) (r d) d (b d)| + C * x / Real.log x ^ A

An unconditional transport with the actual li-centered discrepancy still visible on the right. An AP producer, not this transport alone, is required to deduce distribution.