A logarithmic joint gcd mean

The angular sum is split into its two triangles. The ordinary gcd mean on the shorter side and the existing reciprocal gcd mean on the longer side replace a dyadic-shell argument.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_angular_mean {A B S : ℕ} (hA : 0 < A) (hB : 0 < B) (hS : 0 < S) : ∑ u ∈ Finset.Ioc 0 S, ∑ v ∈ Finset.Ioc 0 S, ↑(u.gcd A) * ↑(v.gcd B) / ↑(max u v) ^ 2 ≤ 2 * ↑((fouvryTau 2) A) * ↑((fouvryTau 2) B) * (1 + Real.log ↑S)

The angular weight has only one logarithm, with no coprimality condition on the enlarged summation domain.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_mean_envelope {a U V : ℤ} (ha : a ≠ 0) (hU : U ≠ 0) (hV : V ≠ 0) {S : ℕ} (hS : 0 < S) {T : ℝ} (hT : 0 ≤ T) (henv : ∀ (n : ℕ), 0 < n → n ≤ a.natAbs * (U.natAbs + V.natAbs) * S → ↑((fouvryTau 2) n) ≤ T) (P : Finset (ℕ × ℕ)) (hP : ∀ 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) ≤ 2 * ↑S ^ 2 * ↑((fouvryTau 2) (a * U).natAbs) * ↑((fouvryTau 2) (a * V).natAbs) * T ^ 2 * (1 + Real.log ↑S)

A genuine rectangular joint mean on any finite positive support with nonzero numerator. The envelope is discharged uniformly in the next module.