Shared fixed-scale large-common-modulus bound for original W

The actual nonzero shifted differences satisfy |m*n-a| ≤ 4*Cscale*x. Two divisor estimates pay these signed modulus rows; a third pays the nonzero beta difference, which still satisfies |n₁-n₂| ≤ x. Consequently the fixed enlargement enters the constant as (4*Cscale)^(2*ε/3), without changing the main power x^ε. The diagonal costs its square mass, not the square of its absolute mass. No WF property of a restricted weight is asserted.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kDelta_natAbs_mul_sub_le_of_cutoff {M T x Cscale : ℝ} (hCscale : 1 ≤ Cscale) (hx : 1 ≤ x) (hM : 0 < M) (hMT : M * T ≤ x) {m n : ℕ} (hn : ↑n ≤ T) (hm : scaledDyadicCutoff M ↑m ≠ 0) (a : ℤ) (ha : |↑a| ≤ Cscale * x) : ↑(↑m * ↑n - a).natAbs ≤ 4 * Cscale * x

On the actual nonzero bump, only the auxiliary divisor-growth enclosure is enlarged. Neither the bump scale nor the original residue is changed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeDelta_pair_mass_kscale (j : ℕ) {ε Cscale : ℝ} (hε : 0 < ε) (hCscale : 1 ≤ Cscale) : ∃ (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| ≤ Cscale * x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (Y : ℝ), 0 < Y → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * ∑ n ∈ N, β n ^ 2 + (M / Y + 1) * (∑ n ∈ N, |β n|) ^ 2)

The constant precedes all scales, supports, coefficients, residues and masks. The beta coefficient is arbitrary apart from the stated support condition; only the modulus coefficient has a fixed divisor order.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeDelta_kscale {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {ε Cscale : ℝ} (hε : 0 < ε) (hCscale : 1 ≤ Cscale) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T x : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ x → M * T ≤ x → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ Cscale * x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (Y : ℝ), 0 < Y → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * T * (1 + Real.log T) ^ (k ^ 2 - 1) + (M / Y + 1) * (T * (1 + Real.log T) ^ (k - 1)) ^ 2)

Evaluating the beta square and absolute masses with fixed-order divisor means leaves the diagonal at length T, while the off-diagonal receives the factor M / Y + 1.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeDelta_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) → ∀ (Y : ℝ), 0 < Y → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * ∑ n ∈ N, β n ^ 2 + (M / Y + 1) * (∑ n ∈ N, |β n|) ^ 2)

The constant precedes all scales, supports, coefficients, residues and masks. The beta coefficient is arbitrary apart from the stated support condition; only the modulus coefficient has a fixed divisor order.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeDelta {k : ℕ} (hk : 1 ≤ k) (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 : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (Y : ℝ), 0 < Y → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.1.1.gcd t.1.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * T * (1 + Real.log T) ^ (k ^ 2 - 1) + (M / Y + 1) * (T * (1 + Real.log T) ^ (k - 1)) ^ 2)

Evaluating the beta square and absolute masses with fixed-order divisor means leaves the diagonal at length T, while the off-diagonal receives the factor M / Y + 1.