Farey sequences

DefinitionFarey set#✓fully proved

For a natural number \(n\), the Farey set \(F_n\) of order \(n\) is the finite set of rationals \(a/d\) with \(a\) and \(d\) natural numbers, \(1 \le d \le n\) and \(0 \le a \le d\).

Equivalently, \(F_n\) consists of the rationals \(q\) with \(0 \le q \le 1\) whose denominator in lowest terms is at most \(n\). In particular \(F_0\) is empty.

def fareyFinset (n : ℕ) : Finset ℚ :=
  ((Finset.Icc 1 n).biUnion fun d : ℕ =>
    ((Finset.Icc 0 d).image fun a : ℕ => ((a : ℤ) /. (d : ℤ) : ℚ)))

Used by 11

Used byConsecutive Farey fractions have determinant one · Determinant one and large denominator sum give Farey neighbors · Farey sets grow with the order · Farey sequence · Mediants generate the next Farey set · Farey neighbors · Arithmetic characterization of Farey neighbors · Mediants that enter the next Farey set · The mediant of Farey neighbors is not in the Farey set · Membership in the Farey set · Farey neighbors have denominator sum exceeding the order

DefinitionFarey sequence#✓fully proved

For a natural number \(n\), the Farey sequence of order \(n\) is the list of the elements of the Farey set \(F_n\) in increasing order.

def fareySeq (n : ℕ) : List ℚ :=
  (fareyFinset n).sort (· ≤ ·)

Uses 1 · Used by 1

Statement usesFarey set

Used byFranel–Landau theorem

TheoremMembership in the Farey set#✓fully proved

For a natural number \(n\) and a rational number \(q\), \(q\) belongs to the Farey set \(F_n\) of order \(n\) if and only if \(0 \le q \le 1\) and the denominator of \(q\) in lowest terms is at most \(n\).

@[simp] theorem mem_fareyFinset_iff (n : ℕ) (q : ℚ) :
    q ∈ fareyFinset n ↔ 0 ≤ q ∧ q ≤ 1 ∧ q.den ≤ n

Uses 1 · Used by 6

Statement usesFarey set

Used byConsecutive Farey fractions have determinant one · Determinant one and large denominator sum give Farey neighbors · Farey sets grow with the order · Mediants generate the next Farey set · Mediants that enter the next Farey set · Farey neighbors have denominator sum exceeding the order

TheoremFarey sets grow with the order#✓fully proved

If \(m \le n\) are natural numbers, then every element of the Farey set \(F_m\) belongs to \(F_n\), that is, \(F_m \subseteq F_n\).

theorem fareyFinset_mono {m n : ℕ} (hmn : m ≤ n) : fareyFinset m ⊆ fareyFinset n

Uses 2 · Used by 1

Statement usesFarey set

Proof usesMembership in the Farey set

Used byMediants generate the next Farey set

DefinitionFarey neighbors#✓fully proved

For a natural number \(n\), rationals \(x\) and \(y\) are Farey neighbors of order \(n\) when both lie in the Farey set \(F_n\), \(x < y\), and no element \(z\) of \(F_n\) satisfies \(x < z < y\).

def IsFareyNeighbor (n : ℕ) (x y : ℚ) : Prop :=
  x ∈ fareyFinset n ∧ y ∈ fareyFinset n ∧ x < y ∧
  ∀ z ∈ fareyFinset n, ¬(x < z ∧ z < y)

Uses 1 · Used by 7

Statement usesFarey set

Used byConsecutive Farey fractions have determinant one · Determinant one and large denominator sum give Farey neighbors · Mediants generate the next Farey set · Arithmetic characterization of Farey neighbors · Mediants that enter the next Farey set · The mediant of Farey neighbors is not in the Farey set · Farey neighbors have denominator sum exceeding the order

DefinitionMediant#✓fully proved

For rational numbers \(x = a/b\) and \(y = c/d\) written in lowest terms with \(b, d > 0\), the mediant of \(x\) and \(y\) is the rational number \((a + c)/(b + d)\).

def mediant (x y : ℚ) : ℚ :=
  ((x.num + y.num) /. ((x.den + y.den : ℕ) : ℤ) : ℚ)

Used by 4

Used byMediants generate the next Farey set · Mediants that enter the next Farey set · The mediant of Farey neighbors is not in the Farey set · Farey neighbors have denominator sum exceeding the order

LemmaFarey neighbors have denominator sum exceeding the order#✓fully proved

Let \(n\) be a natural number and let \(F_n\) be the Farey set of order \(n\). If \(x < y\) are neighbors in \(F_n\), meaning that \(x, y \in F_n\) and no element of \(F_n\) lies strictly between them, then the denominators \(b\) of \(x\) and \(d\) of \(y\) in lowest terms satisfy \(b + d > n\).

lemma neighbor_den_sum_gt (n : ℕ) (x y : ℚ) (h : IsFareyNeighbor n x y) :
    n < x.den + y.den

Uses 4 · Used by 2

Statement usesFarey neighbors

Proof usesFarey set · Mediant · Membership in the Farey set

