src/HOL/ex/Sum_of_Powers.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 60603 09ecbd791d4a child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
 bulwahn@60603 ` 1` ```(* Title: HOL/ex/Sum_of_Powers.thy ``` bulwahn@60603 ` 2` ``` Author: Lukas Bulwahn ``` bulwahn@60603 ` 3` ```*) ``` bulwahn@60603 ` 4` bulwahn@60603 ` 5` ```section {* Sum of Powers *} ``` bulwahn@60603 ` 6` bulwahn@60603 ` 7` ```theory Sum_of_Powers ``` bulwahn@60603 ` 8` ```imports Complex_Main ``` bulwahn@60603 ` 9` ```begin ``` bulwahn@60603 ` 10` bulwahn@60603 ` 11` ```subsection {* Additions to @{theory Binomial} Theory *} ``` bulwahn@60603 ` 12` bulwahn@60603 ` 13` ```lemma of_nat_binomial_eq_mult_binomial_Suc: ``` bulwahn@60603 ` 14` ``` assumes "k \ n" ``` bulwahn@60603 ` 15` ``` shows "(of_nat :: (nat \ ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)" ``` bulwahn@60603 ` 16` ```proof - ``` bulwahn@60603 ` 17` ``` have "of_nat (n + 1) * (\i 'a)) (n + 1 - k) * (\ii 'a)) (n + 1) * (\i\Suc ` {..i\k. of_nat (Suc n - i))" ``` bulwahn@60603 ` 22` ``` proof (cases k) ``` bulwahn@60603 ` 23` ``` case (Suc k') ``` bulwahn@60603 ` 24` ``` have "of_nat (n + 1) * (\i\Suc ` {..i\insert 0 (Suc ` {..k'}). of_nat (Suc n - i))" ``` bulwahn@60603 ` 25` ``` by (subst setprod.insert) (auto simp add: lessThan_Suc_atMost) ``` bulwahn@60603 ` 26` ``` also have "... = (\i\Suc k'. of_nat (Suc n - i))" by (simp only: Iic_Suc_eq_insert_0) ``` bulwahn@60603 ` 27` ``` finally show ?thesis using Suc by simp ``` bulwahn@60603 ` 28` ``` qed (simp) ``` bulwahn@60603 ` 29` ``` also have "... = (of_nat :: (nat \ 'a)) (Suc n - k) * (\i 'a)) (n + 1 - k) * (\ii 'a)) (n + 1 - k) / of_nat (n + 1) * (\i n" ``` bulwahn@60603 ` 43` ``` shows "(n choose k) = (n + 1 - k) / (n + 1) * (Suc n choose k)" ``` bulwahn@60603 ` 44` ```proof - ``` bulwahn@60603 ` 45` ``` have "real (n choose k) = of_nat (n choose k)" by auto ``` bulwahn@60603 ` 46` ``` also have "... = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)" ``` bulwahn@60603 ` 47` ``` by (simp add: assms of_nat_binomial_eq_mult_binomial_Suc) ``` bulwahn@60603 ` 48` ``` also have "... = (n + 1 - k) / (n + 1) * (Suc n choose k)" ``` bulwahn@60603 ` 49` ``` using real_of_nat_def by auto ``` bulwahn@60603 ` 50` ``` finally show ?thesis ``` bulwahn@60603 ` 51` ``` by (metis (no_types, lifting) assms le_add1 le_trans of_nat_diff real_of_nat_1 real_of_nat_add real_of_nat_def) ``` bulwahn@60603 ` 52` ```qed ``` bulwahn@60603 ` 53` bulwahn@60603 ` 54` ```subsection {* Preliminaries *} ``` bulwahn@60603 ` 55` bulwahn@60603 ` 56` ```lemma integrals_eq: ``` bulwahn@60603 ` 57` ``` assumes "f 0 = g 0" ``` bulwahn@60603 ` 58` ``` assumes "\ x. ((\x. f x - g x) has_real_derivative 0) (at x)" ``` bulwahn@60603 ` 59` ``` shows "f x = g x" ``` bulwahn@60603 ` 60` ```proof - ``` bulwahn@60603 ` 61` ``` show "f x = g x" ``` bulwahn@60603 ` 62` ``` proof (cases "x \ 0") ``` bulwahn@60603 ` 63` ``` case True ``` bulwahn@60603 ` 64` ``` from assms DERIV_const_ratio_const[OF this, of "\x. f x - g x" 0] ``` bulwahn@60603 ` 65` ``` show ?thesis by auto ``` bulwahn@60603 ` 66` ``` qed (simp add: assms) ``` bulwahn@60603 ` 67` ```qed ``` bulwahn@60603 ` 68` bulwahn@60603 ` 69` ```lemma setsum_diff: "((\i\n::nat. f (i + 1) - f i)::'a::field) = f (n + 1) - f 0" ``` bulwahn@60603 ` 70` ```by (induct n) (auto simp add: field_simps) ``` bulwahn@60603 ` 71` bulwahn@60603 ` 72` ```declare One_nat_def [simp del] ``` bulwahn@60603 ` 73` bulwahn@60603 ` 74` ```subsection {* Bernoulli Numbers and Bernoulli Polynomials *} ``` bulwahn@60603 ` 75` bulwahn@60603 ` 76` ```declare setsum.cong [fundef_cong] ``` bulwahn@60603 ` 77` bulwahn@60603 ` 78` ```fun bernoulli :: "nat \ real" ``` bulwahn@60603 ` 79` ```where ``` bulwahn@60603 ` 80` ``` "bernoulli 0 = (1::real)" ``` bulwahn@60603 ` 81` ```| "bernoulli (Suc n) = (-1 / (n + 2)) * (\k \ n. ((n + 2 choose k) * bernoulli k))" ``` bulwahn@60603 ` 82` bulwahn@60603 ` 83` ```declare bernoulli.simps[simp del] ``` bulwahn@60603 ` 84` bulwahn@60603 ` 85` ```definition ``` bulwahn@60603 ` 86` ``` "bernpoly n = (\x. \k \ n. (n choose k) * bernoulli k * x ^ (n - k))" ``` bulwahn@60603 ` 87` bulwahn@60603 ` 88` ```subsection {* Basic Observations on Bernoulli Polynomials *} ``` bulwahn@60603 ` 89` bulwahn@60603 ` 90` ```lemma bernpoly_0: "bernpoly n 0 = bernoulli n" ``` bulwahn@60603 ` 91` ```proof (cases n) ``` bulwahn@60603 ` 92` ``` case 0 ``` bulwahn@60603 ` 93` ``` from this show "bernpoly n 0 = bernoulli n" ``` bulwahn@60603 ` 94` ``` unfolding bernpoly_def bernoulli.simps by auto ``` bulwahn@60603 ` 95` ```next ``` bulwahn@60603 ` 96` ``` case (Suc n') ``` bulwahn@60603 ` 97` ``` have "(\k\n'. real (Suc n' choose k) * bernoulli k * 0 ^ (Suc n' - k)) = 0" ``` bulwahn@60603 ` 98` ``` by (rule setsum.neutral) auto ``` bulwahn@60603 ` 99` ``` with Suc show ?thesis ``` bulwahn@60603 ` 100` ``` unfolding bernpoly_def by simp ``` bulwahn@60603 ` 101` ```qed ``` bulwahn@60603 ` 102` bulwahn@60603 ` 103` ```lemma setsum_binomial_times_bernoulli: ``` bulwahn@60603 ` 104` ``` "(\k\n. ((Suc n) choose k) * bernoulli k) = (if n = 0 then 1 else 0)" ``` bulwahn@60603 ` 105` ```proof (cases n) ``` bulwahn@60603 ` 106` ``` case 0 ``` bulwahn@60603 ` 107` ``` from this show ?thesis by (simp add: bernoulli.simps) ``` bulwahn@60603 ` 108` ```next ``` bulwahn@60603 ` 109` ``` case Suc ``` bulwahn@60603 ` 110` ``` from this show ?thesis ``` bulwahn@60603 ` 111` ``` by (simp add: bernoulli.simps) ``` bulwahn@60603 ` 112` ``` (simp add: field_simps add_2_eq_Suc'[symmetric] del: add_2_eq_Suc add_2_eq_Suc') ``` bulwahn@60603 ` 113` ```qed ``` bulwahn@60603 ` 114` bulwahn@60603 ` 115` ```subsection {* Sum of Powers with Bernoulli Polynomials *} ``` bulwahn@60603 ` 116` bulwahn@60603 ` 117` ```lemma bernpoly_derivative [derivative_intros]: ``` bulwahn@60603 ` 118` ``` "(bernpoly (Suc n) has_real_derivative ((n + 1) * bernpoly n x)) (at x)" ``` bulwahn@60603 ` 119` ```proof - ``` bulwahn@60603 ` 120` ``` have "(bernpoly (Suc n) has_real_derivative (\k\n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k))) (at x)" ``` bulwahn@60603 ` 121` ``` unfolding bernpoly_def by (rule DERIV_cong) (fast intro!: derivative_intros, simp) ``` bulwahn@60603 ` 122` ``` moreover have "(\k\n. real (Suc n - k) * x ^ (n - k) * (real (Suc n choose k) * bernoulli k)) = (n + 1) * bernpoly n x" ``` bulwahn@60603 ` 123` ``` unfolding bernpoly_def ``` bulwahn@60603 ` 124` ``` by (auto intro: setsum.cong simp add: setsum_right_distrib real_binomial_eq_mult_binomial_Suc[of _ n] Suc_eq_plus1 real_of_nat_diff) ``` bulwahn@60603 ` 125` ``` ultimately show ?thesis by auto ``` bulwahn@60603 ` 126` ```qed ``` bulwahn@60603 ` 127` bulwahn@60603 ` 128` ```lemma diff_bernpoly: ``` bulwahn@60603 ` 129` ``` "bernpoly n (x + 1) - bernpoly n x = n * x ^ (n - 1)" ``` bulwahn@60603 ` 130` ```proof (induct n arbitrary: x) ``` bulwahn@60603 ` 131` ``` case 0 ``` bulwahn@60603 ` 132` ``` show ?case unfolding bernpoly_def by auto ``` bulwahn@60603 ` 133` ```next ``` bulwahn@60603 ` 134` ``` case (Suc n) ``` bulwahn@60603 ` 135` ``` have "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = (Suc n) * 0 ^ n" ``` bulwahn@60603 ` 136` ``` unfolding bernpoly_0 unfolding bernpoly_def by (simp add: setsum_binomial_times_bernoulli zero_power) ``` bulwahn@60603 ` 137` ``` from this have const: "bernpoly (Suc n) (0 + 1) - bernpoly (Suc n) 0 = real (Suc n) * 0 ^ n" by (simp add: power_0_left) ``` bulwahn@60603 ` 138` ``` have hyps': "\x. (real n + 1) * bernpoly n (x + 1) - (real n + 1) * bernpoly n x = real n * x ^ (n - Suc 0) * real (Suc n)" ``` bulwahn@60603 ` 139` ``` unfolding right_diff_distrib[symmetric] by (simp add: Suc.hyps One_nat_def) ``` bulwahn@60603 ` 140` ``` note [derivative_intros] = DERIV_chain'[where f = "\x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"] ``` bulwahn@60603 ` 141` ``` have derivative: "\x. ((%x. bernpoly (Suc n) (x + 1) - bernpoly (Suc n) x - real (Suc n) * x ^ n) has_real_derivative 0) (at x)" ``` bulwahn@60603 ` 142` ``` by (rule DERIV_cong) (fast intro!: derivative_intros, simp add: hyps') ``` bulwahn@60603 ` 143` ``` from integrals_eq[OF const derivative] show ?case by simp ``` bulwahn@60603 ` 144` ```qed ``` bulwahn@60603 ` 145` bulwahn@60603 ` 146` ```lemma sum_of_powers: "(\k\n::nat. (real k) ^ m) = (bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0) / (m + 1)" ``` bulwahn@60603 ` 147` ```proof - ``` bulwahn@60603 ` 148` ``` from diff_bernpoly[of "Suc m", simplified] have "(m + (1::real)) * (\k\n. (real k) ^ m) = (\k\n. bernpoly (Suc m) (real k + 1) - bernpoly (Suc m) (real k))" ``` bulwahn@60603 ` 149` ``` by (auto simp add: setsum_right_distrib intro!: setsum.cong) ``` bulwahn@60603 ` 150` ``` also have "... = (\k\n. bernpoly (Suc m) (real (k + 1)) - bernpoly (Suc m) (real k))" ``` bulwahn@60603 ` 151` ``` by (simp only: real_of_nat_1[symmetric] real_of_nat_add[symmetric]) ``` bulwahn@60603 ` 152` ``` also have "... = bernpoly (Suc m) (n + 1) - bernpoly (Suc m) 0" ``` bulwahn@60603 ` 153` ``` by (simp only: setsum_diff[where f="\k. bernpoly (Suc m) (real k)"]) simp ``` bulwahn@60603 ` 154` ``` finally show ?thesis by (auto simp add: field_simps intro!: eq_divide_imp) ``` bulwahn@60603 ` 155` ```qed ``` bulwahn@60603 ` 156` bulwahn@60603 ` 157` ```subsection {* Instances for Square And Cubic Numbers *} ``` bulwahn@60603 ` 158` bulwahn@60603 ` 159` ```lemma binomial_unroll: ``` bulwahn@60603 ` 160` ``` "n > 0 \ (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))" ``` bulwahn@60603 ` 161` ```by (cases n) (auto simp add: binomial.simps(2)) ``` bulwahn@60603 ` 162` bulwahn@60603 ` 163` ```lemma setsum_unroll: ``` bulwahn@60603 ` 164` ``` "(\k\n::nat. f k) = (if n = 0 then f 0 else f n + (\k\n - 1. f k))" ``` bulwahn@60603 ` 165` ```by auto (metis One_nat_def Suc_pred add.commute setsum_atMost_Suc) ``` bulwahn@60603 ` 166` bulwahn@60603 ` 167` ```lemma bernoulli_unroll: ``` bulwahn@60603 ` 168` ``` "n > 0 \ bernoulli n = - 1 / (real n + 1) * (\k\n - 1. real (n + 1 choose k) * bernoulli k)" ``` bulwahn@60603 ` 169` ```by (cases n) (simp add: bernoulli.simps One_nat_def)+ ``` bulwahn@60603 ` 170` bulwahn@60603 ` 171` ```lemmas unroll = binomial.simps(1) binomial_unroll ``` bulwahn@60603 ` 172` ``` bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def ``` bulwahn@60603 ` 173` bulwahn@60603 ` 174` ```lemma sum_of_squares: "(\k\n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6" ``` bulwahn@60603 ` 175` ```proof - ``` bulwahn@60603 ` 176` ``` have "real (\k\n::nat. k ^ 2) = (\k\n::nat. (real k) ^ 2)" by simp ``` bulwahn@60603 ` 177` ``` also have "... = (bernpoly 3 (real (n + 1)) - bernpoly 3 0) / real (3 :: nat)" ``` bulwahn@60603 ` 178` ``` by (auto simp add: sum_of_powers) ``` bulwahn@60603 ` 179` ``` also have "... = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6" ``` bulwahn@60603 ` 180` ``` by (simp add: unroll algebra_simps power2_eq_square power3_eq_cube One_nat_def[symmetric]) ``` bulwahn@60603 ` 181` ``` finally show ?thesis by simp ``` bulwahn@60603 ` 182` ```qed ``` bulwahn@60603 ` 183` bulwahn@60603 ` 184` ```lemma sum_of_squares_nat: "(\k\n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6" ``` bulwahn@60603 ` 185` ```proof - ``` bulwahn@60603 ` 186` ``` from sum_of_squares have "real (6 * (\k\n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)" ``` bulwahn@60603 ` 187` ``` by (auto simp add: field_simps) ``` bulwahn@60603 ` 188` ``` from this have "6 * (\k\n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n" ``` bulwahn@60603 ` 189` ``` by (simp only: real_of_nat_inject[symmetric]) ``` bulwahn@60603 ` 190` ``` from this show ?thesis by auto ``` bulwahn@60603 ` 191` ```qed ``` bulwahn@60603 ` 192` bulwahn@60603 ` 193` ```lemma sum_of_cubes: "(\k\n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4" ``` bulwahn@60603 ` 194` ```proof - ``` bulwahn@60603 ` 195` ``` have two_plus_two: "2 + 2 = 4" by simp ``` bulwahn@60603 ` 196` ``` have power4_eq: "\x::real. x ^ 4 = x * x * x * x" ``` bulwahn@60603 ` 197` ``` by (simp only: two_plus_two[symmetric] power_add power2_eq_square) ``` bulwahn@60603 ` 198` ``` have "real (\k\n::nat. k ^ 3) = (\k\n::nat. (real k) ^ 3)" by simp ``` bulwahn@60603 ` 199` ``` also have "... = ((bernpoly 4 (n + 1) - bernpoly 4 0)) / (real (4 :: nat))" ``` bulwahn@60603 ` 200` ``` by (auto simp add: sum_of_powers) ``` bulwahn@60603 ` 201` ``` also have "... = ((n ^ 2 + n) / 2) ^ 2" ``` bulwahn@60603 ` 202` ``` by (simp add: unroll algebra_simps power2_eq_square power4_eq power3_eq_cube) ``` bulwahn@60603 ` 203` ``` finally show ?thesis by simp ``` bulwahn@60603 ` 204` ```qed ``` bulwahn@60603 ` 205` bulwahn@60603 ` 206` ```lemma sum_of_cubes_nat: "(\k\n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4" ``` bulwahn@60603 ` 207` ```proof - ``` bulwahn@60603 ` 208` ``` from sum_of_cubes have "real (4 * (\k\n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)" ``` bulwahn@60603 ` 209` ``` by (auto simp add: field_simps) ``` bulwahn@60603 ` 210` ``` from this have "4 * (\k\n. k ^ 3) = (n ^ 2 + n) ^ 2" ``` bulwahn@60603 ` 211` ``` by (simp only: real_of_nat_inject[symmetric]) ``` bulwahn@60603 ` 212` ``` from this show ?thesis by auto ``` bulwahn@60603 ` 213` ```qed ``` bulwahn@60603 ` 214` bulwahn@60603 ` 215` ```end ```