Actual AP errors at a common real moving profile

The finite character and cofactor algebra of Pan--Wang--Ding (1975), p. 601, (2.4), is applied to the actual Wu count, not to a surrogate main term. The profile and coefficients are common across moduli; the reduced residue may be chosen separately for each modulus, but not for each source coordinate.

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

Equations

• Wu2004MeanValue.actualAPSum S f r d b = ∑ m ∈ S, if m.Coprime d then f m * Wu2004MeanValue.ebar (↑m * r m) d b m else 0

noncomputable def Wu2004MeanValue.actualAmplitude (S : Finset ℕ) (f r : ℕ → ℝ) (d : ℕ) (χ : DirichletCharacter ℂ d) : ℂ

Equations

• Wu2004MeanValue.actualAmplitude S f r d χ = ∑ m ∈ S, if m.Coprime d then ↑(f m) * χ ↑m * AnalyticNumberTheory.LargeSieve.PanLow.coprimePrimePrefix χ ⌊r m⌋₊ d else 0

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

Equations

• Wu2004MeanValue.actualNonprincipalMass S f r d = ∑ χ ∈ Finset.univ.erase 1, ‖Wu2004MeanValue.actualAmplitude S f r d χ‖

theorem Wu2004MeanValue.actualCount_eq_characterMean (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hS : ∀ m ∈ S, 0 < m) (hd : 0 < d) (hb : IsUnit ↑b) : (∑ m ∈ S, if m.Coprime d then ↑(f m) * ↑(scaledPrimeCount (↑m * r m) d b m) else 0) = (↑d.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ d, star (χ ↑b) * actualAmplitude S f r d χ

theorem Wu2004MeanValue.actualAPSum_eq_characterExpansion (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hS : ∀ m ∈ S, 0 < m) (hd : 0 < d) (hb : IsUnit ↑b) : ↑(actualAPSum S f r d b) = (∑ χ ∈ Finset.univ.erase 1, star (χ ↑b) * actualAmplitude S f r d χ + ↑(coprimePrincipalSum ({m ∈ S | m.Coprime d}) f r d)) / ↑d.totient

theorem Wu2004MeanValue.abs_actualAPSum_le_characterMass (S : Finset ℕ) (f r : ℕ → ℝ) (d b : ℕ) (hS : ∀ m ∈ S, 0 < m) (hd : 0 < d) (hb : IsUnit ↑b) : |actualAPSum S f r d b| ≤ (actualNonprincipalMass S f r d + |coprimePrincipalSum ({m ∈ S | m.Coprime d}) f r d|) / ↑d.totient

noncomputable def Wu2004MeanValue.cofactorAmplitude (S : Finset ℕ) (f r : ℕ → ℝ) (h : ℕ) {q : ℕ} (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : ℂ

Equations

• Wu2004MeanValue.cofactorAmplitude S f r h χ = ∑ m ∈ S, (if m.Coprime h then ↑(f m) else 0) * ↑χ ↑m * ∑ p ∈ Finset.Icc 1 ⌊r m⌋₊, (if Nat.Prime p ∧ p.Coprime h then 1 else 0) * ↑χ ↑p

theorem Wu2004MeanValue.actualAmplitude_eq_primitive_cofactor (S : Finset ℕ) (f r : ℕ → ℝ) (d : ℕ) (hd : 0 < d) (χ : DirichletCharacter ℂ d) : actualAmplitude S f r d χ = cofactorAmplitude S f r (d / χ.conductor) (AnalyticNumberTheory.LargeSieve.conductorPrimitiveCharacter χ)

theorem Wu2004MeanValue.actualNonprincipalMass_eq_primitive_cofactor (S : Finset ℕ) (f r : ℕ → ℝ) (d : ℕ) (hd : 0 < d) : actualNonprincipalMass S f r d = ∑ q ∈ d.divisors, ∑ χ ∈ AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters q, ‖cofactorAmplitude S f r (d / q) χ‖

noncomputable def Wu2004MeanValue.cofactorLedger (S : Finset ℕ) (f r : ℕ → ℝ) (h Q : ℕ) : ℝ

Equations

• Wu2004MeanValue.cofactorLedger S f r h Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalPrimitiveCharacters q, ‖Wu2004MeanValue.cofactorAmplitude S f r h χ‖

theorem Wu2004MeanValue.actualNonprincipal_sum_le_cofactor (S : Finset ℕ) (f r : ℕ → ℝ) (Q : ℕ) : ∑ d ∈ Finset.Icc 1 Q, (↑d.totient)⁻¹ * actualNonprincipalMass S f r d ≤ ∑ h ∈ Finset.Icc 1 Q, (↑h.totient)⁻¹ * cofactorLedger S f r h Q

theorem Wu2004MeanValue.sum_abs_actualAP_le_principal_add_cofactor (S : Finset ℕ) (f r : ℕ → ℝ) (Q : ℕ) (b : ℕ → ℕ) (hS : ∀ m ∈ S, 0 < m) (hb : ∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) : ∑ d ∈ Finset.Icc 1 Q, |actualAPSum S f r d (b d)| ≤ ∑ d ∈ Finset.Icc 1 Q, |coprimePrincipalSum ({m ∈ S | m.Coprime d}) f r d| / ↑d.totient + ∑ h ∈ Finset.Icc 1 Q, (↑h.totient)⁻¹ * cofactorLedger S f r h Q

theorem Wu2004MeanValue.cofactorAmplitude_interval (f r : ℕ → ℝ) (h L U : ℕ) {q : ℕ} (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : cofactorAmplitude (Finset.Ioc L U) f r h χ = realMovingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG (fun (m : ℕ) => ↑(f m)) h) (AnalyticNumberTheory.LargeSieve.panSourceD h) r L U χ

theorem Wu2004MeanValue.cofactorLedger_interval (f r : ℕ → ℝ) (h Q L U : ℕ) : cofactorLedger (Finset.Ioc L U) f r h Q = ∑ q ∈ Finset.Icc 2 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖realMovingAmplitude (AnalyticNumberTheory.LargeSieve.panSourceG (fun (m : ℕ) => ↑(f m)) h) (AnalyticNumberTheory.LargeSieve.panSourceD h) r L U χ‖