# HG changeset patch
# User hoelzl
# Date 1300109865 -3600
# Node ID 656298577a335f070a95198ac17ba2f2edd25a99
# Parent  dbfc073c310d232150e2e14fccd4f69b2836a0bd
add infinite sums and power on extreal

diff -r dbfc073c310d -r 656298577a33 src/HOL/Library/Extended_Reals.thy
--- a/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:44 2011 +0100
+++ b/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:45 2011 +0100
@@ -1,4 +1,4 @@
- (* Title: Extended_Reals.thy
+(* Title: Extended_Reals.thy
    Author: Johannes Hölzl, Robert Himmelmann, Armin Heller; TU München
    Author: Bogdan Grechuk; University of Edinburgh *)
 
@@ -254,6 +254,12 @@
 qed
 end
 
+instance extreal :: ordered_ab_semigroup_add
+proof
+  fix a b c :: extreal assume "a \<le> b" then show "c + a \<le> c + b"
+    by (cases rule: extreal3_cases[of a b c]) auto
+qed
+
 lemma extreal_MInfty_lessI[intro, simp]:
   "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   by (cases a) auto
@@ -334,6 +340,33 @@
   shows "EX z. x < extreal z & extreal z < y"
   by (metis extreal_dense[OF `x < y`] extreal_cases less_extreal.simps(2,3))
 
+lemma
+  fixes f :: "nat \<Rightarrow> extreal"
+  shows incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"
+  and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
+  unfolding decseq_def incseq_def by auto
+
+lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
+  by (auto simp: incseq_def)
+
+lemma extreal_add_nonneg_nonneg:
+  fixes a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
+  using add_mono[of 0 a 0 b] by simp
+
+lemma image_eqD: "f ` A = B \<Longrightarrow> (\<forall>x\<in>A. f x \<in> B)"
+  by auto
+
+lemma incseq_setsumI:
+  fixes f :: "nat \<Rightarrow> extreal"
+  assumes "\<And>i. 0 \<le> f i"
+  shows "incseq (\<lambda>i. setsum f {..< i})"
+proof (intro incseq_SucI)
+  fix n have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
+    using assms by (rule add_left_mono)
+  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
+    by auto
+qed
+
 subsubsection "Multiplication"
 
 instantiation extreal :: "{comm_monoid_mult, sgn}"
@@ -468,6 +501,36 @@
   fixes a b c :: extreal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
   using extreal_mult_right_mono by (simp add: mult_commute[of c])
 
+lemma zero_less_one_extreal[simp]: "0 \<le> (1::extreal)"
+  by (simp add: one_extreal_def zero_extreal_def)
+
+lemma extreal_distrib_right:
+  fixes a b c :: extreal
+  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * (a + b) = c * a + c * b"
+  by (cases rule: extreal3_cases[of a b c])
+     (simp_all add: field_simps)
+
+subsubsection {* Power *}
+
+instantiation extreal :: power
+begin
+primrec power_extreal where
+  "power_extreal x 0 = 1" |
+  "power_extreal x (Suc n) = x * x ^ n"
+instance ..
+end
+
+lemma extreal_power[simp]: "(extreal x) ^ n = extreal (x^n)"
+  by (induct n) (auto simp: one_extreal_def)
+
+lemma extreal_power_PInf[simp]: "\<infinity> ^ n = (if n = 0 then 1 else \<infinity>)"
+  by (induct n) (auto simp: one_extreal_def)
+
+lemma extreal_power_uminus[simp]:
+  fixes x :: extreal
+  shows "(- x) ^ n = (if even n then x ^ n else - (x^n))"
+  by (induct n) (auto simp: one_extreal_def)
+
 subsubsection {* Subtraction *}
 
 lemma extreal_minus_minus_image[simp]:
@@ -657,6 +720,11 @@
   "\<infinity> / extreal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
   unfolding divide_extreal_def by simp
 
+lemma zero_le_divide_extreal[simp]:
+  fixes a :: extreal assumes "0 \<le> a" "0 \<le> b"
+  shows "0 \<le> a / b"
+  using assms by (cases rule: extreal2_cases[of a b]) (auto simp: zero_le_divide_iff)
+
 lemma extreal_mult_le_0_iff:
   fixes a b :: extreal
   shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)"
