Preserve the frozen SW prefix maximum when transporting to N / a. No new Siegel--Walfisz input is assumed.

theorem Wu2004MeanValue.low_primePrefix_max (b s : ℝ) : ∃ (J : ℝ), 0 < J ∧ ∃ (M : ℕ), ∀ N ≥ M, ∀ (q : ℕ), 2 ≤ q → ↑q ≤ Real.log ↑N ^ b → ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ y ≤ N, ‖AnalyticNumberTheory.LargeSieve.PanLow.primePrefix (↑χ) y‖ ≤ J * ↑N / Real.log ↑N ^ s

Real logarithmic exponents, with every prefix below the common scale. The constants precede the modulus, character, and independently chosen prefix.

theorem Wu2004MeanValue.low_primePrefix_nat_div_max (b s : ℝ) (hb : 0 ≤ b) (hs : 0 < s) : ∃ (J : ℝ), 0 < J ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (a : ℕ), 1 ≤ a → ↑a ≤ ↑N ^ (2 / 3) → ∀ (q : ℕ), 2 ≤ q → ↑q ≤ Real.log ↑N ^ b → ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ y ≤ N / a, ‖AnalyticNumberTheory.LargeSieve.PanLow.primePrefix (↑χ) y‖ ≤ J * ↑N / Real.log ↑N ^ s / ↑a

The genuine maximal quotient estimate: y need not equal N / a. It can subsequently be chosen separately for every modulus, character and a.