diff -r 8558e4a37b48 -r a0cfa9050fa8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:39:10 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:40:47 2015 +0200
@@ -3182,6 +3182,77 @@
 qed
 
 
+lemma SUP_ereal_add_directed:
+  fixes f g :: "'a \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
+  assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
+  shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+proof cases
+  assume "I = {}" then show ?thesis
+    by (simp add: bot_ereal_def)
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (rule antisym)
+    show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+      by (rule SUP_least; intro ereal_add_mono SUP_upper)
+  next
+    have "bot < (SUP i:I. g i)"
+      using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
+    then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+      by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
+    also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+      using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
+    also have "\<dots> \<le> (SUP i:I. f i + g i)"
+      using directed by (intro SUP_least) (blast intro: SUP_upper2)
+    finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+  qed
+qed
+
+lemma SUP_ereal_setsum_directed:
+  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
+  assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
+  shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
+proof -
+  have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
+  proof (induction N rule: infinite_finite_induct)
+    case (insert n N)
+    moreover have "(SUP i:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
+    proof (rule SUP_ereal_add_directed)
+      fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
+        using insert by (auto intro!: setsum_nonneg nonneg)
+    next
+      fix i j assume "i \<in> I" "j \<in> I"
+      from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
+      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
+        by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
+    qed
+    ultimately show ?case
+      by simp
+  qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)
+  from this[of A] show ?thesis by simp
+qed
+
+lemma suminf_SUP_eq_directed:
+  fixes f :: "_ \<Rightarrow> nat \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
+  assumes nonneg: "\<And>n i. 0 \<le> f n i"
+  shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
+proof (subst (1 2) suminf_ereal_eq_SUP)
+  show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
+    using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
+  show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
+    apply (subst SUP_commute)
+    apply (subst SUP_ereal_setsum_directed)
+    apply (auto intro!: assms simp: finite_subset)
+    done
+qed
+
+subsection \<open>More Limits\<close>
+
 lemma convergent_limsup_cl:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   shows "convergent X \<Longrightarrow> limsup X = lim X"