src/HOL/Limits.thy
 changeset 57276 49c51eeaa623 parent 57275 0ddb5b755cdc child 57447 87429bdecad5
```     1.1 --- a/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
1.2 +++ b/src/HOL/Limits.thy	Wed Jun 18 14:31:32 2014 +0200
1.3 @@ -3,7 +3,6 @@
1.4      Author:     Jacques D. Fleuriot, University of Cambridge
1.5      Author:     Lawrence C Paulson
1.6      Author:     Jeremy Avigad
1.7 -
1.8  *)
1.9
1.10  header {* Limits on Real Vector Spaces *}
1.11 @@ -15,43 +14,27 @@
1.12  subsection {* Filter going to infinity norm *}
1.13
1.14  definition at_infinity :: "'a::real_normed_vector filter" where
1.15 -  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
1.16 +  "at_infinity = (INF r. principal {x. r \<le> norm x})"
1.17
1.18 -lemma eventually_at_infinity:
1.19 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
1.20 -unfolding at_infinity_def
1.21 -proof (rule eventually_Abs_filter, rule is_filter.intro)
1.22 -  fix P Q :: "'a \<Rightarrow> bool"
1.23 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
1.24 -  then obtain r s where
1.25 -    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
1.26 -  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
1.27 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
1.28 -qed auto
1.29 +lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
1.30 +  unfolding at_infinity_def
1.31 +  by (subst eventually_INF_base)
1.32 +     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
1.33
1.34  lemma at_infinity_eq_at_top_bot:
1.35    "(at_infinity \<Colon> real filter) = sup at_top at_bot"
1.36 -  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
1.37 -proof (intro arg_cong[where f=Abs_filter] ext iffI)
1.38 -  fix P :: "real \<Rightarrow> bool"
1.39 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
1.40 -  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
1.41 -  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
1.42 -  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
1.43 -next
1.44 -  fix P :: "real \<Rightarrow> bool"
1.45 -  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
1.46 -  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
1.47 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
1.48 -    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
1.49 -qed
1.50 +  apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
1.51 +                   eventually_at_top_linorder eventually_at_bot_linorder)
1.52 +  apply safe
1.53 +  apply (rule_tac x="b" in exI, simp)
1.54 +  apply (rule_tac x="- b" in exI, simp)
1.55 +  apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def)
1.56 +  done
1.57
1.58 -lemma at_top_le_at_infinity:
1.59 -  "at_top \<le> (at_infinity :: real filter)"
1.60 +lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)"
1.61    unfolding at_infinity_eq_at_top_bot by simp
1.62
1.63 -lemma at_bot_le_at_infinity:
1.64 -  "at_bot \<le> (at_infinity :: real filter)"
1.65 +lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)"
1.66    unfolding at_infinity_eq_at_top_bot by simp
1.67
1.68  lemma filterlim_at_top_imp_at_infinity:
```