theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeGCD_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 : ℝ) (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) → |wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * ∑ p ∈ largeGCDPairs N Y, |β p.1 * β p.2|

Change only the auxiliary divisor-growth scale, not the original smoothed sum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_shifted_tau_sum_le_kscale (r s : ℕ) {Cscale x : ℝ} (hC : 1 ≤ Cscale) (hx : 1 ≤ x) (a : ℤ) (ha : |↑a| ≤ Cscale * x) : ∑ t ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau r) t) * ↑((fouvryTau s) (↑t - a).natAbs) ≤ 5 * Cscale * x * (1 + Real.log (2 * Cscale * x)) ^ (r ^ 2 + s ^ 2)

The original shifted moment is dominated by a larger auxiliary interval. The original shift and its two-preimage multiplicity are unchanged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.kscale_log_cost {Cscale x : ℝ} (hC : 1 ≤ Cscale) (hx : 1 ≤ x) (p : ℕ) : (1 + Real.log (2 * Cscale * x)) ^ p ≤ (1 + Real.log Cscale) ^ p * (1 + Real.log (2 * x)) ^ p

The fixed enlargement costs a constant, not an extra power of the main scale.