equal
deleted
inserted
replaced
9 imports Formal_Power_Series Binomial Complex |
9 imports Formal_Power_Series Binomial Complex |
10 begin |
10 begin |
11 |
11 |
12 section{* The generalized binomial theorem *} |
12 section{* The generalized binomial theorem *} |
13 lemma gbinomial_theorem: |
13 lemma gbinomial_theorem: |
14 "((a::'a::{ring_char_0, field, division_by_zero, recpower})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
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))" |
15 proof- |
15 proof- |
16 from E_add_mult[of a b] |
16 from E_add_mult[of a b] |
17 have "(E (a + b)) $ n = (E a * E b)$n" by simp |
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))))" |
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) |
19 by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib) |
36 |
36 |
37 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" |
37 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" |
38 by (simp add: fps_binomial_def) |
38 by (simp add: fps_binomial_def) |
39 |
39 |
40 lemma fps_binomial_ODE_unique: |
40 lemma fps_binomial_ODE_unique: |
41 fixes c :: "'a::{field, recpower,ring_char_0}" |
41 fixes c :: "'a::{field, ring_char_0}" |
42 shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" |
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") |
43 (is "?lhs \<longleftrightarrow> ?rhs") |
44 proof- |
44 proof- |
45 let ?da = "fps_deriv a" |
45 let ?da = "fps_deriv a" |
46 let ?x1 = "(1 + X):: 'a fps" |
46 let ?x1 = "(1 + X):: 'a fps" |