Uniform subpower payment of the joint gcd mean

The constant is chosen before all three signed coefficients and the scale. Zero numerators are excluded by the support, not charged as ordinary rows. There is no coprimality hypothesis on either original summation variable.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_mean_subpower {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a U V : ℤ) (S : ℕ) (P : Finset (ℕ × ℕ)), a ≠ 0 → U ≠ 0 → V ≠ 0 → (∀ p ∈ P, (0 < p.1 ∧ p.1 ≤ S) ∧ (0 < p.2 ∧ p.2 ≤ S) ∧ mainJointNumerator a U V p.1 p.2 ≠ 0) → ∑ p ∈ P, ↑((p.1 * p.2).gcd (mainJointNumerator a U V p.1 p.2).natAbs) * ↑((fouvryTau 2) (mainJointNumerator a U V p.1 p.2).natAbs) ≤ C * ↑S ^ 2 * (1 + Real.log ↑S) * ↑(a.natAbs * (U.natAbs + V.natAbs) * S) ^ δ

The divisor-weighted joint mean, with a constant depending only on the positive exponent. This includes empty supports and the zero scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_mean_unweighted_subpower {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a U V : ℤ) (S : ℕ) (P : Finset (ℕ × ℕ)), a ≠ 0 → U ≠ 0 → V ≠ 0 → (∀ p ∈ P, (0 < p.1 ∧ p.1 ≤ S) ∧ (0 < p.2 ∧ p.2 ≤ S) ∧ mainJointNumerator a U V p.1 p.2 ≠ 0) → ∑ p ∈ P, ↑((p.1 * p.2).gcd (mainJointNumerator a U V p.1 p.2).natAbs) ≤ C * ↑S ^ 2 * (1 + Real.log ↑S) * ↑(a.natAbs * (U.natAbs + V.natAbs) * S) ^ δ

The same joint mean without the optional divisor weight.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_rectangular_subpower {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a U V : ℤ) (S : ℕ), a ≠ 0 → U ≠ 0 → V ≠ 0 → have P := {p ∈ Finset.Ioc 0 S ×ˢ Finset.Ioc 0 S | mainJointNumerator a U V p.1 p.2 ≠ 0}; have B := C * ↑S ^ 2 * (1 + Real.log ↑S) * ↑(a.natAbs * (U.natAbs + V.natAbs) * S) ^ δ; ∑ p ∈ P, ↑((p.1 * p.2).gcd (mainJointNumerator a U V p.1 p.2).natAbs) * ↑((fouvryTau 2) (mainJointNumerator a U V p.1 p.2).natAbs) ≤ B ∧ ∑ p ∈ P, ↑((p.1 * p.2).gcd (mainJointNumerator a U V p.1 p.2).natAbs) ≤ B

The full positive rectangle, with only its zero numerators removed. Both the weighted and unweighted estimates use the same uniform constant.