From 632c4baa435a291283dc44171a3c115f4053a2b9 Mon Sep 17 00:00:00 2001 From: Kevin Kappelmann Date: Sat, 25 Apr 2020 18:43:05 +0000 Subject: [PATCH] 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 --- docs/references.bib | 7 + src/algebra/continued_fractions/basic.lean | 31 +- .../continuants_recurrence.lean | 12 +- .../convergents_equiv.lean | 415 ++++++++++++++++++ src/algebra/continued_fractions/default.lean | 1 + .../terminated_stable.lean | 8 +- .../continued_fractions/translations.lean | 30 +- 7 files changed, 473 insertions(+), 31 deletions(-) create mode 100644 src/algebra/continued_fractions/convergents_equiv.lean diff --git a/docs/references.bib b/docs/references.bib index 182f3d9cac28e..792fb45a19e74 100644 --- a/docs/references.bib +++ b/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}, diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean index 41e8d8fb797db..38d573b2959d8 100644 --- a/src/algebra/continued_fractions/basic.lean +++ b/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 diff --git a/src/algebra/continued_fractions/continuants_recurrence.lean b/src/algebra/continued_fractions/continuants_recurrence.lean index 0ad5fa1c03ce4..68ea94b4deab5 100644 --- a/src/algebra/continued_fractions/continuants_recurrence.lean +++ b/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) : diff --git a/src/algebra/continued_fractions/convergents_equiv.lean b/src/algebra/continued_fractions/convergents_equiv.lean new file mode 100644 index 0000000000000..ca938f44f5a1a --- /dev/null +++ b/src/algebra/continued_fractions/convergents_equiv.lean @@ -0,0 +1,415 @@ +/- +Copyright (c) 2020 Kevin Kappelmann. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Kappelmann +-/ +import algebra.continued_fractions.continuants_recurrence +import algebra.continued_fractions.terminated_stable +import tactic.linarith +/-! +# Equivalence of Recursive and Direct Computations of `gcf` Convergents + +## Summary + +We show the equivalence of two computations of convergents (recurrence relation (`convergents`) vs. +direct evaluation (`convergents'`)) for `gcf`s on linear ordered fields. We follow the proof from +[hardy2008introduction], Chapter 10. Here's a sketch: + +Let `c` be a continued fraction `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`, visually: + a₀ + h + --------------------------- + a₁ + b₀ + -------------------- + a₂ + b₁ + -------------- + a₃ + b₂ + -------- + b₃ + ... + +One can compute the convergents of `c` in two ways: +1. Directly evaluating the fraction described by `c` up to a given `n` (`convergents'`) +2. Using the recurrence (`convergents`) + `A₋₁ = 1, A₀ = h, Aₙ = bₙ-₁ * Aₙ₋₁ + aₙ-₁ * Aₙ₋₂`, and + `B₋₁ = 0, B₀ = 1, Bₙ = bₙ-₁ * Bₙ₋₁ + aₙ-₁ * Bₙ₋₂`. + +To show the equivalence of the computations in the main theorem of this file +`convergents_eq_convergents'`, we proceed by induction. The case `n = 0` is trivial. + +For `n + 1`, we first "squash" the `n + 1`th position of `c` into the `n`th position to obtain +another continued fraction + `c' := [h; (a₀, b₀),..., (aₙ-₁, bₙ-₁), (aₙ, bₙ + aₙ₊₁ / bₙ₊₁), (aₙ₊₁, bₙ₊₁),...]`. +This squashing process is formalised in section `squash`. Note that directly evaluating `c` up to +position `n + 1` is equal to evaluating `c'` up to `n`. This is shown in lemma +`succ_nth_convergent'_eq_squash_gcf_nth_convergent'`. + +By the inductive hypothesis, the two computations for the `n`th convergent of `c` coincide. +So all that is left to show is that the recurrence relation for `c` at `n + 1` and and `c'` at +`n` coincide. This can be shown by another induction. +The corresponding lemma in this file is `succ_nth_convergent_eq_squash_gcf_nth_convergent`. + +## Main Theorems + +- `generalized_continued_fraction.convergents_eq_convergents'` shows the equivalence under a strict +positivity restriction on the sequence. +- `continued_fractions.convergents_eq_convergents'` shows the equivalence for (regular) continued +fractions. + +## References + +- https://en.wikipedia.org/wiki/Generalized_continued_fraction +- [*Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph*][hardy2008introduction] + +## Tags + +fractions, recurrence, equivalence +-/ + +variables {K : Type*} {n : ℕ} +namespace generalized_continued_fraction +open generalized_continued_fraction as gcf +variables {g : gcf K} {s : seq $ gcf.pair K} + +section squash +/-! +We will show the equivalence of the computations by induction. To make the induction work, we need +to be able to *squash* the nth and (n + 1)th value of a sequence. This squashing itself and the +lemmas about it are not very interesting. As a reader, you hence might want to skip this section. +-/ + +section with_division_ring +variable [division_ring K] + +/-- +Given a sequence of gcf.pairs `s = [(a₀, bₒ), (a₁, b₁), ...]`, `squash_seq s n` +combines `⟨aₙ, bₙ⟩` and `⟨aₙ₊₁, bₙ₊₁⟩` at position `n` to `⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩`. For example, +`squash_seq s 0 = [(a₀, bₒ + a₁ / b₁), (a₁, b₁),...]`. +If `s.terminated_at (n + 1)`, then `squash_seq s n = s`. +-/ +def squash_seq (s : seq $ gcf.pair K) (n : ℕ) : seq (gcf.pair K) := +match prod.mk (s.nth n) (s.nth (n + 1)) with +| ⟨some gp_n, some gp_succ_n⟩ := seq.nats.zip_with + -- return the squashed value at position `n`; otherwise, do nothing. + (λ n' gp, if n' = n then ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ else gp) s +| _ := s +end + +/-! We now prove some simple lemmas about the squashed sequence -/ + +/-- If the sequence already terminated at position `n + 1`, nothing gets squashed. -/ +lemma squash_seq_eq_self_of_terminated (terminated_at_succ_n : s.terminated_at (n + 1)) : + squash_seq s n = s := +begin + change s.nth (n + 1) = none at terminated_at_succ_n, + cases s_nth_eq : (s.nth n); + simp only [*, squash_seq] +end + +/-- If the sequence has not terminated before position `n + 1`, the value at `n + 1` gets +squashed into position `n`. -/ +lemma squash_seq_nth_of_not_terminated {gp_n gp_succ_n : gcf.pair K} + (s_nth_eq : s.nth n = some gp_n) (s_succ_nth_eq : s.nth (n + 1) = some gp_succ_n) : + (squash_seq s n).nth n = some ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ := +by simp [*, squash_seq, (seq.zip_with_nth_some (seq.nats_nth n) s_nth_eq _)] + +/-- The values before the squashed position stay the same. -/ +lemma squash_seq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squash_seq s n).nth m = s.nth m := +begin + cases s_succ_nth_eq : s.nth (n + 1), + case option.none { rw (squash_seq_eq_self_of_terminated s_succ_nth_eq) }, + case option.some + { obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.nth n = some gp_n, from + s.ge_stable n.le_succ s_succ_nth_eq, + obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.nth m = some gp_m, from + s.ge_stable (le_of_lt m_lt_n) s_nth_eq, + simp [*, squash_seq, (seq.zip_with_nth_some (seq.nats_nth m) s_mth_eq _), + (ne_of_lt m_lt_n)] } +end + +/-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the +sequence at position `n`. -/ +lemma squash_seq_succ_n_tail_eq_squash_seq_tail_n : + (squash_seq s (n + 1)).tail = squash_seq s.tail n := +begin + cases s_succ_succ_nth_eq : s.nth (n + 2) with gp_succ_succ_n, + case option.none + { have : squash_seq s (n + 1) = s, from squash_seq_eq_self_of_terminated s_succ_succ_nth_eq, + cases s_succ_nth_eq : (s.nth (n + 1)); + simp only [squash_seq, seq.nth_tail, s_succ_nth_eq, s_succ_succ_nth_eq] }, + case option.some + { obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.nth (n + 1) = some gp_succ_n, from + s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq, + -- apply extensionality with `m` and continue by cases `m = n`. + ext m, + cases decidable.em (m = n) with m_eq_n m_ne_n, + { have : s.tail.nth n = some gp_succ_n, from (s.nth_tail n).trans s_succ_nth_eq, + simp [*, squash_seq, seq.nth_tail, (seq.zip_with_nth_some (seq.nats_nth n) this), + (seq.zip_with_nth_some (seq.nats_nth (n + 1)) s_succ_nth_eq)] }, + { have : s.tail.nth m = s.nth (m + 1), from s.nth_tail m, + cases s_succ_mth_eq : s.nth (m + 1), + all_goals { have s_tail_mth_eq, from this.trans s_succ_mth_eq }, + { simp only [*, squash_seq, seq.nth_tail, (seq.zip_with_nth_none' s_succ_mth_eq), + (seq.zip_with_nth_none' s_tail_mth_eq)] }, + { simp [*, squash_seq, seq.nth_tail, + (seq.zip_with_nth_some (seq.nats_nth (m + 1)) s_succ_mth_eq), + (seq.zip_with_nth_some (seq.nats_nth m) s_tail_mth_eq)] } } } +end + +/-- The auxiliary function `convergents'_aux` returns the same value for a sequence and the +corresponding squashed sequence at the squashed position. -/ +lemma succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squash_seq : + convergents'_aux s (n + 2) = convergents'_aux (squash_seq s n) (n + 1) := +begin + cases s_succ_nth_eq : (s.nth $ n + 1) with gp_succ_n, + case option.none + { rw [(squash_seq_eq_self_of_terminated s_succ_nth_eq), + (convergents'_aux_stable_step_of_terminated s_succ_nth_eq)] }, + case option.some + { induction n with m IH generalizing s gp_succ_n, + case nat.zero + { obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head, from + s.ge_stable zero_le_one s_succ_nth_eq, + have : (squash_seq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩, + from squash_seq_nth_of_not_terminated s_head_eq s_succ_nth_eq, + simp [*, convergents'_aux, seq.head, seq.nth_tail] }, + case nat.succ + { obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head, from + s.ge_stable (m + 2).zero_le s_succ_nth_eq, + suffices : gp_head.a / (gp_head.b + convergents'_aux s.tail (m + 2)) + = convergents'_aux (squash_seq s (m + 1)) (m + 2), by + simpa only [convergents'_aux, s_head_eq], + have : convergents'_aux s.tail (m + 2) = convergents'_aux (squash_seq s.tail m) (m + 1),by + { have : s.tail.nth (m + 1) = some gp_succ_n, by simpa [seq.nth_tail] using s_succ_nth_eq, + exact (IH _ this) }, + have : (squash_seq s (m + 1)).head = some gp_head, from + (squash_seq_nth_of_lt m.succ_pos).trans s_head_eq, + simp only [*, convergents'_aux, squash_seq_succ_n_tail_eq_squash_seq_tail_n] } } +end + +/-! Let us now lift the squashing operation to gcfs. -/ + +/-- +Given a gcf `g = [h; (a₀, bₒ), (a₁, b₁), ...]`, we have +- `squash_nth.gcf g 0 = [h + a₀ / b₀); (a₀, bₒ), ...]`, +- `squash_nth.gcf g (n + 1) = ⟨g.h, squash_seq g.s n⟩` +-/ +def squash_gcf (g : gcf K) : ℕ → gcf K +| 0 := match g.s.nth 0 with + | none := g + | some gp := ⟨g.h + gp.a / gp.b, g.s⟩ + end +| (n + 1) := ⟨g.h, squash_seq g.s n⟩ + +/-! Again, we derive some simple lemmas that are not really of interest. This time for the +squashed gcf. -/ + +/-- If the gcf already terminated at position `n`, nothing gets squashed. -/ +lemma squash_gcf_eq_self_of_terminated (terminated_at_n : terminated_at g n) : + squash_gcf g n = g := +begin + cases n, + case nat.zero + { change g.s.nth 0 = none at terminated_at_n, + simp only [convergents', squash_gcf, convergents'_aux, terminated_at_n] }, + case nat.succ + { cases g, simp [(squash_seq_eq_self_of_terminated terminated_at_n), squash_gcf] } +end + +/-- The values before the squashed position stay the same. -/ +lemma squash_gcf_nth_of_lt {m : ℕ} (m_lt_n : m < n) : + (squash_gcf g (n + 1)).s.nth m = g.s.nth m := +by simp only [squash_gcf, (squash_seq_nth_of_lt m_lt_n)] + +/-- `convergents'` returns the same value for a gcf and the corresponding squashed gcf at the +squashed position. -/ +lemma succ_nth_convergent'_eq_squash_gcf_nth_convergent' : + g.convergents' (n + 1) = (squash_gcf g n).convergents' n := +begin + cases n, + case nat.zero + { cases g_s_head_eq : (g.s.nth 0); + simp [g_s_head_eq, squash_gcf, convergents', convergents'_aux, seq.head] }, + case nat.succ + { simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squash_seq, + convergents', squash_gcf] } +end + +/-- The auxiliary continuants before the squashed position stay the same. -/ +lemma continuants_aux_eq_continuants_aux_squash_gcf_of_le {m : ℕ} : + m ≤ n → continuants_aux g m = (squash_gcf g n).continuants_aux m := +nat.strong_induction_on m +(begin + clear m, + assume m IH m_le_n, + cases m with m', + { refl }, + { cases n with n', + { have : false, from m'.not_succ_le_zero m_le_n, contradiction }, -- 1 ≰ 0 + { cases m' with m'', + { refl }, + { -- get some inequalities to instantiate the IH for m'' and m'' + 1 + have m'_lt_n : m'' + 1 < n' + 1, from m_le_n, + have : m'' + 1 < m'' + 2, by linarith, + have succ_m''th_conts_aux_eq := IH (m'' + 1) this (le_of_lt m'_lt_n), + have : m'' < m'' + 2, by linarith, + have m''th_conts_aux_eq := IH m'' this (le_of_lt $ lt_of_lt_of_le (by linarith) n'.le_succ), + have : (squash_gcf g (n' + 1)).s.nth m'' = g.s.nth m'', from + squash_gcf_nth_of_lt (by linarith), + simp [continuants_aux, succ_m''th_conts_aux_eq, m''th_conts_aux_eq, this] } } } +end) + +end with_division_ring + +/-- The convergents coincide in the expected way at the squashed position if the partial denominator +at the squashed position is not zero. -/ +lemma succ_nth_convergent_eq_squash_gcf_nth_convergent [field K] + (nth_part_denom_ne_zero : ∀ {b : K}, g.partial_denominators.nth n = some b → b ≠ 0) : + g.convergents (n + 1) = (squash_gcf g n).convergents n := +begin + cases decidable.em (g.terminated_at n) with terminated_at_n not_terminated_at_n, + { have : squash_gcf g n = g, from squash_gcf_eq_self_of_terminated terminated_at_n, + simp only [this, (convergents_stable_of_terminated n.le_succ terminated_at_n)] }, + { obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.nth n = some gp_n, from + with_one.ne_one_iff_exists.elim_left not_terminated_at_n, + have b_ne_zero : b ≠ 0, from nth_part_denom_ne_zero (part_denom_eq_s_b s_nth_eq), + cases n with n', + case nat.zero + { suffices : (b * g.h + a) / b = g.h + a / b, by + simpa [squash_gcf, s_nth_eq, convergent_eq_conts_a_div_conts_b, + (continuants_recurrence_aux s_nth_eq zeroth_continuant_aux_eq_one_zero + first_continuant_aux_eq_h_one)], + calc + (b * g.h + a) / b = b * g.h / b + a / b : by ring -- requires `field` rather than `division_ring` + ... = g.h + a / b : by rw (mul_div_cancel_left _ b_ne_zero) }, + case nat.succ + { obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.nth n' = some gp_n', from + g.s.ge_stable n'.le_succ s_nth_eq, + -- Notations + let g' := squash_gcf g (n' + 1), + set predConts := g.continuants_aux (n' + 1) with succ_n'th_conts_aux_eq, + set ppredConts := g.continuants_aux n' with n'th_conts_aux_eq, + let pA := predConts.a, let pB := predConts.b, let ppA := ppredConts.a, let ppB := ppredConts.b, + set predConts' := g'.continuants_aux (n' + 1) with succ_n'th_conts_aux_eq', + set ppredConts' := g'.continuants_aux n' with n'th_conts_aux_eq', + let pA' := predConts'.a, let pB' := predConts'.b, let ppA' := ppredConts'.a, + let ppB' := ppredConts'.b, + -- first compute the convergent of the squashed gcf + have : g'.convergents (n' + 1) + = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB'), by + { have : g'.s.nth n' = some ⟨pa, pb + a / b⟩, by + simpa only [squash_nth_gcf] using + (squash_seq_nth_of_not_terminated s_n'th_eq s_nth_eq), + rw [convergent_eq_conts_a_div_conts_b, + (continuants_recurrence_aux this n'th_conts_aux_eq'.symm succ_n'th_conts_aux_eq'.symm)], }, + rw this, + -- then compute the convergent of the original gcf by recursively unfolding the continuants + -- computation twice + have : g.convergents (n' + 2) + = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB), by + { -- use the recurrence once + have : g.continuants_aux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩, from + continuants_aux_recurrence s_n'th_eq n'th_conts_aux_eq.symm succ_n'th_conts_aux_eq.symm, + -- and a second time + rw [convergent_eq_conts_a_div_conts_b, + (continuants_recurrence_aux s_nth_eq succ_n'th_conts_aux_eq.symm this)] }, + rw this, + suffices : ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) + = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) * b/b, by + { obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB, by + simp [*, (continuants_aux_eq_continuants_aux_squash_gcf_of_le $ le_refl $ n' + 1).symm, + (continuants_aux_eq_continuants_aux_squash_gcf_of_le n'.le_succ).symm], + symmetry, + simpa only [eq1, eq2, eq3, eq4, mul_div_cancel'' _ b_ne_zero] }, + field_simp [b_ne_zero], + congr' 1; + ring } } +end + +end squash + +/-- Shows that the recurrence relation (`convergents`) and direct evaluation (`convergents'`) of the +gcf coincide at position `n` if the sequence of fractions contains strictly positive values only. +Requiring positivity of all values is just one possible condition to obtain this result. +For example, the dual - sequences with strictly negative values only - would also work. + +In practice, one most commonly deals with (regular) continued fractions, which satisfy the +positivity criterion required here. The analogous result for them +(see `continued_fractions.convergents_eq_convergents`) hence follows directly from this theorem. +-/ +theorem convergents_eq_convergents' [linear_ordered_field K] + (s_pos : ∀ {gp : gcf.pair K} {m : ℕ}, m < n → g.s.nth m = some gp → 0 < gp.a ∧ 0 < gp.b) : + g.convergents n = g.convergents' n := +begin + induction n with n IH generalizing g, + case nat.zero { simp }, + case nat.succ + { let g' := squash_gcf g n, -- first replace the rhs with the squashed computation + suffices : g.convergents (n + 1) = g'.convergents' n, by + rwa [succ_nth_convergent'_eq_squash_gcf_nth_convergent'], + cases decidable.em (terminated_at g n) with terminated_at_n not_terminated_at_n, + { have g'_eq_g : g' = g, from squash_gcf_eq_self_of_terminated terminated_at_n, + have : ∀ ⦃gp m⦄, m < n → g.s.nth m = some gp → 0 < gp.a ∧ 0 < gp.b, by + { assume _ _ m_lt_n s_mth_eq, exact (s_pos (nat.lt.step m_lt_n) s_mth_eq) }, + rw [(convergents_stable_of_terminated n.le_succ terminated_at_n), g'_eq_g, (IH this)] }, + { suffices : g.convergents (n + 1) = g'.convergents n, by -- invoke the IH for the squashed gcf + { have : ∀ ⦃gp' m⦄, m < n → g'.s.nth m = some gp' → 0 < gp'.a ∧ 0 < gp'.b, by + { assume gp' m m_lt_n s_mth_eq', + -- case distinction on m + 1 = n or m + 1 < n + cases m_lt_n with n succ_m_lt_n, + { -- the difficult case at the squashed position: we first obtain the values from + -- the sequence + obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.nth (m + 1) = some gp_succ_m, from + with_one.ne_one_iff_exists.elim_left not_terminated_at_n, + obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.nth m = some gp_m, from + g.s.ge_stable m.le_succ s_succ_mth_eq, + -- we then plug them into the recurrence + suffices : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b, by { + have : g'.s.nth m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩, from + squash_seq_nth_of_not_terminated mth_s_eq s_succ_mth_eq, + have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩, by cc, + rwa this }, + split, + { exact (s_pos (nat.lt.step m_lt_n) mth_s_eq).left }, + { have : 0 < gp_m.b, from (s_pos (nat.lt.step m_lt_n) mth_s_eq).right, + have : 0 < gp_succ_m.a / gp_succ_m.b, by + { have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b, from + s_pos (lt_add_one $ m + 1) s_succ_mth_eq, + exact (div_pos this.left this.right) }, + linarith } }, + { -- the easy case: before the squashed position, nothing changes + have : g.s.nth m = some gp', by { + have : g'.s.nth m = g.s.nth m, from squash_gcf_nth_of_lt succ_m_lt_n, + rwa this at s_mth_eq' }, + exact s_pos (nat.lt.step $ nat.lt.step succ_m_lt_n) this } }, + rwa [(IH this).symm] }, + -- now the result follows from the fact that the convergents coincide at the squashed position + -- as established in `succ_nth_convergent_eq_squash_gcf_nth_convergent`. + have : ∀ ⦃b⦄, g.partial_denominators.nth n = some b → b ≠ 0, by + { assume b nth_part_denom_eq, + obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.nth n = some gp ∧ gp.b = b, from + obtain_s_b_of_part_denom nth_part_denom_eq, + exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm }, + exact succ_nth_convergent_eq_squash_gcf_nth_convergent this } } +end + +end generalized_continued_fraction + +namespace continued_fraction +open generalized_continued_fraction as gcf +open simple_continued_fraction as scf +open continued_fraction as cf + +/-- Shows that the recurrence relation (`convergents`) and direct evaluation (`convergents'`) of a +(regular) continued fraction coincide. -/ +theorem convergents_eq_convergents' [linear_ordered_field K] {c : cf K} : + (↑c : gcf K).convergents = (↑c : gcf K).convergents' := +begin + ext n, + apply gcf.convergents_eq_convergents', + assume gp m m_lt_n s_nth_eq, + split, + { have : gp.a = 1, from (c : scf K).property m gp.a (gcf.part_num_eq_s_a s_nth_eq), + simp only [zero_lt_one, this] }, + { exact (c.property m gp.b $ gcf.part_denom_eq_s_b s_nth_eq) } +end + +end continued_fraction diff --git a/src/algebra/continued_fractions/default.lean b/src/algebra/continued_fractions/default.lean index f12d9dc53c971..fc9fd8b946a80 100644 --- a/src/algebra/continued_fractions/default.lean +++ b/src/algebra/continued_fractions/default.lean @@ -5,6 +5,7 @@ Authors: Kevin Kappelmann -/ import algebra.continued_fractions.continuants_recurrence import algebra.continued_fractions.terminated_stable +import algebra.continued_fractions.convergents_equiv /-! # Default Exports for Continued Fractions -/ diff --git a/src/algebra/continued_fractions/terminated_stable.lean b/src/algebra/continued_fractions/terminated_stable.lean index 25def8a55ea4c..08c9cccfcc795 100644 --- a/src/algebra/continued_fractions/terminated_stable.lean +++ b/src/algebra/continued_fractions/terminated_stable.lean @@ -14,14 +14,14 @@ We show that the continuants and convergents of a gcf stabilise once the gcf ter namespace generalized_continued_fraction open generalized_continued_fraction as gcf -variables {α : Type*} {g : gcf α} {n m : ℕ} +variables {K : Type*} {g : gcf K} {n m : ℕ} /-- If a gcf terminated at position `n`, it also terminated at `m ≥ n`.-/ lemma terminated_stable (n_le_m : n ≤ m) (terminated_at_n : g.terminated_at n) : g.terminated_at m := g.s.terminated_stable n_le_m terminated_at_n -variable [division_ring α] +variable [division_ring K] lemma continuants_aux_stable_step_of_terminated (terminated_at_n : g.terminated_at n) : g.continuants_aux (n + 2) = g.continuants_aux (n + 1) := @@ -45,7 +45,7 @@ begin exact (eq.trans this IH) } end -lemma convergents'_aux_stable_step_of_terminated {s : seq $ gcf.pair α} +lemma convergents'_aux_stable_step_of_terminated {s : seq $ gcf.pair K} (terminated_at_n : s.terminated_at n) : convergents'_aux s (n + 1) = convergents'_aux s n := begin @@ -61,7 +61,7 @@ begin simp only [convergents'_aux, s_head_eq, (IH this)] }} end -lemma convergents'_aux_stable_of_terminated {s : seq $ gcf.pair α} (n_le_m : n ≤ m) +lemma convergents'_aux_stable_of_terminated {s : seq $ gcf.pair K} (n_le_m : n ≤ m) (terminated_at_n : s.terminated_at n) : convergents'_aux s m = convergents'_aux s n := begin diff --git a/src/algebra/continued_fractions/translations.lean b/src/algebra/continued_fractions/translations.lean index bbf979f30a85a..111307de560ef 100644 --- a/src/algebra/continued_fractions/translations.lean +++ b/src/algebra/continued_fractions/translations.lean @@ -5,16 +5,25 @@ Authors: Kevin Kappelmann -/ import algebra.continued_fractions.basic /-! -# Translation Lemmas Between Functions Defined for Continued Fractions +# Basic Translation Lemmas Between Functions Defined for Continued Fractions ## Summary -Some simple translation lemmas between the different functions defined in +Some simple translation lemmas between the different definitions of functions defined in `algebra.continued_fractions.basic`. -/ namespace generalized_continued_fraction open generalized_continued_fraction as gcf + +section general +/-! +### Translations Between General Access Functions + +Here we give some basic translations that hold by definition between the various methods that allow +us to access the numerators and denominators of a continued fraction. +-/ + variables {α : Type*} {g : gcf α} {n : ℕ} lemma terminated_at_iff_s_terminated_at : g.terminated_at n ↔ g.s.terminated_at n := by refl @@ -49,8 +58,17 @@ lemma obtain_s_b_of_part_denom {b : α} (nth_part_denom_eq : g.partial_denominat ∃ gp, g.s.nth n = some gp ∧ gp.b = b := by simpa [partial_denominators, seq.map_nth] using nth_part_denom_eq +end general + section with_division_ring -variable [division_ring α] +/-! +### Translations Between Computational Functions + +Here we give some basic translations that hold by definition for the computational methods of a +continued fraction. +-/ + +variables {K : Type*} {g : gcf K} {n : ℕ} [division_ring K] lemma nth_cont_eq_succ_nth_cont_aux : g.continuants n = g.continuants_aux (n + 1) := rfl lemma num_eq_conts_a : g.numerators n = (g.continuants n).a := rfl @@ -59,11 +77,11 @@ lemma convergent_eq_num_div_denom : g.convergents n = g.numerators n / g.denomin lemma convergent_eq_conts_a_div_conts_b : g.convergents n = (g.continuants n).a / (g.continuants n).b := rfl -lemma obtain_conts_a_of_num {A : α} (nth_num_eq : g.numerators n = A) : +lemma obtain_conts_a_of_num {A : K} (nth_num_eq : g.numerators n = A) : ∃ conts, g.continuants n = conts ∧ conts.a = A := by simpa -lemma obtain_conts_b_of_denom {B : α} (nth_denom_eq : g.denominators n = B) : +lemma obtain_conts_b_of_denom {B : K} (nth_denom_eq : g.denominators n = B) : ∃ conts, g.continuants n = conts ∧ conts.b = B := by simpa @@ -77,7 +95,7 @@ lemma zeroth_continuant_eq_h_one : g.continuants 0 = ⟨g.h, 1⟩ := rfl lemma zeroth_convergent_eq_h : g.convergents 0 = g.h := by simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one] @[simp] -lemma zeroth_convergent'_aux_eq_zero {s : seq $ gcf.pair α} : convergents'_aux s 0 = 0 := rfl +lemma zeroth_convergent'_aux_eq_zero {s : seq $ gcf.pair K} : convergents'_aux s 0 = 0 := rfl @[simp] lemma zeroth_convergent'_eq_h : g.convergents' 0 = g.h := by simp [convergents']