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