Weight payment for the actual Wu AP discrepancy

The elementary envelope below is for arbitrary bounded coefficients, not the special Liu semiprime coefficient. The source sum precedes its absolute value, and one residue is retained across all its coordinates.

noncomputable def Wu2004MeanValue.actualAPError (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) : ℝ

Equations

• Wu2004MeanValue.actualAPError S f r d b = |∑ m ∈ S with m.Coprime d, f m * Wu2004MeanValue.ebar (↑m * r m) d b m|

theorem Wu2004MeanValue.actualAPError_nonneg (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) : 0 ≤ actualAPError S f r d b

theorem Wu2004MeanValue.ap_source_reciprocal_bound (x : ℝ) (S : Finset ℕ) (hx : 2 ≤ x) (hS : ∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ x) : ∑ m ∈ S, 1 / ↑m ≤ 1 + Real.log x

theorem Wu2004MeanValue.wuLi_abs_le_linear {r : ℝ} (hr : 2 ≤ r) : |wuLi r| ≤ MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant 0 * r

theorem Wu2004MeanValue.totient_mul_abs_ebar_le (d b m : ℕ) (r : ℝ) (hd : 0 < d) (hm : 0 < m) (hmd : m.Coprime d) (hr : 2 ≤ r) : ↑d.totient * |ebar (↑m * r) d b m| ≤ (1 + MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant 0) * r + ↑d

noncomputable def Wu2004MeanValue.apEnvelopeConstant (F K : ℝ) : ℝ

Equations

• Wu2004MeanValue.apEnvelopeConstant F K = F * ((1 + MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant 0) * K + 1)

theorem Wu2004MeanValue.apEnvelopeConstant_nonneg {F K : ℝ} (hF : 0 ≤ F) (hK : 0 ≤ K) : 0 ≤ apEnvelopeConstant F K

theorem Wu2004MeanValue.totient_mul_actualAPError_le (x F K : ℝ) (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hx : 2 ≤ x) (hF : 0 ≤ F) (hK : 0 ≤ K) (hd : 0 < d) (hdx : ↑d ≤ √x) (hS : ∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) (hf : ∀ m ∈ S, |f m| ≤ F) (hr : ∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) : ↑d.totient * actualAPError S f r d b ≤ apEnvelopeConstant F K * x * (1 + Real.log x)

The actual complete AP sum has a reciprocal-totient envelope. No distribution theorem, restriction on the residue, or special coefficient identity is assumed. The +1 in a residue-class count is paid by d|S|≤x.

theorem Wu2004MeanValue.ap_totient_ratio_le_log (x : ℝ) (d : ℕ) (hx : 2 ≤ x) (hd : 0 < d) (hdx : ↑d ≤ x) : ↑d / ↑d.totient ≤ MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant * Real.log x

theorem Wu2004MeanValue.modulus_mul_actualAPError_le (x F K : ℝ) (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hx : 2 ≤ x) (hF : 0 ≤ F) (hK : 0 ≤ K) (hd : 0 < d) (hdx : ↑d ≤ √x) (hS : ∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) (hf : ∀ m ∈ S, |f m| ≤ F) (hr : ∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) : ↑d * actualAPError S f r d b ≤ apEnvelopeConstant F K * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant * x * (1 + Real.log x) ^ 2

A modulus, rather than totient, envelope makes the frozen reciprocal ninth divisor moment directly applicable.