src/HOL/Series.thy
changeset 62376 85f38d5f8807
parent 62368 106569399cd6
child 62377 ace69956d018
     1.1 --- a/src/HOL/Series.thy	Tue Feb 09 09:21:10 2016 +0100
     1.2 +++ b/src/HOL/Series.thy	Wed Feb 10 18:43:19 2016 +0100
     1.3 @@ -211,22 +211,6 @@
     1.4  lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
     1.5    using setsum_le_suminf[of 0] by simp
     1.6  
     1.7 -lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
     1.8 -  using
     1.9 -    setsum_le_suminf[of "Suc i"]
    1.10 -    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
    1.11 -    setsum_mono2[of "{..<i}" "{..<n}" f]
    1.12 -  by (auto simp: less_imp_le ac_simps)
    1.13 -
    1.14 -lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
    1.15 -  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
    1.16 -
    1.17 -lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
    1.18 -  using setsum_less_suminf2[of 0 i] by simp
    1.19 -
    1.20 -lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    1.21 -  using suminf_pos2[of 0] by (simp add: less_imp_le)
    1.22 -
    1.23  lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
    1.24    by (metis LIMSEQ_le_const2 summable_LIMSEQ)
    1.25  
    1.26 @@ -244,8 +228,31 @@
    1.27      by (auto intro!: antisym)
    1.28  qed (metis suminf_zero fun_eq_iff)
    1.29  
    1.30 -lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    1.31 -  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
    1.32 +end
    1.33 +
    1.34 +context
    1.35 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add, linorder_topology}"
    1.36 +begin
    1.37 +
    1.38 +lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
    1.39 +  using
    1.40 +    setsum_le_suminf[of f "Suc i"]
    1.41 +    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
    1.42 +    setsum_mono2[of "{..<i}" "{..<n}" f]
    1.43 +  by (auto simp: less_imp_le ac_simps)
    1.44 +
    1.45 +lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
    1.46 +  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
    1.47 +
    1.48 +lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
    1.49 +  using setsum_less_suminf2[of 0 i] by simp
    1.50 +
    1.51 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
    1.52 +  using suminf_pos2[of 0] by (simp add: less_imp_le)
    1.53 +
    1.54 +lemma suminf_pos_iff:
    1.55 +  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    1.56 +  using setsum_le_suminf[of f 0] suminf_eq_zero_iff[of f] by (simp add: less_le)
    1.57  
    1.58  end
    1.59