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