src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 57025 e7fd64f82876
parent 56218 1c3f1f2431f9
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -1220,6 +1220,39 @@
     1.4    by (metis INF_absorb centre_in_ball)
     1.5  
     1.6  
     1.7 +lemma suminf_ereal_offset_le:
     1.8 +  fixes f :: "nat \<Rightarrow> ereal"
     1.9 +  assumes f: "\<And>i. 0 \<le> f i"
    1.10 +  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
    1.11 +proof -
    1.12 +  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
    1.13 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
    1.14 +  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
    1.15 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
    1.16 +  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
    1.17 +    by (rule LIMSEQ_ignore_initial_segment)
    1.18 +  ultimately show ?thesis
    1.19 +  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
    1.20 +    fix n assume "k \<le> n"
    1.21 +    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
    1.22 +      by simp
    1.23 +    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
    1.24 +      by (subst setsum_reindex) auto
    1.25 +    also have "\<dots> \<le> setsum f {..<n + k}"
    1.26 +      by (intro setsum_mono3) (auto simp: f)
    1.27 +    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
    1.28 +  qed
    1.29 +qed
    1.30 +
    1.31 +lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
    1.32 +  by (metis sums_ereal sums_unique)
    1.33 +
    1.34 +lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
    1.35 +  by (metis sums_ereal sums_unique summable_def)
    1.36 +
    1.37 +lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
    1.38 +  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
    1.39 +
    1.40  subsection {* monoset *}
    1.41  
    1.42  definition (in order) mono_set: