Membership in the Farey dissection of order $P$

Proved

Farey.mem_pairs

by dbenbenn · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorycircle-methodfareynumber-theory

A pair $(q,a)$ of natural numbers belongs to the Farey dissection of order $P$ if and only if

1 \le q \le P, \qquad 1 \le a \le q, \qquad \gcd(a,q) = 1.

This unfolds the definition, which is built as an iterated union over denominators, into the flat list of conditions one actually reasons with. It is the workhorse lemma for the dissection: every other statement about Farey pairs is proved by rewriting membership this way.

Preamble

import Definitions.Def_Farey
import Mathlib

Formal statement

namespace Farey

theorem mem_pairs {P : ℕ} {p : ℕ × ℕ} :
    p ∈ pairs P ↔ 1 ≤ p.1 ∧ p.1 ≤ P ∧ 1 ≤ p.2 ∧ p.2 ≤ p.1 ∧ Nat.Coprime p.2 p.1 := by
  sorry

end Farey

Source

Standard Farey-dissection facts. See R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge University Press 1997, Chapter 2; Hardy & Wright, An Introduction to the Theory of Numbers, Chapter III.

View graph

Membership in the Farey dissection of order PPP

Membership in the Farey dissection of order $P$