Small-coefficient Wu errors with fully independent real endpoints

For a logarithmically small coefficient carrier it suffices to use the same ordinary AP prefix maximum for each coefficient. We deliberately pay the whole cardinality, rather than rescaling BV separately at every coefficient. Extra logarithmic saving pays this loss. Endpoints, coefficients and supports can all be selected independently for each modulus.

theorem Wu2004MeanValue.small_ebar_le_prime_prefix (N d b m : ℕ) (r : ℝ) (hd : 0 < d) (hm : 0 < m) (hmd : m.Coprime d) (hb : b.Coprime d) (hr : 2 ≤ r) (hrN : r ≤ ↑N) : |ebar (↑m * r) d b m| ≤ AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d + 1 / Real.log 2 / ↑d.totient

The inverse residue is retained. Richert's frozen normalization is already Wu's, so only rounding the prime endpoint costs 1/(log 2 * phi d).

theorem Wu2004MeanValue.small_ebar_sum_le_prefix (N d b : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (F : ℝ) (hd : 0 < d) (hb : b.Coprime d) (hF : 0 ≤ F) (hS : ∀ m ∈ S, 1 ≤ m) (hf : ∀ m ∈ S, |f m| ≤ F) (hr : ∀ m ∈ S, 2 ≤ r m ∧ r m ≤ ↑N) : |∑ m ∈ S with m.Coprime d, f m * ebar (↑m * r m) d b m| ≤ F * ↑S.card * (AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d + 1 / Real.log 2 / ↑d.totient)

noncomputable def Wu2004MeanValue.smallModulusSup (N : ℕ) (J F : ℝ) (d : ℕ) : ℝ

The genuine moduluswise supremum includes independent coefficient supports and weights, reduced residues and real prime endpoints.

Equations

• Wu2004MeanValue.smallModulusSup N J F d = sSup (insert 0 {v : ℝ | ∃ (S : Finset ℕ) (f : ℕ → ℝ) (r : ℕ → ℝ) (b : ℕ), (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ Real.log ↑N ^ J) ∧ (∀ m ∈ S, |f m| ≤ F) ∧ (∀ m ∈ S, 2 ≤ r m ∧ r m ≤ ↑N) ∧ b.Coprime d ∧ v = |∑ m ∈ S with m.Coprime d, f m * Wu2004MeanValue.ebar (↑m * r m) d b m|})

theorem Wu2004MeanValue.small_support_card_le (S : Finset ℕ) (M : ℝ) (hM : 0 ≤ M) (hS : ∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ M) : ↑S.card ≤ M

theorem Wu2004MeanValue.smallModulusSup_le_prefix (N d : ℕ) (J F : ℝ) (hN : 2 ≤ N) (hd : 0 < d) (hF : 0 ≤ F) : smallModulusSup N J F d ≤ F * Real.log ↑N ^ J * (AnalyticNumberTheory.LargeSieve.Bombieri1965Richert418.primeAPPrefixMaxError N d + 1 / Real.log 2 / ↑d.totient)

theorem Wu2004MeanValue.small_weighted_sup_log_saving (A J F : ℝ) (hA : 0 < A) (hJ : 0 ≤ J) (hF : 0 ≤ F) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ Q ≤ MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B, ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * smallModulusSup N J F d ≤ C * ↑N / Real.log ↑N ^ A

Full weighted small-coefficient W1/W3 source norm at a natural ambient endpoint. The real endpoints can vary independently with both d and m; indeed they are only required to lie in [2,N], a larger domain than N/m. All constants precede all choices, and the supremum stays inside the sum.