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₀ : ℕ), ∀ N ≥ N₀, ∀ (a : ℕ), 1 ≤ a → ↑a ≤ ↑N ^ (2 / 3) → ∀ (q : ℕ), 2 ≤ q → ↑q ≤ Real.log ↑N ^ b → ∀ (χ : PrimitiveCharacter q), ↑χ ≠ 1 → ‖primePrefix (↑χ) (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.

Inspect dependencies

AnalyticNumberTheory.LargeSieve.PanLow.primePrefix_siegelWalfisz_nat_div · compiled type and proof/definition references.