theorem Wu2004MeanValue.actualAPError_eq_abs_actualAPSum (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) : actualAPError S f r d b = |actualAPSum S f r d b|

theorem Wu2004MeanValue.actualAPSum_weighted_log_saving_of_unweighted (A F K U : ℝ) (hF : 0 ≤ F) (hK : 0 ≤ K) (hU : 0 ≤ U) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), Real.exp 1 ≤ x → ↑Q ≤ √x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → ∑ d ∈ Finset.Icc 1 Q, |actualAPSum S f r d (b d)| ≤ U * x / Real.log x ^ (2 * A + 11) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (b d)| ≤ C * x / Real.log x ^ A

The weight transfer consumes exactly the parent's actual unweighted AP source sum, with its common coefficient/profile and selected residue.

theorem Wu2004MeanValue.actualAPSum_weighted_sq_le_log_eleven : ∃ (C₉ : ℝ), 0 < C₉ ∧ ∀ (x F K : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), Real.exp 1 ≤ x → 0 ≤ F → 0 ≤ K → ↑Q ≤ √x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → (∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (b d)|) ^ 2 ≤ 4 * C₉ * apEnvelopeConstant F K * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant * x * Real.log x ^ 11 * ∑ d ∈ Finset.Icc 1 Q, |actualAPSum S f r d (b d)|

Finite interpolation with the full logarithmic loss displayed. The carrier S may be just the large-source mask; no small-source mass occurs.

theorem Wu2004MeanValue.actualAPSum_weighted_log_saving_of_unweighted_exponent (A T F K U : ℝ) (hT : 2 * A + 11 ≤ T) (hF : 0 ≤ F) (hK : 0 ≤ K) (hU : 0 ≤ U) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), Real.exp 1 ≤ x → ↑Q ≤ √x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → ∑ d ∈ Finset.Icc 1 Q, |actualAPSum S f r d (b d)| ≤ U * x / Real.log x ^ T → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * |actualAPSum S f r d (b d)| ≤ C * x / Real.log x ^ A

A large-source unweighted saving T pays any weighted saving A with T ≥ 2*A+11. In particular the parent may choose T=2*A+12 before selecting its conductor split, source cutoff and final modulus level.