mathlib3 documentation

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 #

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.

source
theorem generalized_continued_fraction.int_fract_pair.stream_zero {K : Type u_1} [linear_ordered_field K] [floor_ring K] (v : K) :
generalized_continued_fraction.int_fract_pair.stream v 0 = option.some (generalized_continued_fraction.int_fract_pair.of v)
source
theorem generalized_continued_fraction.int_fract_pair.stream_eq_none_of_fr_eq_zero {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {ifp_n : generalized_continued_fraction.int_fract_pair K} (stream_nth_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n) (nth_fr_eq_zero : ifp_n.fr = 0) :
generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.none
source
theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_eq_none_iff {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} :
generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.none ↔ generalized_continued_fraction.int_fract_pair.stream v n = option.none ∨ ∃ (ifp : generalized_continued_fraction.int_fract_pair K), generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp ∧ ifp.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.

source
theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_eq_some_iff {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} :
generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.some ifp_succ_n ↔ ∃ (ifp_n : generalized_continued_fraction.int_fract_pair K), generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n ∧ ifp_n.fr ≠ 0 ∧ generalized_continued_fraction.int_fract_pair.of (ifp_n.fr)⁻¹ = 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.

source
theorem generalized_continued_fraction.int_fract_pair.stream_succ_of_some {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {p : generalized_continued_fraction.int_fract_pair K} (h : generalized_continued_fraction.int_fract_pair.stream v n = option.some p) (h' : p.fr ≠ 0) :
generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.some (generalized_continued_fraction.int_fract_pair.of (p.fr)⁻¹)

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

source
theorem generalized_continued_fraction.int_fract_pair.stream_succ_of_int {K : Type u_1} [linear_ordered_field K] [floor_ring K] (a : ℤ) (n : ℕ) :
generalized_continued_fraction.int_fract_pair.stream ↑a (n + 1) = option.none

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

source
theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_fr_zero {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.some ifp_succ_n) (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
∃ (ifp_n : generalized_continued_fraction.int_fract_pair K), generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n ∧ (ifp_n.fr)⁻¹ = ↑⌊(ifp_n.fr)⁻¹⌋
source
theorem generalized_continued_fraction.int_fract_pair.stream_succ {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} (h : int.fract v ≠ 0) (n : ℕ) :
generalized_continued_fraction.int_fract_pair.stream v (n + 1) = generalized_continued_fraction.int_fract_pair.stream (int.fract v)⁻¹ 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.

source
@[simp]
theorem generalized_continued_fraction.int_fract_pair.seq1_fst_eq_of {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} :
(generalized_continued_fraction.int_fract_pair.seq1 v).fst = generalized_continued_fraction.int_fract_pair.of v

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

source
theorem generalized_continued_fraction.of_h_eq_int_fract_pair_seq1_fst_b {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} :
(generalized_continued_fraction.of v).h = ↑((generalized_continued_fraction.int_fract_pair.seq1 v).fst.b)
source
@[simp]
theorem generalized_continued_fraction.of_h_eq_floor {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} :
(generalized_continued_fraction.of v).h = ↑⌊v⌋

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.

source
theorem generalized_continued_fraction.int_fract_pair.nth_seq1_eq_succ_nth_stream {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} :
(generalized_continued_fraction.int_fract_pair.seq1 v).snd.nth n = generalized_continued_fraction.int_fract_pair.stream v (n + 1)

Translation of the Termination of the Sequences #

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

source
theorem generalized_continued_fraction.of_terminated_at_iff_int_fract_pair_seq1_terminated_at {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} :
(generalized_continued_fraction.of v).terminated_at n ↔ (generalized_continued_fraction.int_fract_pair.seq1 v).snd.terminated_at n
source
theorem generalized_continued_fraction.of_terminated_at_n_iff_succ_nth_int_fract_pair_stream_eq_none {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} :
(generalized_continued_fraction.of v).terminated_at n ↔ generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.none

Translation of the Values of the Sequence #

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

source
theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {gp_n : generalized_continued_fraction.pair K} (s_nth_eq : (generalized_continued_fraction.of v).s.nth n = option.some gp_n) :
∃ (ifp : generalized_continued_fraction.int_fract_pair K), generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.some ifp ∧ ↑(ifp.b) = gp_n.b
source
theorem generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.some ifp_succ_n) :
(generalized_continued_fraction.of v).s.nth 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.

source
theorem generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} {n : ℕ} {ifp_n : generalized_continued_fraction.int_fract_pair K} (stream_nth_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n) (nth_fr_ne_zero : ifp_n.fr ≠ 0) :
(generalized_continued_fraction.of v).s.nth n = option.some {a := 1, b := ↑((generalized_continued_fraction.int_fract_pair.of (ifp_n.fr)⁻¹).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.

source
theorem generalized_continued_fraction.of_s_head_aux {K : Type u_1} [linear_ordered_field K] [floor_ring K] (v : K) :
(generalized_continued_fraction.of v).s.nth 0 = (generalized_continued_fraction.int_fract_pair.stream v 1).bind (option.some ∘ λ (p : generalized_continued_fraction.int_fract_pair K), {a := 1, b := ↑(p.b)})
source
theorem generalized_continued_fraction.of_s_head {K : Type u_1} [linear_ordered_field K] [floor_ring K] {v : K} (h : int.fract v ≠ 0) :
(generalized_continued_fraction.of v).s.head = option.some {a := 1, b := ↑⌊(int.fract v)⁻¹⌋}

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

source
theorem generalized_continued_fraction.of_s_of_int (K : Type u_1) [linear_ordered_field K] [floor_ring K] (a : ℤ) :
(generalized_continued_fraction.of ↑a).s = stream.seq.nil

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

source
theorem generalized_continued_fraction.of_s_succ {K : Type u_1} [linear_ordered_field K] [floor_ring K] (v : K) (n : ℕ) :
(generalized_continued_fraction.of v).s.nth (n + 1) = (generalized_continued_fraction.of (int.fract v)⁻¹).s.nth n

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.

source
theorem generalized_continued_fraction.of_s_tail {K : Type u_1} [linear_ordered_field K] [floor_ring K] (v : K) :
(generalized_continued_fraction.of v).s.tail = (generalized_continued_fraction.of (int.fract v)⁻¹).s

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.

source
theorem generalized_continued_fraction.convergents'_of_int (K : Type u_1) [linear_ordered_field K] [floor_ring K] (n : ℕ) (a : ℤ) :
(generalized_continued_fraction.of ↑a).convergents' n = ↑a

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

source
theorem generalized_continued_fraction.convergents'_succ {K : Type u_1} [linear_ordered_field K] [floor_ring K] (v : K) (n : ℕ) :
(generalized_continued_fraction.of v).convergents' (n + 1) = ↑⌊v⌋ + 1 / (generalized_continued_fraction.of (int.fract v)⁻¹).convergents' 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.