--- 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 \<le> n} \<noteq> {}" by blast
qed
-lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
+lemma sqrt_unique:
+ assumes "m^2 \<le> n" "n < (Suc m)^2"
+ shows "Discrete.sqrt n = m"
+proof -
+ have "m' \<le> m" if "m'^2 \<le> 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' \<le> m" by simp
+ qed
+ with \<open>m^2 \<le> n\<close> 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 (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
proof -
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
then show ?thesis by (simp add: sqrt_def Set.filter_def)
@@ -161,6 +177,9 @@
by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
qed
+lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
+ using mono_sqrt unfolding mono_def by auto
+
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
proof -
have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
--- 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 \<longleftrightarrow> p \<le> n"
+proof (induction n)
+ case 0
+ with assms show ?case by auto
+next
+ case (Suc n)
+ have "p dvd fact (Suc n) \<longleftrightarrow> p dvd (Suc n) * fact n" by simp
+ also from assms have "\<dots> \<longleftrightarrow> p dvd Suc n \<or> p dvd fact n"
+ by (rule prime_dvd_mult_iff)
+ also note Suc.IH
+ also have "p dvd Suc n \<or> p \<le> n \<longleftrightarrow> p \<le> 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]
--- 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 \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _ summable_geometric])
qed
+subsection \<open>More facts about binomial coefficients\<close>
+
+text \<open>
+ These facts could have been proven before, but having real numbers
+ makes the proofs a lot easier.
+\<close>
+
+lemma central_binomial_odd:
+ "odd n \<Longrightarrow> n choose (Suc (n div 2)) = n choose (n div 2)"
+proof -
+ assume "odd n"
+ hence "Suc (n div 2) \<le> n" by presburger
+ hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
+ by (rule binomial_symmetric)
+ also from \<open>odd n\<close> 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 \<le> n" "Suc k \<le> 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 \<dots> = (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' \<le> n"
+ shows "n choose k < n choose k'"
+proof -
+ from assms have "k \<le> 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 "\<dots> < n choose k'" by (rule step.IH)
+ finally show ?case .
+ qed
+qed
+
+lemma binomial_mono:
+ assumes "k \<le> k'" "2*k' \<le> n"
+ shows "n choose k \<le> 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 \<ge> n" "k' \<le> 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 \<le> k'" "k \<ge> n div 2" "k' \<le> n"
+ shows "n choose k \<ge> n choose k'"
+proof (cases "k = k'")
+ case False
+ note not_eq = False
+ show ?thesis
+ proof (cases "k = n div 2 \<and> odd n")
+ case False
+ with assms(2) have "2*k \<ge> 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' \<le> 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 "\<dots> = n choose k" by (simp add: central_binomial_odd)
+ finally show ?thesis .
+ qed
+qed simp_all
+
+lemma binomial_maximum: "n choose k \<le> n choose (n div 2)"
+proof -
+ have "k \<le> n div 2 \<longleftrightarrow> 2*k \<le> n" by linarith
+ consider "2*k \<le> n" | "2*k \<ge> n" "k \<le> 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 \<le> (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) \<le> real ((2*n) choose n)"
+proof -
+ from binomial[of 1 1 "2*n"]
+ have "4 ^ n = (\<Sum>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} \<union> {0,2*n}" by auto
+ also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
+ (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
+ by (subst setsum.union_disjoint) auto
+ also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
+ by (cases n) simp_all
+ also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
+ by (intro setsum_mono3) auto
+ also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
+ also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
+ by (intro setsum_mono binomial_maximum')
+ also have "\<dots> = card {0<..<2*n} * ((2*n) choose n)" by simp
+ also have "card {0<..<2*n} \<le> 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 \<le> (2 * n choose n) * (2 * n)" by - simp_all
+ hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))"
+ by (subst of_nat_le_iff)
+ with assms show ?thesis by (simp add: field_simps)
+qed
+
subsection \<open>Properties of Power Series\<close>