The low/high conductor split for a common balanced prime profile.

theorem Wu2004MeanValue.balanced_commonPrimitiveSource_log_saving_of_split (A b eta : ℝ) (hA : 0 < A) (hb : 0 ≤ b) (hAb : A + 6 ≤ b) (heta : 0 < eta) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (h Q L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), 1 ≤ h → h ≤ x → ↑U ≤ ↑x ^ (1 - eta) → ↑Q ≤ √↑x / Real.log ↑x ^ b → Real.log ↑x ^ (2 * b) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → (∀ m ∈ Finset.Ioc L U, 0 ≤ r m ∧ ↑m * r m ≤ ↑x) → commonPrimitiveSource f r h Q L U ≤ C * ↑x / Real.log ↑x ^ A

theorem Wu2004MeanValue.balanced_commonPrimitiveSource_log_saving_uniform_level (A eta : ℝ) (hA : 0 < A) (heta : 0 < eta) : ∃ (b : ℝ) (C : ℝ), 0 ≤ b ∧ 0 < C ∧ ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (B : ℝ), b ≤ B → ∀ (h Q L U : ℕ) (f : ℕ → ℂ) (r : ℕ → ℝ), 1 ≤ h → h ≤ x → ↑U ≤ ↑x ^ (1 - eta) → ↑Q ≤ √↑x / Real.log ↑x ^ B → Real.log ↑x ^ (2 * b) ≤ ↑L → (∀ (n : ℕ), ‖f n‖ ≤ 1) → (∀ m ∈ Finset.Ioc L U, 0 ≤ r m ∧ ↑m * r m ≤ ↑x) → commonPrimitiveSource f r h Q L U ≤ C * ↑x / Real.log ↑x ^ A