feat(algebra/continued_fractions): add convergence theorem (#6607)

1. Add convergence theorem for continued fractions, i.e. `(gcf.of v).convergents` converges to `v`. 
2. Add some simple corollaries following from the already existing approximation lemmas for continued fractions, e.g. the equivalence of the convergent computations for continued fractions computed by `gcf.of` (`(gcf.of v).convergents` and `(gcf.of v).convergents'`).

Author: kappelmann

src/algebra/continued_fractions/basic.lean

@@ -210,7 +210,7 @@ end simple_continued_fraction
 A simple continued fraction is a *(regular) continued fraction* ((r)cf) if all partial denominators
 `bᵢ` are positive, i.e. `0 < bᵢ`.
 -/
-def simple_continued_fraction.is_regular_continued_fraction [has_one α] [has_zero α] [has_lt α]
+def simple_continued_fraction.is_continued_fraction [has_one α] [has_zero α] [has_lt α]
   (s : simple_continued_fraction α) : Prop :=
 ∀ (n : ℕ) (bₙ : α),
   (↑s : generalized_continued_fraction α).partial_denominators.nth n = some bₙ → 0 < bₙ
@@ -220,10 +220,10 @@ variable (α)
 /--
 A *(regular) continued fraction* ((r)cf) is a simple continued fraction (scf) whose partial
 denominators are all positive. It is the subtype of scfs that satisfy
-`simple_continued_fraction.is_regular_continued_fraction`.
+`simple_continued_fraction.is_continued_fraction`.
  -/
 def continued_fraction [has_one α] [has_zero α] [has_lt α] :=
-{s : simple_continued_fraction α // s.is_regular_continued_fraction}
+{s : simple_continued_fraction α // s.is_continued_fraction}
 
 variable {α}
 

src/algebra/continued_fractions/computation/approximation_corollaries.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2021 Kevin Kappelmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Kappelmann
+-/
+import algebra.continued_fractions.computation.approximations
+import algebra.continued_fractions.convergents_equiv
+import topology.instances.ennreal
+/-!
+# Corollaries From Approximation Lemmas (`algebra.continued_fractions.computation.approximations`)
+
+## Summary
+
+We show that the generalized_continued_fraction given by `generalized_continued_fraction.of` in fact
+is a (regular) continued fraction. Using the equivalence of the convergents computations
+(`generalized_continued_fraction.convergents` and `generalized_continued_fraction.convergents'`) for
+continued fractions (see `algebra.continued_fractions.convergents_equiv`), it follows that the
+convergents computations for `generalized_continued_fraction.of` are equivalent.
+
+Moreover, we show the convergence of the continued fractions computations, that is
+`(generalized_continued_fraction.of v).convergents` indeed computes `v` in the limit.
+
+## Main Definitions
+
+- `continued_fraction.of` returns the (regular) continued fraction of a value.
+
+## Main Theorems
+
+- `generalized_continued_fraction.of_convergents_eq_convergents'` shows that the convergents
+  computations for `generalized_continued_fraction.of` are equivalent.
+- `generalized_continued_fraction.of_convergence` shows that
+  `(generalized_continued_fraction.of v).convergents` converges to `v`.
+
+## Tags
+
+convergence, fractions
+-/
+
+variables {K : Type*} (v : K) [linear_ordered_field K] [floor_ring K]
+open generalized_continued_fraction as gcf
+
+lemma generalized_continued_fraction.of_is_simple_continued_fraction :
+  (gcf.of v).is_simple_continued_fraction :=
+(λ _ _ nth_part_num_eq, gcf.of_part_num_eq_one nth_part_num_eq)
+
+/-- Creates the simple continued fraction of a value. -/
+def simple_continued_fraction.of : simple_continued_fraction K :=
+⟨gcf.of v, generalized_continued_fraction.of_is_simple_continued_fraction v⟩
+
+lemma simple_continued_fraction.of_is_continued_fraction :
+  (simple_continued_fraction.of v).is_continued_fraction :=
+(λ _ denom nth_part_denom_eq,
+  lt_of_lt_of_le zero_lt_one(gcf.of_one_le_nth_part_denom nth_part_denom_eq))
+
+/-- Creates the continued fraction of a value. -/
+def continued_fraction.of : continued_fraction K :=
+⟨simple_continued_fraction.of v, simple_continued_fraction.of_is_continued_fraction v⟩
+
+namespace generalized_continued_fraction
+
+open continued_fraction as cf
+
+lemma of_convergents_eq_convergents' : (gcf.of v).convergents = (gcf.of v).convergents' :=
+@cf.convergents_eq_convergents'  _ _ (continued_fraction.of v)
+
+section convergence
+/-!
+### Convergence
+
+We next show that `(generalized_continued_fraction.of v).convergents v` converges to `v`.
+-/
+
+variable [archimedean K]
+local notation `|` x `|` := abs x
+open nat
+
+theorem of_convergence_epsilon :
+  ∀ (ε > (0 : K)), ∃ (N : ℕ), ∀ (n ≥ N), |v - (gcf.of v).convergents n| < ε :=
+begin
+  assume ε ε_pos,
+  -- use the archemidean property to obtian a suitable N
+  rcases (exists_nat_gt (1 / ε) : ∃ (N' : ℕ), 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩,
+  let N := max N' 5, -- set minimum to 5 to have N ≤ fib N work
+  existsi N,
+  assume n n_ge_N,
+  let g := gcf.of v,
+  cases decidable.em (g.terminated_at n) with terminated_at_n not_terminated_at_n,
+  { have : v = g.convergents n, from of_correctness_of_terminated_at terminated_at_n,
+    have : v - g.convergents n = 0, from sub_eq_zero.elim_right this,
+    rw [this],
+    exact_mod_cast ε_pos },
+  { let B := g.denominators n,
+    let nB := g.denominators (n + 1),
+    have abs_v_sub_conv_le : |v - g.convergents n| ≤ 1 / (B * nB), from
+      abs_sub_convergents_le not_terminated_at_n,
+    suffices : 1 / (B * nB) < ε, from lt_of_le_of_lt abs_v_sub_conv_le this,
+    -- show that `0 < (B * nB)` and then multiply by `B * nB` to get rid of the division
+    have nB_ineq : (fib (n + 2) : K) ≤ nB, by
+    { have : ¬g.terminated_at (n + 1 - 1), from not_terminated_at_n,
+      exact (succ_nth_fib_le_of_nth_denom (or.inr this)) },
+    have B_ineq : (fib (n + 1) : K) ≤ B, by
+    { have : ¬g.terminated_at (n - 1), from mt (terminated_stable n.pred_le) not_terminated_at_n,
+      exact (succ_nth_fib_le_of_nth_denom (or.inr this)) },
+    have zero_lt_B : 0 < B, by
+    { have : (0 : K) < fib (n + 1), by exact_mod_cast fib_pos n.zero_lt_succ,
+      exact (lt_of_lt_of_le this B_ineq) },
+    have zero_lt_mul_conts : 0 < B * nB, by
+    { have : 0 < nB, by
+      { have : (0 : K) < fib (n + 2), by exact_mod_cast fib_pos (n + 1).zero_lt_succ,
+        exact (lt_of_lt_of_le this nB_ineq) },
+      solve_by_elim [mul_pos] },
+    suffices : 1 < ε * (B * nB), from (div_lt_iff zero_lt_mul_conts).elim_right this,
+    -- use that `N ≥ n` was obtained from the archimedian property to show the following
+    have one_lt_ε_mul_N : 1 < ε * n, by
+    { have one_lt_ε_mul_N' : 1 < ε * (N' : K), from (div_lt_iff' ε_pos).elim_left one_div_ε_lt_N',
+      have : (N' : K) ≤ N, by exact_mod_cast (le_max_left  _ _),
+      have : ε * N' ≤ ε * n, from
+        (mul_le_mul_left ε_pos).elim_right (le_trans this (by exact_mod_cast n_ge_N)),
+      exact (lt_of_lt_of_le one_lt_ε_mul_N' this) },
+    suffices : ε * n ≤ ε * (B * nB), from lt_of_lt_of_le one_lt_ε_mul_N this,
+    -- cancel `ε`
+    suffices : (n : K) ≤ B * nB, from (mul_le_mul_left ε_pos).elim_right this,
+    show (n : K) ≤ B * nB,
+      calc (n : K)
+          ≤ fib n                     : by exact_mod_cast (le_fib_self $ le_trans
+                                           (le_max_right N' 5) n_ge_N)
+      ... ≤ fib (n + 1)               : by exact_mod_cast fib_le_fib_succ
+      ... ≤ fib (n + 1) * fib (n + 1) : by exact_mod_cast ((fib (n + 1)).le_mul_self)
+      ... ≤ fib (n + 1) * fib (n + 2) : mul_le_mul_of_nonneg_left
+                                          (by exact_mod_cast fib_le_fib_succ)
+                                          (by exact_mod_cast (fib (n + 1)).zero_le)
+      ... ≤ B * nB                    : mul_le_mul B_ineq nB_ineq
+                                          (by exact_mod_cast (fib (n + 2)).zero_le)
+                                          (le_of_lt zero_lt_B) }
+end
+
+local attribute [instance] preorder.topology
+
+theorem of_convergence [order_topology K] :
+  filter.tendsto ((gcf.of v).convergents) filter.at_top $ nhds v :=
+by simpa [linear_ordered_add_comm_group.tendsto_nhds, abs_sub] using (of_convergence_epsilon v)
+
+end convergence
+
+end generalized_continued_fraction

src/algebra/continued_fractions/computation/approximations.lean

@@ -7,36 +7,35 @@ import algebra.continued_fractions.computation.correctness_terminating
 import data.nat.fib
 import tactic.solve_by_elim
 /-!
-# Approximations for Continued Fraction Computations (`gcf.of`)
+# Approximations for Continued Fraction Computations (`generalized_continued_fraction.of`)
 
 ## Summary
 
-Let us write `gcf` for `generalized_continued_fraction`. This file contains useful approximations
-for the values involved in the continued fractions computation `gcf.of`.
-In particular, we derive the so-called *determinant formula* for `gcf.of`:
+This file contains useful approximations for the values involved in the continued fractions
+computation `generalized_continued_fraction.of`. In particular, we derive the so-called
+*determinant formula* for `generalized_continued_fraction.of`:
 `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`.
 
 Moreover, we derive some upper bounds for the error term when computing a continued fraction up a
-given position, i.e. bounds for the term `|v - (gcf.of v).convergents n|`.
-The derived bounds will show us that the error term indeed gets smaller.
+given position, i.e. bounds for the term
+`|v - (generalized_continued_fraction.of v).convergents n|`. The derived bounds will show us that
+the error term indeed gets smaller. As a corollary, we will be able to show that
+`(generalized_continued_fraction.of v).convergents` converges to `v` in
+`algebra.continued_fractions.computation.approximation_corollaries`.
 
 ## Main Theorems
 
-- `gcf.of_part_num_eq_one`: shows that all partial numerators `aᵢ` are equal to one.
-- `gcf.exists_int_eq_of_part_denom`: shows that all partial denominators `bᵢ` correspond to an
-  integer.
-- `gcf.one_le_of_nth_part_denom`: shows that `1 ≤ bᵢ`.
-- `gcf.succ_nth_fib_le_of_nth_denom`: shows that the `n`th denominator `Bₙ` is greater than or equal
-  to the `n + 1`th fibonacci number `nat.fib (n + 1)`.
-- `gcf.le_of_succ_nth_denom`: shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is the `n`th partial
-  denominator of the continued fraction.
-- `gcf.abs_sub_convergents_le`: shows that `|v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁)`, where `Aₙ` is the
-  nth partial numerator.
-
-## TODO
-As a corollary of `gcf.abs_sub_convergents_le`, we will be able to show that
-`(gcf.of v).convergents` converges to `v`. (reference to this convergence lemma will be added in the
-upcoming PR about continued fractions)
+- `generalized_continued_fraction.of_part_num_eq_one`: shows that all partial numerators `aᵢ` are
+  equal to one.
+- `generalized_continued_fraction.exists_int_eq_of_part_denom`: shows that all partial denominators
+  `bᵢ` correspond to an integer.
+- `generalized_continued_fraction.one_le_of_nth_part_denom`: shows that `1 ≤ bᵢ`.
+- `generalized_continued_fraction.succ_nth_fib_le_of_nth_denom`: shows that the `n`th denominator
+  `Bₙ` is greater than or equal to the `n + 1`th fibonacci number `nat.fib (n + 1)`.
+- `generalized_continued_fraction.le_of_succ_nth_denom`: shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is
+  the `n`th partial denominator of the continued fraction.
+- `generalized_continued_fraction.abs_sub_convergents_le`: shows that
+  `|v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁)`, where `Aₙ` is the nth partial numerator.
 
 ## References
 
@@ -123,7 +122,7 @@ end int_fract_pair
 
 /-!
 Next we translate above results about the stream of `int_fract_pair`s to the computed continued
-fraction `gcf.of`.
+fraction `generalized_continued_fraction.of`.
 -/
 
 /-- Shows that the integer parts of the continued fraction are at least one. -/
@@ -321,7 +320,7 @@ section determinant
 /-!
 ### Determinant Formula
 
-Next we prove the so-called *determinant formula* for `gcf.of`:
+Next we prove the so-called *determinant formula* for `generalized_continued_fraction.of`:
 `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`.
 -/
 
@@ -379,7 +378,7 @@ section error_term
 ### Approximation of Error Term
 
 Next we derive some approximations for the error term when computing a continued fraction up a given
-position, i.e. bounds for the term `|v - (gcf.of v).convergents n|`.
+position, i.e. bounds for the term `|v - (generalized_continued_fraction.of v).convergents n|`.
 -/
 
 /-- This lemma follows from the finite correctness proof, the determinant equality, and

src/algebra/continued_fractions/computation/correctness_terminating.lean

@@ -9,32 +9,38 @@ import algebra.continued_fractions.continuants_recurrence
 import order.filter.at_top_bot
 
 /-!
-# Correctness of Terminating Continued Fraction Computations (`gcf.of`)
+# Correctness of Terminating Continued Fraction Computations (`generalized_continued_fraction.of`)
 
 ## Summary
 
-Let us write `gcf` for `generalized_continued_fraction`. We show the correctness of the
-algorithm computing continued fractions (`gcf.of`) in case of termination in the following sense:
+We show the correctness of the
+algorithm computing continued fractions (`generalized_continued_fraction.of`) in case of termination
+in the following sense:
 
 At every step `n : ℕ`, we can obtain the value `v` by adding a specific residual term to the last
-denominator of the fraction described by `(gcf.of v).convergents' n`. The residual term will be zero
-exactly when the continued fraction terminated; otherwise, the residual term will be given by the
-fractional part stored in `gcf.int_fract_pair.stream v n`.
+denominator of the fraction described by `(generalized_continued_fraction.of v).convergents' n`.
+The residual term will be zero exactly when the continued fraction terminated; otherwise, the
+residual term will be given by the fractional part stored in
+`generalized_continued_fraction.int_fract_pair.stream v n`.
 
-For an example, refer to `gcf.comp_exact_value_correctness_of_stream_eq_some` and for more
+For an example, refer to
+`generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some` and for more
 information about the computation process, refer to `algebra.continued_fraction.computation.basic`.
 
 ## Main definitions
 
-- `gcf.comp_exact_value` can be used to compute the exact value approximated by the continued
-  fraction `gcf.of v` by adding a residual term as described in the summary.
+- `generalized_continued_fraction.comp_exact_value` can be used to compute the exact value
+  approximated by the continued fraction `generalized_continued_fraction.of v` by adding a residual
+  term as described in the summary.
 
 ## Main Theorems
 
-- `gcf.comp_exact_value_correctness_of_stream_eq_some` shows that `gcf.comp_exact_value` indeed
-  returns the value `v` when given the convergent and fractional part as described in the summary.
-- `gcf.of_correctness_of_terminated_at` shows the equality `v = (gcf.of v).convergents n`
-  if `gcf.of v` terminated at position `n`.
+- `generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some` shows that
+  `generalized_continued_fraction.comp_exact_value` indeed returns the value `v` when given the
+  convergent and fractional part as described in the summary.
+- `generalized_continued_fraction.of_correctness_of_terminated_at` shows the equality
+  `v = (generalized_continued_fraction.of v).convergents n` if `generalized_continued_fraction.of v`
+  terminated at position `n`.
 -/
 
 namespace generalized_continued_fraction
@@ -48,8 +54,9 @@ Given two continuants `pconts` and `conts` and a value `fr`, this function retur
 - `exact_conts.a / exact_conts.b` where `exact_conts = next_continuants 1 fr⁻¹ pconts conts`
   otherwise.
 
-This function can be used to compute the exact value approxmated by a continued fraction `gcf.of v`
-as described in lemma `comp_exact_value_correctness_of_stream_eq_some`.
+This function can be used to compute the exact value approxmated by a continued fraction
+`generalized_continued_fraction.of v` as described in lemma
+`comp_exact_value_correctness_of_stream_eq_some`.
 -/
 protected def comp_exact_value (pconts conts : gcf.pair K) (fr : K) : K :=
 -- if the fractional part is zero, we exactly approximated the value by the last continuants
@@ -69,20 +76,20 @@ by { field_simp [fract_a_ne_zero], rw [fract], ring }
 open generalized_continued_fraction as gcf
 
 /--
-Shows the correctness of `comp_exact_value` in case the continued fraction `gcf.of v` did not
-terminate at position `n`. That is, we obtain the value `v` if we pass the two successive
-(auxiliary) continuants at positions `n` and `n + 1` as well as the fractional part at
-`int_fract_pair.stream n` to `comp_exact_value`.
+Shows the correctness of `comp_exact_value` in case the continued fraction
+`generalized_continued_fraction.of v` did not terminate at position `n`. That is, we obtain the
+value `v` if we pass the two successive (auxiliary) continuants at positions `n` and `n + 1` as well
+as the fractional part at `int_fract_pair.stream n` to `comp_exact_value`.
 
 The correctness might be seen more readily if one uses `convergents'` to evaluate the continued
 fraction. Here is an example to illustrate the idea:
 
 Let `(v : ℚ) := 3.4`. We have
-- `gcf.int_fract_pair.stream v 0 = some ⟨3, 0.4⟩`, and
-- `gcf.int_fract_pair.stream v 1 = some ⟨2, 0.5⟩`.
-Now `(gcf.of v).convergents' 1 = 3 + 1/2`, and our fractional term at position `2` is `0.5`. We
-hence have `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`. This computation corresponds exactly to the one
-using the recurrence equation in `comp_exact_value`.
+- `generalized_continued_fraction.int_fract_pair.stream v 0 = some ⟨3, 0.4⟩`, and
+- `generalized_continued_fraction.int_fract_pair.stream v 1 = some ⟨2, 0.5⟩`.
+Now `(generalized_continued_fraction.of v).convergents' 1 = 3 + 1/2`, and our fractional term at
+position `2` is `0.5`. We hence have `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`. This computation
+corresponds exactly to the one using the recurrence equation in `comp_exact_value`.
 -/
 lemma comp_exact_value_correctness_of_stream_eq_some :
   ∀ {ifp_n : int_fract_pair K}, int_fract_pair.stream v n = some ifp_n →
@@ -173,8 +180,8 @@ begin
       ac_refl } }
 end
 
-/-- The convergent of `gcf.of v` at step `n - 1` is exactly `v` if the `int_fract_pair.stream` of
-the corresponding continued fraction terminated at step `n`. -/
+/-- The convergent of `generalized_continued_fraction.of v` at step `n - 1` is exactly `v` if the
+`int_fract_pair.stream` of the corresponding continued fraction terminated at step `n`. -/
 lemma of_correctness_of_nth_stream_eq_none
   (nth_stream_eq_none : int_fract_pair.stream v n = none) :
   v = (gcf.of v).convergents (n - 1) :=
@@ -202,15 +209,20 @@ begin
       (comp_exact_value_correctness_of_stream_eq_some nth_stream_eq) } }
 end
 
-/-- If `gcf.of v` terminated at step `n`, then the `n`th convergent is exactly `v`. -/
+/--
+If `generalized_continued_fraction.of v` terminated at step `n`, then the `n`th convergent is
+exactly `v`.
+-/
 theorem of_correctness_of_terminated_at (terminated_at_n : (gcf.of v).terminated_at n) :
   v = (gcf.of v).convergents n :=
 have int_fract_pair.stream v (n + 1) = none, from
   gcf.of_terminated_at_n_iff_succ_nth_int_fract_pair_stream_eq_none.elim_left terminated_at_n,
  of_correctness_of_nth_stream_eq_none this
 
-/-- If `gcf.of v` terminates, then there is `n : ℕ` such that the `n`th convergent is exactly
-`v`. -/
+/--
+If `generalized_continued_fraction.of v` terminates, then there is `n : ℕ` such that the `n`th
+convergent is exactly `v`.
+-/
 lemma of_correctness_of_terminates (terminates : (gcf.of v).terminates) :
   ∃ (n : ℕ), v = (gcf.of v).convergents n :=
 exists.elim terminates
@@ -219,7 +231,10 @@ exists.elim terminates
 
 open filter
 
-/-- If `gcf.of v` terminates, then its convergents will eventually always be `v`. -/
+/--
+If `generalized_continued_fraction.of v` terminates, then its convergents will eventually always
+be `v`.
+-/
 lemma of_correctness_at_top_of_terminates (terminates : (gcf.of v).terminates) :
   ∀ᶠ n in at_top, v = (gcf.of v).convergents n :=
 begin