equal
deleted
inserted
replaced
217 |
217 |
218 lemma setsum_le_suminf: |
218 lemma setsum_le_suminf: |
219 fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}" |
219 fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}" |
220 shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> setsum f I \<le> suminf f" |
220 shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> setsum f I \<le> suminf f" |
221 by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto |
221 by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto |
|
222 |
|
223 lemma suminf_eq_SUP_real: |
|
224 assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)" |
|
225 by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP) |
|
226 (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] setsum_le_suminf X monoI setsum_mono3) |
222 |
227 |
223 subsection \<open>Defining the extended non-negative reals\<close> |
228 subsection \<open>Defining the extended non-negative reals\<close> |
224 |
229 |
225 text \<open>Basic definitions and type class setup\<close> |
230 text \<open>Basic definitions and type class setup\<close> |
226 |
231 |