# HG changeset patch # User hoelzl # Date 1396260999 -7200 # Node ID 5c4d3be7a6b023311cfc607b4e228cdd1d27afec # Parent 9597a53b3429f39d56142e6db13af2548785522a add limits of power at top and bot diff -r 9597a53b3429 -r 5c4d3be7a6b0 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Mar 31 12:16:37 2014 +0200 +++ b/src/HOL/Limits.thy Mon Mar 31 12:16:39 2014 +0200 @@ -1164,6 +1164,25 @@ using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) unfolding filterlim_uminus_at_bot by simp +lemma filterlim_pow_at_top: + fixes f :: "real \ real" + assumes "0 < n" and f: "LIM x F. f x :> at_top" + shows "LIM x F. (f x)^n :: real :> at_top" +using `0 < n` proof (induct n) + case (Suc n) with f show ?case + by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) +qed simp + +lemma filterlim_pow_at_bot_even: + fixes f :: "real \ real" + shows "0 < n \ LIM x F. f x :> at_bot \ even n \ LIM x F. (f x)^n :> at_top" + using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_top) + +lemma filterlim_pow_at_bot_odd: + fixes f :: "real \ real" + shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" + using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) + lemma filterlim_tendsto_add_at_top: assumes f: "(f ---> c) F" assumes g: "LIM x F. g x :> at_top"