Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.PanWangDingLowMovingPrefix

Uniform transport to the natural quotient in Pan's low-conductor endpoint.

theorem AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_siegelWalfisz_nat_div (b s : ) (hb : 0 b) (hs : 0 < s) :
∃ (K : ), 0 < K ∃ (N₀ : ), NN₀, ∀ (a : ), 1 aa N ^ (2 / 3)∀ (q : ), 2 qq Real.log N ^ b∀ (χ : PrimitiveCharacter q), χ 1primePrefix (↑χ) (N / a) K * N / Real.log N ^ s / a

The constants and cutoff are chosen before every a, modulus and character. The endpoint is the literal natural quotient; the carrier is the real N^(2/3) range.