author paulson Mon Mar 17 15:48:30 2014 +0000 (2014-03-17) changeset 56178 2a6f58938573 parent 56177 bfa9dfb722de child 56179 6b5c46582260
a few new theorems
 src/HOL/Number_Theory/Binomial.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions
```     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.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.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"
```