The finite signed dispersion reduction

The arithmetic sums below are the finite-support versions of Fouvry (1987), (3.4), and Fouvry (1984), (7.7)--(7.10). No absolute values are inserted inside the modulus sum. The integer residue and the two supports are arbitrary.

The square expansion and Cauchy--Schwarz reduction are proved here; no logarithmic saving, Siegel--Walfisz estimate or Kloosterman estimate is assumed.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionMass (N : Finset ℕ) (β : ℕ → ℝ) (a : ℤ) (q m : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionMass N β a q m = ∑ n ∈ N, if ↑m * ↑n ≡ a [ZMOD ↑q] then β n else 0

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass (N : Finset ℕ) (β : ℕ → ℝ) (q : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β q = ∑ n ∈ N, if n.Coprime q then β n else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy (M N : Finset ℕ) (α β : ℕ → ℝ) (a : ℤ) (q : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy M N α β a q = (∑ m ∈ M, ∑ n ∈ N, if ↑m * ↑n ≡ a [ZMOD ↑q] then α m * β n else 0) - (∑ m ∈ M, ∑ n ∈ N, if (m * n).Coprime q then α m * β n else 0) / ↑q.totient

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli (Q : Finset ℕ) (a : ℤ) : Finset ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a = {q ∈ Q | a.gcd ↑q = 1}

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (M N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError M N Q α β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, c q * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy M N α β a q

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionRow (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (m : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionRow N Q β c a m = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, if m.Coprime q then c q * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionMass N β a q m else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.principalRow (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (m : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.principalRow N Q β c a m = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, if m.Coprime q then c q * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β q / ↑q.totient else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprime_of_product_congruent {a : ℤ} {q m n : ℕ} (ha : a.gcd ↑q = 1) (h : ↑m * ↑n ≡ a [ZMOD ↑q]) : m.Coprime q ∧ n.Coprime q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionMass_eq_zero_of_not_coprime (N : Finset ℕ) (β : ℕ → ℝ) {a : ℤ} {q m : ℕ} (ha : a.gcd ↑q = 1) (hm : ¬m.Coprime q) : progressionMass N β a q m = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_coprime_product_factor (N : Finset ℕ) (α β : ℕ → ℝ) (m q : ℕ) : (∑ n ∈ N, if (m * n).Coprime q then α m * β n else 0) = if m.Coprime q then α m * coprimeMass N β q else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy_eq_rows (M N : Finset ℕ) (α β : ℕ → ℝ) {a : ℤ} {q : ℕ} (ha : a.gcd ↑q = 1) : bilinearDiscrepancy M N α β a q = ∑ m ∈ M, α m * if m.Coprime q then progressionMass N β a q m - coprimeMass N β q / ↑q.totient else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_eq_rows (M N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : signedError M N Q α β c a = ∑ m ∈ M, α m * (progressionRow N Q β c a m - principalRow N Q β c a m)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW S N Q w β c a = ∑ m ∈ S, w m * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionRow N Q β c a m ^ 2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionV S N Q w β c a = ∑ m ∈ S, w m * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.progressionRow N Q β c a m * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.principalRow N Q β c a m

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionU S N Q w β c a = ∑ m ∈ S, w m * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.principalRow N Q β c a m ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersion_identity (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : ∑ m ∈ S, w m * (progressionRow N Q β c a m - principalRow N Q β c a m) ^ 2 = dispersionW S N Q w β c a - 2 * dispersionV S N Q w β c a + dispersionU S N Q w β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersion_nonneg (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) (hw : ∀ m ∈ S, 0 ≤ w m) : 0 ≤ dispersionW S N Q w β c a - 2 * dispersionV S N Q w β c a + dispersionU S N Q w β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_dispersion (M N Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) : signedError M N Q α β c a ^ 2 ≤ (∑ m ∈ M, α m ^ 2) * (dispersionW M N Q (fun (x : ℕ) => 1) β c a - 2 * dispersionV M N Q (fun (x : ℕ) => 1) β c a + dispersionU M N Q (fun (x : ℕ) => 1) β c a)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError_sq_le_smoothed_dispersion (M S N Q : Finset ℕ) (α β c w : ℕ → ℝ) (a : ℤ) (hMS : M ⊆ S) (hw : ∀ m ∈ S, 0 ≤ w m) (hmajor : ∀ m ∈ M, 1 ≤ w m) : signedError M N Q α β c a ^ 2 ≤ (∑ m ∈ M, α m ^ 2) * (dispersionW S N Q w β c a - 2 * dispersionV S N Q w β c a + dispersionU S N Q w β c a)

A nonnegative cutoff majorizing 1 on the alpha support may enlarge the m-sum.