Low conductors on every fixed balanced cofactor range.

theorem Wu2004MeanValue.balanced_lowMovingSource_le_budget (f : ℕ → ℂ) (t : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℕ) (S : Finset ℕ) (N U h Q : ℕ) (J s F : ℝ) (hN : 3 ≤ N) (hU : U ≤ N) (hS : S ⊆ Finset.Icc 1 U) (hh : 0 < h) (hJ : 0 ≤ J) (hF : 0 ≤ F) (hf : ∀ a ∈ S, ‖f a‖ ≤ F) (hp : ∀ a ∈ S, ∀ q ∈ Finset.Icc 2 Q, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ‖AnalyticNumberTheory.LargeSieve.PanLow.primePrefix (↑χ) (t q χ a)‖ ≤ J * ↑N / Real.log ↑N ^ s / ↑a) : lowMovingSource f t S h Q ≤ F * (↑Q * (J * ↑N / Real.log ↑N ^ s * (1 + Real.log ↑N) + ↑U * ↑h.primeFactors.card))

theorem Wu2004MeanValue.balanced_low_source_nat_moving (A b eta F : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (h U Q : ℕ) (S : Finset ℕ) (f : ℕ → ℂ) (t : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℕ), 1 ≤ h → h ≤ N → ↑U ≤ ↑N ^ (1 - eta) → S ⊆ Finset.Icc 1 U → ↑Q ≤ Real.log ↑N ^ b → (∀ a ∈ S, ‖f a‖ ≤ F) → (∀ q ∈ Finset.Icc 2 Q, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ a ∈ S, t q χ a ≤ N / a) → lowMovingSource f t S h Q ≤ C * ↑N / Real.log ↑N ^ A

theorem Wu2004MeanValue.balanced_low_source_real_moving (A b eta F : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (h Q : ℕ) (S : Finset ℕ) (f : ℕ → ℂ) (r : (q : ℕ) → AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q → ℕ → ℝ), 1 ≤ h → h ≤ N → (∀ a ∈ S, 1 ≤ a ∧ ↑a ≤ ↑N ^ (1 - eta)) → ↑Q ≤ Real.log ↑N ^ b → (∀ a ∈ S, ‖f a‖ ≤ F) → (∀ q ∈ Finset.Icc 2 Q, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q), ∀ a ∈ S, 0 ≤ r q χ a ∧ ↑a * r q χ a ≤ ↑N) → lowRealMovingSource f r S h Q ≤ C * ↑N / Real.log ↑N ^ A