equal
deleted
inserted
replaced
436 have "(\<lambda>n. log 2 (real ((n + 3) choose 3) / 4) + 1) = |
436 have "(\<lambda>n. log 2 (real ((n + 3) choose 3) / 4) + 1) = |
437 (\<lambda>n. log 2 ((real n + 1) * (real n + 2) * (real n + 3) / 24) + 1)" |
437 (\<lambda>n. log 2 ((real n + 1) * (real n + 2) * (real n + 3) / 24) + 1)" |
438 by (subst binomial_gbinomial) |
438 by (subst binomial_gbinomial) |
439 (simp add: gbinomial_pochhammer' numeral_3_eq_3 pochhammer_Suc add_ac) |
439 (simp add: gbinomial_pochhammer' numeral_3_eq_3 pochhammer_Suc add_ac) |
440 moreover have "\<dots> \<sim> (\<lambda>n. 3 / ln 2 * ln n)" |
440 moreover have "\<dots> \<sim> (\<lambda>n. 3 / ln 2 * ln n)" |
441 by (real_asymp simp: divide_simps) |
441 by (real_asymp simp: field_split_simps) |
442 ultimately show ?thesis by simp |
442 ultimately show ?thesis by simp |
443 qed |
443 qed |
444 |
444 |
445 end |
445 end |
446 |
446 |
485 |
485 |
486 lemma "eventually (\<lambda>x::real. 1 / x^2 \<ge> 1 / x) (at_left 0)" |
486 lemma "eventually (\<lambda>x::real. 1 / x^2 \<ge> 1 / x) (at_left 0)" |
487 by real_asymp |
487 by real_asymp |
488 |
488 |
489 lemma "A > 1 \<Longrightarrow> (\<lambda>n. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) \<longlonglongrightarrow> 0" |
489 lemma "A > 1 \<Longrightarrow> (\<lambda>n. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) \<longlonglongrightarrow> 0" |
490 by (real_asymp simp: divide_simps add_pos_pos) |
490 by (real_asymp simp: field_split_simps add_pos_pos) |
491 |
491 |
492 lemma |
492 lemma |
493 assumes "c > (1 :: real)" "k \<noteq> 0" |
493 assumes "c > (1 :: real)" "k \<noteq> 0" |
494 shows "(\<lambda>n. real n ^ k) \<in> o(\<lambda>n. c ^ n)" |
494 shows "(\<lambda>n. real n ^ k) \<in> o(\<lambda>n. c ^ n)" |
495 using assms by (real_asymp (verbose)) |
495 using assms by (real_asymp (verbose)) |