limits of inverse using filters
authorhuffman
Mon Jun 01 10:36:42 2009 -0700 (2009-06-01)
changeset 313553d18766ddc4b
parent 31354 2ad53771c30f
child 31356 ec8b9b6c47dc
limits of inverse using filters
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Mon Jun 01 08:04:19 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Mon Jun 01 10:36:42 2009 -0700
     1.3 @@ -413,67 +413,16 @@
     1.4  
     1.5  subsubsection {* Derived theorems about @{term LIM} *}
     1.6  
     1.7 -lemma LIM_inverse_lemma:
     1.8 -  fixes x :: "'a::real_normed_div_algebra"
     1.9 -  assumes r: "0 < r"
    1.10 -  assumes x: "norm (x - 1) < min (1/2) (r/2)"
    1.11 -  shows "norm (inverse x - 1) < r"
    1.12 -proof -
    1.13 -  from r have r2: "0 < r/2" by simp
    1.14 -  from x have 0: "x \<noteq> 0" by clarsimp
    1.15 -  from x have x': "norm (1 - x) < min (1/2) (r/2)"
    1.16 -    by (simp only: norm_minus_commute)
    1.17 -  hence less1: "norm (1 - x) < r/2" by simp
    1.18 -  have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2)
    1.19 -  also from x' have "norm (1 - x) < 1/2" by simp
    1.20 -  finally have "1/2 < norm x" by simp
    1.21 -  hence "inverse (norm x) < inverse (1/2)"
    1.22 -    by (rule less_imp_inverse_less, simp)
    1.23 -  hence less2: "norm (inverse x) < 2"
    1.24 -    by (simp add: nonzero_norm_inverse 0)
    1.25 -  from less1 less2 r2 norm_ge_zero
    1.26 -  have "norm (1 - x) * norm (inverse x) < (r/2) * 2"
    1.27 -    by (rule mult_strict_mono)
    1.28 -  thus "norm (inverse x - 1) < r"
    1.29 -    by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0)
    1.30 -qed
    1.31 +lemma LIM_inverse:
    1.32 +  fixes L :: "'a::real_normed_div_algebra"
    1.33 +  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
    1.34 +unfolding LIM_conv_tendsto
    1.35 +by (rule tendsto_inverse)
    1.36  
    1.37  lemma LIM_inverse_fun:
    1.38    assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
    1.39    shows "inverse -- a --> inverse a"
    1.40 -proof (rule LIM_equal2)
    1.41 -  from a show "0 < norm a" by simp
    1.42 -next
    1.43 -  fix x assume "norm (x - a) < norm a"
    1.44 -  hence "x \<noteq> 0" by auto
    1.45 -  with a show "inverse x = inverse (inverse a * x) * inverse a"
    1.46 -    by (simp add: nonzero_inverse_mult_distrib
    1.47 -                  nonzero_imp_inverse_nonzero
    1.48 -                  nonzero_inverse_inverse_eq mult_assoc)
    1.49 -next
    1.50 -  have 1: "inverse -- 1 --> inverse (1::'a)"
    1.51 -    apply (rule LIM_I)
    1.52 -    apply (rule_tac x="min (1/2) (r/2)" in exI)
    1.53 -    apply (simp add: LIM_inverse_lemma)
    1.54 -    done
    1.55 -  have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
    1.56 -    by (intro LIM_mult LIM_ident LIM_const)
    1.57 -  hence "(\<lambda>x. inverse a * x) -- a --> 1"
    1.58 -    by (simp add: a)
    1.59 -  with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
    1.60 -    by (rule LIM_compose)
    1.61 -  hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1"
    1.62 -    by simp
    1.63 -  hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a"
    1.64 -    by (intro LIM_mult LIM_const)
    1.65 -  thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a"
    1.66 -    by simp
    1.67 -qed
    1.68 -
    1.69 -lemma LIM_inverse:
    1.70 -  fixes L :: "'a::real_normed_div_algebra"
    1.71 -  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
    1.72 -by (rule LIM_inverse_fun [THEN LIM_compose])
    1.73 +by (rule LIM_inverse [OF LIM_ident a])
    1.74  
    1.75  lemma LIM_sgn:
    1.76    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
     2.1 --- a/src/HOL/Limits.thy	Mon Jun 01 08:04:19 2009 -0700
     2.2 +++ b/src/HOL/Limits.thy	Mon Jun 01 10:36:42 2009 -0700
     2.3 @@ -81,6 +81,27 @@
     2.4  using assms by (auto elim!: eventually_rev_mp)
     2.5  
     2.6  
     2.7 +subsection {* Boundedness *}
     2.8 +
     2.9 +definition
    2.10 +  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    2.11 +  "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
    2.12 +
    2.13 +lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
    2.14 +unfolding Bfun_def
    2.15 +proof (intro exI conjI allI)
    2.16 +  show "0 < max K 1" by simp
    2.17 +next
    2.18 +  show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F"
    2.19 +    using K by (rule eventually_elim1, simp)
    2.20 +qed
    2.21 +
    2.22 +lemma BfunE:
    2.23 +  assumes "Bfun S F"
    2.24 +  obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F"
    2.25 +using assms unfolding Bfun_def by fast
    2.26 +
    2.27 +
    2.28  subsection {* Convergence to Zero *}
    2.29  
    2.30  definition
    2.31 @@ -95,6 +116,10 @@
    2.32    "\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F"
    2.33  unfolding Zfun_def by simp
    2.34  
    2.35 +lemma Zfun_ssubst:
    2.36 +  "eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F"
    2.37 +unfolding Zfun_def by (auto elim!: eventually_rev_mp)
    2.38 +
    2.39  lemma Zfun_zero: "Zfun (\<lambda>i. 0) F"
    2.40  unfolding Zfun_def by simp
    2.41  
    2.42 @@ -103,7 +128,7 @@
    2.43  
    2.44  lemma Zfun_imp_Zfun:
    2.45    assumes X: "Zfun X F"
    2.46 -  assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
    2.47 +  assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F"
    2.48    shows "Zfun (\<lambda>n. Y n) F"
    2.49  proof (cases)
    2.50    assume K: "0 < K"
    2.51 @@ -114,26 +139,34 @@
    2.52        using K by (rule divide_pos_pos)
    2.53      then have "eventually (\<lambda>i. norm (X i) < r / K) F"
    2.54        using ZfunD [OF X] by fast
    2.55 -    then show "eventually (\<lambda>i. norm (Y i) < r) F"
    2.56 -    proof (rule eventually_elim1)
    2.57 -      fix i assume "norm (X i) < r / K"
    2.58 +    with Y show "eventually (\<lambda>i. norm (Y i) < r) F"
    2.59 +    proof (rule eventually_elim2)
    2.60 +      fix i
    2.61 +      assume *: "norm (Y i) \<le> norm (X i) * K"
    2.62 +      assume "norm (X i) < r / K"
    2.63        hence "norm (X i) * K < r"
    2.64          by (simp add: pos_less_divide_eq K)
    2.65        thus "norm (Y i) < r"
    2.66 -        by (simp add: order_le_less_trans [OF Y])
    2.67 +        by (simp add: order_le_less_trans [OF *])
    2.68      qed
    2.69    qed
    2.70  next
    2.71    assume "\<not> 0 < K"
    2.72    hence K: "K \<le> 0" by (simp only: not_less)
    2.73 -  {
    2.74 -    fix i
    2.75 -    have "norm (Y i) \<le> norm (X i) * K" by (rule Y)
    2.76 -    also have "\<dots> \<le> norm (X i) * 0"
    2.77 -      using K norm_ge_zero by (rule mult_left_mono)
    2.78 -    finally have "norm (Y i) = 0" by simp
    2.79 -  }
    2.80 -  thus ?thesis by (simp add: Zfun_zero)
    2.81 +  show ?thesis
    2.82 +  proof (rule ZfunI)
    2.83 +    fix r :: real
    2.84 +    assume "0 < r"
    2.85 +    from Y show "eventually (\<lambda>i. norm (Y i) < r) F"
    2.86 +    proof (rule eventually_elim1)
    2.87 +      fix i
    2.88 +      assume "norm (Y i) \<le> norm (X i) * K"
    2.89 +      also have "\<dots> \<le> norm (X i) * 0"
    2.90 +        using K norm_ge_zero by (rule mult_left_mono)
    2.91 +      finally show "norm (Y i) < r"
    2.92 +        using `0 < r` by simp
    2.93 +    qed
    2.94 +  qed
    2.95  qed
    2.96  
    2.97  lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F"
    2.98 @@ -176,6 +209,8 @@
    2.99  proof -
   2.100    obtain K where "\<And>x. norm (f x) \<le> norm x * K"
   2.101      using bounded by fast
   2.102 +  then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F"
   2.103 +    by simp
   2.104    with X show ?thesis
   2.105      by (rule Zfun_imp_Zfun)
   2.106  qed
   2.107 @@ -293,4 +328,135 @@
   2.108  by (simp only: tendsto_Zfun_iff prod_diff_prod
   2.109                 Zfun_add Zfun Zfun_left Zfun_right)
   2.110  
   2.111 +
   2.112 +subsection {* Continuity of Inverse *}
   2.113 +
   2.114 +lemma (in bounded_bilinear) Zfun_prod_Bfun:
   2.115 +  assumes X: "Zfun X F"
   2.116 +  assumes Y: "Bfun Y F"
   2.117 +  shows "Zfun (\<lambda>n. X n ** Y n) F"
   2.118 +proof -
   2.119 +  obtain K where K: "0 \<le> K"
   2.120 +    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   2.121 +    using nonneg_bounded by fast
   2.122 +  obtain B where B: "0 < B"
   2.123 +    and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F"
   2.124 +    using Y by (rule BfunE)
   2.125 +  have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F"
   2.126 +  using norm_Y proof (rule eventually_elim1)
   2.127 +    fix i
   2.128 +    assume *: "norm (Y i) \<le> B"
   2.129 +    have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
   2.130 +      by (rule norm_le)
   2.131 +    also have "\<dots> \<le> norm (X i) * B * K"
   2.132 +      by (intro mult_mono' order_refl norm_Y norm_ge_zero
   2.133 +                mult_nonneg_nonneg K *)
   2.134 +    also have "\<dots> = norm (X i) * (B * K)"
   2.135 +      by (rule mult_assoc)
   2.136 +    finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" .
   2.137 +  qed
   2.138 +  with X show ?thesis
   2.139 +  by (rule Zfun_imp_Zfun)
   2.140 +qed
   2.141 +
   2.142 +lemma (in bounded_bilinear) flip:
   2.143 +  "bounded_bilinear (\<lambda>x y. y ** x)"
   2.144 +apply default
   2.145 +apply (rule add_right)
   2.146 +apply (rule add_left)
   2.147 +apply (rule scaleR_right)
   2.148 +apply (rule scaleR_left)
   2.149 +apply (subst mult_commute)
   2.150 +using bounded by fast
   2.151 +
   2.152 +lemma (in bounded_bilinear) Bfun_prod_Zfun:
   2.153 +  assumes X: "Bfun X F"
   2.154 +  assumes Y: "Zfun Y F"
   2.155 +  shows "Zfun (\<lambda>n. X n ** Y n) F"
   2.156 +using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
   2.157 +
   2.158 +lemma inverse_diff_inverse:
   2.159 +  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
   2.160 +   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
   2.161 +by (simp add: algebra_simps)
   2.162 +
   2.163 +lemma Bfun_inverse_lemma:
   2.164 +  fixes x :: "'a::real_normed_div_algebra"
   2.165 +  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
   2.166 +apply (subst nonzero_norm_inverse, clarsimp)
   2.167 +apply (erule (1) le_imp_inverse_le)
   2.168 +done
   2.169 +
   2.170 +lemma Bfun_inverse:
   2.171 +  fixes a :: "'a::real_normed_div_algebra"
   2.172 +  assumes X: "tendsto X a F"
   2.173 +  assumes a: "a \<noteq> 0"
   2.174 +  shows "Bfun (\<lambda>n. inverse (X n)) F"
   2.175 +proof -
   2.176 +  from a have "0 < norm a" by simp
   2.177 +  hence "\<exists>r>0. r < norm a" by (rule dense)
   2.178 +  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   2.179 +  have "eventually (\<lambda>i. dist (X i) a < r) F"
   2.180 +    using tendstoD [OF X r1] by fast
   2.181 +  hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F"
   2.182 +  proof (rule eventually_elim1)
   2.183 +    fix i
   2.184 +    assume "dist (X i) a < r"
   2.185 +    hence 1: "norm (X i - a) < r"
   2.186 +      by (simp add: dist_norm)
   2.187 +    hence 2: "X i \<noteq> 0" using r2 by auto
   2.188 +    hence "norm (inverse (X i)) = inverse (norm (X i))"
   2.189 +      by (rule nonzero_norm_inverse)
   2.190 +    also have "\<dots> \<le> inverse (norm a - r)"
   2.191 +    proof (rule le_imp_inverse_le)
   2.192 +      show "0 < norm a - r" using r2 by simp
   2.193 +    next
   2.194 +      have "norm a - norm (X i) \<le> norm (a - X i)"
   2.195 +        by (rule norm_triangle_ineq2)
   2.196 +      also have "\<dots> = norm (X i - a)"
   2.197 +        by (rule norm_minus_commute)
   2.198 +      also have "\<dots> < r" using 1 .
   2.199 +      finally show "norm a - r \<le> norm (X i)" by simp
   2.200 +    qed
   2.201 +    finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" .
   2.202 +  qed
   2.203 +  thus ?thesis by (rule BfunI)
   2.204 +qed
   2.205 +
   2.206 +lemma tendsto_inverse_lemma:
   2.207 +  fixes a :: "'a::real_normed_div_algebra"
   2.208 +  shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk>
   2.209 +         \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
   2.210 +apply (subst tendsto_Zfun_iff)
   2.211 +apply (rule Zfun_ssubst)
   2.212 +apply (erule eventually_elim1)
   2.213 +apply (erule (1) inverse_diff_inverse)
   2.214 +apply (rule Zfun_minus)
   2.215 +apply (rule Zfun_mult_left)
   2.216 +apply (rule mult.Bfun_prod_Zfun)
   2.217 +apply (erule (1) Bfun_inverse)
   2.218 +apply (simp add: tendsto_Zfun_iff)
   2.219 +done
   2.220 +
   2.221 +lemma tendsto_inverse:
   2.222 +  fixes a :: "'a::real_normed_div_algebra"
   2.223 +  assumes X: "tendsto X a F"
   2.224 +  assumes a: "a \<noteq> 0"
   2.225 +  shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
   2.226 +proof -
   2.227 +  from a have "0 < norm a" by simp
   2.228 +  with X have "eventually (\<lambda>i. dist (X i) a < norm a) F"
   2.229 +    by (rule tendstoD)
   2.230 +  then have "eventually (\<lambda>i. X i \<noteq> 0) F"
   2.231 +    unfolding dist_norm by (auto elim!: eventually_elim1)
   2.232 +  with X a show ?thesis
   2.233 +    by (rule tendsto_inverse_lemma)
   2.234 +qed
   2.235 +
   2.236 +lemma tendsto_divide:
   2.237 +  fixes a b :: "'a::real_normed_field"
   2.238 +  shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk>
   2.239 +    \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F"
   2.240 +by (simp add: mult.tendsto tendsto_inverse divide_inverse)
   2.241 +
   2.242  end
     3.1 --- a/src/HOL/SEQ.thy	Mon Jun 01 08:04:19 2009 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Mon Jun 01 10:36:42 2009 -0700
     3.3 @@ -132,6 +132,13 @@
     3.4  apply (drule_tac x="n - k" in spec, simp)
     3.5  done
     3.6  
     3.7 +lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
     3.8 +unfolding Bfun_def eventually_sequentially
     3.9 +apply (rule iffI)
    3.10 +apply (simp add: Bseq_def, fast)
    3.11 +apply (fast intro: BseqI2')
    3.12 +done
    3.13 +
    3.14  
    3.15  subsection {* Sequences That Converge to Zero *}
    3.16  
    3.17 @@ -156,7 +163,8 @@
    3.18    assumes X: "Zseq X"
    3.19    assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
    3.20    shows "Zseq (\<lambda>n. Y n)"
    3.21 -using assms unfolding Zseq_conv_Zfun by (rule Zfun_imp_Zfun)
    3.22 +using X Y Zfun_imp_Zfun [of X sequentially Y K]
    3.23 +unfolding Zseq_conv_Zfun by simp
    3.24  
    3.25  lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
    3.26  by (erule_tac K="1" in Zseq_imp_Zseq, simp)
    3.27 @@ -180,54 +188,14 @@
    3.28  unfolding Zseq_conv_Zfun by (rule Zfun)
    3.29  
    3.30  lemma (in bounded_bilinear) Zseq_prod_Bseq:
    3.31 -  assumes X: "Zseq X"
    3.32 -  assumes Y: "Bseq Y"
    3.33 -  shows "Zseq (\<lambda>n. X n ** Y n)"
    3.34 -proof -
    3.35 -  obtain K where K: "0 \<le> K"
    3.36 -    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
    3.37 -    using nonneg_bounded by fast
    3.38 -  obtain B where B: "0 < B"
    3.39 -    and norm_Y: "\<And>n. norm (Y n) \<le> B"
    3.40 -    using Y [unfolded Bseq_def] by fast
    3.41 -  from X show ?thesis
    3.42 -  proof (rule Zseq_imp_Zseq)
    3.43 -    fix n::nat
    3.44 -    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
    3.45 -      by (rule norm_le)
    3.46 -    also have "\<dots> \<le> norm (X n) * B * K"
    3.47 -      by (intro mult_mono' order_refl norm_Y norm_ge_zero
    3.48 -                mult_nonneg_nonneg K)
    3.49 -    also have "\<dots> = norm (X n) * (B * K)"
    3.50 -      by (rule mult_assoc)
    3.51 -    finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" .
    3.52 -  qed
    3.53 -qed
    3.54 +  "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    3.55 +unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    3.56 +by (rule Zfun_prod_Bfun)
    3.57  
    3.58  lemma (in bounded_bilinear) Bseq_prod_Zseq:
    3.59 -  assumes X: "Bseq X"
    3.60 -  assumes Y: "Zseq Y"
    3.61 -  shows "Zseq (\<lambda>n. X n ** Y n)"
    3.62 -proof -
    3.63 -  obtain K where K: "0 \<le> K"
    3.64 -    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
    3.65 -    using nonneg_bounded by fast
    3.66 -  obtain B where B: "0 < B"
    3.67 -    and norm_X: "\<And>n. norm (X n) \<le> B"
    3.68 -    using X [unfolded Bseq_def] by fast
    3.69 -  from Y show ?thesis
    3.70 -  proof (rule Zseq_imp_Zseq)
    3.71 -    fix n::nat
    3.72 -    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
    3.73 -      by (rule norm_le)
    3.74 -    also have "\<dots> \<le> B * norm (Y n) * K"
    3.75 -      by (intro mult_mono' order_refl norm_X norm_ge_zero
    3.76 -                mult_nonneg_nonneg K)
    3.77 -    also have "\<dots> = norm (Y n) * (B * K)"
    3.78 -      by (simp only: mult_ac)
    3.79 -    finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" .
    3.80 -  qed
    3.81 -qed
    3.82 +  "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    3.83 +unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    3.84 +by (rule Bfun_prod_Zfun)
    3.85  
    3.86  lemma (in bounded_bilinear) Zseq_left:
    3.87    "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
    3.88 @@ -363,11 +331,6 @@
    3.89    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    3.90  by (rule mult.LIMSEQ)
    3.91  
    3.92 -lemma inverse_diff_inverse:
    3.93 -  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    3.94 -   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
    3.95 -by (simp add: algebra_simps)
    3.96 -
    3.97  lemma Bseq_inverse_lemma:
    3.98    fixes x :: "'a::real_normed_div_algebra"
    3.99    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
   3.100 @@ -377,69 +340,15 @@
   3.101  
   3.102  lemma Bseq_inverse:
   3.103    fixes a :: "'a::real_normed_div_algebra"
   3.104 -  assumes X: "X ----> a"
   3.105 -  assumes a: "a \<noteq> 0"
   3.106 -  shows "Bseq (\<lambda>n. inverse (X n))"
   3.107 -proof -
   3.108 -  from a have "0 < norm a" by simp
   3.109 -  hence "\<exists>r>0. r < norm a" by (rule dense)
   3.110 -  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   3.111 -  obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
   3.112 -    using LIMSEQ_D [OF X r1] by fast
   3.113 -  show ?thesis
   3.114 -  proof (rule BseqI2' [rule_format])
   3.115 -    fix n assume n: "N \<le> n"
   3.116 -    hence 1: "norm (X n - a) < r" by (rule N)
   3.117 -    hence 2: "X n \<noteq> 0" using r2 by auto
   3.118 -    hence "norm (inverse (X n)) = inverse (norm (X n))"
   3.119 -      by (rule nonzero_norm_inverse)
   3.120 -    also have "\<dots> \<le> inverse (norm a - r)"
   3.121 -    proof (rule le_imp_inverse_le)
   3.122 -      show "0 < norm a - r" using r2 by simp
   3.123 -    next
   3.124 -      have "norm a - norm (X n) \<le> norm (a - X n)"
   3.125 -        by (rule norm_triangle_ineq2)
   3.126 -      also have "\<dots> = norm (X n - a)"
   3.127 -        by (rule norm_minus_commute)
   3.128 -      also have "\<dots> < r" using 1 .
   3.129 -      finally show "norm a - r \<le> norm (X n)" by simp
   3.130 -    qed
   3.131 -    finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" .
   3.132 -  qed
   3.133 -qed
   3.134 -
   3.135 -lemma LIMSEQ_inverse_lemma:
   3.136 -  fixes a :: "'a::real_normed_div_algebra"
   3.137 -  shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk>
   3.138 -         \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
   3.139 -apply (subst LIMSEQ_Zseq_iff)
   3.140 -apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
   3.141 -apply (rule Zseq_minus)
   3.142 -apply (rule Zseq_mult_left)
   3.143 -apply (rule mult.Bseq_prod_Zseq)
   3.144 -apply (erule (1) Bseq_inverse)
   3.145 -apply (simp add: LIMSEQ_Zseq_iff)
   3.146 -done
   3.147 +  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
   3.148 +unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
   3.149 +by (rule Bfun_inverse)
   3.150  
   3.151  lemma LIMSEQ_inverse:
   3.152    fixes a :: "'a::real_normed_div_algebra"
   3.153 -  assumes X: "X ----> a"
   3.154 -  assumes a: "a \<noteq> 0"
   3.155 -  shows "(\<lambda>n. inverse (X n)) ----> inverse a"
   3.156 -proof -
   3.157 -  from a have "0 < norm a" by simp
   3.158 -  then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a"
   3.159 -    using LIMSEQ_D [OF X] by fast
   3.160 -  hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto
   3.161 -  hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp
   3.162 -
   3.163 -  from X have "(\<lambda>n. X (n + k)) ----> a"
   3.164 -    by (rule LIMSEQ_ignore_initial_segment)
   3.165 -  hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a"
   3.166 -    using a k by (rule LIMSEQ_inverse_lemma)
   3.167 -  thus "(\<lambda>n. inverse (X n)) ----> inverse a"
   3.168 -    by (rule LIMSEQ_offset)
   3.169 -qed
   3.170 +  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
   3.171 +unfolding LIMSEQ_conv_tendsto
   3.172 +by (rule tendsto_inverse)
   3.173  
   3.174  lemma LIMSEQ_divide:
   3.175    fixes a b :: "'a::real_normed_field"