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))"