A common-index and r mean in the main nonzero branch

Fouvry (1987), p. 632, (4.8). The constant term, not the slope, is nonzero when h'*s ≠ h*s'. The r mean removes the whole r gcd cost. The subsequent common-index mean uses that constant term. The remaining s*s' gcd and divisor weight are retained explicitly, not bounded by a power of the scale and silently absorbed into an epsilon loss.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3MainConstant (n₂ n₂' s s' : ℕ) (a h h' : ℤ) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3MainConstant n₂ n₂' s s' a h h' = a * ↑n₂ * ↑n₂' * (h' * ↑s - h * ↑s')

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator_affine (d₁ n n₂ n₂' s s' : ℕ) (a h h' : ℤ) : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = iv3MainConstant n₂ n₂' s s' a h h' + a * ↑d₁ * (h * ↑n₂' * ↑s' - h' * ↑n₂ * ↑s) * ↑n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3MainConstant_ne_zero {n₂ n₂' s s' : ℕ} {a h h' : ℤ} (ha : a ≠ 0) (hn₂ : 0 < n₂) (hn₂' : 0 < n₂') (hmain : h' * ↑s ≠ h * ↑s') : iv3MainConstant n₂ n₂' s s' a h h' ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_main_index_gcd (d₁ n n₂ n₂' s s' : ℕ) (a h h' : ℤ) : n.gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs = n.gcd (iv3MainConstant n₂ n₂' s s' a h h').natAbs

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_main_gcd_le {d₁ n n₂ n₂' r s s' : ℕ} {a h h' : ℤ} (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) : (n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs ≤ n.gcd (iv3MainConstant n₂ n₂' s s' a h h').natAbs * (s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs * r.gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs

The complete modulus gcd is separated without a loss of r, s, or s'. No coprimality assumptions are needed for this inequality.

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

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

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3MainResidual (d₁ n₂ n₂' s s' : ℕ) (a h h' : ℤ) (N : ℕ) : ℕ

The genuinely remaining arithmetic: the s*s' gcd and divisor count, with zero numerators excluded. The n and r factors of the modulus no longer occur in this residual sum.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3MainResidual d₁ n₂ n₂' s s' a h h' N = ∑ n ∈ Finset.Ioc 0 N with MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0, (s * s').gcd (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs.divisors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_main_sqrt_gcd_sum {d₁ n₂ n₂' s s' : ℕ} {a h h' : ℤ} (ha : a ≠ 0) (hn₂ : 0 < n₂) (hn₂' : 0 < n₂') (hmain : h' * ↑s ≠ h * ↑s') (N R : ℕ) : ∑ n ∈ Finset.Ioc 0 N with iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0, ∑ r ∈ Finset.Ioc 0 R, √↑((n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs) ≤ ↑R * (√↑(N * (iv3MainConstant n₂ n₂' s s' a h h').natAbs.divisors.card) * √↑(iv3MainResidual d₁ n₂ n₂' s s' a h h' N))

A simultaneous common-index and r mean for the original signed numerator. It applies even if its slope in the common index vanishes.