Basic Translation Lemmas Between Structures Defined for Computing Continued Fractions

Summary

This is a collection of simple lemmas between the different structures used for the computation of continued fractions defined in Algebra.ContinuedFractions.Computation.Basic. The file consists of three sections:

1. Recurrences and inversion lemmas for IntFractPair.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 (IntFractPair.stream, IntFractPair.seq1, and GenContFract.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.
• get?_of_eq_some_of_succ_get?_intFractPair_stream and get?_of_eq_some_of_get?_intFractPair_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 IntFractPair.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 GenContFract.IntFractPair.stream_zero {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : GenContFract.IntFractPair.stream v 0 = some (GenContFract.IntFractPair.of v)

theorem GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {ifp_n : GenContFract.IntFractPair K} (stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp_n) (nth_fr_eq_zero : ifp_n.fr = 0) : GenContFract.IntFractPair.stream v (n + 1) = none

theorem GenContFract.IntFractPair.succ_nth_stream_eq_none_iff {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} : GenContFract.IntFractPair.stream v (n + 1) = none ↔ GenContFract.IntFractPair.stream v n = none ∨ ∃ (ifp : GenContFract.IntFractPair K), GenContFract.IntFractPair.stream v n = 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.

theorem GenContFract.IntFractPair.succ_nth_stream_eq_some_iff {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {ifp_succ_n : GenContFract.IntFractPair K} : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n ↔ ∃ (ifp_n : GenContFract.IntFractPair K), GenContFract.IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ GenContFract.IntFractPair.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.

theorem GenContFract.IntFractPair.stream_succ_of_some {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {p : GenContFract.IntFractPair K} (h : GenContFract.IntFractPair.stream v n = some p) (h' : p.fr ≠ 0) : GenContFract.IntFractPair.stream v (n + 1) = some (GenContFract.IntFractPair.of p.fr⁻¹)

An easier to use version of one direction of GenContFract.IntFractPair.succ_nth_stream_eq_some_iff.

theorem GenContFract.IntFractPair.stream_succ_of_int {K : Type u_1} [LinearOrderedField K] [FloorRing K] (a : ℤ) (n : ℕ) : GenContFract.IntFractPair.stream (↑a) (n + 1) = none

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

theorem GenContFract.IntFractPair.exists_succ_nth_stream_of_fr_zero {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {ifp_succ_n : GenContFract.IntFractPair K} (stream_succ_nth_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n) (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) : ∃ (ifp_n : GenContFract.IntFractPair K), GenContFract.IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

theorem GenContFract.IntFractPair.stream_succ {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} (h : Int.fract v ≠ 0) (n : ℕ) : GenContFract.IntFractPair.stream v (n + 1) = GenContFract.IntFractPair.stream (Int.fract v)⁻¹ n

A recurrence relation that expresses the (n+1)th term of the stream of IntFractPairs 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]

theorem GenContFract.IntFractPair.seq1_fst_eq_of {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} : (GenContFract.IntFractPair.seq1 v).1 = GenContFract.IntFractPair.of v

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

theorem GenContFract.of_h_eq_intFractPair_seq1_fst_b {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} : (GenContFract.of v).h = ↑(GenContFract.IntFractPair.seq1 v).1.b

@[simp]

theorem GenContFract.of_h_eq_floor {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} : (GenContFract.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 (IntFractPair.stream, IntFractPair.seq1, and GenContFract.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.

theorem GenContFract.IntFractPair.get?_seq1_eq_succ_get?_stream {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} : (GenContFract.IntFractPair.seq1 v).2.get? n = GenContFract.IntFractPair.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.

theorem GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} : (GenContFract.of v).TerminatedAt n ↔ (GenContFract.IntFractPair.seq1 v).2.TerminatedAt n

theorem GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} : (GenContFract.of v).TerminatedAt n ↔ GenContFract.IntFractPair.stream v (n + 1) = none

Translation of the Values of the Sequence

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

theorem GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {gp_n : GenContFract.Pair K} (s_nth_eq : (GenContFract.of v).s.get? n = some gp_n) : ∃ (ifp : GenContFract.IntFractPair K), GenContFract.IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b

theorem GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {ifp_succ_n : GenContFract.IntFractPair K} (stream_succ_nth_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n) : (GenContFract.of v).s.get? n = 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 GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} {n : ℕ} {ifp_n : GenContFract.IntFractPair K} (stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp_n) (nth_fr_ne_zero : ifp_n.fr ≠ 0) : (GenContFract.of v).s.get? n = some { a := 1, b := ↑(GenContFract.IntFractPair.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.

theorem GenContFract.of_s_head_aux {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : (GenContFract.of v).s.get? 0 = (GenContFract.IntFractPair.stream v 1).bind (some ∘ fun (p : GenContFract.IntFractPair K) => { a := 1, b := ↑p.b })

theorem GenContFract.of_s_head {K : Type u_1} [LinearOrderedField K] [FloorRing K] {v : K} (h : Int.fract v ≠ 0) : (GenContFract.of v).s.head = some { a := 1, b := ↑⌊(Int.fract v)⁻¹⌋ }

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

theorem GenContFract.of_s_of_int (K : Type u_1) [LinearOrderedField K] [FloorRing K] (a : ℤ) : (GenContFract.of ↑a).s = Stream'.Seq.nil

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

theorem GenContFract.of_s_succ {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) (n : ℕ) : (GenContFract.of v).s.get? (n + 1) = (GenContFract.of (Int.fract v)⁻¹).s.get? n

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

theorem GenContFract.of_s_tail {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : (GenContFract.of v).s.tail = (GenContFract.of (Int.fract v)⁻¹).s

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

theorem GenContFract.convs'_of_int (K : Type u_1) [LinearOrderedField K] [FloorRing K] (n : ℕ) (a : ℤ) : (GenContFract.of ↑a).convs' n = ↑a

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

theorem GenContFract.convs'_succ {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) (n : ℕ) : (GenContFract.of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs' n

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