117 |
117 |
118 lemma sums_iff: |
118 lemma sums_iff: |
119 fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" |
119 fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" |
120 shows "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)" |
120 shows "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)" |
121 by (metis summable_sums sums_summable sums_unique) |
121 by (metis summable_sums sums_summable sums_unique) |
|
122 |
|
123 lemma sums_finite: |
|
124 assumes [simp]: "finite N" |
|
125 assumes f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" |
|
126 shows "f sums (\<Sum>n\<in>N. f n)" |
|
127 proof - |
|
128 { fix n |
|
129 have "setsum f {..<n + Suc (Max N)} = setsum f N" |
|
130 proof cases |
|
131 assume "N = {}" |
|
132 with f have "f = (\<lambda>x. 0)" by auto |
|
133 then show ?thesis by simp |
|
134 next |
|
135 assume [simp]: "N \<noteq> {}" |
|
136 show ?thesis |
|
137 proof (safe intro!: setsum_mono_zero_right f) |
|
138 fix i assume "i \<in> N" |
|
139 then have "i \<le> Max N" by simp |
|
140 then show "i < n + Suc (Max N)" by simp |
|
141 qed |
|
142 qed } |
|
143 note eq = this |
|
144 show ?thesis unfolding sums_def |
|
145 by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) |
|
146 (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right) |
|
147 qed |
|
148 |
|
149 lemma suminf_finite: |
|
150 fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" |
|
151 assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" |
|
152 shows "suminf f = (\<Sum>n\<in>N. f n)" |
|
153 using sums_finite[OF assms, THEN sums_unique] by simp |
|
154 |
|
155 lemma sums_If_finite_set: |
|
156 "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (\<Sum>r\<in>A. f r)" |
|
157 using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp |
|
158 |
|
159 lemma sums_If_finite: |
|
160 "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (\<Sum>r | P r. f r)" |
|
161 using sums_If_finite_set[of "{r. P r}" f] by simp |
|
162 |
|
163 lemma sums_single: |
|
164 "(\<lambda>r. if r = i then f r else 0::'a::{comm_monoid_add,t2_space}) sums f i" |
|
165 using sums_If_finite[of "\<lambda>r. r = i" f] by simp |
122 |
166 |
123 lemma sums_split_initial_segment: |
167 lemma sums_split_initial_segment: |
124 fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
168 fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
125 shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))" |
169 shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))" |
126 apply (unfold sums_def) |
170 apply (unfold sums_def) |