src/HOL/Limits.thy
changeset 59613 7103019278f0
parent 58889 5b7a9633cfa8
child 59867 58043346ca64
     1.1 --- a/src/HOL/Limits.thy	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/HOL/Limits.thy	Thu Mar 05 17:30:29 2015 +0000
     1.3 @@ -42,6 +42,11 @@
     1.4    shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
     1.5    by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
     1.6  
     1.7 +lemma lim_infinity_imp_sequentially:
     1.8 +  "(f ---> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) ---> l) sequentially"
     1.9 +by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
    1.10 +
    1.11 +
    1.12  subsubsection {* Boundedness *}
    1.13  
    1.14  definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.15 @@ -885,7 +890,6 @@
    1.16    qed
    1.17  qed force
    1.18  
    1.19 -
    1.20  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
    1.21  
    1.22  text {*
    1.23 @@ -1093,6 +1097,36 @@
    1.24  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
    1.25   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
    1.26  
    1.27 +
    1.28 +lemma at_to_infinity:
    1.29 +  fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
    1.30 +  shows "(at (0::'a)) = filtermap inverse at_infinity"
    1.31 +proof (rule antisym)
    1.32 +  have "(inverse ---> (0::'a)) at_infinity"
    1.33 +    by (fact tendsto_inverse_0)
    1.34 +  then show "filtermap inverse at_infinity \<le> at (0::'a)"
    1.35 +    apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def)
    1.36 +    apply (rule_tac x="1" in exI, auto)
    1.37 +    done
    1.38 +next
    1.39 +  have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity"
    1.40 +    using filterlim_inverse_at_infinity unfolding filterlim_def
    1.41 +    by (rule filtermap_mono)
    1.42 +  then show "at (0::'a) \<le> filtermap inverse at_infinity"
    1.43 +    by (simp add: filtermap_ident filtermap_filtermap)
    1.44 +qed
    1.45 +
    1.46 +lemma lim_at_infinity_0:
    1.47 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
    1.48 +  shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
    1.49 +by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
    1.50 +
    1.51 +lemma lim_zero_infinity:
    1.52 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
    1.53 +  shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
    1.54 +by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
    1.55 +
    1.56 +
    1.57  text {*
    1.58  
    1.59  We only show rules for multiplication and addition when the functions are either against a real