Shifted divisor moments without a power loss

Regrouping the product m*n uses the exact divisor antidiagonal. The absolute-value shift has at most two preimages. The inequality u*v ≤ u²+v² then gives a uniform fixed logarithmic cost.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_convolution_le (i k : ℕ) (S N : Finset ℕ) (X : ℕ) (hprod : ∀ m ∈ S, ∀ n ∈ N, 0 < m * n ∧ m * n ≤ X) (F : ℕ → ℝ) (hF : ∀ (t : ℕ), 0 ≤ F t) : ∑ m ∈ S, ∑ n ∈ N, ↑((fouvryTau i) m) * ↑((fouvryTau k) n) * F (m * n) ≤ ∑ t ∈ Finset.Ioc 0 X, ↑((fouvryTau (i + k)) t) * F t

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_shift_fiber_card_le (S : Finset ℕ) (a : ℤ) (d : ℕ) : {t ∈ S | (↑t - a).natAbs = d}.card ≤ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_shift_sum_le (S : Finset ℕ) (a : ℤ) (Y : ℕ) (hY : ∀ t ∈ S, (↑t - a).natAbs ≤ Y) (F : ℕ → ℝ) (hF : ∀ (d : ℕ), 0 ≤ F d) (hF0 : F 0 = 0) : ∑ t ∈ S, F (↑t - a).natAbs ≤ 2 * ∑ d ∈ Finset.Ioc 0 Y, F d

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