src/HOL/Series.thy
changeset 56213 e5720d3c18f0
parent 56194 9ffbb4004c81
child 56217 dc429a5b13c4
     1.1 --- a/src/HOL/Series.thy	Tue Mar 18 22:11:46 2014 +0100
     1.2 +++ b/src/HOL/Series.thy	Wed Mar 19 15:34:57 2014 +0100
     1.3 @@ -7,12 +7,14 @@
     1.4  Additional contributions by Jeremy Avigad
     1.5  *)
     1.6  
     1.7 -header {* Finite Summation and Infinite Series *}
     1.8 +header {* Infinite Series *}
     1.9  
    1.10  theory Series
    1.11  imports Limits
    1.12  begin
    1.13  
    1.14 +subsection {* Definition of infinite summability *}
    1.15 +
    1.16  definition
    1.17    sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
    1.18    (infixr "sums" 80)
    1.19 @@ -28,6 +30,8 @@
    1.20  where
    1.21    "suminf f = (THE s. f sums s)"
    1.22  
    1.23 +subsection {* Infinite summability on topological monoids *}
    1.24 +
    1.25  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
    1.26    by simp
    1.27  
    1.28 @@ -40,6 +44,24 @@
    1.29  lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
    1.30    by (simp add: suminf_def sums_def lim_def)
    1.31  
    1.32 +lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
    1.33 +  unfolding sums_def by (simp add: tendsto_const)
    1.34 +
    1.35 +lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    1.36 +  by (rule sums_zero [THEN sums_summable])
    1.37 +
    1.38 +lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
    1.39 +  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
    1.40 +  apply safe
    1.41 +  apply (erule_tac x=S in allE)
    1.42 +  apply safe
    1.43 +  apply (rule_tac x="N" in exI, safe)
    1.44 +  apply (drule_tac x="n*k" in spec)
    1.45 +  apply (erule mp)
    1.46 +  apply (erule order_trans)
    1.47 +  apply simp
    1.48 +  done
    1.49 +
    1.50  lemma sums_finite:
    1.51    assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    1.52    shows "f sums (\<Sum>n\<in>N. f n)"
    1.53 @@ -65,36 +87,26 @@
    1.54         (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
    1.55  qed
    1.56  
    1.57 +lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
    1.58 +  by (rule sums_summable) (rule sums_finite)
    1.59 +
    1.60  lemma sums_If_finite_set: "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0) sums (\<Sum>r\<in>A. f r)"
    1.61    using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
    1.62  
    1.63 +lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)"
    1.64 +  by (rule sums_summable) (rule sums_If_finite_set)
    1.65 +
    1.66  lemma sums_If_finite: "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0) sums (\<Sum>r | P r. f r)"
    1.67    using sums_If_finite_set[of "{r. P r}"] by simp
    1.68  
    1.69 +lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)"
    1.70 +  by (rule sums_summable) (rule sums_If_finite)
    1.71 +
    1.72  lemma sums_single: "(\<lambda>r. if r = i then f r else 0) sums f i"
    1.73    using sums_If_finite[of "\<lambda>r. r = i"] by simp
    1.74  
    1.75 -lemma series_zero: (* REMOVE *)
    1.76 -  "(\<And>m. n \<le> m \<Longrightarrow> f m = 0) \<Longrightarrow> f sums (\<Sum>i<n. f i)"
    1.77 -  by (rule sums_finite) auto
    1.78 -
    1.79 -lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
    1.80 -  unfolding sums_def by (simp add: tendsto_const)
    1.81 -
    1.82 -lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    1.83 -  by (rule sums_zero [THEN sums_summable])
    1.84 -
    1.85 -lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
    1.86 -  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
    1.87 -  apply safe
    1.88 -  apply (erule_tac x=S in allE)
    1.89 -  apply safe
    1.90 -  apply (rule_tac x="N" in exI, safe)
    1.91 -  apply (drule_tac x="n*k" in spec)
    1.92 -  apply (erule mp)
    1.93 -  apply (erule order_trans)
    1.94 -  apply simp
    1.95 -  done
    1.96 +lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)"
    1.97 +  by (rule sums_summable) (rule sums_single)
    1.98  
    1.99  context
   1.100    fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
   1.101 @@ -123,26 +135,53 @@
   1.102  lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0"
   1.103    by (rule sums_zero [THEN sums_unique, symmetric])
   1.104  
   1.105 +
   1.106 +subsection {* Infinite summability on ordered, topological monoids *}
   1.107 +
   1.108 +lemma sums_le:
   1.109 +  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   1.110 +  shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
   1.111 +  by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
   1.112 +
   1.113  context
   1.114    fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   1.115  begin
   1.116  
   1.117 -lemma series_pos_le: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
   1.118 -  apply (rule LIMSEQ_le_const[OF summable_LIMSEQ])
   1.119 -  apply assumption
   1.120 -  apply (intro exI[of _ n])
   1.121 -  apply (auto intro!: setsum_mono2 simp: not_le[symmetric])
   1.122 -  done
   1.123 +lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   1.124 +  by (auto dest: sums_summable intro: sums_le)
   1.125 +
   1.126 +lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
   1.127 +  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
   1.128 +
   1.129 +lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
   1.130 +  using setsum_le_suminf[of 0] by simp
   1.131 +
   1.132 +lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
   1.133 +  using
   1.134 +    setsum_le_suminf[of "Suc i"]
   1.135 +    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   1.136 +    setsum_mono2[of "{..<i}" "{..<n}" f]
   1.137 +  by (auto simp: less_imp_le ac_simps)
   1.138 +
   1.139 +lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   1.140 +  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
   1.141 +
   1.142 +lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
   1.143 +  using setsum_less_suminf2[of 0 i] by simp
   1.144 +
   1.145 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
   1.146 +  using suminf_pos2[of 0] by (simp add: less_imp_le)
   1.147 +
   1.148 +lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   1.149 +  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
   1.150  
   1.151  lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
   1.152  proof
   1.153    assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
   1.154 -  then have "f sums 0"
   1.155 -    by (simp add: sums_iff)
   1.156    then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
   1.157 -    by (simp add: sums_def atLeast0LessThan)
   1.158 -  have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
   1.159 -  proof (rule LIMSEQ_le_const[OF f])
   1.160 +    using summable_LIMSEQ[of f] by simp
   1.161 +  then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
   1.162 +  proof (rule LIMSEQ_le_const)
   1.163      fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
   1.164        using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
   1.165    qed
   1.166 @@ -150,33 +189,34 @@
   1.167      by (auto intro!: antisym)
   1.168  qed (metis suminf_zero fun_eq_iff)
   1.169  
   1.170 -lemma suminf_gt_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   1.171 -  using series_pos_le[of 0] suminf_eq_zero_iff by (simp add: less_le)
   1.172 -
   1.173 -lemma suminf_gt_zero: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
   1.174 -  using suminf_gt_zero_iff by (simp add: less_imp_le)
   1.175 -
   1.176 -lemma suminf_ge_zero: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
   1.177 -  by (drule_tac n="0" in series_pos_le) simp_all
   1.178 -
   1.179 -lemma suminf_le: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   1.180 -  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
   1.181 -
   1.182 -lemma summable_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   1.183 -  by (rule LIMSEQ_le) (auto intro: setsum_mono summable_LIMSEQ)
   1.184 +lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   1.185 +  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   1.186  
   1.187  end
   1.188  
   1.189 -lemma series_pos_less:
   1.190 -  fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
   1.191 -  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {..<n} < suminf f"
   1.192 -  apply simp
   1.193 -  apply (rule_tac y="setsum f {..<Suc n}" in order_less_le_trans)
   1.194 -  using add_less_cancel_left [of "setsum f {..<n}" 0 "f n"]
   1.195 -  apply simp
   1.196 -  apply (erule series_pos_le)
   1.197 -  apply (simp add: order_less_imp_le)
   1.198 -  done
   1.199 +lemma summableI_nonneg_bounded:
   1.200 +  fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}"
   1.201 +  assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
   1.202 +  shows "summable f"
   1.203 +  unfolding summable_def sums_def[abs_def]
   1.204 +proof (intro exI order_tendstoI)
   1.205 +  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
   1.206 +    using le by (auto simp: bdd_above_def)
   1.207 +  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
   1.208 +    then obtain n where "a < (\<Sum>i<n. f i)"
   1.209 +      by (auto simp add: less_cSUP_iff)
   1.210 +    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
   1.211 +      by (rule less_le_trans) (auto intro!: setsum_mono2)
   1.212 +    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
   1.213 +      by (auto simp: eventually_sequentially) }
   1.214 +  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
   1.215 +    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
   1.216 +      by (auto intro: cSUP_upper)
   1.217 +    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
   1.218 +      by (auto intro: le_less_trans simp: eventually_sequentially) }
   1.219 +qed
   1.220 +
   1.221 +subsection {* Infinite summability on real normed vector spaces *}
   1.222  
   1.223  lemma sums_Suc_iff:
   1.224    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.225 @@ -289,6 +329,8 @@
   1.226  lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
   1.227  lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
   1.228  
   1.229 +subsection {* Infinite summability on real normed algebras *}
   1.230 +
   1.231  context
   1.232    fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra"
   1.233  begin
   1.234 @@ -313,6 +355,8 @@
   1.235  
   1.236  end
   1.237  
   1.238 +subsection {* Infinite summability on real normed fields *}
   1.239 +
   1.240  context
   1.241    fixes c :: "'a::real_normed_field"
   1.242  begin
   1.243 @@ -361,6 +405,8 @@
   1.244      by simp
   1.245  qed
   1.246  
   1.247 +subsection {* Infinite summability on Banach spaces *}
   1.248 +
   1.249  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   1.250  
   1.251  lemma summable_Cauchy:
   1.252 @@ -452,12 +498,6 @@
   1.253  
   1.254  end
   1.255  
   1.256 -lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.257 -  by (rule summable_comparison_test) auto
   1.258 -
   1.259 -lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
   1.260 -  by (rule summable_norm_cancel) simp
   1.261 -
   1.262  text{*Summability of geometric series for real algebras*}
   1.263  
   1.264  lemma complete_algebra_summable_geometric:
   1.265 @@ -470,34 +510,6 @@
   1.266      by (simp add: summable_geometric)
   1.267  qed
   1.268  
   1.269 -
   1.270 -text{*A summable series of positive terms has limit that is at least as
   1.271 -great as any partial sum.*}
   1.272 -
   1.273 -lemma pos_summable:
   1.274 -  fixes f:: "nat \<Rightarrow> real"
   1.275 -  assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {..<n} \<le> x"
   1.276 -  shows "summable f"
   1.277 -proof -
   1.278 -  have "convergent (\<lambda>n. setsum f {..<n})"
   1.279 -  proof (rule Bseq_mono_convergent)
   1.280 -    show "Bseq (\<lambda>n. setsum f {..<n})"
   1.281 -      by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
   1.282 -  qed (auto intro: setsum_mono2 pos)
   1.283 -  thus ?thesis
   1.284 -    by (force simp add: summable_def sums_def convergent_def)
   1.285 -qed
   1.286 -
   1.287 -lemma summable_rabs_comparison_test:
   1.288 -  fixes f :: "nat \<Rightarrow> real"
   1.289 -  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
   1.290 -  by (rule summable_comparison_test) auto
   1.291 -
   1.292 -lemma summable_rabs:
   1.293 -  fixes f :: "nat \<Rightarrow> real"
   1.294 -  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   1.295 -by (fold real_norm_def, rule summable_norm)
   1.296 -
   1.297  subsection {* Cauchy Product Formula *}
   1.298  
   1.299  text {*
   1.300 @@ -507,14 +519,14 @@
   1.301  
   1.302  lemma setsum_triangle_reindex:
   1.303    fixes n :: nat
   1.304 -  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i=0..k. f i (k - i))"
   1.305 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
   1.306  proof -
   1.307    have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
   1.308 -    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {0..k}). f i (k - i))"
   1.309 +    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
   1.310    proof (rule setsum_reindex_cong)
   1.311 -    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {0..k})"
   1.312 +    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
   1.313        by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
   1.314 -    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {0..k})"
   1.315 +    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
   1.316        by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
   1.317      show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
   1.318        by clarify
   1.319 @@ -526,7 +538,7 @@
   1.320    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.321    assumes a: "summable (\<lambda>k. norm (a k))"
   1.322    assumes b: "summable (\<lambda>k. norm (b k))"
   1.323 -  shows "(\<lambda>k. \<Sum>i=0..k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
   1.324 +  shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
   1.325  proof -
   1.326    let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}"
   1.327    let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}"
   1.328 @@ -598,8 +610,22 @@
   1.329    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.330    assumes a: "summable (\<lambda>k. norm (a k))"
   1.331    assumes b: "summable (\<lambda>k. norm (b k))"
   1.332 -  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
   1.333 -using a b
   1.334 -by (rule Cauchy_product_sums [THEN sums_unique])
   1.335 +  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))"
   1.336 +  using a b
   1.337 +  by (rule Cauchy_product_sums [THEN sums_unique])
   1.338 +
   1.339 +subsection {* Series on @{typ real}s *}
   1.340 +
   1.341 +lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.342 +  by (rule summable_comparison_test) auto
   1.343 +
   1.344 +lemma summable_rabs_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n :: real\<bar>)"
   1.345 +  by (rule summable_comparison_test) auto
   1.346 +
   1.347 +lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
   1.348 +  by (rule summable_norm_cancel) simp
   1.349 +
   1.350 +lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   1.351 +  by (fold real_norm_def) (rule summable_norm)
   1.352  
   1.353  end