# HG changeset patch # User Manuel Eberl # Date 1472723587 -7200 # Node ID 695d60817cb11eb1179781c8beecacaf465500df # Parent 89b6d339c6c4a5b9a179b4cae760c63af544bec4 Some facts about factorial and binomial coefficients diff -r 89b6d339c6c4 -r 695d60817cb1 src/HOL/Library/Discrete.thy --- a/src/HOL/Library/Discrete.thy Tue Aug 30 16:39:47 2016 +0200 +++ b/src/HOL/Library/Discrete.thy Thu Sep 01 11:53:07 2016 +0200 @@ -132,7 +132,23 @@ then show *: "{m. m\<^sup>2 \ n} \ {}" by blast qed -lemma [code]: "sqrt n = Max (Set.filter (\m. m\<^sup>2 \ n) {0..n})" +lemma sqrt_unique: + assumes "m^2 \ n" "n < (Suc m)^2" + shows "Discrete.sqrt n = m" +proof - + have "m' \ m" if "m'^2 \ n" for m' + proof - + note that + also note assms(2) + finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all + thus "m' \ m" by simp + qed + with \m^2 \ n\ sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def + by (intro antisym Max.boundedI Max.coboundedI) simp_all +qed + + +lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\m. m\<^sup>2 \ n) {0..n})" proof - from power2_nat_le_imp_le [of _ n] have "{m. m \ n \ m\<^sup>2 \ n} = {m. m\<^sup>2 \ n}" by auto then show ?thesis by (simp add: sqrt_def Set.filter_def) @@ -161,6 +177,9 @@ by (auto intro!: Max_mono \0 * 0 \ m\ finite_less_ub simp add: power2_eq_square sqrt_def) qed +lemma mono_sqrt': "m \ n \ Discrete.sqrt m \ Discrete.sqrt n" + using mono_sqrt unfolding mono_def by auto + lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \ n > 0" proof - have *: "0 < Max {m. m\<^sup>2 \ n} \ (\a\{m. m\<^sup>2 \ n}. 0 < a)" diff -r 89b6d339c6c4 -r 695d60817cb1 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Tue Aug 30 16:39:47 2016 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Thu Sep 01 11:53:07 2016 +0200 @@ -597,6 +597,23 @@ finally show ?thesis . qed +lemma prime_dvd_fact_iff: + assumes "prime p" + shows "p dvd fact n \ p \ n" +proof (induction n) + case 0 + with assms show ?case by auto +next + case (Suc n) + have "p dvd fact (Suc n) \ p dvd (Suc n) * fact n" by simp + also from assms have "\ \ p dvd Suc n \ p dvd fact n" + by (rule prime_dvd_mult_iff) + also note Suc.IH + also have "p dvd Suc n \ p \ n \ p \ Suc n" + by (auto dest: dvd_imp_le simp: le_Suc_eq) + finally show ?case . +qed + (* TODO Legacy names *) lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat] lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int] diff -r 89b6d339c6c4 -r 695d60817cb1 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Aug 30 16:39:47 2016 +0200 +++ b/src/HOL/Transcendental.thy Thu Sep 01 11:53:07 2016 +0200 @@ -71,6 +71,146 @@ using z \0 \ x\ by (auto intro!: summable_comparison_test[OF _ summable_geometric]) qed +subsection \More facts about binomial coefficients\ + +text \ + These facts could have been proven before, but having real numbers + makes the proofs a lot easier. +\ + +lemma central_binomial_odd: + "odd n \ n choose (Suc (n div 2)) = n choose (n div 2)" +proof - + assume "odd n" + hence "Suc (n div 2) \ n" by presburger + hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))" + by (rule binomial_symmetric) + also from \odd n\ have "n - Suc (n div 2) = n div 2" by presburger + finally show ?thesis . +qed + +lemma binomial_less_binomial_Suc: + assumes k: "k < n div 2" + shows "n choose k < n choose (Suc k)" +proof - + from k have k': "k \ n" "Suc k \ n" by simp_all + from k' have "real (n choose k) = fact n / (fact k * fact (n - k))" + by (simp add: binomial_fact) + also from k' have "n - k = Suc (n - Suc k)" by simp + also from k' have "fact \ = (real n - real k) * fact (n - Suc k)" + by (subst fact_Suc) (simp_all add: of_nat_diff) + also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps) + also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) = + (n choose (Suc k)) * ((real k + 1) / (real n - real k))" + using k by (simp add: divide_simps binomial_fact) + also from assms have "(real k + 1) / (real n - real k) < 1" by simp + finally show ?thesis using k by (simp add: mult_less_cancel_left) +qed + +lemma binomial_strict_mono: + assumes "k < k'" "2*k' \ n" + shows "n choose k < n choose k'" +proof - + from assms have "k \ k' - 1" by simp + thus ?thesis + proof (induction rule: inc_induct) + case base + with assms binomial_less_binomial_Suc[of "k' - 1" n] + show ?case by simp + next + case (step k) + from step.prems step.hyps assms have "n choose k < n choose (Suc k)" + by (intro binomial_less_binomial_Suc) simp_all + also have "\ < n choose k'" by (rule step.IH) + finally show ?case . + qed +qed + +lemma binomial_mono: + assumes "k \ k'" "2*k' \ n" + shows "n choose k \ n choose k'" + using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all + +lemma binomial_strict_antimono: + assumes "k < k'" "2 * k \ n" "k' \ n" + shows "n choose k > n choose k'" +proof - + from assms have "n choose (n - k) > n choose (n - k')" + by (intro binomial_strict_mono) (simp_all add: algebra_simps) + with assms show ?thesis by (simp add: binomial_symmetric [symmetric]) +qed + +lemma binomial_antimono: + assumes "k \ k'" "k \ n div 2" "k' \ n" + shows "n choose k \ n choose k'" +proof (cases "k = k'") + case False + note not_eq = False + show ?thesis + proof (cases "k = n div 2 \ odd n") + case False + with assms(2) have "2*k \ n" by presburger + with not_eq assms binomial_strict_antimono[of k k' n] + show ?thesis by simp + next + case True + have "n choose k' \ n choose (Suc (n div 2))" + proof (cases "k' = Suc (n div 2)") + case False + with assms True not_eq have "Suc (n div 2) < k'" by simp + with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True + show ?thesis by auto + qed simp_all + also from True have "\ = n choose k" by (simp add: central_binomial_odd) + finally show ?thesis . + qed +qed simp_all + +lemma binomial_maximum: "n choose k \ n choose (n div 2)" +proof - + have "k \ n div 2 \ 2*k \ n" by linarith + consider "2*k \ n" | "2*k \ n" "k \ n" | "k > n" by linarith + thus ?thesis + proof cases + case 1 + thus ?thesis by (intro binomial_mono) linarith+ + next + case 2 + thus ?thesis by (intro binomial_antimono) simp_all + qed (simp_all add: binomial_eq_0) +qed + +lemma binomial_maximum': "(2*n) choose k \ (2*n) choose n" + using binomial_maximum[of "2*n"] by simp + +lemma central_binomial_lower_bound: + assumes "n > 0" + shows "4^n / (2*real n) \ real ((2*n) choose n)" +proof - + from binomial[of 1 1 "2*n"] + have "4 ^ n = (\k=0..2*n. (2*n) choose k)" + by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def) + also have "{0..2*n} = {0<..<2*n} \ {0,2*n}" by auto + also have "(\k\\. (2*n) choose k) = + (\k\{0<..<2*n}. (2*n) choose k) + (\k\{0,2*n}. (2*n) choose k)" + by (subst setsum.union_disjoint) auto + also have "(\k\{0,2*n}. (2*n) choose k) \ (\k\1. (n choose k)\<^sup>2)" + by (cases n) simp_all + also from assms have "\ \ (\k\n. (n choose k)\<^sup>2)" + by (intro setsum_mono3) auto + also have "\ = (2*n) choose n" by (rule choose_square_sum) + also have "(\k\{0<..<2*n}. (2*n) choose k) \ (\k\{0<..<2*n}. (2*n) choose n)" + by (intro setsum_mono binomial_maximum') + also have "\ = card {0<..<2*n} * ((2*n) choose n)" by simp + also have "card {0<..<2*n} \ 2*n - 1" by (cases n) simp_all + also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)" + using assms by (simp add: algebra_simps) + finally have "4 ^ n \ (2 * n choose n) * (2 * n)" by - simp_all + hence "real (4 ^ n) \ real ((2 * n choose n) * (2 * n))" + by (subst of_nat_le_iff) + with assms show ?thesis by (simp add: field_simps) +qed + subsection \Properties of Power Series\