Primitive coordinates for the joint main-term gcd

Only the reduced coordinates are coprime. The original two summation variables are unrestricted positive integers, and all coefficients are signed.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJointNumerator (a U V : ℤ) (s t : ℕ) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJointNumerator a U V s t = a * (U * ↑t - V * ↑s)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJointNumerator_scale (a U V : ℤ) (g u v : ℕ) : mainJointNumerator a U V (g * u) (g * v) = ↑g * mainJointNumerator a U V u v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJointNumerator_natAbs_le (a U V : ℤ) {s t S : ℕ} (hs : s ≤ S) (ht : t ≤ S) : (mainJointNumerator a U V s t).natAbs ≤ a.natAbs * (U.natAbs + V.natAbs) * S

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_gcd_primitive_left (a U V : ℤ) {u v : ℕ} (huv : u.Coprime v) : u.gcd (mainJointNumerator a U V u v).natAbs = u.gcd (a * U).natAbs

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_gcd_primitive_right (a U V : ℤ) {u v : ℕ} (huv : u.Coprime v) : v.gcd (mainJointNumerator a U V u v).natAbs = v.gcd (a * V).natAbs

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_gcd_normalized (a U V : ℤ) {g u v : ℕ} (huv : u.Coprime v) (hD : mainJointNumerator a U V u v ≠ 0) : (g * u * (g * v)).gcd (mainJointNumerator a U V (g * u) (g * v)).natAbs ≤ g * g.gcd (mainJointNumerator a U V u v).natAbs * u.gcd (a * U).natAbs * v.gcd (a * V).natAbs

The common factor is paid by a one-dimensional gcd mean, rather than discarded at its worst possible size.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainJoint_radial_mean (a U V : ℤ) {u v G L : ℕ} {T : ℝ} (huv : u.Coprime v) (hD : mainJointNumerator a U V u v ≠ 0) (hDle : (mainJointNumerator a U V u v).natAbs ≤ L) (hscale : ∀ g ∈ Finset.Ioc 0 G, (mainJointNumerator a U V (g * u) (g * v)).natAbs ≤ L) (hT : 0 ≤ T) (henv : ∀ (n : ℕ), 0 < n → n ≤ L → ↑((fouvryTau 2) n) ≤ T) : ∑ g ∈ Finset.Ioc 0 G, ↑((g * u * (g * v)).gcd (mainJointNumerator a U V (g * u) (g * v)).natAbs) * ↑((fouvryTau 2) (mainJointNumerator a U V (g * u) (g * v)).natAbs) ≤ ↑G ^ 2 * T ^ 2 * ↑(u.gcd (a * U).natAbs) * ↑(v.gcd (a * V).natAbs)

A complete radial mean, with the divisor envelope explicit.