src/HOL/ex/Sum_of_Powers.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 61694 6571c78c9667 child 63367 6c731c8b7f03 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Author:     Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)
```
```     2 section \<open>Sum of Powers\<close>
```
```     3
```
```     4 theory Sum_of_Powers
```
```     5 imports Complex_Main
```
```     6 begin
```
```     7
```
```     8 subsection \<open>Additions to @{theory Binomial} Theory\<close>
```
```     9
```
```    10 lemma of_nat_binomial_eq_mult_binomial_Suc:
```
```    11   assumes "k \<le> n"
```
```    12   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)"
```
```    13 proof -
```
```    14   have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
```
```    15   proof -
```
```    16     have "of_nat (n + 1) * (\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1) * (\<Prod>i\<in>Suc ` {..<k}. of_nat (Suc n - i))"
```
```    17       by (auto simp add: setprod.reindex)
```
```    18     also have "... = (\<Prod>i\<le>k. of_nat (Suc n - i))"
```
```    19     proof (cases k)
```
```    20       case (Suc k')
```
```    21       have "of_nat (n + 1) * (\<Prod>i\<in>Suc ` {..<Suc k'}. of_nat (Suc n - i)) = (\<Prod>i\<in>insert 0 (Suc ` {..k'}). of_nat (Suc n - i))"
```
```    22         by (subst setprod.insert) (auto simp add: lessThan_Suc_atMost)
```
```    23       also have "... = (\<Prod>i\<le>Suc k'. of_nat (Suc n - i))" by (simp only: Iic_Suc_eq_insert_0)
```
```    24       finally show ?thesis using Suc by simp
```
```    25     qed (simp)
```
```    26     also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i<k. of_nat (Suc n - i))"
```
```    27       by (cases k) (auto simp add: atMost_Suc lessThan_Suc_atMost)
```
```    28     also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
```
```    29       by (simp only: Suc_eq_plus1)
```
```    30     finally show ?thesis .
```
```    31   qed
```
```    32   then have "(\<Prod>i<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i<k. of_nat (Suc n - i))"
```
```    33     by (metis (no_types, lifting) le_add2 nonzero_mult_divide_cancel_left not_one_le_zero of_nat_eq_0_iff times_divide_eq_left)
```
```    34   from assms this show ?thesis
```
```    35     by (auto simp add: binomial_altdef_of_nat setprod_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>
```
```    44
```
```    45 lemma integrals_eq:
```
```    46   assumes "f 0 = g 0"
```
```    47   assumes "\<And> x. ((\<lambda>x. f x - g x) has_real_derivative 0) (at x)"
```
```    48   shows "f x = g x"
```
```    49 proof -
```
```    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
```
```    58 lemma setsum_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)
```
```    60
```
```    61 declare One_nat_def [simp del]
```
```    62
```
```    63 subsection \<open>Bernoulli Numbers and Bernoulli Polynomials\<close>
```
```    64
```
```    65 declare setsum.cong [fundef_cong]
```
```    66
```
```    67 fun bernoulli :: "nat \<Rightarrow> real"
```
```    68 where
```
```    69   "bernoulli 0 = (1::real)"
```
```    70 | "bernoulli (Suc n) =  (-1 / (n + 2)) * (\<Sum>k \<le> n. ((n + 2 choose k) * bernoulli k))"
```
```    71
```
```    72 declare bernoulli.simps[simp del]
```
```    73
```
```    74 definition
```
```    75   "bernpoly n = (\<lambda>x. \<Sum>k \<le> n. (n choose k) * bernoulli k * x ^ (n - k))"
```
```    76
```
```    77 subsection \<open>Basic Observations on Bernoulli Polynomials\<close>
```
```    78
```
```    79 lemma bernpoly_0: "bernpoly n 0 = bernoulli n"
```
```    80 proof (cases n)
```
```    81   case 0
```
```    82   then show "bernpoly n 0 = bernoulli n"
```
```    83     unfolding bernpoly_def bernoulli.simps by auto
```
```    84 next
```
```    85   case (Suc n')
```
```    86   have "(\<Sum>k\<le>n'. real (Suc n' choose k) * bernoulli k * 0 ^ (Suc n' - k)) = 0"
```
```    87     by (rule setsum.neutral) auto
```
```    88   with Suc show ?thesis
```
```    89     unfolding bernpoly_def by simp
```
```    90 qed
```
```    91
```
```    92 lemma setsum_binomial_times_bernoulli:
```
```    93   "(\<Sum>k\<le>n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)"
```
```    94 proof (cases n)
```
```    95   case 0
```
```    96   then show ?thesis by (simp add: bernoulli.simps)
```
```    97 next
```
```    98   case Suc
```
```    99   then show ?thesis
```
```   100   by (simp add: bernoulli.simps)
```
```   101     (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc')
```
```   102 qed
```
```   103
```
```   104 subsection \<open>Sum of Powers with Bernoulli Polynomials\<close>
```
```   105
```
```   106 lemma bernpoly_derivative [derivative_intros]:
```
```   107   "(bernpoly (Suc n) has_real_derivative ((n + 1) * bernpoly n x)) (at x)"
```
```   108 proof -
```
```   109   have "(bernpoly (Suc n) has_real_derivative (\<Sum>k\<le>n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k))) (at x)"
```
```   110     unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp)
```
```   111   moreover have "(\<Sum>k\<le>n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k)) = (n + 1) * bernpoly n x"
```
```   112     unfolding bernpoly_def
```
```   113     by (auto intro: setsum.cong simp add: setsum_right_distrib real_binomial_eq_mult_binomial_Suc[of _ n] Suc_eq_plus1 of_nat_diff)
```
```   114   ultimately show ?thesis by auto
```
```   115 qed
```
```   116
```
```   117 lemma diff_bernpoly:
```
```   118   "bernpoly n (x + 1) - bernpoly n x = n * x ^ (n - 1)"
```
```   119 proof (induct n arbitrary: x)
```
```   120   case 0
```
```   121   show ?case unfolding bernpoly_def by auto
```
```   122 next
```
```   123   case (Suc n)
```
```   124   have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = (Suc n) * 0 ^ n"
```
```   125     unfolding bernpoly_0 unfolding bernpoly_def by (simp add: setsum_binomial_times_bernoulli zero_power)
```
```   126   then have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = real (Suc n) * 0 ^ n" by (simp add: power_0_left)
```
```   127   have hyps': "\<And>x. (real n + 1) * bernpoly n (x + 1) - (real n + 1) * bernpoly n x = real n * x ^ (n - Suc 0) * real (Suc n)"
```
```   128     unfolding right_diff_distrib[symmetric] by (simp add: Suc.hyps One_nat_def)
```
```   129   note [derivative_intros] = DERIV_chain'[where f = "\<lambda>x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"]
```
```   130   have derivative: "\<And>x. ((%x. bernpoly (Suc n) (x + 1) - bernpoly (Suc n) x - real (Suc n) * x ^ n) has_real_derivative 0) (at x)"
```
```   131     by (rule DERIV_cong) (fast intro!: derivative_intros, simp add: hyps')
```
```   132   from integrals_eq[OF const derivative] show ?case by simp
```
```   133 qed
```
```   134
```
```   135 lemma sum_of_powers: "(\<Sum>k\<le>n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)"
```
```   136 proof -
```
```   137   from diff_bernpoly[of "Suc m", simplified] have "(m + (1::real)) * (\<Sum>k\<le>n. (real k) ^ m) = (\<Sum>k\<le>n. bernpoly (Suc m) (real k + 1) - bernpoly (Suc m) (real k))"
```
```   138     by (auto simp add: setsum_right_distrib intro!: setsum.cong)
```
```   139   also have "... = (\<Sum>k\<le>n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))"
```
```   140     by simp
```
```   141   also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0"
```
```   142     by (simp only: setsum_diff[where f="\<lambda>k. bernpoly (Suc m) (real k)"]) simp
```
```   143   finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp)
```
```   144 qed
```
```   145
```
```   146 subsection \<open>Instances for Square And Cubic Numbers\<close>
```
```   147
```
```   148 lemma binomial_unroll:
```
```   149   "n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
```
```   150 by (cases n) (auto simp add: binomial.simps(2))
```
```   151
```
```   152 lemma setsum_unroll:
```
```   153   "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
```
```   154 by auto (metis One_nat_def Suc_pred add.commute setsum_atMost_Suc)
```
```   155
```
```   156 lemma bernoulli_unroll:
```
```   157   "n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
```
```   158 by (cases n) (simp add: bernoulli.simps One_nat_def)+
```
```   159
```
```   160 lemmas unroll = binomial.simps(1) binomial_unroll
```
```   161   bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def
```
```   162
```
```   163 lemma sum_of_squares: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
```
```   164 proof -
```
```   165   have "real (\<Sum>k\<le>n::nat. k ^ 2) = (\<Sum>k\<le>n::nat. (real k) ^ 2)" by simp
```
```   166   also have "... = (bernpoly 3 (real (n + 1)) - bernpoly 3 0) / real (3 :: nat)"
```
```   167     by (auto simp add: sum_of_powers)
```
```   168   also have "... = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
```
```   169     by (simp add: unroll algebra_simps power2_eq_square power3_eq_cube One_nat_def[symmetric])
```
```   170   finally show ?thesis by simp
```
```   171 qed
```
```   172
```
```   173 lemma sum_of_squares_nat: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6"
```
```   174 proof -
```
```   175   from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
```
```   176     by (auto simp add: field_simps)
```
```   177   then have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
```
```   178     using of_nat_eq_iff by blast
```
```   179   then show ?thesis by auto
```
```   180 qed
```
```   181
```
```   182 lemma sum_of_cubes: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4"
```
```   183 proof -
```
```   184   have two_plus_two: "2 + 2 = 4" by simp
```
```   185   have power4_eq: "\<And>x::real. x ^ 4 = x * x * x * x"
```
```   186     by (simp only: two_plus_two[symmetric] power_add power2_eq_square)
```
```   187   have "real (\<Sum>k\<le>n::nat. k ^ 3) = (\<Sum>k\<le>n::nat. (real k) ^ 3)" by simp
```
```   188   also have "... = ((bernpoly 4 (n + 1) - bernpoly 4 0)) / (real (4 :: nat))"
```
```   189     by (auto simp add: sum_of_powers)
```
```   190   also have "... = ((n ^ 2 + n) / 2) ^ 2"
```
```   191     by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube)
```
```   192   finally show ?thesis by (simp add: power_divide)
```
```   193 qed
```
```   194
```
```   195 lemma sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
```
```   196 proof -
```
```   197   from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
```
```   198     by (auto simp add: field_simps)
```
```   199   then have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
```
```   200     using of_nat_eq_iff by blast
```
```   201   then show ?thesis by auto
```
```   202 qed
```
```   203
```
```   204 end
```