Documentation

MathlibNt.SieveTheory.Distribution.LiuPan.LiuPanPrincipalMoving

Uniform elementary quotient transport through PanQuotientBounds; no nonprincipal-character theorem is consumed.

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

Uniform PNT at the literal real quotient. The threshold precedes every a. The proof uses only the q=1 Standard BV extraction above, never nonprincipal SW.

Inspect dependencies

AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount_li_moving_prefix · compiled type and proof/definition references.