Quantitative first large-gcd exclusion for the actual nonzero W sum

The original progression sum, its zero mode and its Fourier tail are estimated on the identical arbitrary mask supported on gcd(n₁,n₂) > x^η. This excludes the first gcd coordinate, not the union of all five large-gcd coordinates. The beta parameter T is an upper endpoint, not a dyadic lower endpoint. The condition β n ≠ 0 → n ∤ a is retained; its preprocessing is separate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_abs_le_largeGCD {k j : ℕ} (hk : 1 ≤ k) (hj : 1 ≤ j) (l : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ) (D : ℝ), 0 < C ∧ 0 < D ∧ ∀ (M T L Y Z x : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → 0 < Y → 0 < Z → 1 ≤ x → M * T ≤ x → ∀ (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 : ℤ), |↑a| ≤ x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) → |wMaskedTruncated M (wUniformCutoff M Z) N Q β c a P| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y)) + |M * dyadicCutoffMass| * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y)) * (1 + Real.log L) ^ (2 * j ^ 2 + 1) + D * ((L * (1 + Real.log L) ^ (j - 1)) ^ 2 * (T * (1 + Real.log T) ^ (k - 1)) ^ 2) / Z ^ l

All three already proved estimates on precisely the same mask. The constants precede all scales, supports, coefficients, residue and mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_wMaskedTruncated_largeGCD_power_saving {k j : ℕ} (hk : 1 ≤ k) (hj : 1 ≤ j) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (β 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 → x ^ η < ↑(t.2.1.gcd t.2.2)) → |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q β c a P| ≤ 3 * M * T ^ 2 * x ^ (-η / 8)

A power saving for the actual finite nonzero-frequency sum. The cutoff is constructed, the mask is arbitrary within the first large-beta-gcd exclusion, and the eventual threshold depends only on the fixed orders and η.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_largeGCD_power_saving {k j : ℕ} (hk : 1 ≤ k) (hj : 1 ≤ j) {η : ℝ} (hη : 0 < η) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (β 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 → x ^ η < ↑(t.2.1.gcd t.2.2)) → |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q β c a P| ≤ 3 * M * T ^ 2 * x ^ (-η / 8)

Explicit uniform threshold version of the power saving.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_largeGCD_alpha_log_payment {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) (A : ℕ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ 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 → x ^ η < ↑(t.2.1.gcd t.2.2)) → (∑ m ∈ S, α m ^ 2) * |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q β c a P| ≤ x ^ 2 / Real.log x ^ A

The actual alpha square sum pays every fixed natural logarithmic loss. The threshold is uniform in both scales, all three signed coefficients, supports, the varying residue and every submask of the first gcd exclusion.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_largeGCD_alpha_real_log_payment {i k j : ℕ} (hi : 1 ≤ i) (hk : 1 ≤ k) (hj : 1 ≤ j) (A : ℝ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ 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 → x ^ η < ↑(t.2.1.gcd t.2.2)) → (∑ m ∈ S, α m ^ 2) * |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q β c a P| ≤ x ^ 2 / Real.log x ^ A

Real logarithmic exponents are paid as well, by rounding the requested loss upward. No restriction on the fixed real exponent is needed.