Poisson extraction with the same arithmetic mask

The exclusions in Fouvry (1984), (8.2)--(8.5), concern the original progression sum, not its truncated nonzero frequencies. This module keeps the same mask on the original sum, zero mode, retained frequencies and tail. No estimate for an unmasked zero mode is restricted to a new subset.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) : Finset WOriginalTuple

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P = Finset.filter P (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTuples N Q a)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient (β c : ℕ → ℝ) (t : WOriginalTuple) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient β c t = c t.1.1 * c t.1.2 * β t.2.1 * β t.2.2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal M N Q β c a P = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient β c t * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffNatSupport M) (fun (m : ℕ) => MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff M ↑m) a t.1.1 t.1.2 t.2.1 t.2.2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode M N Q β c a P = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient β c t * (M / ↑(t.1.1.lcm t.1.2) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated M H N Q β c a P = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTerm M H β c a t

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTail (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTail M H N Q β c a P = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient β c t * (∑' (h : ℤ), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a t.1.1 t.1.2 t.2.1 t.2.2 h - ∑ h ∈ Finset.Icc (-↑(H t.1.1 t.1.2)) ↑(H t.1.1 t.1.2), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a t.1.1 t.1.2 t.2.1 t.2.2 h).re

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTailEnvelope (k : ℕ) (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTailEnvelope k M H N Q β c a P = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples N Q a P, |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wTupleCoefficient β c t| / (1 + M / ↑(t.1.1.lcm t.1.2) * ↑(H t.1.1 t.1.2)) ^ k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTuples_spec {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {t : WOriginalTuple} (ht : t ∈ wMaskedTuples N Q a P) : t.1.1 ∈ Q ∧ t.1.2 ∈ Q ∧ WCompatible t.1.1 t.1.2 t.2.1 t.2.2 ∧ P t

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_eq_zero_add_truncated_add_tail {M : ℝ} (hM : 0 < M) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (hQ : ∀ q ∈ Q, q ≠ 0) : wMaskedOriginal M N Q β c a P = wMaskedZeroMode M N Q β c a P + wMaskedTruncated M H N Q β c a P + wMaskedTail M H N Q β c a P

Exact extraction on any arithmetic subdomain, with no positivity assumptions on the coefficients or restrictions on the changing residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTail_uniform (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop), (∀ q ∈ Q, q ≠ 0) → |wMaskedTail M H N Q β c a P| ≤ C * wMaskedTailEnvelope k M H N Q β c a P

The tail constant is chosen before the mask, all coefficients, both supports, the residue, and the modulus-dependent frequency cutoffs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_abs_le (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop), (∀ q ∈ Q, q ≠ 0) → |wMaskedTruncated M H N Q β c a P| ≤ |wMaskedOriginal M N Q β c a P| + |wMaskedZeroMode M N Q β c a P| + C * wMaskedTailEnvelope k M H N Q β c a P

Transport a bound for an original progression sum only with its own zero mode and its own tail, never with the unmasked SW main term.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_eq_gcdMask (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WGCDData → Prop) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : (wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => P (wGCDTuple t)) = ∑ v ∈ wGCDTuples N Q a with P v, wGCDTerm M H β c a v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDLargeSum_eq_maskedTruncated (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : wGCDLargeSum M Y H N Q β c a = wMaskedTruncated M H N Q β c a fun (t : WOriginalTuple) => ¬(wGCDTuple t).Small Y

The exact large five-gcd contribution is a masked frequency sum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDLargeSum_eq_original_sub_zero_sub_tail {M : ℝ} (hM : 0 < M) (Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : wGCDLargeSum M Y H N Q β c a = ((wMaskedOriginal M N Q β c a fun (t : WOriginalTuple) => ¬(wGCDTuple t).Small Y) - wMaskedZeroMode M N Q β c a fun (t : WOriginalTuple) => ¬(wGCDTuple t).Small Y) - wMaskedTail M H N Q β c a fun (t : WOriginalTuple) => ¬(wGCDTuple t).Small Y

Weighted dyadic payment

The same-mask extraction above also transports a dyadic power saving and a paid tail to a logarithmic bound. No geometric or moment estimate is assumed beyond the explicit scalar hypotheses below.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_dyadic_power_payment {M T x E b : ℝ} {u A : ℕ} (hM0 : 0 < M) (hT0 : 0 < T) (hx0 : 0 < x) (hMT : M * (2 * T) ≤ x) (hlog : 2 ≤ Real.log x) (hα0 : 0 ≤ E) (hAlpha : E ≤ 2 * M * (1 + Real.log x) ^ u) (hpay : 4 * (1 + Real.log x) ^ (u + (A + 1)) * x ^ b ≤ 1) (cutoff : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (hQpos : ∀ q ∈ Q, q ≠ 0) (hheadPower : |wMaskedOriginal M N Q β c a P| + |wMaskedZeroMode M N Q β c a P| ≤ 2 * M * (2 * T) ^ 2 * x ^ b) (htailPay : E * |wMaskedTail M cutoff N Q β c a P| ≤ x ^ 2 / Real.log x ^ (A + 1)) : E * |wMaskedTruncated M cutoff N Q β c a P| ≤ x ^ 2 / Real.log x ^ A

Convert a dyadic power saving and a paid tail into a logarithmic bound.