Large common modulus in the original W progression sum

Compatibility is retained until the common modulus has become a divisor of the beta difference. The diagonal is separated before this divisor set is formed. All additional arithmetic masks and signed weights are allowed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_product_modEq_le (K d n : ℕ) (a : ℤ) (hn : n.Coprime d) : {m ∈ Finset.Icc 0 K | ↑m * ↑n ≡ a [ZMOD ↑d]}.card ≤ K / d + 1

Coprimality makes the product progression occupy at most one point in each interval of length d.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_cutoff_product_modEq_le {M : ℝ} (hM : 1 ≤ M) {d n : ℕ} (hd : 0 < d) (hn : n.Coprime d) (a : ℤ) : (∑ m ∈ dyadicCutoffNatSupport M, if ↑m * ↑n ≡ a [ZMOD ↑d] then scaledDyadicCutoff M ↑m else 0) ≤ 4 * M / ↑d + 1

A bound for the actual bump, not a postulated progression asymptotic.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WLargeDeltaWitness (Y : ℝ) (a : ℤ) (n₁ n₂ m : ℕ) : Prop

An off-diagonal witness includes the progression condition on m. Discarding that condition would lose the common-modulus saving.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WLargeDeltaWitness Y a n₁ n₂ m = (n₁ = n₂ ∨ ∃ d ∈ (↑n₁ - ↑n₂).natAbs.divisors, Y < ↑d ∧ n₁.Coprime d ∧ ↑m * ↑n₁ ≡ a [ZMOD ↑d])

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wLargeDeltaWitness_of_compatible {Y : ℝ} {a : ℤ} {q r n₁ n₂ m : ℕ} (hc : WCompatible q r n₁ n₂) (hY : Y < ↑(q.gcd r)) (hm : ↑m * ↑n₁ ≡ a [ZMOD ↑q]) : WLargeDeltaWitness Y a n₁ n₂ m

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_cutoff_largeDeltaWitness_le {M Y : ℝ} (hM : 1 ≤ M) (hY : 0 < Y) (a : ℤ) (n₁ n₂ : ℕ) (hne : n₁ ≠ n₂) : (∑ m ∈ dyadicCutoffNatSupport M, if WLargeDeltaWitness Y a n₁ n₂ m then scaledDyadicCutoff M ↑m else 0) ≤ (4 * M / Y + 1) * ↑((fouvryTau 2) (↑n₁ - ↑n₂).natAbs)

The off-diagonal union bound is over divisors of a nonzero difference. Each divisor is paid with its own product progression.

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

The modulus rows can be enlarged independently only after retaining the existence of the large common divisor and its progression.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeDelta_row_cap {M Y A : ℝ} (hM : 1 ≤ M) (hY : 0 < Y) (hA : 0 ≤ A) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hrow : ∀ n ∈ N, β n ≠ 0 → ∀ (m : ℕ), scaledDyadicCutoff M ↑m ≠ 0 → (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ A) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) : |wMaskedOriginal M N Q β c a P| ≤ A ^ 2 * ∑ p ∈ N ×ˢ N, |β p.1 * β p.2| * if p.1 = p.2 then 5 * M else (4 * M / Y + 1) * ↑((fouvryTau 2) (↑p.1 - ↑p.2).natAbs)

A finite quantitative estimate, separating the diagonal before forming divisors of the difference. The row cap is needed only on the actual support.