The same-mask zero mode for a large common modulus

Every further submask of gcd(q,r)>Y is allowed, without symmetry or positivity assumptions on the mask or coefficients. Absolute values are enlarged to the full symmetric congruence relation before applying the quadratic energy bound. The exact lcm denominator is retained throughout.

This bounds the actual masked zero mode, not a centered covariance or Siegel--Walfisz cancellation restricted to a mask. The original progression sum, nonzero modes, and their signed-error composition are separate results.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_modEq_row_le (K d n : ℕ) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 K) : {m ∈ N | n ≡ m [MOD d]}.card ≤ K / d + 1

Quotients distinguish the elements of a fixed residue class.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_modEq_pairs_le {T Y : ℝ} (hT : 1 ≤ T) (hY : 0 < Y) (d : ℕ) (hd : Y < ↑d) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) : (∑ p ∈ N ×ˢ N, if p.1 ≡ p.2 [MOD d] then |β p.1 * β p.2| else 0) ≤ (T / Y + 1) * ∑ n ∈ N, β n ^ 2

The full congruence relation is symmetric; its row bound pays the absolute beta products by the quadratic beta mass.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.masked_beta_pair_abs_le_largeDelta {T Y : ℝ} (hT : 1 ≤ T) (hY : 0 < Y) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) {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| ≤ (T / Y + 1) * ∑ n ∈ N, β n ^ 2

A possibly nonsymmetric submask is discarded only after taking absolute values, leaving the full congruence relation for the energy bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_largeDelta_energy (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 : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) : |wMaskedZeroMode M N Q β c a P| ≤ |M * dyadicCutoffMass| * ((T / Y + 1) * ∑ n ∈ N, β n ^ 2) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Quantitative common-modulus zero-mode bound, with arbitrary signed beta weights and every further arithmetic submask. The constant is one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_largeDelta {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 < ↑(t.1.1.gcd t.1.2)) : |wMaskedZeroMode M N Q β c a P| ≤ |M * dyadicCutoffMass| * ((T / Y + 1) * (T * (1 + Real.log T) ^ (k ^ 2 - 1))) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Fully evaluated version for beta weights bounded by a divisor function of positive order. The modulus order may still be zero.