Pan (2.4)'s actual principal remainder for Liu's weight, before division by φ(q). This does not assert any estimate for the nonprincipal-character contribution.

def AnalyticNumberTheory.LargeSieve.PanPrincipal.coprimePrimeCount (t q : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.PanPrincipal.coprimePrimeCount t q = ∑ p ∈ Finset.range (t + 1), if Nat.Prime p ∧ p.Coprime q then 1 else 0

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.abs_primeCount_sub_coprimePrimeCount_le (t q : ℕ) (hq : 0 < q) : |primeCount t - coprimePrimeCount t q| ≤ ↑q.primeFactors.card

The literal prime deletion is bounded by ω(q); q must be positive.

noncomputable def AnalyticNumberTheory.LargeSieve.PanPrincipal.principalError (N A₁ A₂ q : ℕ) : ℝ

Exact principal error Pκ₀, not divided by φ(q), with real Li argument N/a.

Equations

• AnalyticNumberTheory.LargeSieve.PanPrincipal.principalError N A₁ A₂ q = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) a * ((∑ p ∈ Finset.range (N / a + 1), if Nat.Prime p ∧ p.Coprime q then 1 else 0) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑a)) else 0

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.principalError_le_budget (N A₁ A₂ q : ℕ) (B : ℝ) (hq : 0 < q) (hA : A₂ ≤ N) (hB : 0 ≤ B) (hp : ∀ a ∈ Finset.Ioc A₁ A₂, |primeCount (N / a) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑a)| ≤ B / ↑a) : |principalError N A₁ A₂ q| ≤ B * (1 + Real.log ↑N) + ↑A₂ * ↑q.primeFactors.card

Elementary finite triangle and harmonic summation. The prime-Li estimates in this finite lemma are supplied unconditionally in the final theorem below.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.principalError_log_saving (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (q A₁ A₂ : ℕ), 1 ≤ q → ↑q ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → |principalError N A₁ A₂ q| ≤ C * ↑N / Real.log ↑N ^ s

Arbitrary logarithmic saving for Pan's actual principal Liu convolution error. C and N₀ precede q and both window endpoints. The unnormalized error uses the fixed true-Li normalization κ₀=2/log 2. No ordinary-BV convolution claim is used.