186 lemma central_binomial_lower_bound: |
186 lemma central_binomial_lower_bound: |
187 assumes "n > 0" |
187 assumes "n > 0" |
188 shows "4^n / (2*real n) \<le> real ((2*n) choose n)" |
188 shows "4^n / (2*real n) \<le> real ((2*n) choose n)" |
189 proof - |
189 proof - |
190 from binomial[of 1 1 "2*n"] |
190 from binomial[of 1 1 "2*n"] |
191 have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)" |
191 have "4 ^ n = (\<Sum>k\<le>2*n. (2*n) choose k)" |
192 by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def) |
192 by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def) |
193 also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto |
193 also have "{..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto |
194 also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = |
194 also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = |
195 (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)" |
195 (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)" |
196 by (subst sum.union_disjoint) auto |
196 by (subst sum.union_disjoint) auto |
197 also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" |
197 also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" |
198 by (cases n) simp_all |
198 by (cases n) simp_all |
199 also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)" |
199 also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)" |
200 by (intro sum_mono2) auto |
200 by (intro sum_mono2) auto |
992 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
992 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
993 assumes s: "0 < s" |
993 assumes s: "0 < s" |
994 and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
994 and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" |
995 shows "(f \<longlongrightarrow> a 0) (at 0)" |
995 shows "(f \<longlongrightarrow> a 0) (at 0)" |
996 proof - |
996 proof - |
997 have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)" |
997 have "norm (of_real s / 2 :: 'a) < s" |
998 apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) |
998 using s by (auto simp: norm_divide) |
999 using s |
999 then have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)" |
1000 apply (auto simp: norm_divide) |
1000 by (rule sums_summable [OF sm]) |
1001 done |
|
1002 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)" |
1001 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)" |
1003 apply (rule termdiffs_strong) |
1002 by (rule termdiffs_strong) (use s in \<open>auto simp: norm_divide\<close>) |
1004 using s |
|
1005 apply (auto simp: norm_divide) |
|
1006 done |
|
1007 then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0" |
1003 then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0" |
1008 by (blast intro: DERIV_continuous) |
1004 by (blast intro: DERIV_continuous) |
1009 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)" |
1005 then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)" |
1010 by (simp add: continuous_within) |
1006 by (simp add: continuous_within) |
1011 then show ?thesis |
1007 then show ?thesis |
1012 apply (rule Lim_transform) |
1008 apply (rule Lim_transform) |
1013 apply (auto simp add: LIM_eq) |
1009 apply (clarsimp simp: LIM_eq) |
1014 apply (rule_tac x="s" in exI) |
1010 apply (rule_tac x="s" in exI) |
1015 using s |
1011 using s sm sums_unique by fastforce |
1016 apply (auto simp: sm [THEN sums_unique]) |
|
1017 done |
|
1018 qed |
1012 qed |
1019 |
1013 |
1020 lemma powser_limit_0_strong: |
1014 lemma powser_limit_0_strong: |
1021 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
1015 fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" |
1022 assumes s: "0 < s" |
1016 assumes s: "0 < s" |