src/HOL/Limits.thy
changeset 50419 3177d0374701
parent 50347 77e3effa50b6
child 50880 b22ecedde1c7
     1.1 --- a/src/HOL/Limits.thy	Fri Dec 07 14:29:08 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Fri Dec 07 14:29:09 2012 +0100
     1.3 @@ -732,6 +732,9 @@
     1.4    "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
     1.5    unfolding filterlim_def by (metis filtermap_mono order_trans)
     1.6  
     1.7 +lemma filterlim_ident: "LIM x F. x :> F"
     1.8 +  by (simp add: filterlim_def filtermap_ident)
     1.9 +
    1.10  lemma filterlim_cong:
    1.11    "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
    1.12    by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
    1.13 @@ -1560,6 +1563,10 @@
    1.14      by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
    1.15  qed
    1.16  
    1.17 +lemma tendsto_inverse_0_at_top:
    1.18 +  "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
    1.19 + by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl)
    1.20 +
    1.21  text {*
    1.22  
    1.23  We only show rules for multiplication and addition when the functions are either against a real
    1.24 @@ -1610,6 +1617,12 @@
    1.25    qed
    1.26  qed
    1.27  
    1.28 +lemma filterlim_tendsto_pos_mult_at_bot:
    1.29 +  assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F"
    1.30 +  shows "LIM x F. f x * g x :> at_bot"
    1.31 +  using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
    1.32 +  unfolding filterlim_uminus_at_bot by simp
    1.33 +
    1.34  lemma filterlim_tendsto_add_at_top: 
    1.35    assumes f: "(f ---> c) F"
    1.36    assumes g: "LIM x F. g x :> at_top"