The complete induced-principal contribution in Wu's weighted norm

The prime count removes primes dividing the modulus. The frozen elementary deletion bound and weighted reciprocal-totient estimate pay for this removal, uniformly even over modulus-dependent coefficient and endpoint choices. No nonprincipal-character estimate is asserted here.

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

Equations

• Wu2004MeanValue.coprimePrincipalSum S f r d = ∑ m ∈ S, f m * (AnalyticNumberTheory.LargeSieve.PanPrincipal.coprimePrimeCount ⌊r m⌋₊ d - Wu2004MeanValue.wuLi (r m))

theorem Wu2004MeanValue.coprimePrincipalSum_sub_core_le (S : Finset ℕ) (f r : ℕ → ℝ) (d : ℕ) (F : ℝ) (hd : 0 < d) (hF : 0 ≤ F) (hf : ∀ m ∈ S, |f m| ≤ F) : |coprimePrincipalSum S f r d - ∑ m ∈ S, f m * principalError (r m)| ≤ F * ↑S.card * ↑d.primeFactors.card

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

The principal character with all primes dividing d removed, before division by phi(d). Constants precede every finite support, weight and moving endpoint, and even all positive moduli d <= x.

def Wu2004MeanValue.wuModulusWeight (d : ℕ) : ℝ

Equations

• Wu2004MeanValue.wuModulusWeight d = ↑(ArithmeticFunction.moebius d) ^ 2 * 3 ^ d.primeFactors.card

theorem Wu2004MeanValue.wuModulusWeight_nonneg (d : ℕ) : 0 ≤ wuModulusWeight d

theorem Wu2004MeanValue.wu_reciprocal_totient_sum_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 2 ≤ x → ∀ (Q : ℕ), ↑Q ≤ x → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d / ↑d.totient ≤ C * Real.log x ^ 6

The exact source weight, not an unweighted replacement.

noncomputable def Wu2004MeanValue.principalModulusSup (x F K : ℝ) (d : ℕ) : ℝ

A genuine supremum, including zero for an empty admissible domain. Its domain is deliberately stronger than Wu needs: the support and weights may also be selected separately for each modulus.

Equations

• Wu2004MeanValue.principalModulusSup x F K d = sSup (insert 0 {v : ℝ | ∃ (S : Finset ℕ) (f : ℕ → ℝ) (r : ℕ → ℝ), (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) ∧ (∀ m ∈ S, |f m| ≤ F) ∧ (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) ∧ v = |Wu2004MeanValue.coprimePrincipalSum ({m ∈ S | m.Coprime d}) f r d| / ↑d.totient})

theorem Wu2004MeanValue.principal_weighted_sup_log_saving (A F K : ℝ) (hA : 0 < A) (hF : 0 ≤ F) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℝ), ∀ x ≥ x₀, ∀ (Q : ℕ), ↑Q ≤ x → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * principalModulusSup x F K d ≤ C * x / Real.log x ^ A

Full mu^2(d) 3^omega(d) modulus payment for the induced-principal contribution, with the supremum inside the modulus sum.