src/HOL/Series.thy
 changeset 59712 6c013328b885 parent 59613 7103019278f0 child 59741 5b762cd73a8e
```     1.1 --- a/src/HOL/Series.thy	Sun Mar 15 23:46:00 2015 +0100
1.2 +++ b/src/HOL/Series.thy	Mon Mar 16 14:52:34 2015 +0100
1.3 @@ -10,8 +10,8 @@
1.4  section {* Infinite Series *}
1.5
1.6  theory Series
1.7 -imports Limits
1.8 -begin
1.9 +imports Limits Inequalities
1.10 +begin
1.11
1.12  subsection {* Definition of infinite summability *}
1.13
1.14 @@ -576,14 +576,6 @@
1.15    @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
1.16  *}
1.17
1.18 -lemma setsum_triangle_reindex:
1.19 -  fixes n :: nat
1.20 -  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.21 -  apply (simp add: setsum.Sigma)
1.22 -  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
1.23 -  apply auto
1.24 -  done
1.25 -
1.26  lemma Cauchy_product_sums:
1.27    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
1.28    assumes a: "summable (\<lambda>k. norm (a k))"
```