src/HOL/SEQ.thy
changeset 31355 3d18766ddc4b
parent 31353 14a58e2ca374
child 31392 69570155ddf8
     1.1 --- a/src/HOL/SEQ.thy	Mon Jun 01 08:04:19 2009 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Mon Jun 01 10:36:42 2009 -0700
     1.3 @@ -132,6 +132,13 @@
     1.4  apply (drule_tac x="n - k" in spec, simp)
     1.5  done
     1.6  
     1.7 +lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
     1.8 +unfolding Bfun_def eventually_sequentially
     1.9 +apply (rule iffI)
    1.10 +apply (simp add: Bseq_def, fast)
    1.11 +apply (fast intro: BseqI2')
    1.12 +done
    1.13 +
    1.14  
    1.15  subsection {* Sequences That Converge to Zero *}
    1.16  
    1.17 @@ -156,7 +163,8 @@
    1.18    assumes X: "Zseq X"
    1.19    assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
    1.20    shows "Zseq (\<lambda>n. Y n)"
    1.21 -using assms unfolding Zseq_conv_Zfun by (rule Zfun_imp_Zfun)
    1.22 +using X Y Zfun_imp_Zfun [of X sequentially Y K]
    1.23 +unfolding Zseq_conv_Zfun by simp
    1.24  
    1.25  lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
    1.26  by (erule_tac K="1" in Zseq_imp_Zseq, simp)
    1.27 @@ -180,54 +188,14 @@
    1.28  unfolding Zseq_conv_Zfun by (rule Zfun)
    1.29  
    1.30  lemma (in bounded_bilinear) Zseq_prod_Bseq:
    1.31 -  assumes X: "Zseq X"
    1.32 -  assumes Y: "Bseq Y"
    1.33 -  shows "Zseq (\<lambda>n. X n ** Y n)"
    1.34 -proof -
    1.35 -  obtain K where K: "0 \<le> K"
    1.36 -    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
    1.37 -    using nonneg_bounded by fast
    1.38 -  obtain B where B: "0 < B"
    1.39 -    and norm_Y: "\<And>n. norm (Y n) \<le> B"
    1.40 -    using Y [unfolded Bseq_def] by fast
    1.41 -  from X show ?thesis
    1.42 -  proof (rule Zseq_imp_Zseq)
    1.43 -    fix n::nat
    1.44 -    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
    1.45 -      by (rule norm_le)
    1.46 -    also have "\<dots> \<le> norm (X n) * B * K"
    1.47 -      by (intro mult_mono' order_refl norm_Y norm_ge_zero
    1.48 -                mult_nonneg_nonneg K)
    1.49 -    also have "\<dots> = norm (X n) * (B * K)"
    1.50 -      by (rule mult_assoc)
    1.51 -    finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" .
    1.52 -  qed
    1.53 -qed
    1.54 +  "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    1.55 +unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    1.56 +by (rule Zfun_prod_Bfun)
    1.57  
    1.58  lemma (in bounded_bilinear) Bseq_prod_Zseq:
    1.59 -  assumes X: "Bseq X"
    1.60 -  assumes Y: "Zseq Y"
    1.61 -  shows "Zseq (\<lambda>n. X n ** Y n)"
    1.62 -proof -
    1.63 -  obtain K where K: "0 \<le> K"
    1.64 -    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
    1.65 -    using nonneg_bounded by fast
    1.66 -  obtain B where B: "0 < B"
    1.67 -    and norm_X: "\<And>n. norm (X n) \<le> B"
    1.68 -    using X [unfolded Bseq_def] by fast
    1.69 -  from Y show ?thesis
    1.70 -  proof (rule Zseq_imp_Zseq)
    1.71 -    fix n::nat
    1.72 -    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
    1.73 -      by (rule norm_le)
    1.74 -    also have "\<dots> \<le> B * norm (Y n) * K"
    1.75 -      by (intro mult_mono' order_refl norm_X norm_ge_zero
    1.76 -                mult_nonneg_nonneg K)
    1.77 -    also have "\<dots> = norm (Y n) * (B * K)"
    1.78 -      by (simp only: mult_ac)
    1.79 -    finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" .
    1.80 -  qed
    1.81 -qed
    1.82 +  "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    1.83 +unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    1.84 +by (rule Bfun_prod_Zfun)
    1.85  
    1.86  lemma (in bounded_bilinear) Zseq_left:
    1.87    "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
    1.88 @@ -363,11 +331,6 @@
    1.89    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    1.90  by (rule mult.LIMSEQ)
    1.91  
    1.92 -lemma inverse_diff_inverse:
    1.93 -  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    1.94 -   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
    1.95 -by (simp add: algebra_simps)
    1.96 -
    1.97  lemma Bseq_inverse_lemma:
    1.98    fixes x :: "'a::real_normed_div_algebra"
    1.99    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
   1.100 @@ -377,69 +340,15 @@
   1.101  
   1.102  lemma Bseq_inverse:
   1.103    fixes a :: "'a::real_normed_div_algebra"
   1.104 -  assumes X: "X ----> a"
   1.105 -  assumes a: "a \<noteq> 0"
   1.106 -  shows "Bseq (\<lambda>n. inverse (X n))"
   1.107 -proof -
   1.108 -  from a have "0 < norm a" by simp
   1.109 -  hence "\<exists>r>0. r < norm a" by (rule dense)
   1.110 -  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   1.111 -  obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
   1.112 -    using LIMSEQ_D [OF X r1] by fast
   1.113 -  show ?thesis
   1.114 -  proof (rule BseqI2' [rule_format])
   1.115 -    fix n assume n: "N \<le> n"
   1.116 -    hence 1: "norm (X n - a) < r" by (rule N)
   1.117 -    hence 2: "X n \<noteq> 0" using r2 by auto
   1.118 -    hence "norm (inverse (X n)) = inverse (norm (X n))"
   1.119 -      by (rule nonzero_norm_inverse)
   1.120 -    also have "\<dots> \<le> inverse (norm a - r)"
   1.121 -    proof (rule le_imp_inverse_le)
   1.122 -      show "0 < norm a - r" using r2 by simp
   1.123 -    next
   1.124 -      have "norm a - norm (X n) \<le> norm (a - X n)"
   1.125 -        by (rule norm_triangle_ineq2)
   1.126 -      also have "\<dots> = norm (X n - a)"
   1.127 -        by (rule norm_minus_commute)
   1.128 -      also have "\<dots> < r" using 1 .
   1.129 -      finally show "norm a - r \<le> norm (X n)" by simp
   1.130 -    qed
   1.131 -    finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" .
   1.132 -  qed
   1.133 -qed
   1.134 -
   1.135 -lemma LIMSEQ_inverse_lemma:
   1.136 -  fixes a :: "'a::real_normed_div_algebra"
   1.137 -  shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk>
   1.138 -         \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
   1.139 -apply (subst LIMSEQ_Zseq_iff)
   1.140 -apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
   1.141 -apply (rule Zseq_minus)
   1.142 -apply (rule Zseq_mult_left)
   1.143 -apply (rule mult.Bseq_prod_Zseq)
   1.144 -apply (erule (1) Bseq_inverse)
   1.145 -apply (simp add: LIMSEQ_Zseq_iff)
   1.146 -done
   1.147 +  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
   1.148 +unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
   1.149 +by (rule Bfun_inverse)
   1.150  
   1.151  lemma LIMSEQ_inverse:
   1.152    fixes a :: "'a::real_normed_div_algebra"
   1.153 -  assumes X: "X ----> a"
   1.154 -  assumes a: "a \<noteq> 0"
   1.155 -  shows "(\<lambda>n. inverse (X n)) ----> inverse a"
   1.156 -proof -
   1.157 -  from a have "0 < norm a" by simp
   1.158 -  then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a"
   1.159 -    using LIMSEQ_D [OF X] by fast
   1.160 -  hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto
   1.161 -  hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp
   1.162 -
   1.163 -  from X have "(\<lambda>n. X (n + k)) ----> a"
   1.164 -    by (rule LIMSEQ_ignore_initial_segment)
   1.165 -  hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a"
   1.166 -    using a k by (rule LIMSEQ_inverse_lemma)
   1.167 -  thus "(\<lambda>n. inverse (X n)) ----> inverse a"
   1.168 -    by (rule LIMSEQ_offset)
   1.169 -qed
   1.170 +  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
   1.171 +unfolding LIMSEQ_conv_tendsto
   1.172 +by (rule tendsto_inverse)
   1.173  
   1.174  lemma LIMSEQ_divide:
   1.175    fixes a b :: "'a::real_normed_field"