theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_two_one_convolution (v : ℕ) : ∑ p ∈ v.divisorsAntidiagonal, ↑((fouvryTau 2) p.1) * ↑((fouvryTau 1) p.2) = ↑((fouvryTau 3) v)

The full ordered divisor convolution, including the zero input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryG9_weighted_product_fibre_le (U V : Finset ℕ) (α β : ℕ → ℝ) (v : ℕ) (hα : ∀ m ∈ U, 0 ≤ α m ∧ α m ≤ ↑((fouvryTau 2) m)) (hβ : ∀ n ∈ V, 0 ≤ β n ∧ β n ≤ ↑((fouvryTau 1) n)) : (∑ p ∈ U ×ˢ V, if p.1 * p.2 = v then α p.1 * β p.2 else 0) ≤ ↑((fouvryTau 3) v)

Arbitrary rectangular weights retain their actual product multiplicities. No positive-support assumption is needed: the divisor weights kill zero factors.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryG9_natAbs_product_values (N m n r : ℕ) (h : (↑N - ↑m * ↑n).natAbs = r) : m * n = N + r ∨ m * n = N - r

The integer absolute-difference fibre has at most two natural product values. Natural subtraction is retained, even when the radius exceeds the centre.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryG9_weighted_natAbs_fibre_le (U V : Finset ℕ) (α β : ℕ → ℝ) (N r : ℕ) (hα : ∀ m ∈ U, 0 ≤ α m ∧ α m ≤ ↑((fouvryTau 2) m)) (hβ : ∀ n ∈ V, 0 ≤ β n ∧ β n ≤ ↑((fouvryTau 1) n)) : (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then α p.1 * β p.2 else 0) ≤ ↑((fouvryTau 3) (N + r)) + ↑((fouvryTau 3) (N - r))

A genuine weighted absolute-difference multiplicity bound, with no r ≤ N premise. At radius zero the harmless doubled upper bound is intentional.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryG9_weighted_natAbs_fibre_le_of_lt (U V : Finset ℕ) (α β : ℕ → ℝ) (N r : ℕ) (hNr : N < r) (hα : ∀ m ∈ U, 0 ≤ α m ∧ α m ≤ ↑((fouvryTau 2) m)) (hβ : ∀ n ∈ V, 0 ≤ β n ∧ β n ≤ ↑((fouvryTau 1) n)) : (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then α p.1 * β p.2 else 0) ≤ ↑((fouvryTau 3) (N + r))

Beyond the centre the lower product is zero and has zero divisor weight.