--- a/src/HOL/Limits.thy Mon Jun 01 08:04:19 2009 -0700
+++ b/src/HOL/Limits.thy Mon Jun 01 10:36:42 2009 -0700
@@ -81,6 +81,27 @@
using assms by (auto elim!: eventually_rev_mp)
+subsection {* Boundedness *}
+
+definition
+ Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
+
+lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
+unfolding Bfun_def
+proof (intro exI conjI allI)
+ show "0 < max K 1" by simp
+next
+ show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F"
+ using K by (rule eventually_elim1, simp)
+qed
+
+lemma BfunE:
+ assumes "Bfun S F"
+ obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F"
+using assms unfolding Bfun_def by fast
+
+
subsection {* Convergence to Zero *}
definition
@@ -95,6 +116,10 @@
"\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F"
unfolding Zfun_def by simp
+lemma Zfun_ssubst:
+ "eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F"
+unfolding Zfun_def by (auto elim!: eventually_rev_mp)
+
lemma Zfun_zero: "Zfun (\<lambda>i. 0) F"
unfolding Zfun_def by simp
@@ -103,7 +128,7 @@
lemma Zfun_imp_Zfun:
assumes X: "Zfun X F"
- assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
+ assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F"
shows "Zfun (\<lambda>n. Y n) F"
proof (cases)
assume K: "0 < K"
@@ -114,26 +139,34 @@
using K by (rule divide_pos_pos)
then have "eventually (\<lambda>i. norm (X i) < r / K) F"
using ZfunD [OF X] by fast
- then show "eventually (\<lambda>i. norm (Y i) < r) F"
- proof (rule eventually_elim1)
- fix i assume "norm (X i) < r / K"
+ with Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+ proof (rule eventually_elim2)
+ fix i
+ assume *: "norm (Y i) \<le> norm (X i) * K"
+ assume "norm (X i) < r / K"
hence "norm (X i) * K < r"
by (simp add: pos_less_divide_eq K)
thus "norm (Y i) < r"
- by (simp add: order_le_less_trans [OF Y])
+ by (simp add: order_le_less_trans [OF *])
qed
qed
next
assume "\<not> 0 < K"
hence K: "K \<le> 0" by (simp only: not_less)
- {
- fix i
- have "norm (Y i) \<le> norm (X i) * K" by (rule Y)
- also have "\<dots> \<le> norm (X i) * 0"
- using K norm_ge_zero by (rule mult_left_mono)
- finally have "norm (Y i) = 0" by simp
- }
- thus ?thesis by (simp add: Zfun_zero)
+ show ?thesis
+ proof (rule ZfunI)
+ fix r :: real
+ assume "0 < r"
+ from Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+ proof (rule eventually_elim1)
+ fix i
+ assume "norm (Y i) \<le> norm (X i) * K"
+ also have "\<dots> \<le> norm (X i) * 0"
+ using K norm_ge_zero by (rule mult_left_mono)
+ finally show "norm (Y i) < r"
+ using `0 < r` by simp
+ qed
+ qed
qed
lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F"
@@ -176,6 +209,8 @@
proof -
obtain K where "\<And>x. norm (f x) \<le> norm x * K"
using bounded by fast
+ then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F"
+ by simp
with X show ?thesis
by (rule Zfun_imp_Zfun)
qed
@@ -293,4 +328,135 @@
by (simp only: tendsto_Zfun_iff prod_diff_prod
Zfun_add Zfun Zfun_left Zfun_right)
+
+subsection {* Continuity of Inverse *}
+
+lemma (in bounded_bilinear) Zfun_prod_Bfun:
+ assumes X: "Zfun X F"
+ assumes Y: "Bfun Y F"
+ shows "Zfun (\<lambda>n. X n ** Y n) F"
+proof -
+ obtain K where K: "0 \<le> K"
+ and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
+ using nonneg_bounded by fast
+ obtain B where B: "0 < B"
+ and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F"
+ using Y by (rule BfunE)
+ have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F"
+ using norm_Y proof (rule eventually_elim1)
+ fix i
+ assume *: "norm (Y i) \<le> B"
+ have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+ by (rule norm_le)
+ also have "\<dots> \<le> norm (X i) * B * K"
+ by (intro mult_mono' order_refl norm_Y norm_ge_zero
+ mult_nonneg_nonneg K *)
+ also have "\<dots> = norm (X i) * (B * K)"
+ by (rule mult_assoc)
+ finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" .
+ qed
+ with X show ?thesis
+ by (rule Zfun_imp_Zfun)
+qed
+
+lemma (in bounded_bilinear) flip:
+ "bounded_bilinear (\<lambda>x y. y ** x)"
+apply default
+apply (rule add_right)
+apply (rule add_left)
+apply (rule scaleR_right)
+apply (rule scaleR_left)
+apply (subst mult_commute)
+using bounded by fast
+
+lemma (in bounded_bilinear) Bfun_prod_Zfun:
+ assumes X: "Bfun X F"
+ assumes Y: "Zfun Y F"
+ shows "Zfun (\<lambda>n. X n ** Y n) F"
+using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
+
+lemma inverse_diff_inverse:
+ "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
+by (simp add: algebra_simps)
+
+lemma Bfun_inverse_lemma:
+ fixes x :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
+apply (subst nonzero_norm_inverse, clarsimp)
+apply (erule (1) le_imp_inverse_le)
+done
+
+lemma Bfun_inverse:
+ fixes a :: "'a::real_normed_div_algebra"
+ assumes X: "tendsto X a F"
+ assumes a: "a \<noteq> 0"
+ shows "Bfun (\<lambda>n. inverse (X n)) F"
+proof -
+ from a have "0 < norm a" by simp
+ hence "\<exists>r>0. r < norm a" by (rule dense)
+ then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
+ have "eventually (\<lambda>i. dist (X i) a < r) F"
+ using tendstoD [OF X r1] by fast
+ hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F"
+ proof (rule eventually_elim1)
+ fix i
+ assume "dist (X i) a < r"
+ hence 1: "norm (X i - a) < r"
+ by (simp add: dist_norm)
+ hence 2: "X i \<noteq> 0" using r2 by auto
+ hence "norm (inverse (X i)) = inverse (norm (X i))"
+ by (rule nonzero_norm_inverse)
+ also have "\<dots> \<le> inverse (norm a - r)"
+ proof (rule le_imp_inverse_le)
+ show "0 < norm a - r" using r2 by simp
+ next
+ have "norm a - norm (X i) \<le> norm (a - X i)"
+ by (rule norm_triangle_ineq2)
+ also have "\<dots> = norm (X i - a)"
+ by (rule norm_minus_commute)
+ also have "\<dots> < r" using 1 .
+ finally show "norm a - r \<le> norm (X i)" by simp
+ qed
+ finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" .
+ qed
+ thus ?thesis by (rule BfunI)
+qed
+
+lemma tendsto_inverse_lemma:
+ fixes a :: "'a::real_normed_div_algebra"
+ shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk>
+ \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+apply (subst tendsto_Zfun_iff)
+apply (rule Zfun_ssubst)
+apply (erule eventually_elim1)
+apply (erule (1) inverse_diff_inverse)
+apply (rule Zfun_minus)
+apply (rule Zfun_mult_left)
+apply (rule mult.Bfun_prod_Zfun)
+apply (erule (1) Bfun_inverse)
+apply (simp add: tendsto_Zfun_iff)
+done
+
+lemma tendsto_inverse:
+ fixes a :: "'a::real_normed_div_algebra"
+ assumes X: "tendsto X a F"
+ assumes a: "a \<noteq> 0"
+ shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+proof -
+ from a have "0 < norm a" by simp
+ with X have "eventually (\<lambda>i. dist (X i) a < norm a) F"
+ by (rule tendstoD)
+ then have "eventually (\<lambda>i. X i \<noteq> 0) F"
+ unfolding dist_norm by (auto elim!: eventually_elim1)
+ with X a show ?thesis
+ by (rule tendsto_inverse_lemma)
+qed
+
+lemma tendsto_divide:
+ fixes a b :: "'a::real_normed_field"
+ shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F"
+by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+
end