@@ -718,6 +786,11 @@
   by (cases rule: extreal3_cases[of a b c])
      (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
 
+lemma zero_le_power_extreal[simp]:
+  fixes a :: extreal assumes "0 \<le> a"
+  shows "0 \<le> a ^ n"
+  using assms by (induct n) (auto simp: extreal_zero_le_0_iff)
+
 subsection "Complete lattice"
 
 lemma extreal_bot:
@@ -1104,6 +1177,72 @@
 thus ?thesis unfolding SUPR_def by auto
 qed
 
+lemma SUP_extreal_le_addI:
+  assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
+  shows "SUPR UNIV f + y \<le> z"
+proof (cases y)
+  case (real r)
+  then have "\<And>i. f i \<le> z - y" using assms by (simp add: extreal_le_minus_iff)
+  then have "SUPR UNIV f \<le> z - y" by (rule SUP_leI)
+  then show ?thesis using real by (simp add: extreal_le_minus_iff)
+qed (insert assms, auto)
+
+lemma SUPR_extreal_add:
+  fixes f g :: "nat \<Rightarrow> extreal"
+  assumes "incseq f" "incseq g" and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
+  shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
+proof (rule extreal_SUPI)
+  fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
+  have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
+    unfolding SUPR_def Sup_eq_MInfty by (auto dest: image_eqD)
+  { fix j
+    { fix i
+      have "f i + g j \<le> f i + g (max i j)"
+        using `incseq g`[THEN incseqD] by (rule add_left_mono) auto
+      also have "\<dots> \<le> f (max i j) + g (max i j)"
+        using `incseq f`[THEN incseqD] by (rule add_right_mono) auto
+      also have "\<dots> \<le> y" using * by auto
+      finally have "f i + g j \<le> y" . }
+    then have "SUPR UNIV f + g j \<le> y"
+      using assms(4)[of j] by (intro SUP_extreal_le_addI) auto
+    then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps) }
+  then have "SUPR UNIV g + SUPR UNIV f \<le> y"
+    using f by (rule SUP_extreal_le_addI)
+  then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
+qed (auto intro!: add_mono le_SUPI)
+
+lemma SUPR_extreal_cmult:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
+  shows "(SUP i. c * f i) = c * SUPR UNIV f"
+proof (rule extreal_SUPI)
+  fix i have "f i \<le> SUPR UNIV f" by (rule le_SUPI) auto
+  then show "c * f i \<le> c * SUPR UNIV f"
+    using `0 \<le> c` by (rule extreal_mult_left_mono)
+next
+  fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
+  show "c * SUPR UNIV f \<le> y"
+  proof cases
+    assume c: "0 < c \<and> c \<noteq> \<infinity>"
+    with * have "SUPR UNIV f \<le> y / c"
+      by (intro SUP_leI) (auto simp: extreal_le_divide_pos)
+    with c show ?thesis
+      by (auto simp: extreal_le_divide_pos)
+  next
+    { assume "c = \<infinity>" have ?thesis
+      proof cases
+        assume "\<forall>i. f i = 0"
+        moreover then have "range f = {0}" by auto
+        ultimately show "c * SUPR UNIV f \<le> y" using * by (auto simp: SUPR_def)
+      next
+        assume "\<not> (\<forall>i. f i = 0)"
+        then obtain i where "f i \<noteq> 0" by auto
+        with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis by (auto split: split_if_asm)
+      qed }
+    moreover assume "\<not> (0 < c \<and> c \<noteq> \<infinity>)"
+    ultimately show ?thesis using * `0 \<le> c` by auto
+  qed
+qed
+
 subsection "Limits on @{typ extreal}"
 
 subsubsection "Topological space"
