3 |
3 |
4 theory Sum_of_Powers |
4 theory Sum_of_Powers |
5 imports Complex_Main |
5 imports Complex_Main |
6 begin |
6 begin |
7 |
7 |
8 subsection \<open>Additions to \<^theory>\<open>HOL.Binomial\<close> Theory\<close> |
|
9 |
|
10 lemma (in field_char_0) one_plus_of_nat_neq_zero [simp]: |
|
11 "1 + of_nat n \<noteq> 0" |
|
12 proof - |
|
13 have "of_nat (Suc n) \<noteq> of_nat 0" |
|
14 unfolding of_nat_eq_iff by simp |
|
15 then show ?thesis by simp |
|
16 qed |
|
17 |
|
18 lemma of_nat_binomial_eq_mult_binomial_Suc: |
|
19 assumes "k \<le> n" |
|
20 shows "(of_nat :: (nat \<Rightarrow> ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)" |
|
21 proof (cases k) |
|
22 case 0 then show ?thesis by simp |
|
23 next |
|
24 case (Suc l) |
|
25 have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))" |
|
26 using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k] |
|
27 by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc) |
|
28 also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))" |
|
29 by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) |
|
30 also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))" |
|
31 by (simp only: Suc_eq_plus1) |
|
32 finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))" |
|
33 by (simp add: field_simps) |
|
34 with assms show ?thesis |
|
35 by (simp add: binomial_altdef_of_nat prod_dividef) |
|
36 qed |
|
37 |
|
38 lemma real_binomial_eq_mult_binomial_Suc: |
|
39 assumes "k \<le> n" |
|
40 shows "(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)" |
|
41 by (metis Suc_eq_plus1 add.commute assms le_SucI of_nat_Suc of_nat_binomial_eq_mult_binomial_Suc of_nat_diff) |
|
42 |
|
43 subsection \<open>Preliminaries\<close> |
8 subsection \<open>Preliminaries\<close> |
44 |
9 |
45 lemma integrals_eq: |
10 lemma integrals_eq: |
46 assumes "f 0 = g 0" |
11 assumes "f a = g a" |
47 assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)" |
12 assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)" |
48 shows "f x = g x" |
13 shows "f x = g x" |
49 proof - |
14 by (metis (no_types, lifting) DERIV_isconst_all assms(1) assms(2) eq_iff_diff_eq_0) |
50 show "f x = g x" |
|
51 proof (cases "x \<noteq> 0") |
|
52 case True |
|
53 from assms DERIV_const_ratio_const[OF this, of "\<lambda>x. f x - g x" 0] |
|
54 show ?thesis by auto |
|
55 qed (simp add: assms) |
|
56 qed |
|
57 |
15 |
58 lemma sum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0" |
16 lemma sum_diff: "((\<Sum>i\<le>n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0" |
59 by (induct n) (auto simp add: field_simps) |
17 by (induct n) (auto simp add: field_simps) |
60 |
18 |
61 declare One_nat_def [simp del] |
19 declare One_nat_def [simp del] |
62 |
20 |
63 subsection \<open>Bernoulli Numbers and Bernoulli Polynomials\<close> |
21 subsection \<open>Bernoulli Numbers and Bernoulli Polynomials\<close> |
64 |
22 |