diff -r 253c98aa935a -r 409ca22dee4c src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Oct 06 14:19:46 2021 +0200
@@ -7,9 +7,12 @@
 section \<open>Sums over Infinite Sets\<close>
 
 theory Infinite_Set_Sum
-  imports Set_Integral
+  imports Set_Integral Infinite_Sum
 begin
 
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
 (* TODO Move *)
 lemma sets_eq_countable:
   assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
@@ -865,4 +868,518 @@
        (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
 qed
 
+lemma abs_summable_finite_sumsI:
+  assumes "\<And>F. finite F \<Longrightarrow> F\<subseteq>S \<Longrightarrow> sum (\<lambda>x. norm (f x)) F \<le> B"
+  shows "f abs_summable_on S"
+proof -
+  have main: "f abs_summable_on S \<and> infsetsum (\<lambda>x. norm (f x)) S \<le> B" if \<open>B \<ge> 0\<close> and \<open>S \<noteq> {}\<close>
+  proof -
+    define M normf where "M = count_space S" and "normf x = ennreal (norm (f x))" for x
+    have "sum normf F \<le> ennreal B"
+      if "finite F" and "F \<subseteq> S" and
+        "\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> (\<Sum>i\<in>F. ennreal (norm (f i))) \<le> ennreal B" and
+        "ennreal 0 \<le> ennreal B" for F
+      using that unfolding normf_def[symmetric] by simp
+    hence normf_B: "finite F \<Longrightarrow> F\<subseteq>S \<Longrightarrow> sum normf F \<le> ennreal B" for F
+      using assms[THEN ennreal_leI]
+      by auto
+    have "integral\<^sup>S M g \<le> B" if "simple_function M g" and "g \<le> normf" for g 
+    proof -
+      define gS where "gS = g ` S"
+      have "finite gS"
+        using that unfolding gS_def M_def simple_function_count_space by simp
+      have "gS \<noteq> {}" unfolding gS_def using \<open>S \<noteq> {}\<close> by auto
+      define part where "part r = g -` {r} \<inter> S" for r
+      have r_finite: "r < \<infinity>" if "r : gS" for r 
+        using \<open>g \<le> normf\<close> that unfolding gS_def le_fun_def normf_def apply auto
+        using ennreal_less_top neq_top_trans top.not_eq_extremum by blast
+      define B' where "B' r = (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum normf F)" for r
+      have B'fin: "B' r < \<infinity>" for r
+      proof -
+        have "B' r \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum normf F)"
+          unfolding B'_def
+          by (metis (mono_tags, lifting) SUP_least SUP_upper)
+        also have "\<dots> \<le> B"
+          using normf_B unfolding part_def
+          by (metis (no_types, lifting) Int_subset_iff SUP_least mem_Collect_eq)
+        also have "\<dots> < \<infinity>"
+          by simp
+        finally show ?thesis by simp
+      qed
+      have sumB': "sum B' gS \<le> ennreal B + \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+      proof -
+        define N \<epsilon>N where "N = card gS" and "\<epsilon>N = \<epsilon> / N"
+        have "N > 0" 
+          unfolding N_def using \<open>gS\<noteq>{}\<close> \<open>finite gS\<close>
+          by (simp add: card_gt_0_iff)
+        from \<epsilon>N_def that have "\<epsilon>N > 0"
+          by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_zero_less_divide)
+        have c1: "\<exists>y. B' r \<le> sum normf y + \<epsilon>N \<and> finite y \<and> y \<subseteq> part r"
+          if "B' r = 0" for r
+          using that by auto
+        have c2: "\<exists>y. B' r \<le> sum normf y + \<epsilon>N \<and> finite y \<and> y \<subseteq> part r" if "B' r \<noteq> 0" for r
+        proof-
+          have "B' r - \<epsilon>N < B' r"
+            using B'fin \<open>0 < \<epsilon>N\<close> ennreal_between that by fastforce
+          have "B' r - \<epsilon>N < Sup (sum normf ` {F. finite F \<and> F \<subseteq> part r}) \<Longrightarrow>
+               \<exists>F. B' r - \<epsilon>N \<le> sum normf F \<and> finite F \<and> F \<subseteq> part r"
+            by (metis (no_types, lifting) leD le_cases less_SUP_iff mem_Collect_eq)
+          hence "B' r - \<epsilon>N < B' r \<Longrightarrow> \<exists>F. B' r - \<epsilon>N \<le> sum normf F \<and> finite F \<and> F \<subseteq> part r"
+            by (subst (asm) (2) B'_def)
+          then obtain F where "B' r - \<epsilon>N \<le> sum normf F" and "finite F" and "F \<subseteq> part r"
+            using \<open>B' r - \<epsilon>N < B' r\<close> by auto  
+          thus "\<exists>F. B' r \<le> sum normf F + \<epsilon>N \<and> finite F \<and> F \<subseteq> part r"
+            by (metis add.commute ennreal_minus_le_iff)
+        qed
+        have "\<forall>x. \<exists>y. B' x \<le> sum normf y + \<epsilon>N \<and>
+            finite y \<and> y \<subseteq> part x"
+          using c1 c2
+          by blast 
+        hence "\<exists>F. \<forall>x. B' x \<le> sum normf (F x) + \<epsilon>N \<and> finite (F x) \<and> F x \<subseteq> part x"
+          by metis 
+        then obtain F where F: "sum normf (F r) + \<epsilon>N \<ge> B' r" and Ffin: "finite (F r)" and Fpartr: "F r \<subseteq> part r" for r
+          using atomize_elim by auto
+        have w1: "finite gS"
+          by (simp add: \<open>finite gS\<close>)          
+        have w2: "\<forall>i\<in>gS. finite (F i)"
+          by (simp add: Ffin)          
+        have False
+          if "\<And>r. F r \<subseteq> g -` {r} \<and> F r \<subseteq> S"
+            and "i \<in> gS" and "j \<in> gS" and "i \<noteq> j" and "x \<in> F i" and "x \<in> F j"
+          for i j x
+          by (metis subsetD that(1) that(4) that(5) that(6) vimage_singleton_eq)          
+        hence w3: "\<forall>i\<in>gS. \<forall>j\<in>gS. i \<noteq> j \<longrightarrow> F i \<inter> F j = {}"
+          using Fpartr[unfolded part_def] by auto          
+        have w4: "sum normf (\<Union> (F ` gS)) + \<epsilon> = sum normf (\<Union> (F ` gS)) + \<epsilon>"
+          by simp
+        have "sum B' gS \<le> (\<Sum>r\<in>gS. sum normf (F r) + \<epsilon>N)"
+          using F by (simp add: sum_mono)
+        also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + (\<Sum>r\<in>gS. \<epsilon>N)"
+          by (simp add: sum.distrib)
+        also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + (card gS * \<epsilon>N)"
+          by auto
+        also have "\<dots> = (\<Sum>r\<in>gS. sum normf (F r)) + \<epsilon>"
+          unfolding \<epsilon>N_def N_def[symmetric] using \<open>N>0\<close> 
+          by (simp add: ennreal_times_divide mult.commute mult_divide_eq_ennreal)
+        also have "\<dots> = sum normf (\<Union> (F ` gS)) + \<epsilon>" 
+          using w1 w2 w3 w4
+          by (subst sum.UNION_disjoint[symmetric])
+        also have "\<dots> \<le> B + \<epsilon>"
+          using \<open>finite gS\<close> normf_B add_right_mono Ffin Fpartr unfolding part_def
+          by (simp add: \<open>gS \<noteq> {}\<close> cSUP_least)          
+        finally show ?thesis
+          by auto
+      qed
+      hence sumB': "sum B' gS \<le> B"
+        using ennreal_le_epsilon ennreal_less_zero_iff by blast
+      have "\<forall>r. \<exists>y. r \<in> gS \<longrightarrow> B' r = ennreal y"
+        using B'fin less_top_ennreal by auto
+      hence "\<exists>B''. \<forall>r. r \<in> gS \<longrightarrow> B' r = ennreal (B'' r)"
+        by (rule_tac choice) 
+      then obtain B'' where B'': "B' r = ennreal (B'' r)" if "r \<in> gS" for r
+        by atomize_elim 
+      have cases[case_names zero finite infinite]: "P" if "r=0 \<Longrightarrow> P" and "finite (part r) \<Longrightarrow> P"
+        and "infinite (part r) \<Longrightarrow> r\<noteq>0 \<Longrightarrow> P" for P r
+        using that by metis
+      have emeasure_B': "r * emeasure M (part r) \<le> B' r" if "r : gS" for r
+      proof (cases rule:cases[of r])
+        case zero
+        thus ?thesis by simp
+      next
+        case finite
+        have s1: "sum g F \<le> sum normf F"
+          if "F \<in> {F. finite F \<and> F \<subseteq> part r}"
+          for F
+          using \<open>g \<le> normf\<close> 
+          by (simp add: le_fun_def sum_mono)
+
+        have "r * of_nat (card (part r)) = r * (\<Sum>x\<in>part r. 1)" by simp
+        also have "\<dots> = (\<Sum>x\<in>part r. r)"
+          using mult.commute by auto
+        also have "\<dots> = (\<Sum>x\<in>part r. g x)"
+          unfolding part_def by auto
+        also have "\<dots> \<le> (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum g F)"
+          using finite
+          by (simp add: Sup_upper)
+        also have "\<dots> \<le> B' r"        
+          unfolding B'_def
+          using s1 SUP_subset_mono by blast
+        finally have "r * of_nat (card (part r)) \<le> B' r" by assumption
+        thus ?thesis
+          unfolding M_def
+          using part_def finite by auto
+      next
+        case infinite
+        from r_finite[OF \<open>r : gS\<close>] obtain r' where r': "r = ennreal r'"
+          using ennreal_cases by auto
+        with infinite have "r' > 0"
+          using ennreal_less_zero_iff not_gr_zero by blast
+        obtain N::nat where N:"N > B / r'" and "real N > 0" apply atomize_elim
+          using reals_Archimedean2
+          by (metis less_trans linorder_neqE_linordered_idom)
+        obtain F where "finite F" and "card F = N" and "F \<subseteq> part r"
+          using infinite(1) infinite_arbitrarily_large by blast
+        from \<open>F \<subseteq> part r\<close> have "F \<subseteq> S" unfolding part_def by simp
+        have "B < r * N"
+          unfolding r' ennreal_of_nat_eq_real_of_nat
+          using N \<open>0 < r'\<close> \<open>B \<ge> 0\<close> r'
+          by (metis enn2real_ennreal enn2real_less_iff ennreal_less_top ennreal_mult' less_le mult_less_cancel_left_pos nonzero_mult_div_cancel_left times_divide_eq_right)
+        also have "r * N = (\<Sum>x\<in>F. r)"
+          using \<open>card F = N\<close> by (simp add: mult.commute)
+        also have "(\<Sum>x\<in>F. r) = (\<Sum>x\<in>F. g x)"
+          using \<open>F \<subseteq> part r\<close>  part_def sum.cong subsetD by fastforce
+        also have "(\<Sum>x\<in>F. g x) \<le> (\<Sum>x\<in>F. ennreal (norm (f x)))"
+          by (metis (mono_tags, lifting) \<open>g \<le> normf\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> le_fun_def 
+              sum_mono)
+        also have "(\<Sum>x\<in>F. ennreal (norm (f x))) \<le> B"
+          using \<open>F \<subseteq> S\<close> \<open>finite F\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> normf_B by blast 
+        finally have "B < B" by auto
+        thus ?thesis by simp
+      qed
+
+      have "integral\<^sup>S M g = (\<Sum>r \<in> gS. r * emeasure M (part r))"
+        unfolding simple_integral_def gS_def M_def part_def by simp
+      also have "\<dots> \<le> (\<Sum>r \<in> gS. B' r)"
+        by (simp add: emeasure_B' sum_mono)
+      also have "\<dots> \<le> B"
+        using sumB' by blast
+      finally show ?thesis by assumption
+    qed
+    hence int_leq_B: "integral\<^sup>N M normf \<le> B"
+      unfolding nn_integral_def by (metis (no_types, lifting) SUP_least mem_Collect_eq)
+    hence "integral\<^sup>N M normf < \<infinity>"
+      using le_less_trans by fastforce
+    hence "integrable M f"
+      unfolding M_def normf_def by (rule integrableI_bounded[rotated], simp)
+    hence v1: "f abs_summable_on S"
+      unfolding abs_summable_on_def M_def by simp  
+
+    have "(\<lambda>x. norm (f x)) abs_summable_on S"
+      using v1 Infinite_Set_Sum.abs_summable_on_norm_iff[where A = S and f = f]
+      by auto
+    moreover have "0 \<le> norm (f x)"
+      if "x \<in> S" for x
+      by simp    
+    moreover have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>count_space S) \<le> ennreal B"
+      using M_def \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> int_leq_B by auto    
+    ultimately have "ennreal (\<Sum>\<^sub>ax\<in>S. norm (f x)) \<le> ennreal B"
+      by (simp add: nn_integral_conv_infsetsum)    
+    hence v2: "(\<Sum>\<^sub>ax\<in>S. norm (f x)) \<le> B"
+      by (subst ennreal_le_iff[symmetric], simp add: assms \<open>B \<ge> 0\<close>)
+    show ?thesis
+      using v1 v2 by auto
+  qed
+  then show "f abs_summable_on S"
+    by (metis abs_summable_on_finite assms empty_subsetI finite.emptyI sum_clauses(1))
+qed
+
+
+lemma infsetsum_nonneg_is_SUPREMUM_ennreal:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes summable: "f abs_summable_on A"
+    and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "ennreal (infsetsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+proof -
+  have sum_F_A: "sum f F \<le> infsetsum f A" 
+    if "F \<in> {F. finite F \<and> F \<subseteq> A}" 
+    for F
+  proof-
+    from that have "finite F" and "F \<subseteq> A" by auto
+    from \<open>finite F\<close> have "sum f F = infsetsum f F" by auto
+    also have "\<dots> \<le> infsetsum f A"
+    proof (rule infsetsum_mono_neutral_left)
+      show "f abs_summable_on F"
+        by (simp add: \<open>finite F\<close>)        
+      show "f abs_summable_on A"
+        by (simp add: local.summable)        
+      show "f x \<le> f x"
+        if "x \<in> F"
+        for x :: 'a
+        by simp 
+      show "F \<subseteq> A"
+        by (simp add: \<open>F \<subseteq> A\<close>)        
+      show "0 \<le> f x"
+        if "x \<in> A - F"
+        for x :: 'a
+        using that fnn by auto 
+    qed
+    finally show ?thesis by assumption
+  qed 
+  hence geq: "ennreal (infsetsum f A) \<ge> (SUP F\<in>{G. finite G \<and> G \<subseteq> A}. (ennreal (sum f F)))"
+    by (meson SUP_least ennreal_leI)
+
+  define fe where "fe x = ennreal (f x)" for x
+
+  have sum_f_int: "infsetsum f A = \<integral>\<^sup>+ x. fe x \<partial>(count_space A)"
+    unfolding infsetsum_def fe_def
+  proof (rule nn_integral_eq_integral [symmetric])
+    show "integrable (count_space A) f"
+      using abs_summable_on_def local.summable by blast      
+    show "AE x in count_space A. 0 \<le> f x"
+      using fnn by auto      
+  qed
+  also have "\<dots> = (SUP g \<in> {g. finite (g`A) \<and> g \<le> fe}. integral\<^sup>S (count_space A) g)"
+    unfolding nn_integral_def simple_function_count_space by simp
+  also have "\<dots> \<le> (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+  proof (rule Sup_least)
+    fix x assume "x \<in> integral\<^sup>S (count_space A) ` {g. finite (g ` A) \<and> g \<le> fe}"
+    then obtain g where xg: "x = integral\<^sup>S (count_space A) g" and fin_gA: "finite (g`A)" 
+      and g_fe: "g \<le> fe" by auto
+    define F where "F = {z:A. g z \<noteq> 0}"
+    hence "F \<subseteq> A" by simp
+
+    have fin: "finite {z:A. g z = t}" if "t \<noteq> 0" for t
+    proof (rule ccontr)
+      assume inf: "infinite {z:A. g z = t}"
+      hence tgA: "t \<in> g ` A"
+        by (metis (mono_tags, lifting) image_eqI not_finite_existsD)
+      have "x = (\<Sum>x \<in> g ` A. x * emeasure (count_space A) (g -` {x} \<inter> A))"
+        unfolding xg simple_integral_def space_count_space by simp
+      also have "\<dots> \<ge> (\<Sum>x \<in> {t}. x * emeasure (count_space A) (g -` {x} \<inter> A))" (is "_ \<ge> \<dots>")
+      proof (rule sum_mono2)
+        show "finite (g ` A)"
+          by (simp add: fin_gA)          
+        show "{t} \<subseteq> g ` A"
+          by (simp add: tgA)          
+        show "0 \<le> b * emeasure (count_space A) (g -` {b} \<inter> A)"
+          if "b \<in> g ` A - {t}"
+          for b :: ennreal
+          using that
+          by simp
+      qed
+      also have "\<dots> = t * emeasure (count_space A) (g -` {t} \<inter> A)"
+        by auto
+      also have "\<dots> = t * \<infinity>"
+      proof (subst emeasure_count_space_infinite)
+        show "g -` {t} \<inter> A \<subseteq> A"
+          by simp             
+        have "{a \<in> A. g a = t} = {a \<in> g -` {t}. a \<in> A}"
+          by auto
+        thus "infinite (g -` {t} \<inter> A)"
+          by (metis (full_types) Int_def inf) 
+        show "t * \<infinity> = t * \<infinity>"
+          by simp
+      qed
+      also have "\<dots> = \<infinity>" using \<open>t \<noteq> 0\<close>
+        by (simp add: ennreal_mult_eq_top_iff)
+      finally have x_inf: "x = \<infinity>"
+        using neq_top_trans by auto
+      have "x = integral\<^sup>S (count_space A) g" by (fact xg)
+      also have "\<dots> = integral\<^sup>N (count_space A) g"
+        by (simp add: fin_gA nn_integral_eq_simple_integral)
+      also have "\<dots> \<le> integral\<^sup>N (count_space A) fe"
+        using g_fe
+        by (simp add: le_funD nn_integral_mono)
+      also have "\<dots> < \<infinity>"
+        by (metis sum_f_int ennreal_less_top infinity_ennreal_def) 
+      finally have x_fin: "x < \<infinity>" by simp
+      from x_inf x_fin show False by simp
+    qed
+    have F: "F = (\<Union>t\<in>g`A-{0}. {z\<in>A. g z = t})"
+      unfolding F_def by auto
+    hence "finite F"
+      unfolding F using fin_gA fin by auto
+    have "x = integral\<^sup>N (count_space A) g"
+      unfolding xg
+      by (simp add: fin_gA nn_integral_eq_simple_integral)
+    also have "\<dots> = set_nn_integral (count_space UNIV) A g"
+      by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+    also have "\<dots> = set_nn_integral (count_space UNIV) F g"
+    proof -
+      have "\<forall>a. g a * (if a \<in> {a \<in> A. g a \<noteq> 0} then 1 else 0) = g a * (if a \<in> A then 1 else 0)"
+        by auto
+      hence "(\<integral>\<^sup>+ a. g a * (if a \<in> A then 1 else 0) \<partial>count_space UNIV)
+           = (\<integral>\<^sup>+ a. g a * (if a \<in> {a \<in> A. g a \<noteq> 0} then 1 else 0) \<partial>count_space UNIV)"
+        by presburger
+      thus ?thesis unfolding F_def indicator_def
+        using mult.right_neutral mult_zero_right nn_integral_cong
+        by (simp add: of_bool_def) 
+    qed
+    also have "\<dots> = integral\<^sup>N (count_space F) g"
+      by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+    also have "\<dots> = sum g F" 
+      using \<open>finite F\<close> by (rule nn_integral_count_space_finite)
+    also have "sum g F \<le> sum fe F"
+      using g_fe unfolding le_fun_def
+      by (simp add: sum_mono) 
+    also have "\<dots> \<le> (SUP F \<in> {G. finite G \<and> G \<subseteq> A}. (sum fe F))"
+      using \<open>finite F\<close> \<open>F\<subseteq>A\<close>
+      by (simp add: SUP_upper)
+    also have "\<dots> = (SUP F \<in> {F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+    proof (rule SUP_cong [OF refl])
+      have "finite x \<Longrightarrow> x \<subseteq> A \<Longrightarrow> (\<Sum>x\<in>x. ennreal (f x)) = ennreal (sum f x)"
+        for x
+        by (metis fnn subsetCE sum_ennreal)
+      thus "sum fe x = ennreal (sum f x)"
+        if "x \<in> {G. finite G \<and> G \<subseteq> A}"
+        for x :: "'a set"
+        using that unfolding fe_def by auto      
+    qed 
+    finally show "x \<le> \<dots>" by simp
+  qed
+  finally have leq: "ennreal (infsetsum f A) \<le> (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+    by assumption
+  from leq geq show ?thesis by simp
+qed
+
+lemma infsetsum_nonneg_is_SUPREMUM_ereal:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes summable: "f abs_summable_on A"
+    and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "ereal (infsetsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+proof -
+  have "ereal (infsetsum f A) = enn2ereal (ennreal (infsetsum f A))"
+    by (simp add: fnn infsetsum_nonneg)
+  also have "\<dots> = enn2ereal (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ennreal (sum f F))"
+    apply (subst infsetsum_nonneg_is_SUPREMUM_ennreal)
+    using fnn by (auto simp add: local.summable)      
+  also have "\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+  proof (simp add: image_def Sup_ennreal.rep_eq)
+    have "0 \<le> Sup {y. \<exists>x. (\<exists>xa. finite xa \<and> xa \<subseteq> A \<and> x = ennreal (sum f xa)) \<and>
+                     y = enn2ereal x}"
+      by (metis (mono_tags, lifting) Sup_upper empty_subsetI ennreal_0 finite.emptyI
+          mem_Collect_eq sum.empty zero_ennreal.rep_eq)
+    moreover have "Sup {y. \<exists>x. (\<exists>y. finite y \<and> y \<subseteq> A \<and> x = ennreal (sum f y)) \<and>
+                y = enn2ereal x} = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
+      using enn2ereal_ennreal fnn in_mono sum_nonneg Collect_cong
+      by smt
+    ultimately show "max 0 (Sup {y. \<exists>x. (\<exists>xa. finite xa \<and> xa \<subseteq> A \<and> x
+                                       = ennreal (sum f xa)) \<and> y = enn2ereal x})
+         = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
+      by linarith
+  qed   
+  finally show ?thesis
+    by simp
+qed
+
+
+text \<open>The following theorem relates \<^const>\<open>Infinite_Set_Sum.abs_summable_on\<close> with \<^const>\<open>Infinite_Sum.abs_summable_on\<close>.
+  Note that while this theorem expresses an equivalence, the notion on the lhs is more general
+  nonetheless because it applies to a wider range of types. (The rhs requires second-countable
+  Banach spaces while the lhs is well-defined on arbitrary real vector spaces.)\<close>
+
+lemma abs_summable_equivalent: \<open>Infinite_Sum.abs_summable_on f A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+  define n where \<open>n x = norm (f x)\<close> for x
+  assume \<open>n summable_on A\<close>
+  then have \<open>sum n F \<le> infsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
+    using that by (auto simp flip: infsum_finite simp: n_def[abs_def] intro!: infsum_mono_neutral)
+    
+  then show \<open>f abs_summable_on A\<close>
+    by (auto intro!: abs_summable_finite_sumsI simp: n_def)
+next
+  define n where \<open>n x = norm (f x)\<close> for x
+  assume \<open>f abs_summable_on A\<close>
+  then have \<open>n abs_summable_on A\<close>
+    by (simp add: \<open>f abs_summable_on A\<close> n_def)
+  then have \<open>sum n F \<le> infsetsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
+    using that by (auto simp flip: infsetsum_finite simp: n_def[abs_def] intro!: infsetsum_mono_neutral)
+  then show \<open>n summable_on A\<close>
+    apply (rule_tac pos_summable_on)
+    by (auto simp add: n_def bdd_above_def)
+qed
+
+lemma infsetsum_infsum:
+  assumes "f abs_summable_on A"
+  shows "infsetsum f A = infsum f A"
+proof -
+  have conv_sum_norm[simp]: "(\<lambda>x. norm (f x)) summable_on A"
+    using abs_summable_equivalent assms by blast
+  have "norm (infsetsum f A - infsum f A) \<le> \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+  proof -
+    define \<delta> where "\<delta> = \<epsilon>/2"
+    with that have [simp]: "\<delta> > 0" by simp
+    obtain F1 where F1A: "F1 \<subseteq> A" and finF1: "finite F1" and leq_eps: "infsetsum (\<lambda>x. norm (f x)) (A-F1) \<le> \<delta>"
+    proof -
+      have sum_SUP: "ereal (infsetsum (\<lambda>x. norm (f x)) A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum (\<lambda>x. norm (f x)) F))"
+        (is "_ = ?SUP")
+        apply (rule infsetsum_nonneg_is_SUPREMUM_ereal)
+        using assms by auto
+
+      have "(SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (\<Sum>x\<in>F. norm (f x))) - ereal \<delta>
+            < (SUP i\<in>{F. finite F \<and> F \<subseteq> A}. ereal (\<Sum>x\<in>i. norm (f x)))"
+        using \<open>\<delta>>0\<close>
+        by (metis diff_strict_left_mono diff_zero ereal_less_eq(3) ereal_minus(1) not_le sum_SUP)
+      then obtain F where "F\<in>{F. finite F \<and> F \<subseteq> A}" and "ereal (sum (\<lambda>x. norm (f x)) F) > ?SUP - ereal (\<delta>)"
+        by (meson less_SUP_iff)
+        
+      hence "sum (\<lambda>x. norm (f x)) F > infsetsum (\<lambda>x. norm (f x)) A -  (\<delta>)"
+        unfolding sum_SUP[symmetric] by auto
+      hence "\<delta> > infsetsum (\<lambda>x. norm (f x)) (A-F)"
+      proof (subst infsetsum_Diff)
+        show "(\<lambda>x. norm (f x)) abs_summable_on A"
+          if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+          using that
+          by (simp add: assms) 
+        show "F \<subseteq> A"
+          if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+          using that \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> by blast 
+        show "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - (\<Sum>\<^sub>ax\<in>F. norm (f x)) < \<delta>"
+          if "(\<Sum>\<^sub>ax\<in>A. norm (f x)) - \<delta> < (\<Sum>x\<in>F. norm (f x))"
+          using that \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> by auto 
+      qed
+      thus ?thesis using that 
+        apply atomize_elim
+        using \<open>F \<in> {F. finite F \<and> F \<subseteq> A}\<close> less_imp_le by blast
+    qed
+    obtain F2 where F2A: "F2 \<subseteq> A" and finF2: "finite F2"
+      and dist: "dist (sum (\<lambda>x. norm (f x)) F2) (infsum (\<lambda>x. norm (f x)) A) \<le> \<delta>"
+      apply atomize_elim
+      by (metis \<open>0 < \<delta>\<close> conv_sum_norm infsum_finite_approximation)
+    have  leq_eps': "infsum (\<lambda>x. norm (f x)) (A-F2) \<le> \<delta>"
+      apply (subst infsum_Diff)
+      using finF2 F2A dist by (auto simp: dist_norm)
+    define F where "F = F1 \<union> F2"
+    have FA: "F \<subseteq> A" and finF: "finite F" 
+      unfolding F_def using F1A F2A finF1 finF2 by auto
+
+    have "(\<Sum>\<^sub>ax\<in>A - (F1 \<union> F2). norm (f x)) \<le> (\<Sum>\<^sub>ax\<in>A - F1. norm (f x))"
+      apply (rule infsetsum_mono_neutral_left)
+      using abs_summable_on_subset assms by fastforce+
+    hence leq_eps: "infsetsum (\<lambda>x. norm (f x)) (A-F) \<le> \<delta>"
+      unfolding F_def
+      using leq_eps by linarith
+    have "infsum (\<lambda>x. norm (f x)) (A - (F1 \<union> F2))
+          \<le> infsum (\<lambda>x. norm (f x)) (A - F2)"
+      apply (rule infsum_mono_neutral)
+      using finF by (auto simp add: finF2 summable_on_cofin_subset F_def)
+    hence leq_eps': "infsum (\<lambda>x. norm (f x)) (A-F) \<le> \<delta>"
+      unfolding F_def 
+      by (rule order.trans[OF _ leq_eps'])
+    have "norm (infsetsum f A - infsetsum f F) = norm (infsetsum f (A-F))"
+      apply (subst infsetsum_Diff [symmetric])
+      by (auto simp: FA assms)
+    also have "\<dots> \<le> infsetsum (\<lambda>x. norm (f x)) (A-F)"
+      using norm_infsetsum_bound by blast
+    also have "\<dots> \<le> \<delta>"
+      using leq_eps by simp
+    finally have diff1: "norm (infsetsum f A - infsetsum f F) \<le> \<delta>"
+      by assumption
+    have "norm (infsum f A - infsum f F) = norm (infsum f (A-F))"
+      apply (subst infsum_Diff [symmetric])
+      by (auto simp: assms abs_summable_summable finF FA)
+    also have "\<dots> \<le> infsum (\<lambda>x. norm (f x)) (A-F)"
+      by (simp add: finF summable_on_cofin_subset norm_infsum_bound)
+    also have "\<dots> \<le> \<delta>"
+      using leq_eps' by simp
+    finally have diff2: "norm (infsum f A - infsum f F) \<le> \<delta>"
+      by assumption
+
+    have x1: "infsetsum f F = infsum f F"
+      using finF by simp
+    have "norm (infsetsum f A - infsum f A) \<le> norm (infsetsum f A - infsetsum f F) + norm (infsum f A - infsum f F)"
+      apply (rule_tac norm_diff_triangle_le)
+       apply auto
+      by (simp_all add: x1 norm_minus_commute)
+    also have "\<dots> \<le> \<epsilon>"
+      using diff1 diff2 \<delta>_def by linarith
+    finally show ?thesis
+      by assumption
+  qed
+  hence "norm (infsetsum f A - infsum f A) = 0"
+    by (meson antisym_conv1 dense_ge norm_not_less_zero)
+  thus ?thesis
+    by auto
+qed
+
 end