add limits of power at top and bot
authorhoelzl
Mon Mar 31 12:16:39 2014 +0200 (2014-03-31)
changeset 563305c4d3be7a6b0
parent 56329 9597a53b3429
child 56331 bea2196627cb
add limits of power at top and bot
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Mon Mar 31 12:16:37 2014 +0200
     1.2 +++ b/src/HOL/Limits.thy	Mon Mar 31 12:16:39 2014 +0200
     1.3 @@ -1164,6 +1164,25 @@
     1.4    using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
     1.5    unfolding filterlim_uminus_at_bot by simp
     1.6  
     1.7 +lemma filterlim_pow_at_top:
     1.8 +  fixes f :: "real \<Rightarrow> real"
     1.9 +  assumes "0 < n" and f: "LIM x F. f x :> at_top"
    1.10 +  shows "LIM x F. (f x)^n :: real :> at_top"
    1.11 +using `0 < n` proof (induct n)
    1.12 +  case (Suc n) with f show ?case
    1.13 +    by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top)
    1.14 +qed simp
    1.15 +
    1.16 +lemma filterlim_pow_at_bot_even:
    1.17 +  fixes f :: "real \<Rightarrow> real"
    1.18 +  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top"
    1.19 +  using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_top)
    1.20 +
    1.21 +lemma filterlim_pow_at_bot_odd:
    1.22 +  fixes f :: "real \<Rightarrow> real"
    1.23 +  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
    1.24 +  using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
    1.25 +
    1.26  lemma filterlim_tendsto_add_at_top: 
    1.27    assumes f: "(f ---> c) F"
    1.28    assumes g: "LIM x F. g x :> at_top"