Actual weighted AP distribution for a balanced common profile

All constants precede the ambient integer, source, coefficient, real prime profile, modulus cutoff and reduced residue selection. The lower bound r(m) ≥ x^eta is not needed: the stronger domain r(m) ≥ 2 suffices.

theorem Wu2004MeanValue.balanced_common_profile_unit_natural (A eta : ℝ) (hA : 0 < A) (heta : 0 < eta) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (a : ℕ → ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ m ∈ S, ↑N ^ eta ≤ ↑m ∧ ↑m ≤ ↑N ^ (1 - eta)) → (∀ m ∈ S, |f m| ≤ 1) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ ↑N) → (∀ d ∈ Finset.Icc 1 Q, (a d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (a d)| ≤ C * ↑N / Real.log ↑N ^ A

theorem Wu2004MeanValue.balanced_common_profile_weighted_natural (A eta F : ℝ) (hA : 0 < A) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (a : ℕ → ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ m ∈ S, ↑N ^ eta ≤ ↑m ∧ ↑m ≤ ↑N ^ (1 - eta)) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ ↑N) → (∀ d ∈ Finset.Icc 1 Q, (a d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (a d)| ≤ C * ↑N / Real.log ↑N ^ A