feat(continued_fractions) add equivalence of convergents computations (…

…#2459)

### What
Add lemmas showing that the two methods for computing the convergents of a continued fraction (recurrence relation vs direct evaluation) coincide. A high-level overview on how the proof works is given in the header of the file. 

### Why
One wants to be able to relate both computations. The recurrence relation can be faster to compute, the direct evaluation is more intuitive and might be easier for some proofs.

### How
The proof of the equivalence is by induction. To make the induction work, one needs to "squash" a sequence into a shorter one while maintaining the value of the convergents computations. Most lemmas in this commit deal with this squashing operation.



Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>

docs/references.bib

@@ -138,6 +138,13 @@ @book{wall2018analytic
   publisher={Dover Publications}
 }
 
+@book{hardy2008introduction,
+  title={An Introduction to the Theory of Numbers},
+  author={Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph},
+  year={2008},
+  publisher={Oxford University Press}
+}
+
 @article{ahrens2017,
  author = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
    year = {2019},

src/algebra/continued_fractions/basic.lean

@@ -53,6 +53,7 @@ instance [has_repr α] : has_repr (gcf.pair α) :=
 ⟨λ p, "(a : " ++ (repr p.a) ++ ", b : " ++ (repr p.b) ++ ")"⟩
 
 section coe
+/-! Interlude: define some expected coercions. -/
 /- Fix another type `β` and assume `α` can be converted to `β`. -/
 variables {α} {β : Type*} [has_coe α β]
 
@@ -72,7 +73,7 @@ end generalized_continued_fraction.pair
 A *generalised continued fraction* (gcf) is a potentially infinite expression of the form
 
                                 a₀
-                h + --------------------------
+                h + ---------------------------
                                   a₁
                       b₀ + --------------------
                                     a₂
@@ -116,8 +117,8 @@ by { unfold terminated_at, apply_instance }
 /-- A gcf terminates if its sequence terminates. -/
 def terminates (g : gcf α) : Prop := g.s.terminates
 
-/- Interlude: define some expected coercions. -/
 section coe
+/-! Interlude: define some expected coercions. -/
 -- Fix another type `β` and assume `α` can be converted to `β`.
 variables {β : Type*} [has_coe α β]
 
@@ -143,7 +144,7 @@ A generalized continued fraction is a *simple continued fraction* if all partial
 equal to one.
 
                                 1
-                h + --------------------------
+                h + ---------------------------
                                   1
                       b₀ + --------------------
                                     1
@@ -163,7 +164,7 @@ A *simple continued fraction* (scf) is a generalized continued fraction (gcf) wh
 numerators are equal to one.
 
                                 1
-                h + --------------------------
+                h + ---------------------------
                                   1
                       b₀ + --------------------
                                     1
@@ -260,7 +261,7 @@ namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
 
 -- Fix a division ring for the computations.
-variable [division_ring α]
+variables {K : Type*} [division_ring K]
 
 /-
 We start with the definition of the recurrence relation. Given a gcf `g`, for all `n ≥ 1`, we define
@@ -276,23 +277,23 @@ We start with the definition of the recurrence relation. Given a gcf `g`, for al
 Returns the next numerator `Aₙ = bₙ-₁ * Aₙ₋₁ + aₙ-₁ * Aₙ₋₂`, where `predA` is `Aₙ₋₁`,
 `ppredA` is `Aₙ₋₂`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
-def next_numerator (a b ppredA predA : α) : α := b * predA + a * ppredA
+def next_numerator (a b ppredA predA : K) : K := b * predA + a * ppredA
 
 /--
 Returns the next denominator `Bₙ = bₙ-₁ * Bₙ₋₁ + aₙ-₁ * Bₙ₋₂``, where `predB` is `Bₙ₋₁` and
 `ppredB` is `Bₙ₋₂`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
-def next_denominator (aₙ bₙ ppredB predB : α) : α := bₙ * predB + aₙ * ppredB
+def next_denominator (aₙ bₙ ppredB predB : K) : K := bₙ * predB + aₙ * ppredB
 
 /--
 Returns the next continuants `⟨Aₙ, Bₙ⟩` using `next_numerator` and `next_denominator`, where `pred`
 is `⟨Aₙ₋₁, Bₙ₋₁⟩`, `ppred` is `⟨Aₙ₋₂, Bₙ₋₂⟩`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
-def next_continuants (a b : α) (ppred pred : gcf.pair α) : gcf.pair α :=
+def next_continuants (a b : K) (ppred pred : gcf.pair K) : gcf.pair K :=
 ⟨next_numerator a b ppred.a pred.a, next_denominator a b ppred.b pred.b⟩
 
 /-- Returns the continuants `⟨Aₙ₋₁, Bₙ₋₁⟩` of `g`. -/
-def continuants_aux (g : gcf α) : stream (gcf.pair α)
+def continuants_aux (g : gcf K) : stream (gcf.pair K)
 | 0 := ⟨1, 0⟩
 | 1 := ⟨g.h, 1⟩
 | (n + 2) :=
@@ -302,23 +303,23 @@ def continuants_aux (g : gcf α) : stream (gcf.pair α)
   end
 
 /-- Returns the continuants `⟨Aₙ, Bₙ⟩` of `g`. -/
-def continuants (g : gcf α) : stream (gcf.pair α) := g.continuants_aux.tail
+def continuants (g : gcf K) : stream (gcf.pair K) := g.continuants_aux.tail
 
 /-- Returns the numerators `Aₙ` of `g`. -/
-def numerators (g : gcf α) : stream α := g.continuants.map gcf.pair.a
+def numerators (g : gcf K) : stream K := g.continuants.map gcf.pair.a
 
 /-- Returns the denominators `Bₙ` of `g`. -/
-def denominators (g : gcf α) : stream α := g.continuants.map gcf.pair.b
+def denominators (g : gcf K) : stream K := g.continuants.map gcf.pair.b
 
 /-- Returns the convergents `Aₙ / Bₙ` of `g`, where `Aₙ, Bₙ` are the nth continuants of `g`. -/
-def convergents (g : gcf α) : stream α := λ (n : ℕ), (g.numerators n) / (g.denominators n)
+def convergents (g : gcf K) : stream K := λ (n : ℕ), (g.numerators n) / (g.denominators n)
 
 /--
 Returns the approximation of the fraction described by the given sequence up to a given position n.
 For example, `convergents'_aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4)` and
 `convergents'_aux [(1, 2), (3, 4), (5, 6)] 0 = 0`.
 -/
-def convergents'_aux : seq (gcf.pair α) → ℕ → α
+def convergents'_aux : seq (gcf.pair K) → ℕ → K
 | s 0 := 0
 | s (n + 1) := match s.head with
   | none := 0
@@ -330,7 +331,7 @@ Returns the convergents of `g` by evaluating the fraction described by `g` up to
 position `n`. For example, `convergents' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4)` and
 `convergents' [9; (1, 2), (3, 4), (5, 6)] 0 = 9`
 -/
-def convergents' (g : gcf α) (n : ℕ) : α := g.h + convergents'_aux g.s n
+def convergents' (g : gcf K) (n : ℕ) : K := g.h + convergents'_aux g.s n
 
 end generalized_continued_fraction
 

src/algebra/continued_fractions/continuants_recurrence.lean

@@ -17,22 +17,22 @@ function indeed satisfies the following recurrences:
 
 namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
-variables {α : Type*} {g : gcf α} {n : ℕ} [division_ring α]
+variables {K : Type*} {g : gcf K} {n : ℕ} [division_ring K]
 
-lemma continuants_aux_recurrence {gp ppred pred : gcf.pair α} (nth_s_eq : g.s.nth n = some gp)
+lemma continuants_aux_recurrence {gp ppred pred : gcf.pair K} (nth_s_eq : g.s.nth n = some gp)
   (nth_conts_aux_eq : g.continuants_aux n = ppred)
   (succ_nth_conts_aux_eq : g.continuants_aux (n + 1) = pred) :
   g.continuants_aux (n + 2) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩ :=
 by simp [*, continuants_aux, next_continuants, next_denominator, next_numerator]
 
-lemma continuants_recurrence_aux {gp ppred pred : gcf.pair α} (nth_s_eq : g.s.nth n = some gp)
+lemma continuants_recurrence_aux {gp ppred pred : gcf.pair K} (nth_s_eq : g.s.nth n = some gp)
   (nth_conts_aux_eq : g.continuants_aux n = ppred)
   (succ_nth_conts_aux_eq : g.continuants_aux (n + 1) = pred) :
   g.continuants (n + 1) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩ :=
 by simp [nth_cont_eq_succ_nth_cont_aux,
   (continuants_aux_recurrence nth_s_eq nth_conts_aux_eq succ_nth_conts_aux_eq)]
 
-theorem continuants_recurrence {gp ppred pred : gcf.pair α}
+theorem continuants_recurrence {gp ppred pred : gcf.pair K}
   (succ_nth_s_eq : g.s.nth (n + 1) = some gp)
   (nth_conts_eq : g.continuants n = ppred)
   (succ_nth_conts_eq : g.continuants (n + 1) = pred) :
@@ -42,7 +42,7 @@ begin
   exact (continuants_recurrence_aux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq)
 end
 
-lemma numerators_recurrence {gp : gcf.pair α} {ppredA predA : α}
+lemma numerators_recurrence {gp : gcf.pair K} {ppredA predA : K}
   (succ_nth_s_eq : g.s.nth (n + 1) = some gp)
   (nth_num_eq : g.numerators n = ppredA)
   (succ_nth_num_eq : g.numerators (n + 1) = predA) :
@@ -56,7 +56,7 @@ begin
   rw [num_eq_conts_a, (continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq)]
 end
 
-lemma denominators_recurrence {gp : gcf.pair α} {ppredB predB : α}
+lemma denominators_recurrence {gp : gcf.pair K} {ppredB predB : K}
   (succ_nth_s_eq : g.s.nth (n + 1) = some gp)
   (nth_denom_eq : g.denominators n = ppredB)
   (succ_nth_denom_eq : g.denominators (n + 1) = predB) :