src/HOL/Series.thy
changeset 44282 f0de18b62d63
parent 41970 47d6e13d1710
child 44289 d81d09cdab9c
     1.1 --- a/src/HOL/Series.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Series.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -211,50 +211,54 @@
     1.4    "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
     1.5  by (intro sums_unique sums summable_sums)
     1.6  
     1.7 +lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
     1.8 +lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
     1.9 +lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
    1.10 +
    1.11  lemma sums_mult:
    1.12    fixes c :: "'a::real_normed_algebra"
    1.13    shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
    1.14 -by (rule mult_right.sums)
    1.15 +  by (rule bounded_linear.sums [OF bounded_linear_mult_right])
    1.16  
    1.17  lemma summable_mult:
    1.18    fixes c :: "'a::real_normed_algebra"
    1.19    shows "summable f \<Longrightarrow> summable (%n. c * f n)"
    1.20 -by (rule mult_right.summable)
    1.21 +  by (rule bounded_linear.summable [OF bounded_linear_mult_right])
    1.22  
    1.23  lemma suminf_mult:
    1.24    fixes c :: "'a::real_normed_algebra"
    1.25    shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
    1.26 -by (rule mult_right.suminf [symmetric])
    1.27 +  by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
    1.28  
    1.29  lemma sums_mult2:
    1.30    fixes c :: "'a::real_normed_algebra"
    1.31    shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
    1.32 -by (rule mult_left.sums)
    1.33 +  by (rule bounded_linear.sums [OF bounded_linear_mult_left])
    1.34  
    1.35  lemma summable_mult2:
    1.36    fixes c :: "'a::real_normed_algebra"
    1.37    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
    1.38 -by (rule mult_left.summable)
    1.39 +  by (rule bounded_linear.summable [OF bounded_linear_mult_left])
    1.40  
    1.41  lemma suminf_mult2:
    1.42    fixes c :: "'a::real_normed_algebra"
    1.43    shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
    1.44 -by (rule mult_left.suminf)
    1.45 +  by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
    1.46  
    1.47  lemma sums_divide:
    1.48    fixes c :: "'a::real_normed_field"
    1.49    shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
    1.50 -by (rule divide.sums)
    1.51 +  by (rule bounded_linear.sums [OF bounded_linear_divide])
    1.52  
    1.53  lemma summable_divide:
    1.54    fixes c :: "'a::real_normed_field"
    1.55    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
    1.56 -by (rule divide.summable)
    1.57 +  by (rule bounded_linear.summable [OF bounded_linear_divide])
    1.58  
    1.59  lemma suminf_divide:
    1.60    fixes c :: "'a::real_normed_field"
    1.61    shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
    1.62 -by (rule divide.suminf [symmetric])
    1.63 +  by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
    1.64  
    1.65  lemma sums_add:
    1.66    fixes a b :: "'a::real_normed_field"
    1.67 @@ -423,7 +427,7 @@
    1.68      by auto
    1.69    have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
    1.70      by simp
    1.71 -  thus ?thesis using divide.sums [OF 2, of 2]
    1.72 +  thus ?thesis using sums_divide [OF 2, of 2]
    1.73      by simp
    1.74  qed
    1.75