prove tendsto_power_div_exp_0
authorhoelzl
Tue Dec 04 18:00:37 2012 +0100 (2012-12-04)
changeset 5034777e3effa50b6
parent 50346 a75c6429c3c3
child 50348 4b4fe0d5ee22
prove tendsto_power_div_exp_0
* * *
missing rename
src/HOL/Deriv.thy
src/HOL/Limits.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Dec 04 18:00:31 2012 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Tue Dec 04 18:00:37 2012 +0100
     1.3 @@ -1862,4 +1862,52 @@
     1.4    unfolding eventually_at_split filterlim_at_split
     1.5    by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f'])
     1.6  
     1.7 +lemma lhospital_at_top_at_top:
     1.8 +  fixes f g :: "real \<Rightarrow> real"
     1.9 +  assumes g_0: "LIM x at_top. g x :> at_top"
    1.10 +  assumes g': "eventually (\<lambda>x. g' x \<noteq> 0) at_top"
    1.11 +  assumes Df: "eventually (\<lambda>x. DERIV f x :> f' x) at_top"
    1.12 +  assumes Dg: "eventually (\<lambda>x. DERIV g x :> g' x) at_top"
    1.13 +  assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) at_top"
    1.14 +  shows "((\<lambda> x. f x / g x) ---> x) at_top"
    1.15 +  unfolding filterlim_at_top_to_right
    1.16 +proof (rule lhopital_right_0_at_top)
    1.17 +  let ?F = "\<lambda>x. f (inverse x)"
    1.18 +  let ?G = "\<lambda>x. g (inverse x)"
    1.19 +  let ?R = "at_right (0::real)"
    1.20 +  let ?D = "\<lambda>f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))"
    1.21 +
    1.22 +  show "LIM x ?R. ?G x :> at_top"
    1.23 +    using g_0 unfolding filterlim_at_top_to_right .
    1.24 +
    1.25 +  show "eventually (\<lambda>x. DERIV ?G x  :> ?D g' x) ?R"
    1.26 +    unfolding eventually_at_right_to_top
    1.27 +    using Dg eventually_ge_at_top[where c="1::real"]
    1.28 +    apply eventually_elim
    1.29 +    apply (rule DERIV_cong)
    1.30 +    apply (rule DERIV_chain'[where f=inverse])
    1.31 +    apply (auto intro!:  DERIV_inverse)
    1.32 +    done
    1.33 +
    1.34 +  show "eventually (\<lambda>x. DERIV ?F x  :> ?D f' x) ?R"
    1.35 +    unfolding eventually_at_right_to_top
    1.36 +    using Df eventually_ge_at_top[where c="1::real"]
    1.37 +    apply eventually_elim
    1.38 +    apply (rule DERIV_cong)
    1.39 +    apply (rule DERIV_chain'[where f=inverse])
    1.40 +    apply (auto intro!:  DERIV_inverse)
    1.41 +    done
    1.42 +
    1.43 +  show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R"
    1.44 +    unfolding eventually_at_right_to_top
    1.45 +    using g' eventually_ge_at_top[where c="1::real"]
    1.46 +    by eventually_elim auto
    1.47 +    
    1.48 +  show "((\<lambda>x. ?D f' x / ?D g' x) ---> x) ?R"
    1.49 +    unfolding filterlim_at_right_to_top
    1.50 +    apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
    1.51 +    using eventually_ge_at_top[where c="1::real"]
    1.52 +    by eventually_elim simp
    1.53 +qed
    1.54 +
    1.55  end
     2.1 --- a/src/HOL/Limits.thy	Tue Dec 04 18:00:31 2012 +0100
     2.2 +++ b/src/HOL/Limits.thy	Tue Dec 04 18:00:37 2012 +0100
     2.3 @@ -413,6 +413,12 @@
     2.4  lemma within_empty [simp]: "F within {} = bot"
     2.5    unfolding filter_eq_iff eventually_within by simp
     2.6  
     2.7 +lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
     2.8 +  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
     2.9 +
    2.10 +lemma at_within_eq: "at x within T = nhds x within (T - {x})"
    2.11 +  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
    2.12 +
    2.13  lemma within_le: "F within S \<le> F"
    2.14    unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
    2.15  
    2.16 @@ -1345,37 +1351,79 @@
    2.17    apply (auto simp: natceiling_le_eq)
    2.18    done
    2.19  
    2.20 -lemma filterlim_inverse_at_top_pos:
    2.21 -  "LIM x (nhds 0 within {0::real <..}). inverse x :> at_top"
    2.22 -  unfolding filterlim_at_top_gt[where c=0] eventually_within
    2.23 -proof safe
    2.24 -  fix Z :: real assume [arith]: "0 < Z"
    2.25 -  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
    2.26 -    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
    2.27 -  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
    2.28 -    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
    2.29 -qed
    2.30 +subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
    2.31 +
    2.32 +text {*
    2.33 +
    2.34 +This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
    2.35 +@{term "at_right x"} and also @{term "at_right 0"}.
    2.36 +
    2.37 +*}
    2.38 +
    2.39 +lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
    2.40 +  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
    2.41 +           elim: eventually_elim2 eventually_elim1)
    2.42 +
    2.43 +lemma filterlim_split_at_real:
    2.44 +  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
    2.45 +  by (subst at_eq_sup_left_right) (rule filterlim_sup)
    2.46  
    2.47 -lemma filterlim_inverse_at_top:
    2.48 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
    2.49 -  by (intro filterlim_compose[OF filterlim_inverse_at_top_pos])
    2.50 -     (simp add: filterlim_def eventually_filtermap le_within_iff)
    2.51 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
    2.52 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.53 +  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
    2.54 +
    2.55 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
    2.56 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.57 +  apply (intro allI ex_cong)
    2.58 +  apply (auto simp: dist_real_def field_simps)
    2.59 +  apply (erule_tac x="-x" in allE)
    2.60 +  apply simp
    2.61 +  done
    2.62 +
    2.63 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
    2.64 +  unfolding at_def filtermap_nhds_shift[symmetric]
    2.65 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.66 +
    2.67 +lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
    2.68 +  unfolding filtermap_at_shift[symmetric]
    2.69 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.70  
    2.71 -lemma filterlim_inverse_at_bot_neg:
    2.72 -  "LIM x (nhds 0 within {..< 0::real}). inverse x :> at_bot"
    2.73 -  unfolding filterlim_at_bot_lt[where c=0] eventually_within
    2.74 -proof safe
    2.75 -  fix Z :: real assume [arith]: "Z < 0"
    2.76 -  have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
    2.77 -    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
    2.78 -  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x \<le> Z) (nhds 0)"
    2.79 -    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
    2.80 -qed
    2.81 +lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
    2.82 +  using filtermap_at_right_shift[of "-a" 0] by simp
    2.83 +
    2.84 +lemma filterlim_at_right_to_0:
    2.85 +  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
    2.86 +  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
    2.87 +
    2.88 +lemma eventually_at_right_to_0:
    2.89 +  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
    2.90 +  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
    2.91 +
    2.92 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
    2.93 +  unfolding at_def filtermap_nhds_minus[symmetric]
    2.94 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.95 +
    2.96 +lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
    2.97 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
    2.98  
    2.99 -lemma filterlim_inverse_at_bot:
   2.100 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
   2.101 -  by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
   2.102 -     (simp add: filterlim_def eventually_filtermap le_within_iff)
   2.103 +lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
   2.104 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
   2.105 +
   2.106 +lemma filterlim_at_left_to_right:
   2.107 +  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   2.108 +  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
   2.109 +
   2.110 +lemma eventually_at_left_to_right:
   2.111 +  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
   2.112 +  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
   2.113 +
   2.114 +lemma filterlim_at_split:
   2.115 +  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   2.116 +  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
   2.117 +
   2.118 +lemma eventually_at_split:
   2.119 +  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   2.120 +  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   2.121  
   2.122  lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
   2.123    unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
   2.124 @@ -1406,6 +1454,30 @@
   2.125  lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
   2.126    unfolding filterlim_uminus_at_top by simp
   2.127  
   2.128 +lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
   2.129 +  unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
   2.130 +proof safe
   2.131 +  fix Z :: real assume [arith]: "0 < Z"
   2.132 +  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
   2.133 +    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
   2.134 +  then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
   2.135 +    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
   2.136 +qed
   2.137 +
   2.138 +lemma filterlim_inverse_at_top:
   2.139 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   2.140 +  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
   2.141 +     (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
   2.142 +
   2.143 +lemma filterlim_inverse_at_bot_neg:
   2.144 +  "LIM x (at_left (0::real)). inverse x :> at_bot"
   2.145 +  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
   2.146 +
   2.147 +lemma filterlim_inverse_at_bot:
   2.148 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
   2.149 +  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
   2.150 +  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
   2.151 +
   2.152  lemma tendsto_inverse_0:
   2.153    fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
   2.154    shows "(inverse ---> (0::'a)) at_infinity"
   2.155 @@ -1422,6 +1494,39 @@
   2.156    qed
   2.157  qed
   2.158  
   2.159 +lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
   2.160 +proof (rule antisym)
   2.161 +  have "(inverse ---> (0::real)) at_top"
   2.162 +    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
   2.163 +  then show "filtermap inverse at_top \<le> at_right (0::real)"
   2.164 +    unfolding at_within_eq
   2.165 +    by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
   2.166 +next
   2.167 +  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
   2.168 +    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
   2.169 +  then show "at_right (0::real) \<le> filtermap inverse at_top"
   2.170 +    by (simp add: filtermap_ident filtermap_filtermap)
   2.171 +qed
   2.172 +
   2.173 +lemma eventually_at_right_to_top:
   2.174 +  "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
   2.175 +  unfolding at_right_to_top eventually_filtermap ..
   2.176 +
   2.177 +lemma filterlim_at_right_to_top:
   2.178 +  "filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)"
   2.179 +  unfolding filterlim_def at_right_to_top filtermap_filtermap ..
   2.180 +
   2.181 +lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))"
   2.182 +  unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident ..
   2.183 +
   2.184 +lemma eventually_at_top_to_right:
   2.185 +  "eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))"
   2.186 +  unfolding at_top_to_right eventually_filtermap ..
   2.187 +
   2.188 +lemma filterlim_at_top_to_right:
   2.189 +  "filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)"
   2.190 +  unfolding filterlim_def at_top_to_right filtermap_filtermap ..
   2.191 +
   2.192  lemma filterlim_inverse_at_infinity:
   2.193    fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
   2.194    shows "filterlim inverse at_infinity (at (0::'a))"
   2.195 @@ -1520,6 +1625,14 @@
   2.196      by eventually_elim simp
   2.197  qed
   2.198  
   2.199 +lemma LIM_at_top_divide:
   2.200 +  fixes f g :: "'a \<Rightarrow> real"
   2.201 +  assumes f: "(f ---> a) F" "0 < a"
   2.202 +  assumes g: "(g ---> 0) F" "eventually (\<lambda>x. 0 < g x) F"
   2.203 +  shows "LIM x F. f x / g x :> at_top"
   2.204 +  unfolding divide_inverse
   2.205 +  by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
   2.206 +
   2.207  lemma filterlim_at_top_add_at_top: 
   2.208    assumes f: "LIM x F. f x :> at_top"
   2.209    assumes g: "LIM x F. g x :> at_top"
   2.210 @@ -1573,79 +1686,5 @@
   2.211      by (auto simp: norm_power)
   2.212  qed simp
   2.213  
   2.214 -subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
   2.215 -
   2.216 -text {*
   2.217 -
   2.218 -This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
   2.219 -@{term "at_right x"} and also @{term "at_right 0"}.
   2.220 -
   2.221 -*}
   2.222 -
   2.223 -lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
   2.224 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
   2.225 -           elim: eventually_elim2 eventually_elim1)
   2.226 -
   2.227 -lemma filterlim_split_at_real:
   2.228 -  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
   2.229 -  by (subst at_eq_sup_left_right) (rule filterlim_sup)
   2.230 -
   2.231 -lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
   2.232 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
   2.233 -  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
   2.234 -
   2.235 -lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
   2.236 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
   2.237 -  apply (intro allI ex_cong)
   2.238 -  apply (auto simp: dist_real_def field_simps)
   2.239 -  apply (erule_tac x="-x" in allE)
   2.240 -  apply simp
   2.241 -  done
   2.242 -
   2.243 -lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
   2.244 -  unfolding at_def filtermap_nhds_shift[symmetric]
   2.245 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
   2.246 -
   2.247 -lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
   2.248 -  unfolding filtermap_at_shift[symmetric]
   2.249 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
   2.250 -
   2.251 -lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
   2.252 -  using filtermap_at_right_shift[of "-a" 0] by simp
   2.253 -
   2.254 -lemma filterlim_at_right_to_0:
   2.255 -  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
   2.256 -  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
   2.257 -
   2.258 -lemma eventually_at_right_to_0:
   2.259 -  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
   2.260 -  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
   2.261 -
   2.262 -lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
   2.263 -  unfolding at_def filtermap_nhds_minus[symmetric]
   2.264 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
   2.265 -
   2.266 -lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
   2.267 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
   2.268 -
   2.269 -lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
   2.270 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
   2.271 -
   2.272 -lemma filterlim_at_left_to_right:
   2.273 -  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   2.274 -  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
   2.275 -
   2.276 -lemma eventually_at_left_to_right:
   2.277 -  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
   2.278 -  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
   2.279 -
   2.280 -lemma filterlim_at_split:
   2.281 -  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   2.282 -  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
   2.283 -
   2.284 -lemma eventually_at_split:
   2.285 -  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   2.286 -  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   2.287 -
   2.288  end
   2.289  
     3.1 --- a/src/HOL/Transcendental.thy	Tue Dec 04 18:00:31 2012 +0100
     3.2 +++ b/src/HOL/Transcendental.thy	Tue Dec 04 18:00:37 2012 +0100
     3.3 @@ -1339,6 +1339,28 @@
     3.4    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
     3.5       (auto intro: eventually_gt_at_top)
     3.6  
     3.7 +lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
     3.8 +proof (induct k)
     3.9 +  show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
    3.10 +    by (simp add: inverse_eq_divide[symmetric])
    3.11 +       (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
    3.12 +              at_top_le_at_infinity order_refl)
    3.13 +next
    3.14 +  case (Suc k)
    3.15 +  show ?case
    3.16 +  proof (rule lhospital_at_top_at_top)
    3.17 +    show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
    3.18 +      by eventually_elim (intro DERIV_intros, simp, simp)
    3.19 +    show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
    3.20 +      by eventually_elim (auto intro!: DERIV_intros)
    3.21 +    show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
    3.22 +      by auto
    3.23 +    from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
    3.24 +    show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
    3.25 +      by simp
    3.26 +  qed (rule exp_at_top)
    3.27 +qed
    3.28 +
    3.29  subsection {* Sine and Cosine *}
    3.30  
    3.31  definition sin_coeff :: "nat \<Rightarrow> real" where