src/HOL/Limits.thy

   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   shows "continuous_on s (\<lambda>x. power_int (f x) n)"
   using assms unfolding continuous_on_def by (blast intro: tendsto_power_int)
 
+lemma tendsto_power_int' [tendsto_intros]:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes f: "(f \<longlongrightarrow> a) F"
+    and a: "a \<noteq> 0 \<or> n \<ge> 0"
+  shows "((\<lambda>x. power_int (f x) n) \<longlongrightarrow> power_int a n) F"
+  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)
+
 lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F"
   for l :: "'a::real_normed_vector"
   unfolding sgn_div_norm by (simp add: tendsto_intros)
 
 lemma continuous_sgn:

     by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
   then show ?thesis
     by (subst filterlim_inverse_at_iff[symmetric]) simp_all
 qed
 
+lemma filterlim_power_int_neg_at_infinity:
+  fixes f :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
+  assumes "n < 0" and lim: "(f \<longlongrightarrow> 0) F" and ev: "eventually (\<lambda>x. f x \<noteq> 0) F"
+  shows   "filterlim (\<lambda>x. f x powi n) at_infinity F"
+proof -
+  have lim': "((\<lambda>x. f x ^ nat (- n)) \<longlongrightarrow> 0) F"
+    by (rule tendsto_eq_intros lim)+ (use \<open>n < 0\<close> in auto)
+  have ev': "eventually (\<lambda>x. f x ^ nat (-n) \<noteq> 0) F"
+    using ev by eventually_elim (use \<open>n < 0\<close> in auto)
+  have "filterlim (\<lambda>x. inverse (f x ^ nat (-n))) at_infinity F"
+    by (intro filterlim_compose[OF filterlim_inverse_at_infinity])
+       (use lim' ev' in \<open>auto simp: filterlim_at\<close>)
+  thus ?thesis
+    using \<open>n < 0\<close> by (simp add: power_int_def power_inverse)
+qed
+  
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
 
 lemma filterlim_inverse_at_top_iff:
   "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. inverse (f x) :> at_top) \<longleftrightarrow> (f \<longlongrightarrow> (0 :: real)) F"

   fixes c :: real
   assumes c: "(f \<longlongrightarrow> c) F" "c < 0" and g: "filterlim g at_top F"
   shows "LIM x F. f x * g x :> at_bot"
   using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g]
   unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
+
+
+lemma filterlim_cmult_at_bot_at_top:
+  assumes "filterlim (h :: _ \<Rightarrow> real) at_top F" "c \<noteq> 0" "G = (if c > 0 then at_top else at_bot)"
+  shows   "filterlim (\<lambda>x. c * h x) G F"
+  using assms filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of c], of h F]
+              filterlim_tendsto_neg_mult_at_bot[OF tendsto_const[of c], of h F] by simp
 
 lemma filterlim_pow_at_top:
   fixes f :: "'a \<Rightarrow> real"
   assumes "0 < n"
     and f: "LIM x F. f x :> at_top"

 lemma LIMSEQ_realpow_zero:
   fixes x :: real
   assumes "0 \<le> x" "x < 1"
   shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
 proof (cases "x = 0")
-  case False
-  with \<open>0 \<le> x\<close> have x0: "0 < x" by simp
-  then have "1 < inverse x"
-    using \<open>x < 1\<close> by (rule one_less_inverse)
+  case False 
+  with \<open>0 \<le> x\<close> have "1 < inverse x"
+    using \<open>x < 1\<close> by (simp add: one_less_inverse)
   then have "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0"
     by (rule LIMSEQ_inverse_realpow_zero)
   then show ?thesis by (simp add: power_inverse)
 next
   case True