# mathlibdocumentation

algebra.continued_fractions.convergents_equiv

# 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 [HWHBS08], 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 + 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_squash_gcf_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 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.

## Tags #

fractions, recurrence, equivalence