add binomial_ge_n_over_k_pow_k
authorhoelzl
Mon Nov 26 14:11:31 2012 +0100 (2012-11-26)
changeset 50224aacd6da09825
parent 50223 bcbdf2179880
child 50225 f478f4ca7f19
add binomial_ge_n_over_k_pow_k
src/HOL/Fact.thy
src/HOL/Library/Binomial.thy
     1.1 --- a/src/HOL/Fact.thy	Mon Nov 26 13:50:25 2012 +0100
     1.2 +++ b/src/HOL/Fact.thy	Mon Nov 26 14:11:31 2012 +0100
     1.3 @@ -306,4 +306,13 @@
     1.4  lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
     1.5  by (auto intro: order_less_imp_le)
     1.6  
     1.7 +lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
     1.8 +  unfolding fact_altdef_nat
     1.9 +proof (rule strong_setprod_reindex_cong)
    1.10 +  { fix i assume "Suc 0 \<le> i" "i \<le> k" then have "\<exists>j\<in>{..<k}. i = k - j"
    1.11 +      by (intro bexI[of _ "k - i"]) simp_all }
    1.12 +  then show "{1..k} = (\<lambda>i. k - i) ` {..<k}"
    1.13 +    by (auto simp: image_iff)
    1.14 +qed (auto intro: inj_onI)
    1.15 +
    1.16  end
     2.1 --- a/src/HOL/Library/Binomial.thy	Mon Nov 26 13:50:25 2012 +0100
     2.2 +++ b/src/HOL/Library/Binomial.thy	Mon Nov 26 14:11:31 2012 +0100
     2.3 @@ -537,4 +537,42 @@
     2.4    then show ?thesis using kn by simp
     2.5  qed
     2.6  
     2.7 +(* Contributed by Manuel Eberl *)
     2.8 +(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *)
     2.9 +lemma binomial_altdef_of_nat:
    2.10 +  fixes n k :: nat and x :: "'a :: {field_char_0, field_inverse_zero}"
    2.11 +  assumes "k \<le> n" shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
    2.12 +proof cases
    2.13 +  assume "0 < k"
    2.14 +  then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n - of_nat i) / of_nat (fact k)"
    2.15 +    unfolding binomial_gbinomial gbinomial_def
    2.16 +    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
    2.17 +  also have "\<dots> = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
    2.18 +    using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod
    2.19 +    by (auto simp add: setprod_dividef intro!: setprod_cong of_nat_diff[symmetric])
    2.20 +  finally show ?thesis .
    2.21 +qed simp
    2.22 +
    2.23 +lemma binomial_ge_n_over_k_pow_k:
    2.24 +  fixes k n :: nat and x :: "'a :: linordered_field_inverse_zero"
    2.25 +  assumes "0 < k" and "k \<le> n" shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
    2.26 +proof -
    2.27 +  have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)"
    2.28 +    by (simp add: setprod_constant)
    2.29 +  also have "\<dots> \<le> of_nat (n choose k)"
    2.30 +    unfolding binomial_altdef_of_nat[OF `k\<le>n`]
    2.31 +  proof (safe intro!: setprod_mono)
    2.32 +    fix i::nat  assume  "i < k"
    2.33 +    from assms have "n * i \<ge> i * k" by simp
    2.34 +    hence "n * k - n * i \<le> n * k - i * k" by arith
    2.35 +    hence "n * (k - i) \<le> (n - i) * k"
    2.36 +      by (simp add: diff_mult_distrib2 nat_mult_commute)
    2.37 +    hence "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)"
    2.38 +      unfolding of_nat_mult[symmetric] of_nat_le_iff .
    2.39 +    with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)"
    2.40 +      using `i < k` by (simp add: field_simps)
    2.41 +  qed (simp add: zero_le_divide_iff)
    2.42 +  finally show ?thesis .
    2.43 +qed
    2.44 +
    2.45  end