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
```