equal
deleted
inserted
replaced
126 note eq = this |
126 note eq = this |
127 show ?thesis unfolding sums_def |
127 show ?thesis unfolding sums_def |
128 by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) |
128 by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) |
129 (simp add: eq atLeast0LessThan del: add_Suc_right) |
129 (simp add: eq atLeast0LessThan del: add_Suc_right) |
130 qed |
130 qed |
|
131 |
|
132 corollary sums_0: |
|
133 "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)" |
|
134 by (metis (no_types) finite.emptyI setsum.empty sums_finite) |
131 |
135 |
132 lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f" |
136 lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f" |
133 by (rule sums_summable) (rule sums_finite) |
137 by (rule sums_summable) (rule sums_finite) |
134 |
138 |
135 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)" |
139 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)" |