Used byMediants generate the next Farey set · Arithmetic characterization of Farey neighbors

TheoremDeterminant one and large denominator sum give Farey neighbors#✓fully proved

Let \(n\) be a natural number and let \(x = a/b\) and \(y = c/d\) be elements of the Farey set \(F_n\), written in lowest terms with \(b, d > 0\). If \(bc = ad + 1\) and \(n < b + d\), then \(x\) and \(y\) are Farey neighbors of order \(n\).

theorem det_one_and_sum_gt_imp_neighbor (n : ℕ) (x y : ℚ)
    (hx : x ∈ fareyFinset n) (hy : y ∈ fareyFinset n)
    (hdet : y.num * (x.den : ℤ) = x.num * (y.den : ℤ) + 1)
    (hsum : n < x.den + y.den) :
    IsFareyNeighbor n x y

Uses 3 · Used by 1

Statement usesFarey neighbors · Farey set

Proof usesMembership in the Farey set

Used byArithmetic characterization of Farey neighbors

TheoremConsecutive Farey fractions have determinant one#✓fully proved

Let \(n\) be a natural number. If \(x\) and \(y\) are Farey neighbors of order \(n\), written in lowest terms as \(x = a/b\) and \(y = c/d\) with \(b, d > 0\), then \(bc = ad + 1\).

theorem IsFareyNeighbor.det_eq_one {n : ℕ} {x y : ℚ}
    (h : IsFareyNeighbor n x y) :
    y.num * (x.den : ℤ) = x.num * (y.den : ℤ) + 1

Uses 3 · Used by 2

Statement usesFarey neighbors

Proof usesFarey set · Membership in the Farey set

Used byMediants generate the next Farey set · Arithmetic characterization of Farey neighbors

TheoremArithmetic characterization of Farey neighbors#✓fully proved

Let \(n\) be a natural number and let \(x = a/b\) and \(y = c/d\) be elements of the Farey set \(F_n\), written in lowest terms with \(b, d > 0\). Then \(x\) and \(y\) are Farey neighbors of order \(n\) if and only if \(bc = ad + 1\) and \(n < b + d\).

theorem isFareyNeighbor_iff_det_and_sum {n : ℕ} {x y : ℚ}
    (hx : x ∈ fareyFinset n) (hy : y ∈ fareyFinset n) :
    IsFareyNeighbor n x y ↔
      y.num * (x.den : ℤ) = x.num * (y.den : ℤ) + 1 ∧ n < x.den + y.den

Uses 5

Statement usesFarey neighbors · Farey set

Proof usesConsecutive Farey fractions have determinant one · Determinant one and large denominator sum give Farey neighbors · Farey neighbors have denominator sum exceeding the order

TheoremThe mediant of Farey neighbors is not in the Farey set#✓fully proved

Let \(n\) be a natural number. If \(x\) and \(y\) are Farey neighbors of order \(n\), then the mediant of \(x\) and \(y\) does not belong to the Farey set \(F_n\).

theorem IsFareyNeighbor.mediant_not_mem {n : ℕ} {x y : ℚ}
    (h : IsFareyNeighbor n x y) : mediant x y ∉ fareyFinset n

Uses 3 · Used by 1

Statement usesFarey neighbors · Farey set · Mediant

Used byMediants that enter the next Farey set

TheoremMediants that enter the next Farey set#✓fully proved

Let \(n\) be a natural number and let \(x\) and \(y\) be Farey neighbors of order \(n\) whose denominators in lowest terms sum to \(n + 1\). Then the mediant of \(x\) and \(y\) belongs to the Farey set \(F_{n+1}\) and does not belong to \(F_n\).

theorem IsFareyNeighbor.mediant_mem_succ {n : ℕ} {x y : ℚ}
    (h : IsFareyNeighbor n x y) (hsum : x.den + y.den = n + 1) :
    mediant x y ∈ fareyFinset (n + 1) ∧ mediant x y ∉ fareyFinset n

Uses 5

Statement usesFarey neighbors · Farey set · Mediant

Proof usesThe mediant of Farey neighbors is not in the Farey set · Membership in the Farey set

TheoremMediants generate the next Farey set#✓fully proved

Let \(n \ge 1\) be a natural number. A rational number \(q\) belongs to the Farey set \(F_{n+1}\) if and only if \(q\) belongs to \(F_n\), or there are Farey neighbors \(x\) and \(y\) of order \(n\) whose denominators in lowest terms sum to \(n + 1\) such that \(q\) is the mediant of \(x\) and \(y\).

theorem farey_succ_generation {n : ℕ} (hn : 0 < n) (q : ℚ) :
    q ∈ fareyFinset (n + 1) ↔
      q ∈ fareyFinset n ∨
        ∃ x y : ℚ, IsFareyNeighbor n x y ∧ x.den + y.den = n + 1 ∧ q = mediant x y

Uses 7

Statement usesFarey neighbors · Farey set · Mediant

Proof usesConsecutive Farey fractions have determinant one · Farey sets grow with the order · Membership in the Farey set · Farey neighbors have denominator sum exceeding the order

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.