a few new theorems
authorpaulson <lp15@cam.ac.uk>
Mon Mar 17 15:48:30 2014 +0000 (2014-03-17)
changeset 561782a6f58938573
parent 56177 bfa9dfb722de
child 56179 6b5c46582260
a few new theorems
src/HOL/Number_Theory/Binomial.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 14:40:59 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 15:48:30 2014 +0000
     1.3 @@ -186,6 +186,37 @@
     1.4             of_nat_setsum [symmetric]
     1.5             of_nat_eq_iff of_nat_id)
     1.6  
     1.7 +lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
     1.8 +  using binomial [of 1 "1" n]
     1.9 +  by (simp add: numeral_2_eq_2)
    1.10 +
    1.11 +lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
    1.12 +  by (induct n) auto
    1.13 +
    1.14 +lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
    1.15 +  by (induct n) auto
    1.16 +
    1.17 +lemma natsum_reverse_index:
    1.18 +  fixes m::nat
    1.19 +  assumes "\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)"
    1.20 +  shows "(\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
    1.21 +apply (rule setsum_reindex_cong [where f = "\<lambda>k. m+n-k"])
    1.22 +apply (auto simp add: inj_on_def image_def)
    1.23 +apply (rule_tac x="m+n-x" in bexI, auto simp: assms)
    1.24 +done
    1.25 +
    1.26 +lemma sum_choose_diagonal:
    1.27 +  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
    1.28 +proof -
    1.29 +  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
    1.30 +    by (rule natsum_reverse_index) (simp add: assms)
    1.31 +  also have "... = Suc (n-m+m) choose m"
    1.32 +    by (rule sum_choose_lower)
    1.33 +  also have "... = Suc n choose m" using assms
    1.34 +    by simp
    1.35 +  finally show ?thesis .
    1.36 +qed
    1.37 +
    1.38  subsection{* Pochhammer's symbol : generalized rising factorial *}
    1.39  
    1.40  text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
    1.41 @@ -605,6 +636,42 @@
    1.42      n choose k = fact n div (fact k * fact (n - k))"
    1.43   by (subst binomial_fact_lemma [symmetric]) auto
    1.44  
    1.45 +lemma fact_fact_dvd_fact_m: fixes k::nat shows "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
    1.46 +  by (metis binomial_fact_lemma dvd_def)
    1.47 +
    1.48 +lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
    1.49 +  by (metis fact_fact_dvd_fact_m diff_add_inverse2 le_add2)
    1.50 +
    1.51 +lemma choose_mult_lemma:
    1.52 +     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
    1.53 +proof -
    1.54 +  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
    1.55 +        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
    1.56 +    by (simp add: assms binomial_altdef_nat)
    1.57 +  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
    1.58 +    apply (subst div_mult_div_if_dvd)
    1.59 +    apply (auto simp: fact_fact_dvd_fact)
    1.60 +    apply (metis ab_semigroup_add_class.add_ac(1) add_commute fact_fact_dvd_fact)
    1.61 +    done
    1.62 +  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
    1.63 +    apply (subst div_mult_div_if_dvd [symmetric])
    1.64 +    apply (auto simp: fact_fact_dvd_fact)
    1.65 +    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult_left_commute)
    1.66 +    done
    1.67 +  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
    1.68 +    apply (subst div_mult_div_if_dvd)
    1.69 +    apply (auto simp: fact_fact_dvd_fact)
    1.70 +    apply(metis mult_left_commute)
    1.71 +    done
    1.72 +  finally show ?thesis
    1.73 +    by (simp add: binomial_altdef_nat mult_commute)
    1.74 +qed
    1.75 +
    1.76 +lemma choose_mult:
    1.77 +  assumes "k\<le>m" "m\<le>n"
    1.78 +    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
    1.79 +using assms choose_mult_lemma [of "m-k" "n-m" k]
    1.80 +by simp
    1.81  
    1.82  
    1.83  subsection {* Binomial coefficients *}
     2.1 --- a/src/HOL/Series.thy	Mon Mar 17 14:40:59 2014 +0100
     2.2 +++ b/src/HOL/Series.thy	Mon Mar 17 15:48:30 2014 +0000
     2.3 @@ -562,6 +562,22 @@
     2.4  apply simp
     2.5  done
     2.6  
     2.7 +lemma norm_bound_subset:
     2.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     2.9 +  assumes "finite s" "t \<subseteq> s"
    2.10 +  assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)"
    2.11 +  shows "norm (setsum f t) \<le> setsum g s"
    2.12 +proof -
    2.13 +  have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))"
    2.14 +    by (rule norm_setsum)
    2.15 +  also have "\<dots> \<le> (\<Sum>i\<in>t. g i)"
    2.16 +    using assms by (auto intro!: setsum_mono)
    2.17 +  also have "\<dots> \<le> setsum g s"
    2.18 +    using assms order.trans[OF norm_ge_zero le]
    2.19 +    by (auto intro!: setsum_mono3)
    2.20 +  finally show ?thesis .
    2.21 +qed
    2.22 +
    2.23  lemma summable_comparison_test:
    2.24    fixes f :: "nat \<Rightarrow> 'a::banach"
    2.25    shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"