Uniform prime-counting error at coefficient-dependent real endpoints

This is the untwisted principal core, not the nonprincipal character estimate in Wu (2004), Lemma 2.3. It consumes the frozen, proved Standard BV theorem through its modulus-one term. All constants precede the moving endpoints. Wu's integral normalization is used exactly, on the domain [2, infinity).

noncomputable def Wu2004MeanValue.realPrimeCount (t : ℝ) : ℝ

Equations

• Wu2004MeanValue.realPrimeCount t = AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊t⌋₊

noncomputable def Wu2004MeanValue.principalError (t : ℝ) : ℝ

Equations

• Wu2004MeanValue.principalError t = Wu2004MeanValue.realPrimeCount t - Wu2004MeanValue.wuLi t

theorem Wu2004MeanValue.realPrimeCount_eq_scaled (t : ℝ) : realPrimeCount t = ↑(scaledPrimeCount t 1 0 1)

theorem Wu2004MeanValue.principalError_le_prefix (N : ℕ) (t : ℝ) (ht : 2 ≤ t) (htN : t ≤ ↑N) : |principalError t| ≤ MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N 1 + 3 / Real.log 2

theorem Wu2004MeanValue.principal_real_prefix_bound (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (t : ℝ), 2 ≤ t → t ≤ ↑N → |principalError t| ≤ C * ↑N / Real.log ↑N ^ A

A genuine maximal estimate over every real prime endpoint in [2,N].

theorem Wu2004MeanValue.principal_moving_term_bound (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ (x : ℝ), x₀ ≤ x → ∀ (m : ℕ), 1 ≤ m → ↑m ≤ √x → ∀ (r : ℝ), 2 ≤ r → r ≤ x / ↑m → |principalError r| ≤ C * x / Real.log x ^ A / ↑m

Coefficient-dependent endpoints, with the essential harmonic 1/m gain.

theorem Wu2004MeanValue.principal_moving_sum_bound (A F : ℝ) (hA : 0 < A) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ (x : ℝ), x₀ ≤ x → ∀ (S : Finset ℕ) (f r : ℕ → ℝ), (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ r m ≤ x / ↑m) → |∑ m ∈ S, f m * principalError (r m)| ≤ C * x / Real.log x ^ A

The untwisted principal core for arbitrary bounded weights and moving endpoints. S may include the modulus-dependent coprimality restriction.

theorem Wu2004MeanValue.principal_moving_sum_bound_ratio (A F K : ℝ) (hA : 0 < A) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ (x : ℝ), x₀ ≤ x → ∀ (S : Finset ℕ) (f r : ℕ → ℝ), (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → |∑ m ∈ S, f m * principalError (r m)| ≤ C * x / Real.log x ^ A

The endpoint ratio constant is fixed before the weight and endpoint families, as required for the principal core of W3.