src/HOL/Series.thy
changeset 62377 ace69956d018
parent 62376 85f38d5f8807
child 62379 340738057c8c
     1.1 --- a/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
     1.2 +++ b/src/HOL/Series.thy	Fri Feb 12 16:09:07 2016 +0100
     1.3 @@ -228,6 +228,24 @@
     1.4      by (auto intro!: antisym)
     1.5  qed (metis suminf_zero fun_eq_iff)
     1.6  
     1.7 +lemma suminf_pos_iff:
     1.8 +  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
     1.9 +  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
    1.10 +
    1.11 +lemma suminf_pos2:
    1.12 +  assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
    1.13 +  shows "0 < suminf f"
    1.14 +proof -
    1.15 +  have "0 < (\<Sum>n<Suc i. f n)"
    1.16 +    using assms by (intro setsum_pos2[where i=i]) auto
    1.17 +  also have "\<dots> \<le> suminf f"
    1.18 +    using assms by (intro setsum_le_suminf) auto
    1.19 +  finally show ?thesis .
    1.20 +qed
    1.21 +
    1.22 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    1.23 +  by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)
    1.24 +
    1.25  end
    1.26  
    1.27  context
    1.28 @@ -244,16 +262,6 @@
    1.29  lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
    1.30    using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
    1.31  
    1.32 -lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
    1.33 -  using setsum_less_suminf2[of 0 i] by simp
    1.34 -
    1.35 -lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    1.36 -  using suminf_pos2[of 0] by (simp add: less_imp_le)
    1.37 -
    1.38 -lemma suminf_pos_iff:
    1.39 -  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    1.40 -  using setsum_le_suminf[of f 0] suminf_eq_zero_iff[of f] by (simp add: less_le)
    1.41 -
    1.42  end
    1.43  
    1.44  lemma summableI_nonneg_bounded:
    1.45 @@ -261,23 +269,18 @@
    1.46    assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
    1.47    shows "summable f"
    1.48    unfolding summable_def sums_def[abs_def]
    1.49 -proof (intro exI order_tendstoI)
    1.50 -  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
    1.51 +proof (rule exI LIMSEQ_incseq_SUP)+
    1.52 +  show "bdd_above (range (\<lambda>n. setsum f {..<n}))"
    1.53      using le by (auto simp: bdd_above_def)
    1.54 -  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
    1.55 -    then obtain n where "a < (\<Sum>i<n. f i)"
    1.56 -      by (auto simp add: less_cSUP_iff)
    1.57 -    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
    1.58 -      by (rule less_le_trans) (auto intro!: setsum_mono2)
    1.59 -    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
    1.60 -      by (auto simp: eventually_sequentially) }
    1.61 -  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
    1.62 -    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
    1.63 -      by (auto intro: cSUP_upper)
    1.64 -    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
    1.65 -      by (auto intro: le_less_trans simp: eventually_sequentially) }
    1.66 +  show "incseq (\<lambda>n. setsum f {..<n})"
    1.67 +    by (auto simp: mono_def intro!: setsum_mono2)
    1.68  qed
    1.69  
    1.70 +lemma summableI[intro, simp]:
    1.71 +  fixes f:: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
    1.72 +  shows "summable f"
    1.73 +  by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
    1.74 +
    1.75  subsection \<open>Infinite summability on topological monoids\<close>
    1.76  
    1.77  lemma Zero_notin_Suc: "0 \<notin> Suc ` A"