# HG changeset patch
# User hoelzl
# Date 1353935491 -3600
# Node ID aacd6da0982584d0e1eb6f6b54179abc181aea39
# Parent  bcbdf217988008e5911bb38e3c94f5ebab1902b2
add binomial_ge_n_over_k_pow_k

diff -r bcbdf2179880 -r aacd6da09825 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Mon Nov 26 13:50:25 2012 +0100
+++ b/src/HOL/Fact.thy	Mon Nov 26 14:11:31 2012 +0100
@@ -306,4 +306,13 @@
 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
 by (auto intro: order_less_imp_le)
 
+lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
+  unfolding fact_altdef_nat
+proof (rule strong_setprod_reindex_cong)
+  { fix i assume "Suc 0 \<le> i" "i \<le> k" then have "\<exists>j\<in>{..<k}. i = k - j"
+      by (intro bexI[of _ "k - i"]) simp_all }
+  then show "{1..k} = (\<lambda>i. k - i) ` {..<k}"
+    by (auto simp: image_iff)
+qed (auto intro: inj_onI)
+
 end
diff -r bcbdf2179880 -r aacd6da09825 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Nov 26 13:50:25 2012 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Nov 26 14:11:31 2012 +0100
@@ -537,4 +537,42 @@
   then show ?thesis using kn by simp
 qed
 
+(* Contributed by Manuel Eberl *)
+(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *)
+lemma binomial_altdef_of_nat:
+  fixes n k :: nat and x :: "'a :: {field_char_0, field_inverse_zero}"
+  assumes "k \<le> n" shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
+proof cases
+  assume "0 < k"
+  then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n - of_nat i) / of_nat (fact k)"
+    unfolding binomial_gbinomial gbinomial_def
+    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
+  also have "\<dots> = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
+    using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod
+    by (auto simp add: setprod_dividef intro!: setprod_cong of_nat_diff[symmetric])
+  finally show ?thesis .
+qed simp
+
+lemma binomial_ge_n_over_k_pow_k:
+  fixes k n :: nat and x :: "'a :: linordered_field_inverse_zero"
+  assumes "0 < k" and "k \<le> n" shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
+proof -
+  have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)"
+    by (simp add: setprod_constant)
+  also have "\<dots> \<le> of_nat (n choose k)"
+    unfolding binomial_altdef_of_nat[OF `k\<le>n`]
+  proof (safe intro!: setprod_mono)
+    fix i::nat  assume  "i < k"
+    from assms have "n * i \<ge> i * k" by simp
+    hence "n * k - n * i \<le> n * k - i * k" by arith
+    hence "n * (k - i) \<le> (n - i) * k"
+      by (simp add: diff_mult_distrib2 nat_mult_commute)
+    hence "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)"
+      unfolding of_nat_mult[symmetric] of_nat_le_iff .
+    with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)"
+      using `i < k` by (simp add: field_simps)
+  qed (simp add: zero_le_divide_iff)
+  finally show ?thesis .
+qed
+
 end