29696
|
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 |
|
29698
|
8 |
theory Formal_Power_Series_Examples
|
29696
|
9 |
imports Formal_Power_Series Binomial Complex
|
|
10 |
begin
|
|
11 |
|
|
12 |
section{* The generalized binomial theorem *}
|
|
13 |
lemma gbinomial_theorem:
|
31021
|
14 |
"((a::'a::{ring_char_0, field, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
|
29696
|
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:
|
31021
|
41 |
fixes c :: "'a::{field, ring_char_0}"
|
29696
|
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 fps_sin_neg[simp]: "fps_sin (- c) = - fps_sin c"
|
|
187 |
by (simp add: fps_eq_iff fps_sin_def)
|
|
188 |
|
|
189 |
lemma fps_cos_neg[simp]: "fps_cos (- c) = fps_cos c"
|
|
190 |
by (simp add: fps_eq_iff fps_cos_def)
|
|
191 |
lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
|
|
192 |
unfolding minus_mult_right Eii_sin_cos by simp
|
|
193 |
|
30748
|
194 |
lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d) "by (simp add: fps_eq_iff fps_const_def)
|
|
195 |
|
|
196 |
lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
|
|
197 |
apply (subst (2) number_of_eq)
|
|
198 |
apply(rule int_induct[of _ 0])
|
|
199 |
apply (simp_all add: number_of_fps_def)
|
|
200 |
by (simp_all add: fps_const_add[symmetric] fps_const_minus[symmetric])
|
|
201 |
|
29696
|
202 |
lemma fps_cos_Eii:
|
|
203 |
"fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
|
|
204 |
proof-
|
|
205 |
have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
|
30748
|
206 |
by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
|
29696
|
207 |
show ?thesis
|
|
208 |
unfolding Eii_sin_cos minus_mult_commute
|
30748
|
209 |
by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
|
29696
|
210 |
qed
|
|
211 |
|
|
212 |
lemma fps_sin_Eii:
|
|
213 |
"fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
|
|
214 |
proof-
|
|
215 |
have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)"
|
30748
|
216 |
by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
|
29696
|
217 |
show ?thesis
|
|
218 |
unfolding Eii_sin_cos minus_mult_commute
|
|
219 |
by (simp add: fps_divide_def fps_const_inverse th)
|
|
220 |
qed
|
|
221 |
|
|
222 |
lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"
|
30748
|
223 |
by (simp add: fps_eq_iff fps_number_of_fps_const)
|
29696
|
224 |
|
|
225 |
lemma fps_const_mult_2_right: "a * fps_const (2::'a::number_ring) = a +a"
|
30748
|
226 |
by (simp add: fps_eq_iff fps_number_of_fps_const)
|
29696
|
227 |
|
|
228 |
lemma fps_tan_Eii:
|
|
229 |
"fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
|
|
230 |
unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
|
|
231 |
apply (simp add: fps_divide_def fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
|
|
232 |
by simp
|
|
233 |
|
|
234 |
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)"
|
|
235 |
unfolding Eii_sin_cos[symmetric] E_power_mult
|
|
236 |
by (simp add: mult_ac)
|
|
237 |
|
|
238 |
text{* Now some trigonometric identities *}
|
|
239 |
lemma fps_sin_add:
|
|
240 |
"fps_sin (a+b) = fps_sin (a::complex) * fps_cos b + fps_cos a * fps_sin b"
|
|
241 |
proof-
|
|
242 |
let ?ca = "fps_cos a"
|
|
243 |
let ?cb = "fps_cos b"
|
|
244 |
let ?sa = "fps_sin a"
|
|
245 |
let ?sb = "fps_sin b"
|
|
246 |
let ?i = "fps_const ii"
|
|
247 |
have i: "?i*?i = fps_const -1" by simp
|
|
248 |
have "fps_sin (a + b) =
|
|
249 |
((?ca + ?i * ?sa) * (?cb + ?i*?sb) - (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
|
|
250 |
fps_const (- (\<i> / 2))"
|
|
251 |
apply(simp add: fps_sin_Eii[of "a+b"] fps_divide_def minus_mult_commute)
|
|
252 |
unfolding right_distrib
|
|
253 |
apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
|
|
254 |
by (simp add: ring_simps)
|
|
255 |
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)"
|
|
256 |
by (simp add: ring_simps)
|
|
257 |
also have "\<dots> = (fps_const 2 * ?i * (?ca * ?sb + ?sa * ?cb)) * fps_const (- ii/2)"
|
|
258 |
apply simp
|
|
259 |
apply (simp add: ring_simps)
|
|
260 |
apply (simp add: ring_simps add: fps_const_mult[symmetric] del:fps_const_mult)
|
|
261 |
unfolding fps_const_mult_2_right
|
|
262 |
by (simp add: ring_simps)
|
|
263 |
also have "\<dots> = (fps_const 2 * ?i * fps_const (- ii/2)) * (?ca * ?sb + ?sa * ?cb)"
|
|
264 |
by (simp only: mult_ac)
|
|
265 |
also have "\<dots> = ?sa * ?cb + ?ca*?sb"
|
|
266 |
by simp
|
|
267 |
finally show ?thesis .
|
|
268 |
qed
|
|
269 |
|
|
270 |
lemma fps_cos_add:
|
|
271 |
"fps_cos (a+b) = fps_cos (a::complex) * fps_cos b - fps_sin a * fps_sin b"
|
|
272 |
proof-
|
|
273 |
let ?ca = "fps_cos a"
|
|
274 |
let ?cb = "fps_cos b"
|
|
275 |
let ?sa = "fps_sin a"
|
|
276 |
let ?sb = "fps_sin b"
|
|
277 |
let ?i = "fps_const ii"
|
|
278 |
have i: "?i*?i = fps_const -1" by simp
|
|
279 |
have i': "\<And>x. ?i * (?i * x) = - x"
|
|
280 |
apply (simp add: mult_assoc[symmetric] i)
|
|
281 |
by (simp add: fps_eq_iff)
|
|
282 |
have m1: "\<And>x. x * fps_const (-1 ::complex) = - x" "\<And>x. fps_const (-1 :: complex) * x = - x"
|
|
283 |
by (auto simp add: fps_eq_iff)
|
|
284 |
|
|
285 |
have "fps_cos (a + b) =
|
|
286 |
((?ca + ?i * ?sa) * (?cb + ?i*?sb) + (?ca - ?i*?sa) * (?cb - ?i*?sb)) *
|
|
287 |
fps_const (1/ 2)"
|
|
288 |
apply(simp add: fps_cos_Eii[of "a+b"] fps_divide_def minus_mult_commute)
|
|
289 |
unfolding right_distrib minus_add_distrib
|
|
290 |
apply (simp add: Eii_sin_cos E_minus_ii_sin_cos fps_const_inverse E_add_mult)
|
|
291 |
by (simp add: ring_simps)
|
|
292 |
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)"
|
|
293 |
apply simp
|
|
294 |
by (simp add: ring_simps i' m1)
|
|
295 |
also have "\<dots> = (fps_const 2 * (?ca * ?cb - ?sa * ?sb)) * fps_const (1/2)"
|
|
296 |
apply simp
|
|
297 |
by (simp add: ring_simps m1 fps_const_mult_2_right)
|
|
298 |
also have "\<dots> = (fps_const 2 * fps_const (1/2)) * (?ca * ?cb - ?sa * ?sb)"
|
|
299 |
by (simp only: mult_ac)
|
|
300 |
also have "\<dots> = ?ca * ?cb - ?sa*?sb"
|
|
301 |
by simp
|
|
302 |
finally show ?thesis .
|
|
303 |
qed
|
|
304 |
|
|
305 |
end |