Sparse-modulus exclusion in the original progression sum

The elementary progression-counting part of Fouvry (1984), p. 236, (8.5). Coprimality is retained in the sparse modulus row until the actual bump progression is counted. Absolute values are taken before enlarging any mask.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalSparseRow (Q S : Finset ℕ) (c : ℕ → ℝ) (a : ℤ) (n m : ℕ) : ℝ

The sparse row retains the coprimality needed for the progression count.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalSparseRow Q S c a n m = ∑ q ∈ Q, if q ∈ S ∧ n.Coprime q ∧ ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalSparseRow_nonneg (Q S : Finset ℕ) (c : ℕ → ℝ) (a : ℤ) (n m : ℕ) : 0 ≤ wOriginalSparseRow Q S c a n m

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_cutoff_wOriginalSparseRow_le {M L Z A : ℝ} (hM : 1 ≤ M) (hL : 1 ≤ L) (hZ : 0 < Z) (hA : 0 ≤ A) (Q S : Finset ℕ) (hS : S ⊆ largeSquareDivisorSet ⌊L⌋₊ Z) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ A) (a : ℤ) (n : ℕ) : ∑ m ∈ dyadicCutoffNatSupport M, scaledDyadicCutoff M ↑m * wOriginalSparseRow Q S c a n m ≤ A * (8 * M * (1 + Real.log L) + 2 * L) / Z

Harmonic mass pays the main progression count, and counting mass pays its endpoint error. This estimate is uniform in the beta index and residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_sparse_modulus_sums (M : ℝ) (N Q S : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.1.1 ∈ S ∨ t.1.2 ∈ S) : |wMaskedOriginal M N Q β c a P| ≤ ∑ p ∈ N ×ˢ N, ∑ m ∈ dyadicCutoffNatSupport M, |β p.1 * β p.2| * scaledDyadicCutoff M ↑m * ((wOriginalSparseRow Q S c a p.1 m * ∑ r ∈ Q, if ↑m * ↑p.2 ≡ a [ZMOD ↑r] then |c r| else 0) + (∑ q ∈ Q, if ↑m * ↑p.1 ≡ a [ZMOD ↑q] then |c q| else 0) * wOriginalSparseRow Q S c a p.2 m)

The two sparse strips majorize any further mask. In particular no symmetry of that mask and no sign restriction on either weight is required.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_sparse_row_cap {M L Z A B : ℝ} (hM : 1 ≤ M) (hL : 1 ≤ L) (hZ : 0 < Z) (hA : 0 ≤ A) (hB : 0 ≤ B) (N Q S : Finset ℕ) (hS : S ⊆ largeSquareDivisorSet ⌊L⌋₊ Z) (β c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ A) (a : ℤ) (hrow : ∀ n ∈ N, β n ≠ 0 → ∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ B) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.1.1 ∈ S ∨ t.1.2 ∈ S) : |wMaskedOriginal M N Q β c a P| ≤ 2 * A * B * (8 * M * (1 + Real.log L) + 2 * L) * (∑ n ∈ N, |β n|) ^ 2 / Z

A finite row-cap estimate for the original sum. The unrestricted row cap is only required where both beta and the actual bump are nonzero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_modulus_support (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T L x Y : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → M * T ≤ x → L ≤ x → 0 < Y → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(wGCDTuple t).δ₁ ∨ Y < ↑(wGCDTuple t).δ₂) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * (1 + Real.log L) + L) * (∑ n ∈ N, |β n|) ^ 2 / √Y

Uniform original-W square-root saving for either canonical supported modulus factor. The constant depends only on the divisor order and exponent, not on the changing residue, supports, scales, signed weights, or further mask. No relation between L and M is imposed.