src/HOL/Transcendental.thy
changeset 50347 77e3effa50b6
parent 50346 a75c6429c3c3
child 51477 2990382dc066
     1.1 --- a/src/HOL/Transcendental.thy	Tue Dec 04 18:00:31 2012 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Dec 04 18:00:37 2012 +0100
     1.3 @@ -1339,6 +1339,28 @@
     1.4    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
     1.5       (auto intro: eventually_gt_at_top)
     1.6  
     1.7 +lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
     1.8 +proof (induct k)
     1.9 +  show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
    1.10 +    by (simp add: inverse_eq_divide[symmetric])
    1.11 +       (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
    1.12 +              at_top_le_at_infinity order_refl)
    1.13 +next
    1.14 +  case (Suc k)
    1.15 +  show ?case
    1.16 +  proof (rule lhospital_at_top_at_top)
    1.17 +    show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
    1.18 +      by eventually_elim (intro DERIV_intros, simp, simp)
    1.19 +    show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
    1.20 +      by eventually_elim (auto intro!: DERIV_intros)
    1.21 +    show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
    1.22 +      by auto
    1.23 +    from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
    1.24 +    show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
    1.25 +      by simp
    1.26 +  qed (rule exp_at_top)
    1.27 +qed
    1.28 +
    1.29  subsection {* Sine and Cosine *}
    1.30  
    1.31  definition sin_coeff :: "nat \<Rightarrow> real" where