Fixed-residue-scale large-supported-factor bound

Only the auxiliary divisor-growth scale is enlarged to Cscale * x. The progression sum, beta endpoint, arbitrary mask and supported-factor threshold Y are unchanged. The fixed enlargement is paid in the constant.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeSupport_kscale {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {ε Cscale : ℝ} (hε : 0 < ε) (hCscale : 1 ≤ Cscale) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T Y x : ℝ), 1 ≤ M → 1 ≤ T → 0 < Y → 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) → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √(2 / √Y))

The large-support original-sum estimate for a fixed larger residue range. The constant is chosen before all varying scales, coefficients and masks.