The original progression sum with a large beta gcd

An elementary substitute for Fouvry (1984), p. 235, (8.2). Modulus sums are bounded by divisors of the nonzero differences m*n-a. The hypothesis that nonzero beta coefficients have n ∤ a is essential: it removes the equality term, and its preprocessing is not proved here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mul_sub_ne_zero_of_not_dvd (m n : ℕ) (a : ℤ) (hn : ¬↑n ∣ a) : ↑m * ↑n - a ≠ 0

The equality progression is impossible under the beta support hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_modEq_abs_le_fouvryTau (j : ℕ) (Q : Finset ℕ) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (m n : ℕ) (a : ℤ) (hne : ↑m * ↑n - a ≠ 0) : (∑ q ∈ Q, if ↑m * ↑n ≡ a [ZMOD ↑q] then |c q| else 0) ≤ ↑((fouvryTau (j + 1)) (↑m * ↑n - a).natAbs)

Summing arbitrary signed divisor-bounded modulus weights costs one additional divisor order, independently of the size of the modulus set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_modulus_sums (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (Y : ℝ) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) : |wMaskedOriginal M N Q β c a P| ≤ ∑ p ∈ largeGCDPairs N Y, ∑ 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

Discarding compatibility and any additional mask gives a nonnegative majorant whose two modulus sums can be paid separately.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_scaledDyadicCutoff_le {M : ℝ} (hM : 1 ≤ M) : ∑ m ∈ dyadicCutoffNatSupport M, scaledDyadicCutoff M ↑m ≤ 5 * M

The finite support enclosure costs at most five times the scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.natAbs_mul_sub_le_of_cutoff {M T x : ℝ} (hM : 0 < M) (hMT : M * T ≤ x) {m n : ℕ} (hn : ↑n ≤ T) (hm : scaledDyadicCutoff M ↑m ≠ 0) (a : ℤ) (ha : |↑a| ≤ x) : ↑(↑m * ↑n - a).natAbs ≤ 4 * x

The differences occurring on the actual nonzero bump support remain uniformly bounded for all changing residues with |a| ≤ x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeGCD_pair_mass (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T x : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ x → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → ∀ (β c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (Y : ℝ) (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * ∑ p ∈ largeGCDPairs N Y, |β p.1 * β p.2|

The original progression sum is paid before invoking any beta mean. The modulus set can even contain zero, since a nonzero difference has no zero divisor. The fixed-order constant precedes every changing datum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeGCD {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T Y x : ℝ), 1 ≤ M → 1 ≤ T → 0 < Y → 1 ≤ x → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ 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 < ↑(t.2.1.gcd t.2.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y))

Uniform large-beta-gcd exclusion for the ORIGINAL smoothed progression sum. This uses the elementary inverse-square-root pair-mass saving, not an estimate for its zero mode or a presumed distribution theorem.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wLargeBetaGCDOriginal_abs_le {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T Y x : ℝ), 1 ≤ M → 1 ≤ T → 0 < Y → 1 ≤ x → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → |wMaskedOriginal M N Q β c a fun (t : WOriginalTuple) => Y < ↑(t.2.1.gcd t.2.2)| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y))

Direct specialization to the first large-gcd exclusion.