Some facts about factorial and binomial coefficients
authorManuel Eberl <eberlm@in.tum.de>
Thu Sep 01 11:53:07 2016 +0200 (2016-09-01)
changeset 63766695d60817cb1
parent 63729 89b6d339c6c4
child 63767 c2cbbd619f38
Some facts about factorial and binomial coefficients
src/HOL/Library/Discrete.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Library/Discrete.thy	Tue Aug 30 16:39:47 2016 +0200
     1.2 +++ b/src/HOL/Library/Discrete.thy	Thu Sep 01 11:53:07 2016 +0200
     1.3 @@ -132,7 +132,23 @@
     1.4    then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
     1.5  qed
     1.6  
     1.7 -lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
     1.8 +lemma sqrt_unique:
     1.9 +  assumes "m^2 \<le> n" "n < (Suc m)^2"
    1.10 +  shows   "Discrete.sqrt n = m"
    1.11 +proof -
    1.12 +  have "m' \<le> m" if "m'^2 \<le> n" for m'
    1.13 +  proof -
    1.14 +    note that
    1.15 +    also note assms(2)
    1.16 +    finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
    1.17 +    thus "m' \<le> m" by simp
    1.18 +  qed
    1.19 +  with \<open>m^2 \<le> n\<close> sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
    1.20 +    by (intro antisym Max.boundedI Max.coboundedI) simp_all
    1.21 +qed
    1.22 +
    1.23 +
    1.24 +lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
    1.25  proof -
    1.26    from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
    1.27    then show ?thesis by (simp add: sqrt_def Set.filter_def)
    1.28 @@ -161,6 +177,9 @@
    1.29      by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
    1.30  qed
    1.31  
    1.32 +lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
    1.33 +  using mono_sqrt unfolding mono_def by auto
    1.34 +
    1.35  lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
    1.36  proof -
    1.37    have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
     2.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Aug 30 16:39:47 2016 +0200
     2.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Sep 01 11:53:07 2016 +0200
     2.3 @@ -597,6 +597,23 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma prime_dvd_fact_iff:
     2.8 +  assumes "prime p"
     2.9 +  shows   "p dvd fact n \<longleftrightarrow> p \<le> n"
    2.10 +proof (induction n)
    2.11 +  case 0
    2.12 +  with assms show ?case by auto
    2.13 +next
    2.14 +  case (Suc n)
    2.15 +  have "p dvd fact (Suc n) \<longleftrightarrow> p dvd (Suc n) * fact n" by simp
    2.16 +  also from assms have "\<dots> \<longleftrightarrow> p dvd Suc n \<or> p dvd fact n"
    2.17 +    by (rule prime_dvd_mult_iff)
    2.18 +  also note Suc.IH
    2.19 +  also have "p dvd Suc n \<or> p \<le> n \<longleftrightarrow> p \<le> Suc n"
    2.20 +    by (auto dest: dvd_imp_le simp: le_Suc_eq)
    2.21 +  finally show ?case .
    2.22 +qed
    2.23 +
    2.24  (* TODO Legacy names *)
    2.25  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
    2.26  lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
     3.1 --- a/src/HOL/Transcendental.thy	Tue Aug 30 16:39:47 2016 +0200
     3.2 +++ b/src/HOL/Transcendental.thy	Thu Sep 01 11:53:07 2016 +0200
     3.3 @@ -71,6 +71,146 @@
     3.4      using z \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _  summable_geometric])
     3.5  qed
     3.6  
     3.7 +subsection \<open>More facts about binomial coefficients\<close>
     3.8 +
     3.9 +text \<open>
    3.10 +  These facts could have been proven before, but having real numbers 
    3.11 +  makes the proofs a lot easier.
    3.12 +\<close>
    3.13 +
    3.14 +lemma central_binomial_odd:
    3.15 +  "odd n \<Longrightarrow> n choose (Suc (n div 2)) = n choose (n div 2)"
    3.16 +proof -
    3.17 +  assume "odd n"
    3.18 +  hence "Suc (n div 2) \<le> n" by presburger
    3.19 +  hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
    3.20 +    by (rule binomial_symmetric)
    3.21 +  also from \<open>odd n\<close> have "n - Suc (n div 2) = n div 2" by presburger
    3.22 +  finally show ?thesis .
    3.23 +qed
    3.24 +
    3.25 +lemma binomial_less_binomial_Suc:
    3.26 +  assumes k: "k < n div 2"
    3.27 +  shows   "n choose k < n choose (Suc k)"
    3.28 +proof -
    3.29 +  from k have k': "k \<le> n" "Suc k \<le> n" by simp_all
    3.30 +  from k' have "real (n choose k) = fact n / (fact k * fact (n - k))"
    3.31 +    by (simp add: binomial_fact)
    3.32 +  also from k' have "n - k = Suc (n - Suc k)" by simp
    3.33 +  also from k' have "fact \<dots> = (real n - real k) * fact (n - Suc k)"
    3.34 +    by (subst fact_Suc) (simp_all add: of_nat_diff)
    3.35 +  also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps)
    3.36 +  also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) =
    3.37 +               (n choose (Suc k)) * ((real k + 1) / (real n - real k))"
    3.38 +    using k by (simp add: divide_simps binomial_fact)
    3.39 +  also from assms have "(real k + 1) / (real n - real k) < 1" by simp
    3.40 +  finally show ?thesis using k by (simp add: mult_less_cancel_left)
    3.41 +qed
    3.42 +
    3.43 +lemma binomial_strict_mono:
    3.44 +  assumes "k < k'" "2*k' \<le> n"
    3.45 +  shows   "n choose k < n choose k'"
    3.46 +proof -
    3.47 +  from assms have "k \<le> k' - 1" by simp
    3.48 +  thus ?thesis
    3.49 +  proof (induction rule: inc_induct)
    3.50 +    case base
    3.51 +    with assms binomial_less_binomial_Suc[of "k' - 1" n] 
    3.52 +      show ?case by simp
    3.53 +  next
    3.54 +    case (step k)
    3.55 +    from step.prems step.hyps assms have "n choose k < n choose (Suc k)" 
    3.56 +      by (intro binomial_less_binomial_Suc) simp_all
    3.57 +    also have "\<dots> < n choose k'" by (rule step.IH)
    3.58 +    finally show ?case .
    3.59 +  qed
    3.60 +qed
    3.61 +
    3.62 +lemma binomial_mono:
    3.63 +  assumes "k \<le> k'" "2*k' \<le> n"
    3.64 +  shows   "n choose k \<le> n choose k'"
    3.65 +  using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all
    3.66 +
    3.67 +lemma binomial_strict_antimono:
    3.68 +  assumes "k < k'" "2 * k \<ge> n" "k' \<le> n"
    3.69 +  shows   "n choose k > n choose k'"
    3.70 +proof -
    3.71 +  from assms have "n choose (n - k) > n choose (n - k')"
    3.72 +    by (intro binomial_strict_mono) (simp_all add: algebra_simps)
    3.73 +  with assms show ?thesis by (simp add: binomial_symmetric [symmetric])
    3.74 +qed
    3.75 +
    3.76 +lemma binomial_antimono:
    3.77 +  assumes "k \<le> k'" "k \<ge> n div 2" "k' \<le> n"
    3.78 +  shows   "n choose k \<ge> n choose k'"
    3.79 +proof (cases "k = k'")
    3.80 +  case False
    3.81 +  note not_eq = False
    3.82 +  show ?thesis
    3.83 +  proof (cases "k = n div 2 \<and> odd n")
    3.84 +    case False
    3.85 +    with assms(2) have "2*k \<ge> n" by presburger
    3.86 +    with not_eq assms binomial_strict_antimono[of k k' n] 
    3.87 +      show ?thesis by simp
    3.88 +  next
    3.89 +    case True
    3.90 +    have "n choose k' \<le> n choose (Suc (n div 2))"
    3.91 +    proof (cases "k' = Suc (n div 2)") 
    3.92 +      case False
    3.93 +      with assms True not_eq have "Suc (n div 2) < k'" by simp
    3.94 +      with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
    3.95 +        show ?thesis by auto
    3.96 +    qed simp_all
    3.97 +    also from True have "\<dots> = n choose k" by (simp add: central_binomial_odd)
    3.98 +    finally show ?thesis .
    3.99 +  qed
   3.100 +qed simp_all
   3.101 +
   3.102 +lemma binomial_maximum: "n choose k \<le> n choose (n div 2)"
   3.103 +proof -
   3.104 +  have "k \<le> n div 2 \<longleftrightarrow> 2*k \<le> n" by linarith
   3.105 +  consider "2*k \<le> n" | "2*k \<ge> n" "k \<le> n" | "k > n" by linarith
   3.106 +  thus ?thesis
   3.107 +  proof cases
   3.108 +    case 1
   3.109 +    thus ?thesis by (intro binomial_mono) linarith+
   3.110 +  next
   3.111 +    case 2
   3.112 +    thus ?thesis by (intro binomial_antimono) simp_all
   3.113 +  qed (simp_all add: binomial_eq_0)
   3.114 +qed
   3.115 +
   3.116 +lemma binomial_maximum': "(2*n) choose k \<le> (2*n) choose n"
   3.117 +  using binomial_maximum[of "2*n"] by simp
   3.118 +
   3.119 +lemma central_binomial_lower_bound:
   3.120 +  assumes "n > 0"
   3.121 +  shows   "4^n / (2*real n) \<le> real ((2*n) choose n)"
   3.122 +proof -
   3.123 +  from binomial[of 1 1 "2*n"]
   3.124 +    have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)"
   3.125 +    by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
   3.126 +  also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
   3.127 +  also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = 
   3.128 +               (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
   3.129 +    by (subst setsum.union_disjoint) auto
   3.130 +  also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" 
   3.131 +    by (cases n) simp_all
   3.132 +  also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
   3.133 +    by (intro setsum_mono3) auto
   3.134 +  also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
   3.135 +  also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
   3.136 +    by (intro setsum_mono binomial_maximum')
   3.137 +  also have "\<dots> = card {0<..<2*n} * ((2*n) choose n)" by simp
   3.138 +  also have "card {0<..<2*n} \<le> 2*n - 1" by (cases n) simp_all
   3.139 +  also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
   3.140 +    using assms by (simp add: algebra_simps)
   3.141 +  finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by - simp_all
   3.142 +  hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))"
   3.143 +    by (subst of_nat_le_iff)
   3.144 +  with assms show ?thesis by (simp add: field_simps)
   3.145 +qed
   3.146 +
   3.147  
   3.148  subsection \<open>Properties of Power Series\<close>
   3.149