Siegel--Walfisz at a balanced quotient, with the harmonic cofactor gain.

theorem Wu2004MeanValue.balanced_low_primePrefix_nat_div_max (b s eta : ℝ) (hb : 0 ≤ b) (hs : 0 < s) (heta : 0 < eta) : ∃ (J : ℝ), 0 < J ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (a : ℕ), 1 ≤ a → ↑a ≤ ↑N ^ (1 - eta) → ∀ (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