src/HOL/Series.thy
changeset 44568 e6f291cb5810
parent 44289 d81d09cdab9c
child 44710 9caf6883f1f4
     1.1 --- a/src/HOL/Series.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/Series.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -183,12 +183,12 @@
     1.4      unfolding sums_def
     1.5      apply (rule LIMSEQ_offset[of _ n])
     1.6      unfolding setsum_const
     1.7 -    apply (rule LIMSEQ_const)
     1.8 +    apply (rule tendsto_const)
     1.9      done
    1.10  qed
    1.11  
    1.12  lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
    1.13 -unfolding sums_def by (simp add: LIMSEQ_const)
    1.14 +  unfolding sums_def by (simp add: tendsto_const)
    1.15  
    1.16  lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    1.17  by (rule sums_zero [THEN sums_summable])
    1.18 @@ -198,7 +198,7 @@
    1.19  
    1.20  lemma (in bounded_linear) sums:
    1.21    "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
    1.22 -unfolding sums_def by (drule LIMSEQ, simp only: setsum)
    1.23 +  unfolding sums_def by (drule tendsto, simp only: setsum)
    1.24  
    1.25  lemma (in bounded_linear) summable:
    1.26    "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
    1.27 @@ -260,7 +260,7 @@
    1.28  lemma sums_add:
    1.29    fixes a b :: "'a::real_normed_field"
    1.30    shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
    1.31 -unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
    1.32 +  unfolding sums_def by (simp add: setsum_addf tendsto_add)
    1.33  
    1.34  lemma summable_add:
    1.35    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
    1.36 @@ -275,7 +275,7 @@
    1.37  lemma sums_diff:
    1.38    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
    1.39    shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)"
    1.40 -unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff)
    1.41 +  unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
    1.42  
    1.43  lemma summable_diff:
    1.44    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
    1.45 @@ -290,7 +290,7 @@
    1.46  lemma sums_minus:
    1.47    fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
    1.48    shows "X sums a ==> (\<lambda>n. - X n) sums (- a)"
    1.49 -unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus)
    1.50 +  unfolding sums_def by (simp add: setsum_negf tendsto_minus)
    1.51  
    1.52  lemma summable_minus:
    1.53    fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
    1.54 @@ -344,7 +344,7 @@
    1.55    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
    1.56  apply (drule summable_sums)
    1.57  apply (simp add: sums_def)
    1.58 -apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
    1.59 +apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
    1.60  apply (erule LIMSEQ_le, blast)
    1.61  apply (rule_tac x="n" in exI, clarify)
    1.62  apply (rule setsum_mono2)
    1.63 @@ -403,7 +403,7 @@
    1.64    from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
    1.65      by (rule LIMSEQ_power_zero)
    1.66    hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"
    1.67 -    using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
    1.68 +    using neq_0 by (intro tendsto_intros)
    1.69    hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
    1.70      by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
    1.71    thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
    1.72 @@ -583,7 +583,7 @@
    1.73  lemma summable_norm:
    1.74    fixes f :: "nat \<Rightarrow> 'a::banach"
    1.75    shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
    1.76 -by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel
    1.77 +  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel
    1.78                  summable_sumr_LIMSEQ_suminf norm_setsum)
    1.79  
    1.80  lemma summable_rabs:
    1.81 @@ -692,7 +692,7 @@
    1.82  
    1.83    have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k))
    1.84             ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    1.85 -    by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf
    1.86 +    by (intro tendsto_mult summable_sumr_LIMSEQ_suminf
    1.87          summable_norm_cancel [OF a] summable_norm_cancel [OF b])
    1.88    hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    1.89      by (simp only: setsum_product setsum_Sigma [rule_format]
    1.90 @@ -700,7 +700,7 @@
    1.91  
    1.92    have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k)))
    1.93         ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
    1.94 -    using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf)
    1.95 +    using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf)
    1.96    hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
    1.97      by (simp only: setsum_product setsum_Sigma [rule_format]
    1.98                     finite_atLeastLessThan)