Original and same-mask zero-mode bounds from finite beta-pair support

A mask may depend on both moduli as well as both beta indices. Its only required support information is that the beta pair belongs to a specified finite set. Both bounds retain arbitrary coefficient signs and do not restrict an unmasked cancellation estimate to a signed submask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_pair_modulus_sums (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (F : Finset (ℕ × ℕ)) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.2 ∈ F) : |wMaskedOriginal M N Q β c a P| ≤ ∑ p ∈ F, ∑ 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

A finite enclosure of the masked beta pairs gives a nonnegative majorant with the two modulus sums separated. No enclosure of F in N ×ˢ N is needed until the individual rows are estimated.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_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) → ∀ F ⊆ N ×ˢ N, ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → t.2 ∈ F) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * ∑ p ∈ F, |β p.1 * β p.2|

The original progression sum is bounded by the absolute mass of any finite beta-pair support enclosure. The constant depends only on j and ε, and is chosen before the scales, coefficients, residue, pair set, and mask. The nondivisibility hypothesis removes the equality progression.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.masked_beta_pair_abs_le_pair_mass (N Q : Finset ℕ) (β : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (F : Finset (ℕ × ℕ)) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.2 ∈ F) {q r : ℕ} (hq : q ∈ reducedModuli Q a) (hr : r ∈ reducedModuli Q a) : |∑ p ∈ N ×ˢ N, if WCompatible q r p.1 p.2 ∧ P ((q, r), p) then β p.1 * β p.2 else 0| ≤ ∑ p ∈ F, |β p.1 * β p.2|

An arbitrary modulus-dependent beta-pair mask is paid by the absolute mass of its finite pair enclosure, without positivity or symmetry of beta.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_pair_mass (j : ℕ) {L : ℝ} (hL : 1 ≤ L) (M : ℝ) (N Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (P : WOriginalTuple → Prop) (F : Finset (ℕ × ℕ)) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.2 ∈ F) : |wMaskedZeroMode M N Q β c a P| ≤ (|M * dyadicCutoffMass| * ∑ p ∈ F, |β p.1 * β p.2|) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

The actual zero mode with the same mask is paid by its absolute beta-pair mass and a logarithmic modulus sum. There is no beta divisor bound, nondivisibility condition, symmetry, or restriction on M or a. Unlike the original-sum row estimate, this also permits extraneous pairs in F.