src/HOL/Series.thy
 changeset 47761 dfe747e72fa8 parent 47108 2a1953f0d20d child 50331 4b6dc5077e98
```     1.1 --- a/src/HOL/Series.thy	Wed Apr 25 17:15:10 2012 +0200
1.2 +++ b/src/HOL/Series.thy	Wed Apr 25 19:26:00 2012 +0200
1.3 @@ -120,6 +120,50 @@
1.4    shows "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
1.5    by (metis summable_sums sums_summable sums_unique)
1.6
1.7 +lemma sums_finite:
1.8 +  assumes [simp]: "finite N"
1.9 +  assumes f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
1.10 +  shows "f sums (\<Sum>n\<in>N. f n)"
1.11 +proof -
1.12 +  { fix n
1.13 +    have "setsum f {..<n + Suc (Max N)} = setsum f N"
1.14 +    proof cases
1.15 +      assume "N = {}"
1.16 +      with f have "f = (\<lambda>x. 0)" by auto
1.17 +      then show ?thesis by simp
1.18 +    next
1.19 +      assume [simp]: "N \<noteq> {}"
1.20 +      show ?thesis
1.21 +      proof (safe intro!: setsum_mono_zero_right f)
1.22 +        fix i assume "i \<in> N"
1.23 +        then have "i \<le> Max N" by simp
1.24 +        then show "i < n + Suc (Max N)" by simp
1.25 +      qed
1.26 +    qed }
1.27 +  note eq = this
1.28 +  show ?thesis unfolding sums_def
1.29 +    by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
1.31 +qed
1.32 +
1.33 +lemma suminf_finite:
1.34 +  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}"
1.35 +  assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
1.36 +  shows "suminf f = (\<Sum>n\<in>N. f n)"
1.37 +  using sums_finite[OF assms, THEN sums_unique] by simp
1.38 +
1.39 +lemma sums_If_finite_set:
1.40 +  "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)"
1.41 +  using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
1.42 +
1.43 +lemma sums_If_finite:
1.44 +  "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)"
1.45 +  using sums_If_finite_set[of "{r. P r}" f] by simp
1.46 +
1.47 +lemma sums_single:
1.48 +  "(\<lambda>r. if r = i then f r else 0::'a::{comm_monoid_add,t2_space}) sums f i"
1.49 +  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
1.50 +
1.51  lemma sums_split_initial_segment:
1.52    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
1.53    shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
```