theorem
FareySeparation.farey_separation
(a₁ a₂ : ℤ)
(p₁ p₂ M : ℕ)
(hp₁ : Nat.Prime p₁)
(hp₂ : Nat.Prime p₂)
(hp₁M : p₁ ≤ M)
(hp₂M : p₂ ≤ M)
(hne : ↑a₁ / ↑p₁ ≠ ↑a₂ / ↑p₂)
:
Farey separation lemma: if a₁/p₁ and a₂/p₂ are distinct rationals with prime
denominators p₁, p₂ ≤ M, then
$$\left|\frac{a_1}{p_1} - \frac{a_2}{p_2}\right| \;\ge\; \frac{1}{M^2}.$$
Proven by clearing denominators: |a₁ p₂ - a₂ p₁| ≥ 1 is an integer, and
p₁ p₂ ≤ M². This is the key separation property used in the proof of Linnik's
large sieve inequality.