A constructed frequency cutoff and uniform masked tail bound

Choosing H(q,r)=ceil(lcm(q,r)*Z/M) makes the dimensionless frequency cutoff at least Z for every modulus pair. The remaining coefficient envelope is evaluated by the proved global fixed-order divisor means.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff (M Z : ℝ) (q r : ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff M Z q r = ⌈↑(q.lcm r) / M * Z⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_scale {M : ℝ} (hM : 0 < M) (Z : ℝ) {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) : Z ≤ M / ↑(q.lcm r) * ↑(wUniformCutoff M Z q r)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wMaskedTuples_abs_coefficient_le (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ∑ t ∈ wMaskedTuples N Q a P, |wTupleCoefficient β c t| ≤ (∑ q ∈ Q, |c q|) ^ 2 * (∑ n ∈ N, |β n|) ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTailEnvelope_uniformCutoff_le (l : ℕ) {M Z : ℝ} (hM : 0 < M) (hZ : 0 < Z) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (hQ : ∀ q ∈ Q, q ≠ 0) : wMaskedTailEnvelope l M (wUniformCutoff M Z) N Q β c a P ≤ (∑ q ∈ Q, |c q|) ^ 2 * (∑ n ∈ N, |β n|) ^ 2 / Z ^ l

The whole absolute tail envelope has a uniform Z^(-l) bound, independently of the chosen arithmetic mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTail_uniformCutoff_fouvryTau (l : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M Z : ℝ), 0 < M → 0 < Z → ∀ (k j : ℕ), 1 ≤ k → 1 ≤ j → ∀ (T L : ℝ), 1 ≤ T → 1 ≤ L → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ) (P : WOriginalTuple → Prop), |wMaskedTail M (wUniformCutoff M Z) N Q β c a P| ≤ C * ((L * (1 + Real.log L) ^ (j - 1)) ^ 2 * (T * (1 + Real.log T) ^ (k - 1)) ^ 2) / Z ^ l

Explicit evaluation of the coefficient envelope for signed fixed-order weights. The tail constant depends only on l and the fixed bump.