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₀ : ), NN₀, ∀ (a : ), 1 aa 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.