Fouvry's finite gcd mean

Fouvry (1987), Lemma 2, p. 622. The divisor expansion is finite and uniform in the nonzero integer whose gcd is being averaged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.gcd_le_divisor_sum {a : ℕ} (ha : a ≠ 0) (n : ℕ) : a.gcd n ≤ ∑ d ∈ a.divisors, if d ∣ n then d else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_divisor_majorant (a N : ℕ) : (∑ n ∈ Finset.Ioc 0 N, ∑ d ∈ a.divisors, if d ∣ n then d else 0) = ∑ d ∈ a.divisors, d * (N / d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_gcd_le_divisor_floor {a : ℕ} (ha : a ≠ 0) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, a.gcd n ≤ ∑ d ∈ a.divisors, d * (N / d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_gcd_le {a : ℕ} (ha : a ≠ 0) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, a.gcd n ≤ N * a.divisors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_int_gcd_le (a : ℤ) (ha : a ≠ 0) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, a.gcd ↑n ≤ N * a.natAbs.divisors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_int_gcd_le_real (a : ℤ) (ha : a ≠ 0) {x : ℝ} (hx : 0 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑(a.gcd ↑n) ≤ x * ↑a.natAbs.divisors.card