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 <lukas.bulwahn-at-gmail.com>
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 \<le> n"
bulwahn@60603
    15
  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)"
bulwahn@60603
    16
proof -
bulwahn@60603
    17
  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))"
bulwahn@60603
    18
  proof -
bulwahn@60603
    19
    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))"
bulwahn@60603
    20
      by (auto simp add: setprod.reindex)
bulwahn@60603
    21
    also have "... = (\<Prod>i\<le>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) * (\<Prod>i\<in>Suc ` {..<Suc k'}. of_nat (Suc n - i)) = (\<Prod>i\<in>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 "... = (\<Prod>i\<le>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 \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i<k. of_nat (Suc n - i))"
bulwahn@60603
    30
      by (cases k) (auto simp add: atMost_Suc lessThan_Suc_atMost)
bulwahn@60603
    31
    also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i<k. of_nat (Suc n - i))"
bulwahn@60603
    32
      by (simp only: Suc_eq_plus1)
bulwahn@60603
    33
    finally show ?thesis .
bulwahn@60603
    34
  qed
bulwahn@60603
    35
  from this 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))"
bulwahn@60603
    36
    by (metis le_add2 nonzero_mult_divide_cancel_left not_one_le_zero of_nat_eq_0_iff times_divide_eq_left)
bulwahn@60603
    37
  from assms this show ?thesis
bulwahn@60603
    38
    by (auto simp add: binomial_altdef_of_nat setprod_dividef)
bulwahn@60603
    39
qed
bulwahn@60603
    40
bulwahn@60603
    41
lemma real_binomial_eq_mult_binomial_Suc:
bulwahn@60603
    42
  assumes "k \<le> 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 "\<And> x. ((\<lambda>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 \<noteq> 0")
bulwahn@60603
    63
    case True
bulwahn@60603
    64
    from assms DERIV_const_ratio_const[OF this, of "\<lambda>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: "((\<Sum>i\<le>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 \<Rightarrow> real"
bulwahn@60603
    79
where
bulwahn@60603
    80
  "bernoulli 0 = (1::real)"
bulwahn@60603
    81
| "bernoulli (Suc n) =  (-1 / (n + 2)) * (\<Sum>k \<le> 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 = (\<lambda>x. \<Sum>k \<le> 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 "(\<Sum>k\<le>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
  "(\<Sum>k\<le>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 (\<Sum>k\<le>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 "(\<Sum>k\<le>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': "\<And>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 = "\<lambda>x::real. x + 1" and g = "bernpoly (Suc n)" and s="UNIV"]
bulwahn@60603
   141
  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)"
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: "(\<Sum>k\<le>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)) * (\<Sum>k\<le>n. (real k) ^ m) = (\<Sum>k\<le>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 "... = (\<Sum>k\<le>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="\<lambda>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 \<Longrightarrow> (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
  "(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>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 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>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: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"
bulwahn@60603
   175
proof -
bulwahn@60603
   176
  have "real (\<Sum>k\<le>n::nat. k ^ 2) = (\<Sum>k\<le>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: "(\<Sum>k\<le>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 * (\<Sum>k\<le>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 * (\<Sum>k\<le>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: "(\<Sum>k\<le>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: "\<And>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 (\<Sum>k\<le>n::nat. k ^ 3) = (\<Sum>k\<le>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: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
bulwahn@60603
   207
proof -
bulwahn@60603
   208
  from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
bulwahn@60603
   209
    by (auto simp add: field_simps)
bulwahn@60603
   210
  from this have "4 * (\<Sum>k\<le>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