Actual prime counting, extracted only from the q=1 term of Standard BV. The fixed normalization is κ₀=2/log 2. Real endpoint changes are paid by an integrable short interval, not by replacing the logarithmic integral argument.

def AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount (t : ℕ) : ℝ

Equations

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

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount_sub_li_eq_standard (t : ℕ) : primeCount t - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑t = MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError t 1 0

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.eventually_log_rpow_le_rpow (b d : ℝ) (hd : 0 < d) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ b ≤ ↑N ^ d

A positive real power dominates any prescribed logarithmic power.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.eventually_one_le_panModulusCutoff (b : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N b

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount_li_pnt (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (M : ℕ), ∀ t ≥ M, |primeCount t - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) ↑t| ≤ C * ↑t / Real.log ↑t ^ s

No PNT hypothesis: the literal Standard BV q=1/residue=0 finite specialization.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.abs_li_sub_le_short (κ : ℝ) {x y : ℝ} (hx : 2 ≤ x) (hxy : x ≤ y) (hy : y ≤ x + 1) : |MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ y - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ x| ≤ 1 / Real.log 2

Actual short-interval bound for Liu's Li, uniformly in its additive normalization.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.abs_li_real_div_sub_nat_div (κ : ℝ) {N a : ℕ} (ha : 0 < a) (ht : 2 ≤ N / a) : |MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (↑N / ↑a) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ ↑(N / a)| ≤ 1 / Real.log 2

Natural floor to real quotient: the missing interval has length strictly less than one.

theorem AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount_li_real_div_pnt (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (M : ℕ), ∀ (N a : ℕ), 0 < a → M ≤ N / a → |primeCount (N / a) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑a)| ≤ C * ↑(N / a) / Real.log ↑(N / a) ^ s

PNT with the real quotient Li argument, still scaled at the natural quotient.