Actual unweighted AP distribution for the common balanced profile.

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