The beta-pair mass discarded at a large common divisor

Here the common divisor is gcd(n₁, n₂) of the two beta variables, not gcd(q, r) of the moduli. The elementary gcd mean and the global second divisor moment give an explicit inverse-square-root cutoff gain. No arithmetic-progression, Siegel--Walfisz, or Shiu estimate is used.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeGCDPairs (N : Finset ℕ) (Y : ℝ) : Finset (ℕ × ℕ)

Ordered pairs of beta indices whose common divisor exceeds a real cutoff.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeGCDPairs N Y = {p ∈ N ×ˢ N | Y < ↑(p.1.gcd p.2)}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_gcd_pairs_le_log {T : ℝ} (hT : 1 ≤ T) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) : ∑ p ∈ N ×ˢ N, ↑(p.1.gcd p.2) ≤ T ^ 2 * (1 + Real.log T)

The double gcd mean on any finite subset of the positive interval.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeGCDPairs_le {T Y : ℝ} (hT : 1 ≤ T) (hY : 0 < Y) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) : ↑(largeGCDPairs N Y).card ≤ T ^ 2 * (1 + Real.log T) / Y

Markov's inequality for the large common divisor of the beta indices.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_pair_mul_le_sqrt_card {ι : Type u_1} (N : Finset ι) (S : Finset (ι × ι)) (hS : S ⊆ N ×ˢ N) (β : ι → ℝ) : ∑ p ∈ S, |β p.1 * β p.2| ≤ √↑S.card * ∑ n ∈ N, β n ^ 2

Cauchy--Schwarz on any set of ordered pairs pays one coefficient square sum and the square root of the number of retained pairs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_largeGCDPairs_le {k : ℕ} (hk : 1 ≤ k) {T Y : ℝ} (hT : 1 ≤ T) (hY : 0 < Y) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) : ∑ p ∈ largeGCDPairs N Y, |β p.1 * β p.2| ≤ T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y)

Quantitative discarded beta-pair mass with inverse-square-root cutoff gain, for arbitrary signed fixed-order divisor-bounded coefficients.