Balanced distribution centered at the actual prime count

This consumes the proved actual AP producer and the filtered principal transport. No distribution or PNT estimate is a caller-supplied premise. It supplies the prime-count normalization used in Wu (2004), (5.7).

theorem Wu2004MeanValue.balanced_common_profile_primeCentered_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 : ℕ → ℝ) (b : ℕ → ℕ), ↑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, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |primeCenteredAPSum S f r d (b d)| ≤ C * ↑N / Real.log ↑N ^ A