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.30 +       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
    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))"