Original and zero-mode bounds for a large supported beta factor

The canonical d₁ condition gives a sparse square-divisor strip in the first beta coordinate. Cauchy--Schwarz then saves a fourth root of the cutoff. The original and zero-mode estimates apply to the identical arbitrary mask; no symmetry or preservation of well-factorability under masking is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_largeSupportPairs_le {k : ℕ} (hk : 1 ≤ k) {T Y : ℝ} (hT : 1 ≤ T) (hY : 0 < Y) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) : ∑ p ∈ largeSupportPairs N Y, |β p.1 * β p.2| ≤ T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √(2 / √Y)

The signed coefficient mass on the large-d₁ pair set has an explicit fourth-root saving, using only the global divisor second moment.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_largeSupportPairs_of_wOriginalTuple {N Q : Finset ℕ} {a : ℤ} {t : WOriginalTuple} (ht : t ∈ wOriginalTuples N Q a) {Y : ℝ} (hlarge : Y < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁) : t.2 ∈ largeSupportPairs N Y

A large canonical supported factor is exactly the pair condition needed by the sparse envelope, regardless of the modulus coordinates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeSupport {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 < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √(2 / √Y))

Uniform large-d₁ exclusion for the actual original progression sum. The nondivisibility condition is supplied later by betaClean.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_largeSupport {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {T L Y : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hY : 0 < Y) (M : ℝ) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁) : |wMaskedZeroMode M N Q β c a P| ≤ |M * dyadicCutoffMass| * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √(2 / √Y)) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Absolute control of the same masked zero mode, without restricting the unmasked SW cancellation or assuming that the mask is symmetric.