equal
deleted
inserted
replaced
653 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
653 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
654 (simp_all add: at_infinity_eq_at_top_bot) |
654 (simp_all add: at_infinity_eq_at_top_bot) |
655 { fix n :: nat assume "2 < n" |
655 { fix n :: nat assume "2 < n" |
656 have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2" |
656 have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2" |
657 using \<open>2 < n\<close> unfolding gbinomial_def binomial_gbinomial |
657 using \<open>2 < n\<close> unfolding gbinomial_def binomial_gbinomial |
658 by (simp add: atLeast0AtMost atMost_Suc field_simps of_nat_diff numeral_2_eq_2) |
658 by (simp add: atLeast0AtMost lessThan_Suc field_simps of_nat_diff numeral_2_eq_2) |
659 also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" |
659 also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" |
660 by (simp add: x_def) |
660 by (simp add: x_def) |
661 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
661 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
662 using \<open>2 < n\<close> by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
662 using \<open>2 < n\<close> by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
663 also have "\<dots> = (x n + 1) ^ n" |
663 also have "\<dots> = (x n + 1) ^ n" |
690 show "(\<lambda>n. c / n) \<longlonglongrightarrow> 0" |
690 show "(\<lambda>n. c / n) \<longlonglongrightarrow> 0" |
691 by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
691 by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially]) |
692 (simp_all add: at_infinity_eq_at_top_bot) |
692 (simp_all add: at_infinity_eq_at_top_bot) |
693 { fix n :: nat assume "1 < n" |
693 { fix n :: nat assume "1 < n" |
694 have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" |
694 have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1" |
695 using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp |
695 using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial |
|
696 by (simp add: lessThan_Suc) |
696 also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" |
697 also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" |
697 by (simp add: x_def) |
698 by (simp add: x_def) |
698 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
699 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
699 using \<open>1 < n\<close> \<open>1 \<le> c\<close> by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
700 using \<open>1 < n\<close> \<open>1 \<le> c\<close> by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
700 also have "\<dots> = (x n + 1) ^ n" |
701 also have "\<dots> = (x n + 1) ^ n" |