Principal errors for balanced cofactor profiles

The cofactor may extend to x^(1-eta). Applying the already proved real prime-prefix estimate at ceil(x/m) retains the harmonic 1/m gain. The logarithmic comparison now costs eta^(-A), not the square-root specialization's 2^A. No source-wise cancellation estimate is used here.

theorem Wu2004MeanValue.balanced_principal_moving_term_bound (A eta : ℝ) (hA : 0 < A) (heta : 0 < eta) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (m : ℕ), 1 ≤ m → ↑m ≤ x ^ (1 - eta) → ∀ (r : ℝ), 2 ≤ r → r ≤ x / ↑m → |principalError r| ≤ C * x / Real.log x ^ A / ↑m

theorem Wu2004MeanValue.balanced_principal_moving_sum_bound (A eta F : ℝ) (hA : 0 < A) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (S : Finset ℕ) (f r : ℕ → ℝ), (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ x ^ (1 - eta)) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ x) → |∑ m ∈ S, f m * principalError (r m)| ≤ C * x / Real.log x ^ A

theorem Wu2004MeanValue.balanced_coprimePrincipalSum_log_saving (A eta F : ℝ) (hA : 0 < A) (heta : 0 < eta) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (d : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ), 0 < d → ↑d ≤ x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ x ^ (1 - eta)) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ x) → |coprimePrincipalSum S f r d| ≤ C * x / Real.log x ^ A