# 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

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.

def generalized_continued_fraction.squash_seq {K : Type u_1} (n : ) :

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.

Equations
• = generalized_continued_fraction.squash_seq._match_1 s n (s.nth n, s.nth (n + 1))
• generalized_continued_fraction.squash_seq._match_1 s n (some gp_n, some gp_succ_n) = seq.zip_with (λ (n' : ) (gp : , ite (n' = n) {a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b} gp) seq.nats s
• generalized_continued_fraction.squash_seq._match_1 s n (some val, = s
• generalized_continued_fraction.squash_seq._match_1 s n , snd) = s

We now prove some simple lemmas about the squashed sequence

theorem generalized_continued_fraction.squash_seq_eq_self_of_terminated {K : Type u_1} {n : } (terminated_at_succ_n : s.terminated_at (n + 1)) :

If the sequence already terminated at position n + 1, nothing gets squashed.

theorem generalized_continued_fraction.squash_seq_nth_of_not_terminated {K : Type u_1} {n : } {gp_n gp_succ_n : generalized_continued_fraction.pair K} (s_nth_eq : s.nth n = some gp_n) (s_succ_nth_eq : s.nth (n + 1) = some gp_succ_n) :
= some {a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b}

If the sequence has not terminated before position n + 1, the value at n + 1 gets squashed into position n.

theorem generalized_continued_fraction.squash_seq_nth_of_lt {K : Type u_1} {n : } {m : } (m_lt_n : m < n) :
= s.nth m

The values before the squashed position stay the same.

Squashing at position n + 1 and taking the tail is the same as squashing the tail of the sequence at position n.

The auxiliary function convergents'_aux returns the same value for a sequence and the corresponding squashed sequence at the squashed position.

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⟩
Equations
• g.squash_gcf (n + 1) = {h := g.h, s :=
• g.squash_gcf 0 = generalized_continued_fraction.squash_gcf._match_1 g (g.s.nth 0)
• generalized_continued_fraction.squash_gcf._match_1 g (some gp) = {h := g.h + gp.a / gp.b, s := g.s}
• generalized_continued_fraction.squash_gcf._match_1 g none = g

Again, we derive some simple lemmas that are not really of interest. This time for the squashed gcf.

theorem generalized_continued_fraction.squash_gcf_eq_self_of_terminated {K : Type u_1} {n : } (terminated_at_n : g.terminated_at n) :

If the gcf already terminated at position n, nothing gets squashed.

theorem generalized_continued_fraction.squash_gcf_nth_of_lt {K : Type u_1} {n : } {m : } (m_lt_n : m < n) :
(g.squash_gcf (n + 1)).s.nth m = g.s.nth m

The values before the squashed position stay the same.

convergents' returns the same value for a gcf and the corresponding squashed gcf at the squashed position.

The auxiliary continuants before the squashed position stay the same.

theorem generalized_continued_fraction.succ_nth_convergent_eq_squash_gcf_nth_convergent {K : Type u_1} {n : } [field K] (nth_part_denom_ne_zero : ∀ {b : K}, = some bb 0) :

The convergents coincide in the expected way at the squashed position if the partial denominator at the squashed position is not zero.

theorem generalized_continued_fraction.convergents_eq_convergents' {K : Type u_1} {n : } (s_pos : ∀ {gp : {m : }, m < ng.s.nth m = some gp0 < gp.a 0 < gp.b) :

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.

Shows that the recurrence relation (convergents) and direct evaluation (convergents') of a (regular) continued fraction coincide.