Removing the artificial progression-step loss in the secondary mean

The previous inclusion of multiples in (0,B*s] paid a full factor s. The gcd product inequality instead pays only gcd(s,|A|). No coprimality of s and A, and no nonzero coefficient of the common n, is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.gcd_mul_le_gcd_mul_gcd {A : ℕ} (hA : 0 < A) (r s : ℕ) : (r * s).gcd A ≤ s.gcd A * r.gcd A

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_gcd_multiples_le {A : ℕ} (hA : A ≠ 0) (s B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, (r * s).gcd A ≤ B * (s.gcd A * A.divisors.card)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_gcd_sum_refined {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) (B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, (n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs ≤ B * (n * s' * (s.gcd (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs * (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs.divisors.card))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_sqrt_gcd_sum_refined {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) (B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, √↑((n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs) ≤ ↑B * √↑(n * s' * (s.gcd (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs * (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs.divisors.card))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_sqrt_gcd_sum_coprime {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) (hsA : s.Coprime (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs) (B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, √↑((n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs) ≤ ↑B * √↑(n * s' * (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs.divisors.card)

With a unit progression step modulo the numerator, the extra square-root step cost vanishes completely. The general result does not require this case.