# HG changeset patch
# User hoelzl
# Date 1354555144 -3600
# Node ID 5e40ad9f212a3231837cd8b27ddedfaa7cc2d306
# Parent  0a1242d5e7d48f351ed6b70dc1a1c94573fa0b50
add filterlim rules for inverse and at_infinity

diff -r 0a1242d5e7d4 -r 5e40ad9f212a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Dec 03 18:19:02 2012 +0100
+++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:04 2012 +0100
@@ -447,7 +447,7 @@
   by (simp add: at_eq_bot_iff not_open_singleton)
 
 lemma eventually_at_infinity:
-  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
+  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
 unfolding at_infinity_def
 proof (rule eventually_Abs_filter, rule is_filter.intro)
   fix P Q :: "'a \<Rightarrow> bool"
@@ -458,6 +458,30 @@
   then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
 qed auto
 
+lemma at_infinity_eq_at_top_bot:
+  "(at_infinity \<Colon> real filter) = sup at_top at_bot"
+  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
+proof (intro arg_cong[where f=Abs_filter] ext iffI)
+  fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
+  then guess r ..
+  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
+  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
+next
+  fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
+  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
+  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
+    by (intro exI[of _ "max p (-q)"])
+       (auto simp: abs_real_def)
+qed
+
+lemma at_top_le_at_infinity:
+  "at_top \<le> (at_infinity :: real filter)"
+  unfolding at_infinity_eq_at_top_bot by simp
+
+lemma at_bot_le_at_infinity:
+  "at_bot \<le> (at_infinity :: real filter)"
+  unfolding at_infinity_eq_at_top_bot by simp
+
 subsection {* Boundedness *}
 
 definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
@@ -641,11 +665,9 @@
 translations
   "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
 
-lemma filterlimE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
-  by (auto simp: filterlim_def eventually_filtermap le_filter_def)
-
-lemma filterlimI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
-  by (auto simp: filterlim_def eventually_filtermap le_filter_def)
+lemma filterlim_iff:
+  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
+  unfolding filterlim_def le_filter_def eventually_filtermap ..
 
 lemma filterlim_compose: 
   "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
@@ -655,6 +677,14 @@
   "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
   unfolding filterlim_def by (metis filtermap_mono order_trans)
 
+lemma filterlim_within:
+  "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
+  unfolding filterlim_def
+proof safe
+  assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
+    by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
+qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
+
 abbreviation (in topological_space)
   tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<equiv> filterlim f (nhds l) F"
@@ -678,6 +708,10 @@
     by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
 qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
 
+lemma filterlim_at:
+  "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
+  by (simp add: at_def filterlim_within)
+
 lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   unfolding tendsto_def le_filter_def by fast
 
@@ -770,15 +804,8 @@
   unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
 
 lemma tendsto_compose_eventually:
-  assumes g: "(g ---> m) (at l)"
-  assumes f: "(f ---> l) F"
-  assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
-  shows "((\<lambda>x. g (f x)) ---> m) F"
-proof -
-  from f inj have "LIM x F. f x :> at l"
-    unfolding filterlim_def at_def by (simp add: le_within_iff eventually_filtermap)
-  from filterlim_compose[OF g this] show ?thesis .
-qed
+  "(g ---> m) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
+  by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
 
 lemma metric_tendsto_imp_tendsto:
   assumes f: "(f ---> a) F"
@@ -1092,8 +1119,7 @@
 lemma filterlim_at_top:
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
-  by (safe elim!: filterlimE intro!: filterlimI)
-     (auto simp: eventually_at_top_dense elim!: eventually_elim1)
+  by (auto simp: filterlim_iff eventually_at_top_dense elim!: eventually_elim1)
 
 lemma filterlim_at_top_gt:
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
@@ -1109,8 +1135,7 @@
 lemma filterlim_at_bot: 
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
-  by (safe elim!: filterlimE intro!: filterlimI)
-     (auto simp: eventually_at_bot_dense elim!: eventually_elim1)
+  by (auto simp: filterlim_iff eventually_at_bot_dense elim!: eventually_elim1)
 
 lemma filterlim_at_bot_lt:
   fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
@@ -1123,6 +1148,25 @@
     by (auto elim!: eventually_elim1)
 qed simp
 
+lemma filterlim_at_infinity:
+  fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
+  assumes "0 \<le> c"
+  shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)"
+  unfolding filterlim_iff eventually_at_infinity
+proof safe
+  fix P :: "'a \<Rightarrow> bool" and b
+  assume *: "\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F"
+    and P: "\<forall>x. b \<le> norm x \<longrightarrow> P x"
+  have "max b (c + 1) > c" by auto
+  with * have "eventually (\<lambda>x. max b (c + 1) \<le> norm (f x)) F"
+    by auto
+  then show "eventually (\<lambda>x. P (f x)) F"
+  proof eventually_elim
+    fix x assume "max b (c + 1) \<le> norm (f x)"
+    with P show "P (f x)" by auto
+  qed
+qed force
+
 lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   unfolding filterlim_at_top
   apply (intro allI)
@@ -1176,6 +1220,55 @@
 lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \<Longrightarrow> LIM x F. - (f x) :: real :> at_bot"
   by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top])
 
+lemma tendsto_inverse_0:
+  fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
+  shows "(inverse ---> (0::'a)) at_infinity"
+  unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity
+proof safe
+  fix r :: real assume "0 < r"
+  show "\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> norm (inverse x :: 'a) < r"
+  proof (intro exI[of _ "inverse (r / 2)"] allI impI)
+    fix x :: 'a
+    from `0 < r` have "0 < inverse (r / 2)" by simp
+    also assume *: "inverse (r / 2) \<le> norm x"
+    finally show "norm (inverse x) < r"
+      using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps)
+  qed
+qed
+
+lemma filterlim_inverse_at_infinity:
+  fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+  shows "filterlim inverse at_infinity (at (0::'a))"
+  unfolding filterlim_at_infinity[OF order_refl]
+proof safe
+  fix r :: real assume "0 < r"
+  then show "eventually (\<lambda>x::'a. r \<le> norm (inverse x)) (at 0)"
+    unfolding eventually_at norm_inverse
+    by (intro exI[of _ "inverse r"])
+       (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide)
+qed
+
+lemma filterlim_inverse_at_iff:
+  fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+  shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)"
+  unfolding filterlim_def filtermap_filtermap[symmetric]
+proof
+  assume "filtermap g F \<le> at_infinity"
+  then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
+    by (rule filtermap_mono)
+  also have "\<dots> \<le> at 0"
+    using tendsto_inverse_0
+    by (auto intro!: le_withinI exI[of _ 1]
+             simp: eventually_filtermap eventually_at_infinity filterlim_def at_def)
+  finally show "filtermap inverse (filtermap g F) \<le> at 0" .
+next
+  assume "filtermap inverse (filtermap g F) \<le> at 0"
+  then have "filtermap inverse (filtermap inverse (filtermap g F)) \<le> filtermap inverse (at 0)"
+    by (rule filtermap_mono)
+  with filterlim_inverse_at_infinity show "filtermap g F \<le> at_infinity"
+    by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
+qed
+
 text {*
 
 We only show rules for multiplication and addition when the functions are either against a real