Counting the secondary frequency-sieve ratio relation

For fixed positive s, the equation h'*s=h*s' forces s' to be a multiple of s/gcd(s,h) and determines h' uniquely. In a dyadic s block this pays only 2*gcd(s,h) partners, not an independent frequency and sieve-variable box. The resulting collision count is logarithmic.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioPartners (H S h s : ℕ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioPartners H S h s = {p ∈ Finset.Ioc 0 H ×ˢ Finset.Ioc 0 S | p.1 * s = h * p.2}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatio_reduced_dvd {h s h' s' : ℕ} (hs : 0 < s) (he : h' * s = h * s') : s / s.gcd h ∣ s'

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioPartners_card_le {h s : ℕ} (hs : 0 < s) (H S : ℕ) : (secondaryRatioPartners H S h s).card ≤ S / (s / s.gcd h)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioPartners_card_le_twice_gcd {h s B : ℕ} (hB : 0 < B) (hs : B ≤ s) (H : ℕ) : (secondaryRatioPartners H (2 * B) h s).card ≤ 2 * s.gcd h

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_pair_gcd_le_log (H S : ℕ) : ∑ h ∈ Finset.Ioc 0 H, ∑ s ∈ Finset.Ioc 0 S, ↑(s.gcd h) ≤ ↑H * ↑S * (1 + Real.log ↑H)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioPartners_dyadic_sum_le {B : ℕ} (hB : 0 < B) (H : ℕ) : ∑ h ∈ Finset.Ioc 0 H, ∑ s ∈ Finset.Ico B (2 * B), ↑(secondaryRatioPartners H (2 * B) h s).card ≤ 4 * ↑H * ↑B * (1 + Real.log ↑H)

Summing over a dyadic first denominator costs only H*B*log H. The partner box has upper endpoints H,2B; arbitrary subboxes only decrease this nonnegative count. No comparison between H*B and a beta scale is used.