Modulus-selected balanced principal errors

The support may be selected separately for every modulus. In particular, the cofactor coprimality mask is applied before the inner absolute value.

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

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