@@ -2337,6 +2476,31 @@
 
 declare trivial_limit_sequentially[simp]
 
+lemma
+  fixes X :: "nat \<Rightarrow> extreal"
+  shows incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
+    and decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
+  unfolding incseq_def decseq_def by auto
+
+lemma extreal_lim_mono:
+  fixes X Y :: "nat => extreal"
+  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
+  assumes "X ----> x" "Y ----> y"
+  shows "x <= y"
+  by (metis extreal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
+
+lemma incseq_le_extreal:
+  fixes X :: "nat \<Rightarrow> extreal"
+  assumes inc: "incseq X" and lim: "X ----> L"
+  shows "X N \<le> L"
+  using inc
+  by (intro extreal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def)
+
+lemma decseq_ge_extreal: assumes dec: "decseq X"
+  and lim: "X ----> (L::extreal)" shows "X N >= L"
+  using dec
+  by (intro extreal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def)
+
 lemma liminf_bounded:
   fixes X Y :: "nat \<Rightarrow> extreal"
   assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
@@ -2389,14 +2553,6 @@
   } then show "?P x0" by auto
 qed
 
-
-lemma extreal_lim_mono:
-  fixes X Y :: "nat => extreal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
-  assumes "X ----> x" "Y ----> y"
-  shows "x <= y"
-  by (metis extreal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
-
 lemma liminf_subseq_mono:
   fixes X :: "nat \<Rightarrow> extreal"
   assumes "subseq r"
@@ -2492,7 +2648,7 @@
 proof -
   from lim_extreal_increasing[of "\<lambda>x. - f x"] assms
   obtain l where "(\<lambda>x. - f x) ----> l" by auto
-  from extreal_lim_mult[OF this, of "- 1"] show thesis 
+  from extreal_lim_mult[OF this, of "- 1"] show thesis
     by (intro that[of "-l"]) (simp add: extreal_uminus_eq_reorder)
 qed
 
@@ -2519,183 +2675,87 @@
   shows "Inf s \<le> a"
 by (metis Lim_bounded2_extreal assms complete_lattice_class.Inf_lower)
 
-lemma incseq_le_extreal: assumes inc: "!!n m. n>=m ==> X n >= X m"
-  and lim: "X ----> (L::extreal)" shows "X N <= L"
-proof(cases "X N = (-\<infinity>)")
-  case True thus ?thesis by auto
-next
-  case False
-  have "ALL n>=N. X n >= X N" using inc by auto
-  hence minf: "ALL n>=N. X n > (-\<infinity>)" using False by auto
-  def Y == "(%n. (if n>=N then X n else X N))"
-  hence incy: "!!n m. n>=m ==> Y n >= Y m" using inc by auto
-  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
-  from lim have limy: "Y ----> L"
-    apply (subst tail_same_limit[of X _ N]) using Y_def by auto
-  show ?thesis
-  proof (cases "\<bar>L\<bar> = \<infinity>")
-    case False have "ALL n. Y n ~= \<infinity>"
-    proof(rule ccontr,unfold not_all not_not,safe)
-      case goal1 hence "ALL n>=x. Y n = \<infinity>" using incy[of x] by auto
-      hence "Y ----> \<infinity>" unfolding tendsto_def eventually_sequentially
-        apply safe apply(rule_tac x=x in exI) by auto
-      note Lim_unique[OF trivial_limit_sequentially this limy]
-      with False show False by auto
-    qed
-    with minfy have *: "\<And>n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
-
-    have **:"ALL m n. m <= n --> extreal (real (Y m)) <= extreal (real (Y n))"
-      unfolding extreal_real using minfy * incy apply (cases "Y m", cases "Y n") by auto
-    have "real (Y N) <= real L" apply-apply(rule incseq_le) defer
-      apply(subst lim_extreal[THEN sym])
-      unfolding extreal_real
-      unfolding incseq_def using * ** limy False by auto
-    hence "extreal (real (Y N)) <= extreal (real L)" by auto
-    hence ***: "Y N <= L" unfolding extreal_real using * False by auto
-    thus ?thesis using Y_def by auto
+
+lemma extreal_le_extreal_bounded:
+  fixes x y z :: extreal
+  assumes "z \<le> y"
+  assumes *: "\<And>B. z < B \<Longrightarrow> B < x \<Longrightarrow> B \<le> y"
+  shows "x \<le> y"
+proof (rule extreal_le_extreal)
+  fix B assume "B < x"
+  show "B \<le> y"
+  proof cases
+    assume "z < B" from *[OF this `B < x`] show "B \<le> y" .
   next
-    case True
-    show ?thesis
-    proof(cases "L=(-\<infinity>)")
-      case True
-      have "open {..<X N}" by auto
-      moreover have "(-\<infinity>) : {..<X N}" using False by auto
-      ultimately obtain N1 where "ALL n>=N1. X n : {..<X N}" using lim True
-        unfolding tendsto_def eventually_sequentially by metis
-      hence "X (max N N1) : {..<X N}" by auto
-      with inc[of N "max N N1"] show ?thesis by auto
-    next
-      case False thus ?thesis using True by auto qed
+    assume "\<not> z < B" with `z \<le> y` show "B \<le> y" by auto
   qed
 qed
 
-lemma decseq_ge_extreal: assumes dec: "!!n m. n>=m ==> X n <= X m"
-  and lim: "X ----> (L::extreal)" shows "X N >= L"
-proof-
-def Y == "(%i. -(X i))"
-hence inc: "!!n m. n>=m ==> Y n >= Y m" using dec extreal_minus_le_minus by auto
-moreover have limy: "Y ----> (-L)" using Y_def extreal_lim_uminus lim by auto
-ultimately have "Y N <= -L" using incseq_le_extreal[of Y "-L"] by auto
-from this show ?thesis using Y_def extreal_minus_le_minus by auto
+lemma fixes x y :: extreal
+  shows Sup_atMost[simp]: "Sup {.. y} = y"
+    and Sup_lessThan[simp]: "Sup {..< y} = y"
+    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
+    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
+    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
+  by (auto simp: Sup_extreal_def intro!: Least_equality
+           intro: extreal_le_extreal extreal_le_extreal_bounded[of x])
+
+lemma Sup_greaterThanlessThan[simp]:
+  fixes x y :: extreal assumes "x < y" shows "Sup { x <..< y} = y"
+  unfolding Sup_extreal_def
+proof (intro Least_equality extreal_le_extreal_bounded[of _ _ y])
+  fix z assume z: "\<forall>u\<in>{x<..<y}. u \<le> z"
+  from extreal_dense[OF `x < y`] guess w .. note w = this
+  with z[THEN bspec, of w] show "x \<le> z" by auto
+qed auto
+
+lemma SUP_Lim_extreal:
+  fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" "X ----> l" shows "(SUP n. X n) = l"
+proof (rule extreal_SUPI)
+  fix n from assms show "X n \<le> l"
+    by (intro incseq_le_extreal) (simp add: incseq_def)
+next
+  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
+  with extreal_Sup_lim[OF _ `X ----> l`, of "{..y}"]
+  show "l \<le> y" by auto
 qed
 
-
-lemma real_interm:
- assumes "(a::real)<b"
- shows "a + (b-a)/2 < b"
-by (metis Bit0_def assms comm_semiring_1_class.normalizing_semiring_rules(24) diff_minus_eq_add number_of_is_id one_is_num_one pth_2 real_average_minus_second real_gt_half_sum succ_def)
-
-
-lemma SUP_Lim_extreal: assumes "!!n m. n>=m ==> f n >= f m" "f ----> l"
-  shows "(SUP n. f n) = (l::extreal)" unfolding SUPR_def Sup_extreal_def
-proof (safe intro!: Least_equality)
-  fix n::nat show "f n <= l" apply(rule incseq_le_extreal)
-    using assms by auto
-next fix y assume y:"ALL x:range f. x <= y" show "l <= y"
-  proof-
-    { assume yinf: "\<bar>y\<bar> \<noteq> \<infinity>"
-      { assume as:"y < l"
-        hence linf: "\<bar>l\<bar> \<noteq> \<infinity>"
-          using Lim_bounded_PInfty[OF assms(2), of "real y"] y yinf by auto
-        have [simp]: "extreal (1 / 2) = 1 / 2" by (auto simp: divide_extreal_def)
-        have yl:"real y < real l" using as
-          apply(subst(asm) extreal_real'[THEN sym,OF yinf])
-          apply(subst(asm) extreal_real'[THEN sym,OF linf]) by auto
-        hence "y + (l - y) * 1 / 2 < l" apply-
-          apply(subst extreal_real'[THEN sym,OF yinf])
-          apply(subst(2) extreal_real'[THEN sym,OF yinf])
-          apply(subst extreal_real'[THEN sym,OF linf])
-          apply(subst(2) extreal_real'[THEN sym,OF linf])
-          using real_interm by auto
-        hence *:"l : {y + (l - y) / 2<..}" by auto
-        have "open {y + (l-y)/2 <..}" by auto
-        note topological_tendstoD[OF assms(2) this *]
-        from this[unfolded eventually_sequentially] guess N .. note this[rule_format, of N]
-        hence "y + (l - y)  / 2 < y" using y[rule_format,of "f N"] by auto
-        hence "extreal (real y) + (extreal (real l) - extreal (real y)) / 2 < extreal (real y)"
-          unfolding extreal_real using yinf linf by auto
-        hence False using yl by auto
-      } hence ?thesis using not_le by auto
-    }
-    moreover
-    { assume "y=(-\<infinity>)" hence "f = (\<lambda>_. -\<infinity>)" using y by (auto simp: fun_eq_iff)
-      hence "l=(-\<infinity>)" using `f ----> l` using tendsto_const[of "-\<infinity>"]
-         Lim_unique[OF trivial_limit_sequentially] by auto
-      hence ?thesis by auto
-    }
-    moreover have "y=\<infinity> --> l <= y" by auto
-    ultimately show ?thesis by blast
-  qed
+lemma LIMSEQ_extreal_SUPR:
+  fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" shows "X ----> (SUP n. X n)"
+proof (rule lim_extreal_increasing)
+  fix n m :: nat assume "m \<le> n" then show "X m \<le> X n"
+    using `incseq X` by (simp add: incseq_def)
+next
+  fix l assume "X ----> l"
+  with SUP_Lim_extreal[of X, OF assms this] show ?thesis by simp
 qed
 
-lemma INF_Lim_extreal: assumes "!!n m. n>=m ==> f n <= f m" "f ----> l"
-  shows "(INF n. f n) = (l::extreal)"
-proof-
-def Y == "(%i. -(f i))"
-hence inc: "!!n m. n>=m ==> Y n >= Y m" using assms extreal_minus_le_minus by auto
-moreover have limy: "Y ----> (-l)" using Y_def extreal_lim_uminus assms by auto
-ultimately have "(SUP n. Y n) = -l" using SUP_Lim_extreal[of Y "-l"] by auto
-hence "- (INF n. f n) = - l" using Y_def extreal_SUPR_uminus[of "UNIV" f] by auto
-from this show ?thesis by simp
-qed
-
-
-lemma incseq_mono: "mono f <-> incseq f"
+lemma INF_Lim_extreal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::extreal)"
+  using SUP_Lim_extreal[of "\<lambda>i. - X i" "- l"]
+  by (simp add: extreal_SUPR_uminus extreal_lim_uminus)
+
+lemma LIMSEQ_extreal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: extreal)"
+  using LIMSEQ_extreal_SUPR[of "\<lambda>i. - X i"]
+  by (simp add: extreal_SUPR_uminus extreal_lim_uminus)
+
+lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
   unfolding mono_def incseq_def by auto
 
-
 lemma SUP_eq_LIMSEQ:
   assumes "mono f"
-  shows "(SUP n. extreal (f n)) = extreal x <-> f ----> x"
+  shows "(SUP n. extreal (f n)) = extreal x \<longleftrightarrow> f ----> x"
 proof
-  assume x: "(SUP n. extreal (f n)) = extreal x"
-  { fix n
-    have "extreal (f n) <= extreal x" using x[symmetric] by (auto intro: le_SUPI)
-    hence "f n <= x" using assms by simp }
-  show "f ----> x"
-  proof (rule LIMSEQ_I)
-    fix r :: real assume "0 < r"
-    show "EX no. ALL n>=no. norm (f n - x) < r"
-    proof (rule ccontr)
-      assume *: "~ ?thesis"
-      { fix N
-        from * obtain n where "N <= n" "r <= x - f n"
-          using `!!n. f n <= x` by (auto simp: not_less)
-        hence "f N <= f n" using `mono f` by (auto dest: monoD)
-        hence "f N <= x - r" using `r <= x - f n` by auto
-        hence "extreal (f N) <= extreal (x - r)" by auto }
-      hence "(SUP n. extreal (f n)) <= extreal (x - r)"
-        and "extreal (x - r) < extreal x" using `0 < r` by (auto intro: SUP_leI)
-      hence "(SUP n. extreal (f n)) < extreal x" by (rule le_less_trans)
-      thus False using x by auto
-    qed
-  qed
-next
-  assume "f ----> x"
-  show "(SUP n. extreal (f n)) = extreal x"
-  proof (rule extreal_SUPI)
-    fix n
-    from incseq_le[of f x] `mono f` `f ----> x`
-    show "extreal (f n) <= extreal x" using assms incseq_mono by auto
-  next
-    fix y assume *: "!!n. n:UNIV ==> extreal (f n) <= y"
-    show "extreal x <= y"
-    proof-
-    { assume "EX r. y = extreal r"
-      from this obtain r where r_def: "y = extreal r" by auto
-      with * have "EX N. ALL n>=N. f n <= r" using assms by fastsimp
-      from LIMSEQ_le_const2[OF `f ----> x` this]
-      have "extreal x <= y" using r_def by auto
-    }
-    moreover
-    { assume "y=\<infinity> | y=(-\<infinity>)"
-      hence ?thesis using * by auto
-    } ultimately show ?thesis by (cases y) auto
-    qed
-  qed
+  have inc: "incseq (\<lambda>i. extreal (f i))"
+    using `mono f` unfolding mono_def incseq_def by auto
+  { assume "f ----> x"
+   then have "(\<lambda>i. extreal (f i)) ----> extreal x" by auto
+   from SUP_Lim_extreal[OF inc this]
+   show "(SUP n. extreal (f n)) = extreal x" . }
+  { assume "(SUP n. extreal (f n)) = extreal x"
+    with LIMSEQ_extreal_SUPR[OF inc]
+    show "f ----> x" by auto }
 qed
 
-
 lemma Liminf_within:
   fixes f :: "'a::metric_space => extreal"
   shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
@@ -3118,9 +3178,128 @@
   then show ?thesis by simp
 qed
 
-lemma setsum_0:
-  fixes f :: "'a \<Rightarrow> pextreal" assumes "finite A"
+lemma setsum_extreal_0:
+  fixes f :: "'a \<Rightarrow> extreal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
   shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
-  using assms by induct auto
+proof
+  assume *: "(\<Sum>x\<in>A. f x) = 0"
+  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto
+  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty)
+  then have "\<forall>i\<in>A. \<exists>r. f i = extreal r" by auto
+  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
+    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
+qed (rule setsum_0')
+
+lemma setsum_extreal_right_distrib:
+  fixes f :: "'a \<Rightarrow> extreal" assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" "0 \<le> r"
+  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
+proof cases
+  assume "finite A" then show ?thesis using assms
+    by induct (auto simp: extreal_distrib_right setsum_nonneg)
+qed simp
+
+lemma sums_extreal_positive:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)"
+proof -
+  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
+    using extreal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
+  from LIMSEQ_extreal_SUPR[OF this]
+  show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
+qed
+
+lemma summable_extreal:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "summable f"
+  using sums_extreal_positive[of f, OF assms] unfolding summable_def by auto
+
+lemma suminf_extreal_eq_SUPR:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i"
+  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
+  using sums_extreal_positive[of f, OF assms, THEN sums_unique] by simp
+
+lemma suminf_extreal:
+  "(\<lambda>x. extreal (f x)) sums extreal x \<longleftrightarrow> f sums x"
+  unfolding sums_def by simp
+
+lemma suminf_bound:
+  fixes f :: "nat \<Rightarrow> extreal"
+  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n"
+  shows "suminf f \<le> x"
+proof (rule Lim_bounded_extreal)
+  have "summable f" using pos[THEN summable_extreal] .
+  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
+    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
+  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
+    using assms by auto
+qed
+
+lemma suminf_bound_add:
+  fixes f :: "nat \<Rightarrow> extreal"
+  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" and pos: "\<And>n. 0 \<le> f n" and "y \<noteq> -\<infinity>"
+  shows "suminf f + y \<le> x"
+proof (cases y)
+  case (real r) then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
+    using assms by (simp add: extreal_le_minus)
+  then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound)
+  then show "(\<Sum> n. f n) + y \<le> x"
+    using assms real by (simp add: extreal_le_minus)
+qed (insert assms, auto)
+
+lemma sums_finite:
+  assumes "\<forall>N\<ge>n. f N = 0"
+  shows "f sums (\<Sum>N<n. f N)"
+proof -
+  { fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)"
+      by (induct i) (insert assms, auto) }
+  note this[simp]
+  show ?thesis unfolding sums_def
+    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan)
+qed
+
+lemma suminf_finite:
+  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0"
+  shows "suminf f = (\<Sum>N<n. f N)"
+  using sums_finite[OF assms, THEN sums_unique] by simp
+
+lemma suminf_upper:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n"
+  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
+  unfolding suminf_extreal_eq_SUPR[OF assms] SUPR_def
+  by (auto intro: complete_lattice_class.Sup_upper image_eqI)
+
+lemma suminf_0_le:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n"
+  shows "0 \<le> (\<Sum>n. f n)"
+  using suminf_upper[of f 0, OF assms] by simp
+
+lemma suminf_le_pos:
+  fixes f g :: "nat \<Rightarrow> extreal"
+  assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N"
+  shows "suminf f \<le> suminf g"
+proof (safe intro!: suminf_bound)
+  fix n { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto }
+  have "setsum f {..<n} \<le> setsum g {..<n}" using assms by (auto intro: setsum_mono)
+  also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper)
+  finally show "setsum f {..<n} \<le> suminf g" .
+qed (rule assms(2))
+
+lemma suminf_half_series_extreal: "(\<Sum>n. (1/2 :: extreal)^Suc n) = 1"
+  using suminf_extreal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
+  by (simp add: one_extreal_def)
+
+lemma suminf_add_extreal:
+  fixes f g :: "nat \<Rightarrow> extreal"
+  assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
+  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
+  apply (subst (1 2 3) suminf_extreal_eq_SUPR)
+  unfolding setsum_addf
+  by (intro assms extreal_add_nonneg_nonneg SUPR_extreal_add incseq_setsumI setsum_nonneg ballI)+
+
+lemma suminf_cmult_extreal:
+  fixes f g :: "nat \<Rightarrow> extreal"
+  assumes "\<And>i. 0 \<le> f i" "0 \<le> a"
+  shows "(\<Sum>i. a * f i) = a * suminf f"
+  by (auto simp: setsum_extreal_right_distrib[symmetric] assms
+                 extreal_zero_le_0_iff setsum_nonneg suminf_extreal_eq_SUPR
+           intro!: SUPR_extreal_cmult )
 
 end