# Documentation

Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

# 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 GCFs 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: $$c = h + \dfrac{a_0} {b_0 + \dfrac{a_1} {b_1 + \dfrac{a_2} {b_2 + \dfrac{a_3} {b_3 + \dots}}}}$$ 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 + 1th position of c into the nth 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_squashGCF_nth_convergent'.

By the inductive hypothesis, the two computations for the nth convergent of c coincide. So all that is left to show is that the recurrence relation for c at n + 1 and c' at n coincide. This can be shown by another induction. The corresponding lemma in this file is succ_nth_convergent_eq_squashGCF_nth_convergent.

## Main Theorems #

• GeneralizedContinuedFraction.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.
• 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