# mathlib3documentation

algebra.continued_fractions.computation.translations

# Basic Translation Lemmas Between Structures Defined for Computing Continued Fractions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Summary #

This is a collection of simple lemmas between the different structures used for the computation of continued fractions defined in algebra.continued_fractions.computation.basic. The file consists of three sections:

1. Recurrences and inversion lemmas for int_fract_pair.stream: these lemmas give us inversion rules and recurrences for the computation of the stream of integer and fractional parts of a value.
2. Translation lemmas for the head term: these lemmas show us that the head term of the computed continued fraction of a value v is ⌊v⌋ and how this head term is moved along the structures used in the computation process.
3. Translation lemmas for the sequence: these lemmas show how the sequences of the involved structures (int_fract_pair.stream, int_fract_pair.seq1, and generalized_continued_fraction.of) are connected, i.e. how the values are moved along the structures and the termination of one sequence implies the termination of another sequence.

## Main Theorems #

• succ_nth_stream_eq_some_iff gives as a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of non-termination.
• succ_nth_stream_eq_none_iff gives as a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of termination.
• nth_of_eq_some_of_succ_nth_int_fract_pair_stream and nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero show how the entries of the sequence of the computed continued fraction can be obtained from the stream of integer and fractional parts.

### Recurrences and Inversion Lemmas for int_fract_pair.stream#

Here we state some lemmas that give us inversion rules and recurrences for the computation of the stream of integer and fractional parts of a value.

theorem generalized_continued_fraction.int_fract_pair.stream_eq_none_of_fr_eq_zero {K : Type u_1} [floor_ring K] {v : K} {n : } (stream_nth_eq : = option.some ifp_n) (nth_fr_eq_zero : ifp_n.fr = 0) :

Gives a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of termination.

theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_eq_some_iff {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} :
= option.some ifp_succ_n (ifp_n : , ifp_n.fr 0 = ifp_succ_n

Gives a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of non-termination.

An easier to use version of one direction of generalized_continued_fraction.int_fract_pair.succ_nth_stream_eq_some_iff.

The stream of int_fract_pairs of an integer stops after the first term.

theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_fr_zero {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : = option.some ifp_succ_n) (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
(ifp_n : , (ifp_n.fr)⁻¹ = (ifp_n.fr)⁻¹
theorem generalized_continued_fraction.int_fract_pair.stream_succ {K : Type u_1} [floor_ring K] {v : K} (h : 0) (n : ) :

A recurrence relation that expresses the (n+1)th term of the stream of int_fract_pairs of v for non-integer v in terms of the nth term of the stream associated to the inverse of the fractional part of v.

### Translation of the Head Term #

Here we state some lemmas that show us that the head term of the computed continued fraction of a value v is ⌊v⌋ and how this head term is moved along the structures used in the computation process.

@[simp]

The head term of the sequence with head of v is just the integer part of v.

@[simp]

The head term of the gcf of v is ⌊v⌋.

### Translation of the Sequences #

Here we state some lemmas that show how the sequences of the involved structures (int_fract_pair.stream, int_fract_pair.seq1, and generalized_continued_fraction.of) are connected, i.e. how the values are moved along the structures and how the termination of one sequence implies the termination of another sequence.

#### Translation of the Termination of the Sequences #

Let's first show how the termination of one sequence implies the termination of another sequence.

#### Translation of the Values of the Sequence #

Now let's show how the values of the sequences correspond to one another.

theorem generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : = option.some ifp_succ_n) :
= option.some {a := 1, b := (ifp_succ_n.b)}

Shows how the entries of the sequence of the computed continued fraction can be obtained by the integer parts of the stream of integer and fractional parts.

theorem generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero {K : Type u_1} [floor_ring K] {v : K} {n : } (stream_nth_eq : = option.some ifp_n) (nth_fr_ne_zero : ifp_n.fr 0) :
= option.some {a := 1, b := .b)}

Shows how the entries of the sequence of the computed continued fraction can be obtained by the fractional parts of the stream of integer and fractional parts.

theorem generalized_continued_fraction.of_s_head_aux {K : Type u_1} [floor_ring K] (v : K) :
= (option.some λ (p : , {a := 1, b := (p.b)})
theorem generalized_continued_fraction.of_s_head {K : Type u_1} [floor_ring K] {v : K} (h : 0) :

This gives the first pair of coefficients of the continued fraction of a non-integer v.

If a is an integer, then the coefficient sequence of its continued fraction is empty.

theorem generalized_continued_fraction.of_s_succ {K : Type u_1} [floor_ring K] (v : K) (n : ) :
(n + 1) =

Recurrence for the generalized_continued_fraction.of an element v of K in terms of that of the inverse of the fractional part of v.

theorem generalized_continued_fraction.of_s_tail {K : Type u_1} [floor_ring K] (v : K) :

This expresses the tail of the coefficient sequence of the generalized_continued_fraction.of an element v of K as the coefficient sequence of that of the inverse of the fractional part of v.

If a is an integer, then the convergents' of its continued fraction expansion are all equal to a.

theorem generalized_continued_fraction.convergents'_succ {K : Type u_1} [floor_ring K] (v : K) (n : ) :
=

The recurrence relation for the convergents' of the continued fraction expansion of an element v of K in terms of the convergents of the inverse of its fractional part.