1 (* Title: Formal_Power_Series_Examples.thy |
|
2 ID: |
|
3 Author: Amine Chaieb, University of Cambridge |
|
4 *) |
|
5 |
|
6 header{* Some applications of formal power series and some properties over complex numbers*} |
|
7 |
|
8 theory Formal_Power_Series_Examples |
|
9 imports Formal_Power_Series Binomial |
|
10 begin |
|
11 |
|
12 section{* The generalized binomial theorem *} |
|
13 lemma gbinomial_theorem: |
|
14 "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
|
15 proof- |
|
16 from E_add_mult[of a b] |
|
17 have "(E (a + b)) $ n = (E a * E b)$n" by simp |
|
18 then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))" |
|
19 by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) |
|
20 then show ?thesis |
|
21 apply simp |
|
22 apply (rule setsum_cong2) |
|
23 apply simp |
|
24 apply (frule binomial_fact[where ?'a = 'a, symmetric]) |
|
25 by (simp add: field_simps of_nat_mult) |
|
26 qed |
|
27 |
|
28 text{* And the nat-form -- also available from Binomial.thy *} |
|
29 lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))" |
|
30 using gbinomial_theorem[of "of_nat a" "of_nat b" n] |
|
31 unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] |
|
32 by simp |
|
33 |
|
34 section {* The binomial series and Vandermonde's identity *} |
|
35 definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)" |
|
36 |
|
37 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" |
|
38 by (simp add: fps_binomial_def) |
|
39 |
|
40 lemma fps_binomial_ODE_unique: |
|
41 fixes c :: "'a::field_char_0" |
|
42 shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" |
|
43 (is "?lhs \<longleftrightarrow> ?rhs") |
|
44 proof- |
|
45 let ?da = "fps_deriv a" |
|
46 let ?x1 = "(1 + X):: 'a fps" |
|
47 let ?l = "?x1 * ?da" |
|
48 let ?r = "fps_const c * a" |
|
49 have x10: "?x1 $ 0 \<noteq> 0" by simp |
|
50 have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp |
|
51 also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1" |
|
52 apply (simp only: fps_divide_def mult_assoc[symmetric] inverse_mult_eq_1[OF x10]) |
|
53 by (simp add: ring_simps) |
|
54 finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp |
|
55 moreover |
|
56 {assume h: "?l = ?r" |
|
57 {fix n |
|
58 from h have lrn: "?l $ n = ?r$n" by simp |
|
59 |
|
60 from lrn |
|
61 have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" |
|
62 apply (simp add: ring_simps del: of_nat_Suc) |
|
63 by (cases n, simp_all add: field_simps del: of_nat_Suc) |
|
64 } |
|
65 note th0 = this |
|
66 {fix n have "a$n = (c gchoose n) * a$0" |
|
67 proof(induct n) |
|
68 case 0 thus ?case by simp |
|
69 next |
|
70 case (Suc m) |
|
71 thus ?case unfolding th0 |
|
72 apply (simp add: field_simps del: of_nat_Suc) |
|
73 unfolding mult_assoc[symmetric] gbinomial_mult_1 |
|
74 by (simp add: ring_simps) |
|
75 qed} |
|
76 note th1 = this |
|
77 have ?rhs |
|
78 apply (simp add: fps_eq_iff) |
|
79 apply (subst th1) |
|
80 by (simp add: ring_simps)} |
|
81 moreover |
|
82 {assume h: ?rhs |
|
83 have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute) |
|
84 have "?l = ?r" |
|
85 apply (subst h) |
|
86 apply (subst (2) h) |
|
87 apply (clarsimp simp add: fps_eq_iff ring_simps) |
|
88 unfolding mult_assoc[symmetric] th00 gbinomial_mult_1 |
|
89 by (simp add: ring_simps gbinomial_mult_1)} |
|
90 ultimately show ?thesis by blast |
|
91 qed |
|
92 |
|
93 lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" |
|
94 proof- |
|
95 let ?a = "fps_binomial c" |
|
96 have th0: "?a = fps_const (?a$0) * ?a" by (simp) |
|
97 from iffD2[OF fps_binomial_ODE_unique, OF th0] show ?thesis . |
|
98 qed |
|
99 |
|
100 lemma fps_binomial_add_mult: "fps_binomial (c+d) = fps_binomial c * fps_binomial d" (is "?l = ?r") |
|
101 proof- |
|
102 let ?P = "?r - ?l" |
|
103 let ?b = "fps_binomial" |
|
104 let ?db = "\<lambda>x. fps_deriv (?b x)" |
|
105 have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp |
|
106 also have "\<dots> = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))" |
|
107 unfolding fps_binomial_deriv |
|
108 by (simp add: fps_divide_def ring_simps) |
|
109 also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P" |
|
110 by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add) |
|
111 finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" |
|
112 by (simp add: fps_divide_def) |
|
113 have "?P = fps_const (?P$0) * ?b (c + d)" |
|
114 unfolding fps_binomial_ODE_unique[symmetric] |
|
115 using th0 by simp |
|
116 hence "?P = 0" by (simp add: fps_mult_nth) |
|
117 then show ?thesis by simp |
|
118 qed |
|
119 |
|
120 lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" |
|
121 (is "?l = inverse ?r") |
|
122 proof- |
|
123 have th: "?r$0 \<noteq> 0" by simp |
|
124 have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)" |
|
125 by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg) |
|
126 have eq: "inverse ?r $ 0 = 1" |
|
127 by (simp add: fps_inverse_def) |
|
128 from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq |
|
129 show ?thesis by (simp add: fps_inverse_def) |
|
130 qed |
|
131 |
|
132 lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n" |
|
133 proof- |
|
134 let ?ba = "fps_binomial a" |
|
135 let ?bb = "fps_binomial b" |
|
136 let ?bab = "fps_binomial (a + b)" |
|
137 from fps_binomial_add_mult[of a b] have "?bab $ n = (?ba * ?bb)$n" by simp |
|
138 then show ?thesis by (simp add: fps_mult_nth) |
|
139 qed |
|
140 |
|
141 lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" |
|
142 using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n] |
|
143 |
|
144 apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric]) |
|
145 by simp |
|
146 |
|
147 lemma binomial_symmetric: assumes kn: "k \<le> n" |
|
148 shows "n choose k = n choose (n - k)" |
|
149 proof- |
|
150 from kn have kn': "n - k \<le> n" by arith |
|
151 from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] |
|
152 have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp |
|
153 then show ?thesis using kn by simp |
|
154 qed |
|
155 |
|
156 lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n" |
|
157 using binomial_Vandermond[of n n n,symmetric] |
|
158 unfolding nat_mult_2 apply (simp add: power2_eq_square) |
|
159 apply (rule setsum_cong2) |
|
160 by (auto intro: binomial_symmetric) |
|
161 |
|
162 section {* Relation between formal sine/cosine and the exponential FPS*} |
|
163 lemma Eii_sin_cos: |
|
164 "E (ii * c) = fps_cos c + fps_const ii * fps_sin c " |
|
165 (is "?l = ?r") |
|
166 proof- |
|
167 {fix n::nat |
|
168 {assume en: "even n" |
|
169 from en obtain m where m: "n = 2*m" |
|
170 unfolding even_mult_two_ex by blast |
|
171 |
|
172 have "?l $n = ?r$n" |
|
173 by (simp add: m fps_sin_def fps_cos_def power_mult_distrib |
|
174 power_mult power_minus)} |
|
175 moreover |
|
176 {assume on: "odd n" |
|
177 from on obtain m where m: "n = 2*m + 1" |
|
178 unfolding odd_nat_equiv_def2 by (auto simp add: nat_mult_2) |
|
179 have "?l $n = ?r$n" |
|
180 by (simp add: m fps_sin_def fps_cos_def power_mult_distrib |
|
181 power_mult power_minus)} |
|
182 ultimately have "?l $n = ?r$n" by blast} |
|
183 then show ?thesis by (simp add: fps_eq_iff) |
|
184 qed |
|
185 |
|
186 lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c " |
|
187 unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd) |
|
188 |
|
189 lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)" |
|
190 by (simp add: fps_eq_iff fps_const_def) |
|
191 |
|
192 lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})" |
|
193 apply (subst (2) number_of_eq) |
|
194 apply(rule int_induct[of _ 0]) |
|
195 apply (simp_all add: number_of_fps_def) |
|
196 by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric]) |
|
197 |
|
198 lemma fps_cos_Eii: |
|
199 "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2" |
|
200 proof- |
|
201 have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" |
|
202 by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric]) |
|
203 show ?thesis |
|
204 unfolding Eii_sin_cos minus_mult_commute |
|
205 by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const |
|
206 fps_divide_def fps_const_inverse th complex_number_of_def[symmetric]) |
|
207 qed |
|
208 |
|
209 lemma fps_sin_Eii: |
|
210 "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)" |
|
211 proof- |
|
212 have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)" |
|
213 by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric]) |
|
214 show ?thesis |
|
215 unfolding Eii_sin_cos minus_mult_commute |
|
216 by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th) |
|
217 qed |
|
218 |
|
219 lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a" |
|
220 by (simp add: fps_eq_iff fps_number_of_fps_const) |
|
221 |
|
222 lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a" |
|
223 by (simp add: fps_eq_iff fps_number_of_fps_const) |
|
224 |
|
225 lemma fps_tan_Eii: |
|
226 "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))" |
|
227 unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg |
|
228 apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) |
|
229 by simp |
|
230 |
|
231 lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)" |
|
232 unfolding Eii_sin_cos[symmetric] E_power_mult |
|
233 by (simp add: mult_ac) |
|
234 |
|
235 text{* Now some trigonometric identities *} |
|
236 |
|
237 lemma fps_sin_add: |
|
238 "fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b" |
|
239 proof- |
|
240 let ?ca = "fps_cos a" |
|
241 let ?cb = "fps_cos b" |
|
242 let ?sa = "fps_sin a" |
|
243 let ?sb = "fps_sin b" |
|
244 let ?i = "fps_const ii" |
|
245 have i: "?i*?i = fps_const -1" by simp |
|
246 have "fps_sin (a + b) = |
|
247 ((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) * |
|
248 fps_const (- (\<i> / 2))" |
|
249 apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute) |
|
250 unfolding right_distrib |
|
251 apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) |
|
252 by (simp add: ring_simps) |
|
253 also have "\<dots> = (?ca * ?cb + ?i*?ca * ?sb + ?i * ?sa * ?cb + (?i*?i)*?sa*?sb - ?ca*?cb + ?i*?ca * ?sb + ?i*?sa*?cb - (?i*?i)*?sa * ?sb) * fps_const (- ii/2)" |
|
254 by (simp add: ring_simps) |
|
255 also have "\<dots> = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)" |
|
256 apply simp |
|
257 apply (simp add: ring_simps) |
|
258 apply (simp add: ring_simps add: fps_const_mult[symmetric] del:fps_const_mult) |
|
259 unfolding fps_const_mult_2_right |
|
260 by (simp add: ring_simps) |
|
261 also have "\<dots> = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)" |
|
262 by (simp only: mult_ac) |
|
263 also have "\<dots> = ?sa * ?cb + ?ca*?sb" |
|
264 by simp |
|
265 finally show ?thesis . |
|
266 qed |
|
267 |
|
268 lemma fps_cos_add: |
|
269 "fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b" |
|
270 proof- |
|
271 let ?ca = "fps_cos a" |
|
272 let ?cb = "fps_cos b" |
|
273 let ?sa = "fps_sin a" |
|
274 let ?sb = "fps_sin b" |
|
275 let ?i = "fps_const ii" |
|
276 have i: "?i*?i = fps_const -1" by simp |
|
277 have i': "\<And>x. ?i * (?i * x) = - x" |
|
278 apply (simp add: mult_assoc[symmetric] i) |
|
279 by (simp add: fps_eq_iff) |
|
280 have m1: "\<And>x. x * fps_const (-1 ::complex) = - x" "\<And>x. fps_const (-1 :: complex) * x = - x" |
|
281 by (auto simp add: fps_eq_iff) |
|
282 |
|
283 have "fps_cos (a + b) = |
|
284 ((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) * |
|
285 fps_const (1/ 2)" |
|
286 apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute) |
|
287 unfolding right_distrib minus_add_distrib |
|
288 apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult) |
|
289 by (simp add: ring_simps) |
|
290 also have "\<dots> = (?ca * ?cb + ?i*?ca * ?sb + ?i * ?sa * ?cb + (?i*?i)*?sa*?sb + ?ca*?cb - ?i*?ca * ?sb - ?i*?sa*?cb + (?i*?i)*?sa * ?sb) * fps_const (1/2)" |
|
291 apply simp |
|
292 by (simp add: ring_simps i' m1) |
|
293 also have "\<dots> = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)" |
|
294 apply simp |
|
295 by (simp add: ring_simps m1 fps_const_mult_2_right) |
|
296 also have "\<dots> = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)" |
|
297 by (simp only: mult_ac) |
|
298 also have "\<dots> = ?ca * ?cb - ?sa*?sb" |
|
299 by simp |
|
300 finally show ?thesis . |
|
301 qed |
|
302 |
|
303 end |
|