-
Notifications
You must be signed in to change notification settings - Fork 238
/
Translations.lean
190 lines (140 loc) · 9.23 KB
/
Translations.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
/-
Copyright (c) 2019 Kevin Kappelmann. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Kappelmann
-/
import Mathlib.Algebra.ContinuedFractions.Basic
import Mathlib.Algebra.GroupWithZero.Basic
#align_import algebra.continued_fractions.translations from "leanprover-community/mathlib"@"a7e36e48519ab281320c4d192da6a7b348ce40ad"
/-!
# Basic Translation Lemmas Between Functions Defined for Continued Fractions
## Summary
Some simple translation lemmas between the different definitions of functions defined in
`Algebra.ContinuedFractions.Basic`.
-/
namespace GeneralizedContinuedFraction
section General
/-!
### Translations Between General Access Functions
Here we give some basic translations that hold by definition between the various methods that allow
us to access the numerators and denominators of a continued fraction.
-/
variable {α : Type*} {g : GeneralizedContinuedFraction α} {n : ℕ}
theorem terminatedAt_iff_s_terminatedAt : g.TerminatedAt n ↔ g.s.TerminatedAt n := by rfl
#align generalized_continued_fraction.terminated_at_iff_s_terminated_at GeneralizedContinuedFraction.terminatedAt_iff_s_terminatedAt
theorem terminatedAt_iff_s_none : g.TerminatedAt n ↔ g.s.get? n = none := by rfl
#align generalized_continued_fraction.terminated_at_iff_s_none GeneralizedContinuedFraction.terminatedAt_iff_s_none
theorem part_num_none_iff_s_none : g.partialNumerators.get? n = none ↔ g.s.get? n = none := by
cases s_nth_eq : g.s.get? n <;> simp [partialNumerators, s_nth_eq]
#align generalized_continued_fraction.part_num_none_iff_s_none GeneralizedContinuedFraction.part_num_none_iff_s_none
theorem terminatedAt_iff_part_num_none : g.TerminatedAt n ↔ g.partialNumerators.get? n = none := by
rw [terminatedAt_iff_s_none, part_num_none_iff_s_none]
#align generalized_continued_fraction.terminated_at_iff_part_num_none GeneralizedContinuedFraction.terminatedAt_iff_part_num_none
theorem part_denom_none_iff_s_none : g.partialDenominators.get? n = none ↔ g.s.get? n = none := by
cases s_nth_eq : g.s.get? n <;> simp [partialDenominators, s_nth_eq]
#align generalized_continued_fraction.part_denom_none_iff_s_none GeneralizedContinuedFraction.part_denom_none_iff_s_none
theorem terminatedAt_iff_part_denom_none : g.TerminatedAt n ↔ g.partialDenominators.get? n = none :=
by rw [terminatedAt_iff_s_none, part_denom_none_iff_s_none]
#align generalized_continued_fraction.terminated_at_iff_part_denom_none GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none
theorem part_num_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) :
g.partialNumerators.get? n = some gp.a := by simp [partialNumerators, s_nth_eq]
#align generalized_continued_fraction.part_num_eq_s_a GeneralizedContinuedFraction.part_num_eq_s_a
theorem part_denom_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) :
g.partialDenominators.get? n = some gp.b := by simp [partialDenominators, s_nth_eq]
#align generalized_continued_fraction.part_denom_eq_s_b GeneralizedContinuedFraction.part_denom_eq_s_b
theorem exists_s_a_of_part_num {a : α} (nth_part_num_eq : g.partialNumerators.get? n = some a) :
∃ gp, g.s.get? n = some gp ∧ gp.a = a := by
simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq
#align generalized_continued_fraction.exists_s_a_of_part_num GeneralizedContinuedFraction.exists_s_a_of_part_num
theorem exists_s_b_of_part_denom {b : α}
(nth_part_denom_eq : g.partialDenominators.get? n = some b) :
∃ gp, g.s.get? n = some gp ∧ gp.b = b := by
simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq
#align generalized_continued_fraction.exists_s_b_of_part_denom GeneralizedContinuedFraction.exists_s_b_of_part_denom
end General
section WithDivisionRing
/-!
### Translations Between Computational Functions
Here we give some basic translations that hold by definition for the computational methods of a
continued fraction.
-/
variable {K : Type*} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K]
theorem nth_cont_eq_succ_nth_cont_aux : g.continuants n = g.continuantsAux (n + 1) :=
rfl
#align generalized_continued_fraction.nth_cont_eq_succ_nth_cont_aux GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux
theorem num_eq_conts_a : g.numerators n = (g.continuants n).a :=
rfl
#align generalized_continued_fraction.num_eq_conts_a GeneralizedContinuedFraction.num_eq_conts_a
theorem denom_eq_conts_b : g.denominators n = (g.continuants n).b :=
rfl
#align generalized_continued_fraction.denom_eq_conts_b GeneralizedContinuedFraction.denom_eq_conts_b
theorem convergent_eq_num_div_denom : g.convergents n = g.numerators n / g.denominators n :=
rfl
#align generalized_continued_fraction.convergent_eq_num_div_denom GeneralizedContinuedFraction.convergent_eq_num_div_denom
theorem convergent_eq_conts_a_div_conts_b :
g.convergents n = (g.continuants n).a / (g.continuants n).b :=
rfl
#align generalized_continued_fraction.convergent_eq_conts_a_div_conts_b GeneralizedContinuedFraction.convergent_eq_conts_a_div_conts_b
theorem exists_conts_a_of_num {A : K} (nth_num_eq : g.numerators n = A) :
∃ conts, g.continuants n = conts ∧ conts.a = A := by simpa
#align generalized_continued_fraction.exists_conts_a_of_num GeneralizedContinuedFraction.exists_conts_a_of_num
theorem exists_conts_b_of_denom {B : K} (nth_denom_eq : g.denominators n = B) :
∃ conts, g.continuants n = conts ∧ conts.b = B := by simpa
#align generalized_continued_fraction.exists_conts_b_of_denom GeneralizedContinuedFraction.exists_conts_b_of_denom
@[simp]
theorem zeroth_continuant_aux_eq_one_zero : g.continuantsAux 0 = ⟨1, 0⟩ :=
rfl
#align generalized_continued_fraction.zeroth_continuant_aux_eq_one_zero GeneralizedContinuedFraction.zeroth_continuant_aux_eq_one_zero
@[simp]
theorem first_continuant_aux_eq_h_one : g.continuantsAux 1 = ⟨g.h, 1⟩ :=
rfl
#align generalized_continued_fraction.first_continuant_aux_eq_h_one GeneralizedContinuedFraction.first_continuant_aux_eq_h_one
@[simp]
theorem zeroth_continuant_eq_h_one : g.continuants 0 = ⟨g.h, 1⟩ :=
rfl
#align generalized_continued_fraction.zeroth_continuant_eq_h_one GeneralizedContinuedFraction.zeroth_continuant_eq_h_one
@[simp]
theorem zeroth_numerator_eq_h : g.numerators 0 = g.h :=
rfl
#align generalized_continued_fraction.zeroth_numerator_eq_h GeneralizedContinuedFraction.zeroth_numerator_eq_h
@[simp]
theorem zeroth_denominator_eq_one : g.denominators 0 = 1 :=
rfl
#align generalized_continued_fraction.zeroth_denominator_eq_one GeneralizedContinuedFraction.zeroth_denominator_eq_one
@[simp]
theorem zeroth_convergent_eq_h : g.convergents 0 = g.h := by
simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one]
#align generalized_continued_fraction.zeroth_convergent_eq_h GeneralizedContinuedFraction.zeroth_convergent_eq_h
theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.continuantsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by
simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator]
#align generalized_continued_fraction.second_continuant_aux_eq GeneralizedContinuedFraction.second_continuant_aux_eq
theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by
simp [nth_cont_eq_succ_nth_cont_aux]
-- Porting note (#10959): simp used to work here, but now it can't figure out that 1 + 1 = 2
convert second_continuant_aux_eq zeroth_s_eq
#align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq
theorem first_numerator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.numerators 1 = gp.b * g.h + gp.a := by simp [num_eq_conts_a, first_continuant_eq zeroth_s_eq]
#align generalized_continued_fraction.first_numerator_eq GeneralizedContinuedFraction.first_numerator_eq
theorem first_denominator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.denominators 1 = gp.b := by simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq]
#align generalized_continued_fraction.first_denominator_eq GeneralizedContinuedFraction.first_denominator_eq
@[simp]
theorem zeroth_convergent'_aux_eq_zero {s : Stream'.Seq <| Pair K} :
convergents'Aux s 0 = (0 : K) :=
rfl
#align generalized_continued_fraction.zeroth_convergent'_aux_eq_zero GeneralizedContinuedFraction.zeroth_convergent'_aux_eq_zero
@[simp]
theorem zeroth_convergent'_eq_h : g.convergents' 0 = g.h := by simp [convergents']
#align generalized_continued_fraction.zeroth_convergent'_eq_h GeneralizedContinuedFraction.zeroth_convergent'_eq_h
theorem convergents'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) :
convergents'Aux s (n + 1) = 0 := by simp [convergents'Aux, h, convergents'Aux.match_1]
#align generalized_continued_fraction.convergents'_aux_succ_none GeneralizedContinuedFraction.convergents'Aux_succ_none
theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p)
(n : ℕ) : convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by
simp [convergents'Aux, h, convergents'Aux.match_1]
#align generalized_continued_fraction.convergents'_aux_succ_some GeneralizedContinuedFraction.convergents'Aux_succ_some
end WithDivisionRing
end GeneralizedContinuedFraction