--- 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