# HG changeset patch
# User desharna
# Date 1633616897 -7200
# Node ID fd5f62176987041396115c9a8554c8f5458089b2
# Parent  6424c54157d94cd157567438f1a376c23d625223# Parent  409ca22dee4c6f0f485fc30661671254f4a72360
merged

diff -r 6424c54157d9 -r fd5f62176987 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Oct 07 10:16:52 2021 +0200
+++ b/CONTRIBUTORS	Thu Oct 07 16:28:17 2021 +0200
@@ -16,6 +16,11 @@
 * July .. September 2021: Jasmin Blanchette, Martin Desharnais
   Various improvements to Sledgehammer.
 
+* September 2021: Dominique Unruh
+  New theory of infinite sums (HOL-Analysis/Infinite_Sum), 
+  ordering of complex numbers (HOL-Library/Complex_Order),
+  and products of uniform spaces (in HOL-Analysis/Product_Vector).
+
 * July 2021: Florian Haftmann
   Further consolidation of bit operations and word types.
 
diff -r 6424c54157d9 -r fd5f62176987 NEWS
--- a/NEWS	Thu Oct 07 10:16:52 2021 +0200
+++ b/NEWS	Thu Oct 07 16:28:17 2021 +0200
@@ -144,6 +144,15 @@
 
 *** HOL ***
 
+* Theory "HOL-Analysis.Infinite_Sum": new theory for infinite sums with
+a more general definition than the existing theory Infinite_Set_Sum.
+(Infinite_Set_Sum contains theorems relating the two definitions.)
+
+* Theory "HOL-Analysis.Product_Vector": Instantiation of the product of
+uniform spaces as a uniform space. Minor INCOMPATIBILITY: the old
+definition "uniformity_prod_def" is available as a derived fact
+"uniformity_dist".
+
 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
@@ -232,6 +241,9 @@
     multiset_inter_count ~> count_inter_mset
     sup_subset_mset_count ~> count_union_mset
 
+* Theory "HOL-Library.Complex_Order": Defines less, less_eq on complex
+numbers. Not imported by default.
+
 * Theory "HOL-Library.Multiset": syntax precendence for membership
 operations has been adjusted to match the corresponding precendences on
 sets. Rare INCOMPATIBILITY.
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Analysis/Analysis.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -34,6 +34,7 @@
   Product_Topology
   Lindelof_Spaces
   Infinite_Products
+  Infinite_Sum
   Infinite_Set_Sum
   Polytope
   Jordan_Curve
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Oct 07 16:28:17 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
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Analysis/Infinite_Sum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -0,0 +1,1977 @@
+(*
+  Title:    HOL/Analysis/Infinite_Sum.thy
+  Author:   Dominique Unruh, University of Tartu
+
+  A theory of sums over possible infinite sets.
+*)
+
+section \<open>Infinite sums\<close>
+\<^latex>\<open>\label{section:Infinite_Sum}\<close>
+
+text \<open>In this theory, we introduce the definition of infinite sums, i.e., sums ranging over an
+infinite, potentially uncountable index set with no particular ordering.
+(This is different from series. Those are sums indexed by natural numbers,
+and the order of the index set matters.)
+
+Our definition is quite standard: $s:=\sum_{x\in A} f(x)$ is the limit of finite sums $s_F:=\sum_{x\in F} f(x)$ for increasing $F$.
+That is, $s$ is the limit of the net $s_F$ where $F$ are finite subsets of $A$ ordered by inclusion.
+We believe that this is the standard definition for such sums.
+See, e.g., Definition 4.11 in \cite{conway2013course}.
+This definition is quite general: it is well-defined whenever $f$ takes values in some
+commutative monoid endowed with a Hausdorff topology.
+(Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
+
+theory Infinite_Sum
+  imports
+    "HOL-Analysis.Elementary_Topology"
+    "HOL-Library.Extended_Nonnegative_Real"
+    "HOL-Library.Complex_Order"
+begin
+
+subsection \<open>Definition and syntax\<close>
+
+definition has_sum :: \<open>('a \<Rightarrow> 'b :: {comm_monoid_add, topological_space}) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool\<close> where
+  \<open>has_sum f A x \<longleftrightarrow> (sum f \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
+
+definition summable_on :: "('a \<Rightarrow> 'b::{comm_monoid_add, topological_space}) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "summable'_on" 46) where
+  "f summable_on A \<longleftrightarrow> (\<exists>x. has_sum f A x)"
+
+definition infsum :: "('a \<Rightarrow> 'b::{comm_monoid_add,t2_space}) \<Rightarrow> 'a set \<Rightarrow> 'b" where
+  "infsum f A = (if f summable_on A then Lim (finite_subsets_at_top A) (sum f) else 0)"
+
+abbreviation abs_summable_on :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "abs'_summable'_on" 46) where
+  "f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
+
+syntax (ASCII)
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10)
+syntax
+  "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"  ("(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)" [0, 51, 10] 10)
+translations \<comment> \<open>Beware of argument permutation!\<close>
+  "\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
+
+syntax (ASCII)
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3INFSUM _./ _)" [0, 10] 10)
+syntax
+  "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>\<^sub>\<infinity>_./ _)" [0, 10] 10)
+translations
+  "\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
+
+syntax (ASCII)
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10)
+syntax
+  "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)" [0, 0, 10] 10)
+translations
+  "\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
+
+print_translation \<open>
+let
+  fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
+        if x <> y then raise Match
+        else
+          let
+            val x' = Syntax_Trans.mark_bound_body (x, Tx);
+            val t' = subst_bound (x', t);
+            val P' = subst_bound (x', P);
+          in
+            Syntax.const @{syntax_const "_qinfsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+          end
+    | sum_tr' _ = raise Match;
+in [(@{const_syntax infsum}, K sum_tr')] end
+\<close>
+
+subsection \<open>General properties\<close>
+
+lemma infsumI:
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+  assumes \<open>has_sum f A x\<close>
+  shows \<open>infsum f A = x\<close>
+  by (metis assms finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+
+lemma infsum_eqI:
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+  assumes \<open>x = y\<close>
+  assumes \<open>has_sum f A x\<close>
+  assumes \<open>has_sum g B y\<close>
+  shows \<open>infsum f A = infsum g B\<close>
+  by (metis assms(1) assms(2) assms(3) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+
+lemma infsum_eqI':
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+  assumes \<open>\<And>x. has_sum f A x \<longleftrightarrow> has_sum g B x\<close>
+  shows \<open>infsum f A = infsum g B\<close>
+  by (metis assms infsum_def infsum_eqI summable_on_def)
+
+lemma infsum_not_exists:
+  fixes f :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+  assumes \<open>\<not> f summable_on A\<close>
+  shows \<open>infsum f A = 0\<close>
+  by (simp add: assms infsum_def)
+
+lemma has_sum_cong_neutral:
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, topological_space}\<close>
+  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
+  shows "has_sum f S x \<longleftrightarrow> has_sum g T x"
+proof -
+  have \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))
+      = eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close> for P
+  proof 
+    assume \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))\<close>
+    then obtain F0 where \<open>finite F0\<close> and \<open>F0 \<subseteq> S\<close> and F0_P: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> F \<supseteq> F0 \<Longrightarrow> P (sum f F)\<close>
+      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
+    define F0' where \<open>F0' = F0 \<inter> T\<close>
+    have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> T\<close>
+      by (simp_all add: F0'_def \<open>finite F0\<close>)
+    have \<open>P (sum g F)\<close> if \<open>finite F\<close> \<open>F \<subseteq> T\<close> \<open>F \<supseteq> F0'\<close> for F
+    proof -
+      have \<open>P (sum f ((F\<inter>S) \<union> (F0\<inter>S)))\<close>
+        apply (rule F0_P)
+        using \<open>F0 \<subseteq> S\<close>  \<open>finite F0\<close> that by auto
+      also have \<open>sum f ((F\<inter>S) \<union> (F0\<inter>S)) = sum g F\<close>
+        apply (rule sum.mono_neutral_cong)
+        using that \<open>finite F0\<close> F0'_def assms by auto
+      finally show ?thesis
+        by -
+    qed
+    with \<open>F0' \<subseteq> T\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close>
+      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
+  next
+    assume \<open>eventually P (filtermap (sum g) (finite_subsets_at_top T))\<close>
+    then obtain F0 where \<open>finite F0\<close> and \<open>F0 \<subseteq> T\<close> and F0_P: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> T \<Longrightarrow> F \<supseteq> F0 \<Longrightarrow> P (sum g F)\<close>
+      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
+    define F0' where \<open>F0' = F0 \<inter> S\<close>
+    have [simp]: \<open>finite F0'\<close> \<open>F0' \<subseteq> S\<close>
+      by (simp_all add: F0'_def \<open>finite F0\<close>)
+    have \<open>P (sum f F)\<close> if \<open>finite F\<close> \<open>F \<subseteq> S\<close> \<open>F \<supseteq> F0'\<close> for F
+    proof -
+      have \<open>P (sum g ((F\<inter>T) \<union> (F0\<inter>T)))\<close>
+        apply (rule F0_P)
+        using \<open>F0 \<subseteq> T\<close>  \<open>finite F0\<close> that by auto
+      also have \<open>sum g ((F\<inter>T) \<union> (F0\<inter>T)) = sum f F\<close>
+        apply (rule sum.mono_neutral_cong)
+        using that \<open>finite F0\<close> F0'_def assms by auto
+      finally show ?thesis
+        by -
+    qed
+    with \<open>F0' \<subseteq> S\<close> \<open>finite F0'\<close> show \<open>eventually P (filtermap (sum f) (finite_subsets_at_top S))\<close>
+      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
+  qed
+
+  then have tendsto_x: "(sum f \<longlongrightarrow> x) (finite_subsets_at_top S) \<longleftrightarrow> (sum g \<longlongrightarrow> x) (finite_subsets_at_top T)" for x
+    by (simp add: le_filter_def filterlim_def)
+
+  then show ?thesis
+    by (simp add: has_sum_def)
+qed
+
+lemma summable_on_cong_neutral: 
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, topological_space}\<close>
+  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
+  shows "f summable_on S \<longleftrightarrow> g summable_on T"
+  using has_sum_cong_neutral[of T S g f, OF assms]
+  by (simp add: summable_on_def)
+
+lemma infsum_cong_neutral: 
+  fixes f g :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add, t2_space}\<close>
+  assumes \<open>\<And>x. x\<in>T-S \<Longrightarrow> g x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S-T \<Longrightarrow> f x = 0\<close>
+  assumes \<open>\<And>x. x\<in>S\<inter>T \<Longrightarrow> f x = g x\<close>
+  shows \<open>infsum f S = infsum g T\<close>
+  apply (rule infsum_eqI')
+  using assms by (rule has_sum_cong_neutral)
+
+lemma has_sum_cong: 
+  assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
+  shows "has_sum f A x \<longleftrightarrow> has_sum g A x"
+  by (smt (verit, best) DiffE IntD2 assms has_sum_cong_neutral)
+
+lemma summable_on_cong:
+  assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
+  shows "f summable_on A \<longleftrightarrow> g summable_on A"
+  by (metis assms summable_on_def has_sum_cong)
+
+lemma infsum_cong:
+  assumes "\<And>x. x\<in>A \<Longrightarrow> f x = g x"
+  shows "infsum f A = infsum g A"
+  using assms infsum_eqI' has_sum_cong by blast
+
+lemma summable_on_cofin_subset:
+  fixes f :: "'a \<Rightarrow> 'b::topological_ab_group_add"
+  assumes "f summable_on A" and [simp]: "finite F"
+  shows "f summable_on (A - F)"
+proof -
+  from assms(1) obtain x where lim_f: "(sum f \<longlongrightarrow> x) (finite_subsets_at_top A)"
+    unfolding summable_on_def has_sum_def by auto
+  define F' where "F' = F\<inter>A"
+  with assms have "finite F'" and "A-F = A-F'"
+    by auto
+  have "filtermap ((\<union>)F') (finite_subsets_at_top (A-F))
+      \<le> finite_subsets_at_top A"
+  proof (rule filter_leI)
+    fix P assume "eventually P (finite_subsets_at_top A)"
+    then obtain X where [simp]: "finite X" and XA: "X \<subseteq> A" 
+      and P: "\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y"
+      unfolding eventually_finite_subsets_at_top by auto
+    define X' where "X' = X-F"
+    hence [simp]: "finite X'" and [simp]: "X' \<subseteq> A-F"
+      using XA by auto
+    hence "finite Y \<and> X' \<subseteq> Y \<and> Y \<subseteq> A - F \<longrightarrow> P (F' \<union> Y)" for Y
+      using P XA unfolding X'_def using F'_def \<open>finite F'\<close> by blast
+    thus "eventually P (filtermap ((\<union>) F') (finite_subsets_at_top (A - F)))"
+      unfolding eventually_filtermap eventually_finite_subsets_at_top
+      by (rule_tac x=X' in exI, simp)
+  qed
+  with lim_f have "(sum f \<longlongrightarrow> x) (filtermap ((\<union>)F') (finite_subsets_at_top (A-F)))"
+    using tendsto_mono by blast
+  have "((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> x) (finite_subsets_at_top (A - F))"
+    if "((sum f \<circ> (\<union>) F') \<longlongrightarrow> x) (finite_subsets_at_top (A - F))"
+    using that unfolding o_def by auto
+  hence "((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> x) (finite_subsets_at_top (A-F))"
+    using tendsto_compose_filtermap [symmetric]
+    by (simp add: \<open>(sum f \<longlongrightarrow> x) (filtermap ((\<union>) F') (finite_subsets_at_top (A - F)))\<close> 
+        tendsto_compose_filtermap)
+  have "\<forall>Y. finite Y \<and> Y \<subseteq> A - F \<longrightarrow> sum f (F' \<union> Y) = sum f F' + sum f Y"
+    by (metis Diff_disjoint Int_Diff \<open>A - F = A - F'\<close> \<open>finite F'\<close> inf.orderE sum.union_disjoint)
+  hence "\<forall>\<^sub>F x in finite_subsets_at_top (A - F). sum f (F' \<union> x) = sum f F' + sum f x"
+    unfolding eventually_finite_subsets_at_top
+    using exI [where x = "{}"]
+    by (simp add: \<open>\<And>P. P {} \<Longrightarrow> \<exists>x. P x\<close>) 
+  hence "((\<lambda>G. sum f F' + sum f G) \<longlongrightarrow> x) (finite_subsets_at_top (A-F))"
+    using tendsto_cong [THEN iffD1 , rotated]
+      \<open>((\<lambda>G. sum f (F' \<union> G)) \<longlongrightarrow> x) (finite_subsets_at_top (A - F))\<close> by fastforce
+  hence "((\<lambda>G. sum f F' + sum f G) \<longlongrightarrow> sum f F' + (x-sum f F')) (finite_subsets_at_top (A-F))"
+    by simp
+  hence "(sum f \<longlongrightarrow> x - sum f F') (finite_subsets_at_top (A-F))"
+    using tendsto_add_const_iff by blast    
+  thus "f summable_on (A - F)"
+    unfolding summable_on_def has_sum_def by auto
+qed
+
+lemma
+  fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add}"
+  assumes \<open>has_sum f B b\<close> and \<open>has_sum f A a\<close> and AB: "A \<subseteq> B"
+  shows has_sum_Diff: "has_sum f (B - A) (b - a)"
+proof -
+  have finite_subsets1:
+    "finite_subsets_at_top (B - A) \<le> filtermap (\<lambda>F. F - A) (finite_subsets_at_top B)"
+  proof (rule filter_leI)
+    fix P assume "eventually P (filtermap (\<lambda>F. F - A) (finite_subsets_at_top B))"
+    then obtain X where "finite X" and "X \<subseteq> B" 
+      and P: "finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> B \<longrightarrow> P (Y - A)" for Y
+      unfolding eventually_filtermap eventually_finite_subsets_at_top by auto
+
+    hence "finite (X-A)" and "X-A \<subseteq> B - A"
+      by auto
+    moreover have "finite Y \<and> X-A \<subseteq> Y \<and> Y \<subseteq> B - A \<longrightarrow> P Y" for Y
+      using P[where Y="Y\<union>X"] \<open>finite X\<close> \<open>X \<subseteq> B\<close>
+      by (metis Diff_subset Int_Diff Un_Diff finite_Un inf.orderE le_sup_iff sup.orderE sup_ge2)
+    ultimately show "eventually P (finite_subsets_at_top (B - A))"
+      unfolding eventually_finite_subsets_at_top by meson
+  qed
+  have finite_subsets2: 
+    "filtermap (\<lambda>F. F \<inter> A) (finite_subsets_at_top B) \<le> finite_subsets_at_top A"
+    apply (rule filter_leI)
+      using assms unfolding eventually_filtermap eventually_finite_subsets_at_top
+      by (metis Int_subset_iff finite_Int inf_le2 subset_trans)
+
+  from assms(1) have limB: "(sum f \<longlongrightarrow> b) (finite_subsets_at_top B)"
+    using has_sum_def by auto
+  from assms(2) have limA: "(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)"
+    using has_sum_def by blast
+  have "((\<lambda>F. sum f (F\<inter>A)) \<longlongrightarrow> a) (finite_subsets_at_top B)"
+  proof (subst asm_rl [of "(\<lambda>F. sum f (F\<inter>A)) = sum f o (\<lambda>F. F\<inter>A)"])
+    show "(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)"
+      unfolding o_def by auto
+    show "((sum f \<circ> (\<lambda>F. F \<inter> A)) \<longlongrightarrow> a) (finite_subsets_at_top B)"
+      unfolding o_def 
+      using tendsto_compose_filtermap finite_subsets2 limA tendsto_mono
+        \<open>(\<lambda>F. sum f (F \<inter> A)) = sum f \<circ> (\<lambda>F. F \<inter> A)\<close> by fastforce
+  qed
+
+  with limB have "((\<lambda>F. sum f F - sum f (F\<inter>A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)"
+    using tendsto_diff by blast
+  have "sum f X - sum f (X \<inter> A) = sum f (X - A)" if "finite X" and "X \<subseteq> B" for X :: "'a set"
+    using that by (metis add_diff_cancel_left' sum.Int_Diff)
+  hence "\<forall>\<^sub>F x in finite_subsets_at_top B. sum f x - sum f (x \<inter> A) = sum f (x - A)"
+    by (rule eventually_finite_subsets_at_top_weakI)  
+  hence "((\<lambda>F. sum f (F-A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)"
+    using tendsto_cong [THEN iffD1 , rotated]
+      \<open>((\<lambda>F. sum f F - sum f (F \<inter> A)) \<longlongrightarrow> b - a) (finite_subsets_at_top B)\<close> by fastforce
+  hence "(sum f \<longlongrightarrow> b - a) (filtermap (\<lambda>F. F-A) (finite_subsets_at_top B))"
+    by (subst tendsto_compose_filtermap[symmetric], simp add: o_def)
+  hence limBA: "(sum f \<longlongrightarrow> b - a) (finite_subsets_at_top (B-A))"
+    apply (rule tendsto_mono[rotated])
+    by (rule finite_subsets1)
+  thus ?thesis
+    by (simp add: has_sum_def)
+qed
+
+
+lemma
+  fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add}"
+  assumes "f summable_on B" and "f summable_on A" and "A \<subseteq> B"
+  shows summable_on_Diff: "f summable_on (B-A)"
+  by (meson assms summable_on_def has_sum_Diff)
+
+lemma
+  fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,t2_space}"
+  assumes "f summable_on B" and "f summable_on A" and AB: "A \<subseteq> B"
+  shows infsum_Diff: "infsum f (B - A) = infsum f B - infsum f A"
+  by (smt (z3) AB assms(1) assms(2) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_Diff has_sum_def tendsto_Lim)
+
+lemma has_sum_mono_neutral:
+  fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+  (* Does this really require a linorder topology? (Instead of order topology.) *)
+  assumes \<open>has_sum f A a\<close> and "has_sum g B b"
+  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
+  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
+  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
+  shows "a \<le> b"
+proof -
+  define f' g' where \<open>f' x = (if x \<in> A then f x else 0)\<close> and \<open>g' x = (if x \<in> B then g x else 0)\<close> for x
+  have [simp]: \<open>f summable_on A\<close> \<open>g summable_on B\<close>
+    using assms(1,2) summable_on_def by auto
+  have \<open>has_sum f' (A\<union>B) a\<close>
+    apply (subst has_sum_cong_neutral[where g=f and T=A])
+    by (auto simp: f'_def assms(1))
+  then have f'_lim: \<open>(sum f' \<longlongrightarrow> a) (finite_subsets_at_top (A\<union>B))\<close>
+    by (meson has_sum_def)
+  have \<open>has_sum g' (A\<union>B) b\<close>
+    apply (subst has_sum_cong_neutral[where g=g and T=B])
+    by (auto simp: g'_def assms(2))
+  then have g'_lim: \<open>(sum g' \<longlongrightarrow> b) (finite_subsets_at_top (A\<union>B))\<close>
+    using has_sum_def by blast
+
+  have *: \<open>\<forall>\<^sub>F x in finite_subsets_at_top (A \<union> B). sum f' x \<le> sum g' x\<close>
+    apply (rule eventually_finite_subsets_at_top_weakI)
+    apply (rule sum_mono)
+    using assms by (auto simp: f'_def g'_def)
+  show ?thesis
+    apply (rule tendsto_le)
+    using * g'_lim f'_lim by auto
+qed
+
+lemma infsum_mono_neutral:
+  fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+  assumes "f summable_on A" and "g summable_on B"
+  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
+  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
+  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
+  shows "infsum f A \<le> infsum g B"
+  apply (rule has_sum_mono_neutral[of f A _ g B _])
+  using assms apply auto
+  by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)+
+
+lemma has_sum_mono:
+  fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+  assumes "has_sum f A x" and "has_sum g A y"
+  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
+  shows "x \<le> y"
+  apply (rule has_sum_mono_neutral)
+  using assms by auto
+
+lemma infsum_mono:
+  fixes f :: "'a\<Rightarrow>'b::{ordered_comm_monoid_add,linorder_topology}"
+  assumes "f summable_on A" and "g summable_on A"
+  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
+  shows "infsum f A \<le> infsum g A"
+  apply (rule infsum_mono_neutral)
+  using assms by auto
+
+lemma has_sum_finite[simp]:
+  assumes "finite F"
+  shows "has_sum f F (sum f F)"
+  using assms
+  by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def has_sum_def principal_eq_bot_iff)
+
+lemma summable_on_finite[simp]:
+  fixes f :: \<open>'a \<Rightarrow> 'b::{comm_monoid_add,topological_space}\<close>
+  assumes "finite F"
+  shows "f summable_on F"
+  using assms summable_on_def has_sum_finite by blast
+
+lemma infsum_finite[simp]:
+  assumes "finite F"
+  shows "infsum f F = sum f F"
+  using assms by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def principal_eq_bot_iff)
+
+lemma has_sum_finite_approximation:
+  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}"
+  assumes "has_sum f A x" and "\<epsilon> > 0"
+  shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) x \<le> \<epsilon>"
+proof -
+  have "(sum f \<longlongrightarrow> x) (finite_subsets_at_top A)"
+    by (meson assms(1) has_sum_def)
+  hence *: "\<forall>\<^sub>F F in (finite_subsets_at_top A). dist (sum f F) x < \<epsilon>"
+    using assms(2) by (rule tendstoD)
+  show ?thesis
+    by (smt (verit) * eventually_finite_subsets_at_top order_refl)
+qed
+
+lemma infsum_finite_approximation:
+  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}"
+  assumes "f summable_on A" and "\<epsilon> > 0"
+  shows "\<exists>F. finite F \<and> F \<subseteq> A \<and> dist (sum f F) (infsum f A) \<le> \<epsilon>"
+  by (metis assms(1) assms(2) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_finite_approximation has_sum_def tendsto_Lim)
+
+lemma abs_summable_summable:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: banach\<close>
+  assumes \<open>f abs_summable_on A\<close>
+  shows \<open>f summable_on A\<close>
+proof -
+  from assms obtain L where lim: \<open>(sum (\<lambda>x. norm (f x)) \<longlongrightarrow> L) (finite_subsets_at_top A)\<close>
+    unfolding has_sum_def summable_on_def by blast
+  then have *: \<open>cauchy_filter (filtermap (sum (\<lambda>x. norm (f x))) (finite_subsets_at_top A))\<close>
+    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
+  have \<open>\<exists>P. eventually P (finite_subsets_at_top A) \<and>
+              (\<forall>F F'. P F \<and> P F' \<longrightarrow> dist (sum f F) (sum f F') < e)\<close> if \<open>e>0\<close> for e
+  proof -
+    define d P where \<open>d = e/4\<close> and \<open>P F \<longleftrightarrow> finite F \<and> F \<subseteq> A \<and> dist (sum (\<lambda>x. norm (f x)) F) L < d\<close> for F
+    then have \<open>d > 0\<close>
+      by (simp add: d_def that)
+    have ev_P: \<open>eventually P (finite_subsets_at_top A)\<close>
+      using lim
+      by (auto simp add: P_def[abs_def] \<open>0 < d\<close> eventually_conj_iff eventually_finite_subsets_at_top_weakI tendsto_iff)
+
+    moreover have \<open>dist (sum f F1) (sum f F2) < e\<close> if \<open>P F1\<close> and \<open>P F2\<close> for F1 F2
+    proof -
+      from ev_P
+      obtain F' where \<open>finite F'\<close> and \<open>F' \<subseteq> A\<close> and P_sup_F': \<open>finite F \<and> F \<supseteq> F' \<and> F \<subseteq> A \<Longrightarrow> P F\<close> for F
+        apply atomize_elim by (simp add: eventually_finite_subsets_at_top)
+      define F where \<open>F = F' \<union> F1 \<union> F2\<close>
+      have \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
+        using F_def P_def[abs_def] that \<open>finite F'\<close> \<open>F' \<subseteq> A\<close> by auto
+      have dist_F: \<open>dist (sum (\<lambda>x. norm (f x)) F) L < d\<close>
+        by (metis F_def \<open>F \<subseteq> A\<close> P_def P_sup_F' \<open>finite F\<close> le_supE order_refl)
+
+      from dist_F have \<open>dist (sum (\<lambda>x. norm (f x)) F) (sum (\<lambda>x. norm (f x)) F2) < 2*d\<close>
+        by (smt (z3) P_def dist_norm real_norm_def that(2))
+      then have \<open>norm (sum (\<lambda>x. norm (f x)) (F-F2)) < 2*d\<close>
+        unfolding dist_norm
+        by (metis F_def \<open>finite F\<close> sum_diff sup_commute sup_ge1)
+      then have \<open>norm (sum f (F-F2)) < 2*d\<close>
+        by (smt (verit, ccfv_threshold) real_norm_def sum_norm_le)
+      then have dist_F_F2: \<open>dist (sum f F) (sum f F2) < 2*d\<close>
+        by (metis F_def \<open>finite F\<close> dist_norm sum_diff sup_commute sup_ge1)
+
+      from dist_F have \<open>dist (sum (\<lambda>x. norm (f x)) F) (sum (\<lambda>x. norm (f x)) F1) < 2*d\<close>
+        by (smt (z3) P_def dist_norm real_norm_def that(1))
+      then have \<open>norm (sum (\<lambda>x. norm (f x)) (F-F1)) < 2*d\<close>
+        unfolding dist_norm
+        by (metis F_def \<open>finite F\<close> inf_sup_ord(3) order_trans sum_diff sup_ge2)
+      then have \<open>norm (sum f (F-F1)) < 2*d\<close>
+        by (smt (verit, ccfv_threshold) real_norm_def sum_norm_le)
+      then have dist_F_F1: \<open>dist (sum f F) (sum f F1) < 2*d\<close>
+        by (metis F_def \<open>finite F\<close> dist_norm inf_sup_ord(3) le_supE sum_diff)
+
+      from dist_F_F2 dist_F_F1 show \<open>dist (sum f F1) (sum f F2) < e\<close>
+        unfolding d_def apply auto
+        by (meson dist_triangle_half_r less_divide_eq_numeral1(1))
+    qed
+    then show ?thesis
+      using ev_P by blast
+  qed
+  then have \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))\<close>
+    by (simp add: cauchy_filter_metric_filtermap)
+  then obtain L' where \<open>(sum f \<longlongrightarrow> L') (finite_subsets_at_top A)\<close>
+    apply atomize_elim unfolding filterlim_def
+    apply (rule complete_uniform[where S=UNIV, simplified, THEN iffD1, rule_format])
+      apply (auto simp add: filtermap_bot_iff)
+    by (meson Cauchy_convergent UNIV_I complete_def convergent_def)
+  then show ?thesis
+    using summable_on_def has_sum_def by blast
+qed
+
+text \<open>The converse of @{thm [source] abs_summable_summable} does not hold:
+  Consider the Hilbert space of square-summable sequences.
+  Let $e_i$ denote the sequence with 1 in the $i$th position and 0 elsewhere.
+  Let $f(i) := e_i/i$ for $i\geq1$. We have \<^term>\<open>\<not> f abs_summable_on UNIV\<close> because $\lVert f(i)\rVert=1/i$
+  and thus the sum over $\lVert f(i)\rVert$ diverges. On the other hand, we have \<^term>\<open>f summable_on UNIV\<close>;
+  the limit is the sequence with $1/i$ in the $i$th position.
+
+  (We have not formalized this separating example here because to the best of our knowledge,
+  this Hilbert space has not been formalized in Isabelle/HOL yet.)\<close>
+
+lemma norm_has_sum_bound:
+  fixes f :: "'b \<Rightarrow> 'a::real_normed_vector"
+    and A :: "'b set"
+  assumes "has_sum (\<lambda>x. norm (f x)) A n"
+  assumes "has_sum f A a"
+  shows "norm a \<le> n"
+proof -
+  have "norm a \<le> n + \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+  proof-
+    have "\<exists>F. norm (a - sum f F) \<le> \<epsilon> \<and> finite F \<and> F \<subseteq> A"
+      using has_sum_finite_approximation[where A=A and f=f and \<epsilon>="\<epsilon>"] assms \<open>0 < \<epsilon>\<close>
+      by (metis dist_commute dist_norm)
+    then obtain F where "norm (a - sum f F) \<le> \<epsilon>"
+      and "finite F" and "F \<subseteq> A"
+      by (simp add: atomize_elim)
+    hence "norm a \<le> norm (sum f F) + \<epsilon>"
+      by (smt norm_triangle_sub)
+    also have "\<dots> \<le> sum (\<lambda>x. norm (f x)) F + \<epsilon>"
+      using norm_sum by auto
+    also have "\<dots> \<le> n + \<epsilon>"
+      apply (rule add_right_mono)
+      apply (rule has_sum_mono_neutral[where A=F and B=A and f=\<open>\<lambda>x. norm (f x)\<close> and g=\<open>\<lambda>x. norm (f x)\<close>])
+      using \<open>finite F\<close> \<open>F \<subseteq> A\<close> assms by auto
+    finally show ?thesis 
+      by assumption
+  qed
+  thus ?thesis
+    using linordered_field_class.field_le_epsilon by blast
+qed
+
+lemma norm_infsum_bound:
+  fixes f :: "'b \<Rightarrow> 'a::real_normed_vector"
+    and A :: "'b set"
+  assumes "f abs_summable_on A"
+  shows "norm (infsum f A) \<le> infsum (\<lambda>x. norm (f x)) A"
+proof (cases "f summable_on A")
+  case True
+  show ?thesis
+    apply (rule norm_has_sum_bound[where A=A and f=f and a=\<open>infsum f A\<close> and n=\<open>infsum (\<lambda>x. norm (f x)) A\<close>])
+    using assms True
+    by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)+
+next
+  case False
+  obtain t where t_def: "(sum (\<lambda>x. norm (f x)) \<longlongrightarrow> t) (finite_subsets_at_top A)"
+    using assms unfolding summable_on_def has_sum_def by blast
+  have sumpos: "sum (\<lambda>x. norm (f x)) X \<ge> 0"
+    for X
+    by (simp add: sum_nonneg)
+  have tgeq0:"t \<ge> 0"
+  proof(rule ccontr)
+    define S::"real set" where "S = {s. s < 0}"
+    assume "\<not> 0 \<le> t"
+    hence "t < 0" by simp
+    hence "t \<in> S"
+      unfolding S_def by blast
+    moreover have "open S"
+    proof-
+      have "closed {s::real. s \<ge> 0}"
+        using Elementary_Topology.closed_sequential_limits[where S = "{s::real. s \<ge> 0}"]
+        by (metis Lim_bounded2 mem_Collect_eq)
+      moreover have "{s::real. s \<ge> 0} = UNIV - S"
+        unfolding S_def by auto
+      ultimately have "closed (UNIV - S)"
+        by simp
+      thus ?thesis
+        by (simp add: Compl_eq_Diff_UNIV open_closed) 
+    qed
+    ultimately have "\<forall>\<^sub>F X in finite_subsets_at_top A. (\<Sum>x\<in>X. norm (f x)) \<in> S"
+      using t_def unfolding tendsto_def by blast
+    hence "\<exists>X. (\<Sum>x\<in>X. norm (f x)) \<in> S"
+      by (metis (no_types, lifting) eventually_mono filterlim_iff finite_subsets_at_top_neq_bot tendsto_Lim)
+    then obtain X where "(\<Sum>x\<in>X. norm (f x)) \<in> S"
+      by blast
+    hence "(\<Sum>x\<in>X. norm (f x)) < 0"
+      unfolding S_def by auto      
+    thus False using sumpos by smt
+  qed
+  have "\<exists>!h. (sum (\<lambda>x. norm (f x)) \<longlongrightarrow> h) (finite_subsets_at_top A)"
+    using t_def finite_subsets_at_top_neq_bot tendsto_unique by blast
+  hence "t = (Topological_Spaces.Lim (finite_subsets_at_top A) (sum (\<lambda>x. norm (f x))))"
+    using t_def unfolding Topological_Spaces.Lim_def
+    by (metis the_equality)     
+  hence "Lim (finite_subsets_at_top A) (sum (\<lambda>x. norm (f x))) \<ge> 0"
+    using tgeq0 by blast
+  thus ?thesis unfolding infsum_def 
+    using False by auto
+qed
+
+lemma has_sum_infsum[simp]:
+  assumes \<open>f summable_on S\<close>
+  shows \<open>has_sum f S (infsum f S)\<close>
+  using assms by (auto simp: summable_on_def infsum_def has_sum_def tendsto_Lim)
+
+lemma infsum_tendsto:
+  assumes \<open>f summable_on S\<close>
+  shows \<open>((\<lambda>F. sum f F) \<longlongrightarrow> infsum f S) (finite_subsets_at_top S)\<close>
+  using assms by (simp flip: has_sum_def)
+
+
+lemma has_sum_0: 
+  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
+  shows \<open>has_sum f M 0\<close>
+  unfolding has_sum_def
+  apply (subst tendsto_cong[where g=\<open>\<lambda>_. 0\<close>])
+   apply (rule eventually_finite_subsets_at_top_weakI)
+  using assms by (auto simp add: subset_iff)
+
+lemma summable_on_0:
+  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
+  shows \<open>f summable_on M\<close>
+  using assms summable_on_def has_sum_0 by blast
+
+lemma infsum_0:
+  assumes \<open>\<And>x. x\<in>M \<Longrightarrow> f x = 0\<close>
+  shows \<open>infsum f M = 0\<close>
+  by (metis assms finite_subsets_at_top_neq_bot infsum_def has_sum_0 has_sum_def tendsto_Lim)
+
+text \<open>Variants of @{thm [source] infsum_0} etc. suitable as simp-rules\<close>
+lemma infsum_0_simp[simp]: \<open>infsum (\<lambda>_. 0) M = 0\<close>
+  by (simp_all add: infsum_0)
+lemma summable_on_0_simp[simp]: \<open>(\<lambda>_. 0) summable_on M\<close>
+  by (simp_all add: summable_on_0)
+lemma has_sum_0_simp[simp]: \<open>has_sum (\<lambda>_. 0) M 0\<close>
+  by (simp_all add: has_sum_0)
+
+
+lemma has_sum_add:
+  fixes f g :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add}"
+  assumes \<open>has_sum f A a\<close>
+  assumes \<open>has_sum g A b\<close>
+  shows \<open>has_sum (\<lambda>x. f x + g x) A (a + b)\<close>
+proof -
+  from assms have lim_f: \<open>(sum f \<longlongrightarrow> a)  (finite_subsets_at_top A)\<close>
+    and lim_g: \<open>(sum g \<longlongrightarrow> b)  (finite_subsets_at_top A)\<close>
+    by (simp_all add: has_sum_def)
+  then have lim: \<open>(sum (\<lambda>x. f x + g x) \<longlongrightarrow> a + b) (finite_subsets_at_top A)\<close>
+    unfolding sum.distrib by (rule tendsto_add)
+  then show ?thesis
+    by (simp_all add: has_sum_def)
+qed
+
+lemma summable_on_add:
+  fixes f g :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add}"
+  assumes \<open>f summable_on A\<close>
+  assumes \<open>g summable_on A\<close>
+  shows \<open>(\<lambda>x. f x + g x) summable_on A\<close>
+  by (metis (full_types) assms(1) assms(2) summable_on_def has_sum_add)
+
+lemma infsum_add:
+  fixes f g :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add, t2_space}"
+  assumes \<open>f summable_on A\<close>
+  assumes \<open>g summable_on A\<close>
+  shows \<open>infsum (\<lambda>x. f x + g x) A = infsum f A + infsum g A\<close>
+proof -
+  have \<open>has_sum (\<lambda>x. f x + g x) A (infsum f A + infsum g A)\<close>
+    by (simp add: assms(1) assms(2) has_sum_add)
+  then show ?thesis
+    by (smt (z3) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+qed
+
+
+lemma has_sum_Un_disjoint:
+  fixes f :: "'a \<Rightarrow> 'b::topological_comm_monoid_add"
+  assumes "has_sum f A a"
+  assumes "has_sum f B b"
+  assumes disj: "A \<inter> B = {}"
+  shows \<open>has_sum f (A \<union> B) (a + b)\<close>
+proof -
+  define fA fB where \<open>fA x = (if x \<in> A then f x else 0)\<close>
+    and \<open>fB x = (if x \<notin> A then f x else 0)\<close> for x
+  have fA: \<open>has_sum fA (A \<union> B) a\<close>
+    apply (subst has_sum_cong_neutral[where T=A and g=f])
+    using assms by (auto simp: fA_def)
+  have fB: \<open>has_sum fB (A \<union> B) b\<close>
+    apply (subst has_sum_cong_neutral[where T=B and g=f])
+    using assms by (auto simp: fB_def)
+  have fAB: \<open>f x = fA x + fB x\<close> for x
+    unfolding fA_def fB_def by simp
+  show ?thesis
+    unfolding fAB
+    using fA fB by (rule has_sum_add)
+qed
+
+lemma summable_on_Un_disjoint:
+  fixes f :: "'a \<Rightarrow> 'b::topological_comm_monoid_add"
+  assumes "f summable_on A"
+  assumes "f summable_on B"
+  assumes disj: "A \<inter> B = {}"
+  shows \<open>f summable_on (A \<union> B)\<close>
+  by (meson assms(1) assms(2) disj summable_on_def has_sum_Un_disjoint)
+
+lemma infsum_Un_disjoint:
+  fixes f :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add, t2_space}"
+  assumes "f summable_on A"
+  assumes "f summable_on B"
+  assumes disj: "A \<inter> B = {}"
+  shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
+  by (smt (verit, ccfv_threshold) assms(1) assms(2) disj finite_subsets_at_top_neq_bot summable_on_def has_sum_Un_disjoint has_sum_def has_sum_infsum tendsto_Lim)
+
+
+text \<open>The following lemma indeed needs a complete space (as formalized by the premise \<^term>\<open>complete UNIV\<close>).
+  The following two counterexamples show this:
+  \begin{itemize}
+  \item Consider the real vector space $V$ of sequences with finite support, and with the $\ell_2$-norm (sum of squares).
+      Let $e_i$ denote the sequence with a $1$ at position $i$.
+      Let $f : \mathbb Z \to V$ be defined as $f(n) := e_{\lvert n\rvert} / n$ (with $f(0) := 0$).
+      We have that $\sum_{n\in\mathbb Z} f(n) = 0$ (it even converges absolutely). 
+      But $\sum_{n\in\mathbb N} f(n)$ does not exist (it would converge against a sequence with infinite support).
+  
+  \item Let $f$ be a positive rational valued function such that $\sum_{x\in B} f(x)$ is $\sqrt 2$ and $\sum_{x\in A} f(x)$ is 1 (over the reals, with $A\subseteq B$).
+      Then $\sum_{x\in B} f(x)$ does not exist over the rationals. But $\sum_{x\in A} f(x)$ exists.
+  \end{itemize}
+
+  The lemma also requires uniform continuity of the addition. And example of a topological group with continuous 
+  but not uniformly continuous addition would be the positive reals with the usual multiplication as the addition.
+  We do not know whether the lemma would also hold for such topological groups.\<close>
+
+lemma summable_on_subset:
+  fixes A B and f :: \<open>'a \<Rightarrow> 'b::{ab_group_add, uniform_space}\<close>
+  assumes \<open>complete (UNIV :: 'b set)\<close>
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b,y). x+y)\<close>
+  assumes \<open>f summable_on A\<close>
+  assumes \<open>B \<subseteq> A\<close>
+  shows \<open>f summable_on B\<close>
+proof -
+  from \<open>f summable_on A\<close>
+  obtain S where \<open>(sum f \<longlongrightarrow> S) (finite_subsets_at_top A)\<close> (is \<open>(sum f \<longlongrightarrow> S) ?filter_A\<close>)
+    using summable_on_def has_sum_def by blast
+  then have cauchy_fA: \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))\<close> (is \<open>cauchy_filter ?filter_fA\<close>)
+    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
+
+  let ?filter_fB = \<open>filtermap (sum f) (finite_subsets_at_top B)\<close>
+
+  have \<open>cauchy_filter (filtermap (sum f) (finite_subsets_at_top B))\<close>
+  proof (unfold cauchy_filter_def, rule filter_leI)
+    fix E :: \<open>('b\<times>'b) \<Rightarrow> bool\<close> assume \<open>eventually E uniformity\<close>
+    then obtain E' where \<open>eventually E' uniformity\<close> and E'E'E: \<open>E' (x, y) \<longrightarrow> E' (y, z) \<longrightarrow> E (x, z)\<close> for x y z
+      using uniformity_trans by blast
+    from plus_cont[simplified uniformly_continuous_on_uniformity filterlim_def le_filter_def, rule_format, 
+                   OF \<open>eventually E' uniformity\<close>]
+    obtain D where \<open>eventually D uniformity\<close> and DE: \<open>D (x, y) \<Longrightarrow> E' (x+c, y+c)\<close> for x y c
+      apply atomize_elim
+      by (auto simp: case_prod_beta eventually_filtermap uniformity_prod_def 
+        eventually_prod_same uniformity_refl)
+    with cauchy_fA have \<open>eventually D (?filter_fA \<times>\<^sub>F ?filter_fA)\<close>
+      unfolding cauchy_filter_def le_filter_def by simp
+    then obtain P1 P2 where ev_P1: \<open>eventually (\<lambda>F. P1 (sum f F)) ?filter_A\<close> and ev_P2: \<open>eventually (\<lambda>F. P2 (sum f F)) ?filter_A\<close>
+      and P1P2E: \<open>P1 x \<Longrightarrow> P2 y \<Longrightarrow> D (x, y)\<close> for x y
+      unfolding eventually_prod_filter eventually_filtermap
+      by auto
+    from ev_P1 obtain F1 where \<open>finite F1\<close> and \<open>F1 \<subseteq> A\<close> and \<open>\<forall>F. F\<supseteq>F1 \<and> finite F \<and> F\<subseteq>A \<longrightarrow> P1 (sum f F)\<close>
+      by (metis eventually_finite_subsets_at_top)
+    from ev_P2 obtain F2 where \<open>finite F2\<close> and \<open>F2 \<subseteq> A\<close> and \<open>\<forall>F. F\<supseteq>F2 \<and> finite F \<and> F\<subseteq>A \<longrightarrow> P2 (sum f F)\<close>
+      by (metis eventually_finite_subsets_at_top)
+    define F0 F0A F0B where \<open>F0 \<equiv> F1 \<union> F2\<close> and \<open>F0A \<equiv> F0 - B\<close> and \<open>F0B \<equiv> F0 \<inter> B\<close>
+    have [simp]: \<open>finite F0\<close>  \<open>F0 \<subseteq> A\<close>
+       apply (simp add: F0_def \<open>finite F1\<close> \<open>finite F2\<close>)
+      by (simp add: F0_def \<open>F1 \<subseteq> A\<close> \<open>F2 \<subseteq> A\<close>)
+    have [simp]: \<open>finite F0A\<close>
+      by (simp add: F0A_def)
+    have \<open>\<forall>F1 F2. F1\<supseteq>F0 \<and> F2\<supseteq>F0 \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>A \<and> F2\<subseteq>A \<longrightarrow> D (sum f F1, sum f F2)\<close>
+      by (simp add: F0_def P1P2E \<open>\<forall>F. F1 \<subseteq> F \<and> finite F \<and> F \<subseteq> A \<longrightarrow> P1 (sum f F)\<close> \<open>\<forall>F. F2 \<subseteq> F \<and> finite F \<and> F \<subseteq> A \<longrightarrow> P2 (sum f F)\<close>)
+    then have \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow> 
+              D (sum f (F1 \<union> F0A), sum f (F2 \<union> F0A))\<close>
+      by (smt (verit) Diff_Diff_Int Diff_subset_conv F0A_def F0B_def \<open>F0 \<subseteq> A\<close> \<open>finite F0A\<close> assms(4) finite_UnI sup.absorb_iff1 sup.mono sup_commute)
+    then have \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow> 
+              D (sum f F1 + sum f F0A, sum f F2 + sum f F0A)\<close>
+      by (metis Diff_disjoint F0A_def \<open>finite F0A\<close> inf.absorb_iff1 inf_assoc inf_bot_right sum.union_disjoint)
+    then have *: \<open>\<forall>F1 F2. F1\<supseteq>F0B \<and> F2\<supseteq>F0B \<and> finite F1 \<and> finite F2 \<and> F1\<subseteq>B \<and> F2\<subseteq>B \<longrightarrow> 
+              E' (sum f F1, sum f F2)\<close>
+      using DE[where c=\<open>- sum f F0A\<close>]
+      apply auto by (metis add.commute add_diff_cancel_left')
+    show \<open>eventually E (?filter_fB \<times>\<^sub>F ?filter_fB)\<close>
+      apply (subst eventually_prod_filter)
+      apply (rule exI[of _ \<open>\<lambda>x. E' (x, sum f F0B)\<close>])
+      apply (rule exI[of _ \<open>\<lambda>x. E' (sum f F0B, x)\<close>])
+      apply (auto simp: eventually_filtermap)
+      using * apply (metis (no_types, lifting) F0B_def Int_lower2 \<open>finite F0\<close> eventually_finite_subsets_at_top finite_Int order_refl)
+      using * apply (metis (no_types, lifting) F0B_def Int_lower2 \<open>finite F0\<close> eventually_finite_subsets_at_top finite_Int order_refl)
+      using E'E'E by auto
+  qed
+
+  then obtain x where \<open>filtermap (sum f) (finite_subsets_at_top B) \<le> nhds x\<close>
+    apply atomize_elim
+    apply (rule complete_uniform[where S=UNIV, THEN iffD1, rule_format, simplified])
+    using assms by (auto simp add: filtermap_bot_iff)
+
+  then have \<open>(sum f \<longlongrightarrow> x) (finite_subsets_at_top B)\<close>
+    by (auto simp: filterlim_def)
+  then show ?thesis
+    by (auto simp: summable_on_def has_sum_def)
+qed
+
+text \<open>A special case of @{thm [source] summable_on_subset} for Banach spaces with less premises.\<close>
+
+lemma summable_on_subset_banach:
+  fixes A B and f :: \<open>'a \<Rightarrow> 'b::banach\<close>
+  assumes \<open>f summable_on A\<close>
+  assumes \<open>B \<subseteq> A\<close>
+  shows \<open>f summable_on B\<close>
+  apply (rule summable_on_subset)
+  using assms apply auto
+  by (metis Cauchy_convergent UNIV_I complete_def convergent_def)
+
+lemma has_sum_empty[simp]: \<open>has_sum f {} 0\<close>
+  by (meson ex_in_conv has_sum_0)
+
+lemma summable_on_empty[simp]: \<open>f summable_on {}\<close>
+  by auto
+
+lemma infsum_empty[simp]: \<open>infsum f {} = 0\<close>
+  by simp
+
+lemma sum_has_sum:
+  fixes f :: "'a \<Rightarrow> 'b::topological_comm_monoid_add"
+  assumes finite: \<open>finite A\<close>
+  assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> has_sum f (B a) (s a)\<close>
+  assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
+  shows \<open>has_sum f (\<Union>a\<in>A. B a) (sum s A)\<close>
+  using assms
+proof (insert finite conv disj, induction)
+  case empty
+  then show ?case 
+    by simp
+next
+  case (insert x A)
+  have \<open>has_sum f (B x) (s x)\<close>
+    by (simp add: insert.prems)
+  moreover have IH: \<open>has_sum f (\<Union>a\<in>A. B a) (sum s A)\<close>
+    using insert by simp
+  ultimately have \<open>has_sum f (B x \<union> (\<Union>a\<in>A. B a)) (s x + sum s A)\<close>
+    apply (rule has_sum_Un_disjoint)
+    using insert by auto
+  then show ?case
+    using insert.hyps by auto
+qed
+
+
+lemma summable_on_finite_union_disjoint:
+  fixes f :: "'a \<Rightarrow> 'b::topological_comm_monoid_add"
+  assumes finite: \<open>finite A\<close>
+  assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> f summable_on (B a)\<close>
+  assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
+  shows \<open>f summable_on (\<Union>a\<in>A. B a)\<close>
+  using finite conv disj apply induction by (auto intro!: summable_on_Un_disjoint)
+
+lemma sum_infsum:
+  fixes f :: "'a \<Rightarrow> 'b::{topological_comm_monoid_add, t2_space}"
+  assumes finite: \<open>finite A\<close>
+  assumes conv: \<open>\<And>a. a \<in> A \<Longrightarrow> f summable_on (B a)\<close>
+  assumes disj: \<open>\<And>a a'. a\<in>A \<Longrightarrow> a'\<in>A \<Longrightarrow> a\<noteq>a' \<Longrightarrow> B a \<inter> B a' = {}\<close>
+  shows \<open>sum (\<lambda>a. infsum f (B a)) A = infsum f (\<Union>a\<in>A. B a)\<close>
+  using sum_has_sum[of A f B \<open>\<lambda>a. infsum f (B a)\<close>]
+  using assms apply auto
+  by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)
+
+text \<open>The lemmas \<open>infsum_comm_additive_general\<close> and \<open>infsum_comm_additive\<close> (and variants) below both state that the infinite sum commutes with
+  a continuous additive function. \<open>infsum_comm_additive_general\<close> is stated more for more general type classes
+  at the expense of a somewhat less compact formulation of the premises.
+  E.g., by avoiding the constant \<^const>\<open>additive\<close> which introduces an additional sort constraint
+  (group instead of monoid). For example, extended reals (\<^typ>\<open>ereal\<close>, \<^typ>\<open>ennreal\<close>) are not covered
+  by \<open>infsum_comm_additive\<close>.\<close>
+
+
+lemma has_sum_comm_additive_general: 
+  fixes f :: \<open>'b :: {comm_monoid_add,topological_space} \<Rightarrow> 'c :: {comm_monoid_add,topological_space}\<close>
+  assumes f_sum: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f o g) F = f (sum g F)\<close>
+      \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
+  assumes cont: \<open>f \<midarrow>x\<rightarrow> f x\<close>
+    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
+  assumes infsum: \<open>has_sum g S x\<close>
+  shows \<open>has_sum (f o g) S (f x)\<close> 
+proof -
+  have \<open>(sum g \<longlongrightarrow> x) (finite_subsets_at_top S)\<close>
+    using infsum has_sum_def by blast
+  then have \<open>((f o sum g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
+    apply (rule tendsto_compose_at)
+    using assms by auto
+  then have \<open>(sum (f o g) \<longlongrightarrow> f x) (finite_subsets_at_top S)\<close>
+    apply (rule tendsto_cong[THEN iffD1, rotated])
+    using f_sum by fastforce
+  then show \<open>has_sum (f o g) S (f x)\<close>
+    using has_sum_def by blast 
+qed
+
+lemma summable_on_comm_additive_general:
+  fixes f :: \<open>'b :: {comm_monoid_add,topological_space} \<Rightarrow> 'c :: {comm_monoid_add,topological_space}\<close>
+  assumes \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f o g) F = f (sum g F)\<close>
+    \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
+  assumes \<open>\<And>x. has_sum g S x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x\<close>
+    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
+  assumes \<open>g summable_on S\<close>
+  shows \<open>(f o g) summable_on S\<close>
+  by (meson assms summable_on_def has_sum_comm_additive_general has_sum_def infsum_tendsto)
+
+lemma infsum_comm_additive_general:
+  fixes f :: \<open>'b :: {comm_monoid_add,t2_space} \<Rightarrow> 'c :: {comm_monoid_add,t2_space}\<close>
+  assumes f_sum: \<open>\<And>F. finite F \<Longrightarrow> F \<subseteq> S \<Longrightarrow> sum (f o g) F = f (sum g F)\<close>
+      \<comment> \<open>Not using \<^const>\<open>additive\<close> because it would add sort constraint \<^class>\<open>ab_group_add\<close>\<close>
+  assumes \<open>isCont f (infsum g S)\<close>
+  assumes \<open>g summable_on S\<close>
+  shows \<open>infsum (f o g) S = f (infsum g S)\<close>
+  by (smt (verit) assms(2) assms(3) continuous_within f_sum finite_subsets_at_top_neq_bot summable_on_comm_additive_general has_sum_comm_additive_general has_sum_def has_sum_infsum tendsto_Lim)
+
+lemma has_sum_comm_additive: 
+  fixes f :: \<open>'b :: {ab_group_add,topological_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
+  assumes \<open>additive f\<close>
+  assumes \<open>f \<midarrow>x\<rightarrow> f x\<close>
+    \<comment> \<open>For \<^class>\<open>t2_space\<close>, this is equivalent to \<open>isCont f x\<close> by @{thm [source] isCont_def}.\<close>
+  assumes infsum: \<open>has_sum g S x\<close>
+  shows \<open>has_sum (f o g) S (f x)\<close>
+  by (smt (verit, best) additive.sum assms(1) assms(2) comp_eq_dest_lhs continuous_within finite_subsets_at_top_neq_bot infsum summable_on_def has_sum_comm_additive_general has_sum_def has_sum_infsum sum.cong tendsto_Lim) 
+
+lemma summable_on_comm_additive:
+  fixes f :: \<open>'b :: {ab_group_add,t2_space} \<Rightarrow> 'c :: {ab_group_add,topological_space}\<close>
+  assumes \<open>additive f\<close>
+  assumes \<open>isCont f (infsum g S)\<close>
+  assumes \<open>g summable_on S\<close>
+  shows \<open>(f o g) summable_on S\<close>
+  by (meson assms(1) assms(2) assms(3) summable_on_def has_sum_comm_additive has_sum_infsum isContD)
+
+lemma infsum_comm_additive:
+  fixes f :: \<open>'b :: {ab_group_add,t2_space} \<Rightarrow> 'c :: {ab_group_add,t2_space}\<close>
+  assumes \<open>additive f\<close>
+  assumes \<open>isCont f (infsum g S)\<close>
+  assumes \<open>g summable_on S\<close>
+  shows \<open>infsum (f o g) S = f (infsum g S)\<close>
+  by (rule infsum_comm_additive_general; auto simp: assms additive.sum)
+
+
+lemma pos_has_sum:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
+  shows \<open>has_sum f A (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+proof -
+  have \<open>(sum f \<longlongrightarrow> (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)) (finite_subsets_at_top A)\<close>
+  proof (rule order_tendstoI)
+    fix a assume \<open>a < (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+    then obtain F where \<open>a < sum f F\<close> and \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
+      by (metis (mono_tags, lifting) Collect_cong Collect_empty_eq assms(2) empty_subsetI finite.emptyI less_cSUP_iff mem_Collect_eq)
+    show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. a < sum f x\<close>
+      unfolding eventually_finite_subsets_at_top
+      apply (rule exI[of _ F])
+      using \<open>a < sum f F\<close> and \<open>finite F\<close> and \<open>F \<subseteq> A\<close>
+      apply auto
+      by (smt (verit, best) Diff_iff assms(1) less_le_trans subset_iff sum_mono2)
+  next
+    fix a assume \<open>(SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F) < a\<close>
+    then have \<open>sum f F < a\<close> if \<open>F\<subseteq>A\<close> and \<open>finite F\<close> for F
+      by (smt (verit, best) Collect_cong antisym_conv assms(2) cSUP_upper dual_order.trans le_less_linear less_le mem_Collect_eq that(1) that(2))
+    then show \<open>\<forall>\<^sub>F x in finite_subsets_at_top A. sum f x < a\<close>
+      by (rule eventually_finite_subsets_at_top_weakI)
+  qed
+  then show ?thesis
+    using has_sum_def by blast
+qed
+
+lemma pos_summable_on:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
+  shows \<open>f summable_on A\<close>
+  using assms(1) assms(2) summable_on_def pos_has_sum by blast
+
+
+lemma pos_infsum:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  assumes \<open>bdd_above (sum f ` {F. F\<subseteq>A \<and> finite F})\<close>
+  shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+  using assms by (auto intro!: infsumI pos_has_sum)
+
+lemma pos_has_sum_complete:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  shows \<open>has_sum f A (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+  using assms pos_has_sum by blast
+
+lemma pos_summable_on_complete:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  shows \<open>f summable_on A\<close>
+  using assms pos_summable_on by blast
+
+lemma pos_infsum_complete:
+  fixes f :: \<open>'a \<Rightarrow> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}\<close>
+  assumes \<open>\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0\<close>
+  shows \<open>infsum f A = (SUP F\<in>{F. finite F \<and> F\<subseteq>A}. sum f F)\<close>
+  using assms pos_infsum by blast
+
+lemma has_sum_nonneg:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
+  assumes "has_sum f M a"
+    and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+  shows "a \<ge> 0"
+  by (metis (no_types, lifting) DiffD1 assms(1) assms(2) empty_iff has_sum_0 has_sum_mono_neutral order_refl)
+
+lemma infsum_nonneg:
+  fixes f :: "'a \<Rightarrow> 'b::{ordered_comm_monoid_add,linorder_topology}"
+  assumes "f summable_on M"
+    and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+  shows "infsum f M \<ge> 0" (is "?lhs \<ge> _")
+  by (metis assms infsum_0_simp summable_on_0_simp infsum_mono)
+
+lemma has_sum_reindex:
+  assumes \<open>inj_on h A\<close>
+  shows \<open>has_sum g (h ` A) x \<longleftrightarrow> has_sum (g \<circ> h) A x\<close>
+proof -
+  have \<open>has_sum g (h ` A) x \<longleftrightarrow> (sum g \<longlongrightarrow> x) (finite_subsets_at_top (h ` A))\<close>
+    by (simp add: has_sum_def)
+  also have \<open>\<dots> \<longleftrightarrow> ((\<lambda>F. sum g (h ` F)) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
+    apply (subst filtermap_image_finite_subsets_at_top[symmetric])
+    using assms by (auto simp: filterlim_def filtermap_filtermap)
+  also have \<open>\<dots> \<longleftrightarrow> (sum (g \<circ> h) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
+    apply (rule tendsto_cong)
+    apply (rule eventually_finite_subsets_at_top_weakI)
+    apply (rule sum.reindex)
+    using assms subset_inj_on by blast
+  also have \<open>\<dots> \<longleftrightarrow> has_sum (g \<circ> h) A x\<close>
+    by (simp add: has_sum_def)
+  finally show ?thesis
+    by -
+qed
+
+
+lemma summable_on_reindex:
+  assumes \<open>inj_on h A\<close>
+  shows \<open>g summable_on (h ` A) \<longleftrightarrow> (g \<circ> h) summable_on A\<close>
+  by (simp add: assms summable_on_def has_sum_reindex)
+
+lemma infsum_reindex:
+  assumes \<open>inj_on h A\<close>
+  shows \<open>infsum g (h ` A) = infsum (g \<circ> h) A\<close>
+  by (metis (no_types, opaque_lifting) assms finite_subsets_at_top_neq_bot infsum_def summable_on_reindex has_sum_def has_sum_infsum has_sum_reindex tendsto_Lim)
+
+
+lemma sum_uniformity:
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'b::{uniform_space,comm_monoid_add},y). x+y)\<close>
+  assumes \<open>eventually E uniformity\<close>
+  obtains D where \<open>eventually D uniformity\<close> 
+    and \<open>\<And>M::'a set. \<And>f f' :: 'a \<Rightarrow> 'b. card M \<le> n \<and> (\<forall>m\<in>M. D (f m, f' m)) \<Longrightarrow> E (sum f M, sum f' M)\<close>
+proof (atomize_elim, insert \<open>eventually E uniformity\<close>, induction n arbitrary: E rule:nat_induct)
+  case 0
+  then show ?case
+    by (metis card_eq_0_iff equals0D le_zero_eq sum.infinite sum.not_neutral_contains_not_neutral uniformity_refl)
+next
+  case (Suc n)
+  from plus_cont[unfolded uniformly_continuous_on_uniformity filterlim_def le_filter_def, rule_format, OF Suc.prems]
+  obtain D1 D2 where \<open>eventually D1 uniformity\<close> and \<open>eventually D2 uniformity\<close> 
+    and D1D2E: \<open>D1 (x, y) \<Longrightarrow> D2 (x', y') \<Longrightarrow> E (x + x', y + y')\<close> for x y x' y'
+    apply atomize_elim
+    by (auto simp: eventually_prod_filter case_prod_beta uniformity_prod_def eventually_filtermap)
+
+  from Suc.IH[OF \<open>eventually D2 uniformity\<close>]
+  obtain D3 where \<open>eventually D3 uniformity\<close> and D3: \<open>card M \<le> n \<Longrightarrow> (\<forall>m\<in>M. D3 (f m, f' m)) \<Longrightarrow> D2 (sum f M, sum f' M)\<close> 
+    for M :: \<open>'a set\<close> and f f'
+    by metis
+
+  define D where \<open>D x \<equiv> D1 x \<and> D3 x\<close> for x
+  have \<open>eventually D uniformity\<close>
+    using D_def \<open>eventually D1 uniformity\<close> \<open>eventually D3 uniformity\<close> eventually_elim2 by blast
+
+  have \<open>E (sum f M, sum f' M)\<close> 
+    if \<open>card M \<le> Suc n\<close> and DM: \<open>\<forall>m\<in>M. D (f m, f' m)\<close>
+    for M :: \<open>'a set\<close> and f f'
+  proof (cases \<open>card M = 0\<close>)
+    case True
+    then show ?thesis
+      by (metis Suc.prems card_eq_0_iff sum.empty sum.infinite uniformity_refl) 
+  next
+    case False
+    with \<open>card M \<le> Suc n\<close> obtain N x where \<open>card N \<le> n\<close> and \<open>x \<notin> N\<close> and \<open>M = insert x N\<close>
+      by (metis card_Suc_eq less_Suc_eq_0_disj less_Suc_eq_le)
+
+    from DM have \<open>\<And>m. m\<in>N \<Longrightarrow> D (f m, f' m)\<close>
+      using \<open>M = insert x N\<close> by blast
+    with D3[OF \<open>card N \<le> n\<close>]
+    have D2_N: \<open>D2 (sum f N, sum f' N)\<close>
+      using D_def by blast
+
+    from DM 
+    have \<open>D (f x, f' x)\<close>
+      using \<open>M = insert x N\<close> by blast
+    then have \<open>D1 (f x, f' x)\<close>
+      by (simp add: D_def)
+
+    with D2_N
+    have \<open>E (f x + sum f N, f' x + sum f' N)\<close>
+      using D1D2E by presburger
+
+    then show \<open>E (sum f M, sum f' M)\<close>
+      by (metis False \<open>M = insert x N\<close> \<open>x \<notin> N\<close> card.infinite finite_insert sum.insert)
+  qed
+  with \<open>eventually D uniformity\<close>
+  show ?case 
+    by auto
+qed
+
+lemma has_sum_Sigma:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::{comm_monoid_add,uniform_space}\<close>
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+  assumes summableAB: "has_sum f (Sigma A B) a"
+  assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (\<lambda>y. f (x, y)) (B x) (b x)\<close>
+  shows "has_sum b A a"
+proof -
+  define F FB FA where \<open>F = finite_subsets_at_top (Sigma A B)\<close> and \<open>FB x = finite_subsets_at_top (B x)\<close>
+    and \<open>FA = finite_subsets_at_top A\<close> for x
+
+  from summableB
+  have sum_b: \<open>(sum (\<lambda>y. f (x, y)) \<longlongrightarrow> b x) (FB x)\<close> if \<open>x \<in> A\<close> for x
+    using FB_def[abs_def] has_sum_def that by auto
+  from summableAB
+  have sum_S: \<open>(sum f \<longlongrightarrow> a) F\<close>
+    using F_def has_sum_def by blast
+
+  have finite_proj: \<open>finite {b| b. (a,b) \<in> H}\<close> if \<open>finite H\<close> for H :: \<open>('a\<times>'b) set\<close> and a
+    apply (subst asm_rl[of \<open>{b| b. (a,b) \<in> H} = snd ` {ab. ab \<in> H \<and> fst ab = a}\<close>])
+    by (auto simp: image_iff that)
+
+  have \<open>(sum b \<longlongrightarrow> a) FA\<close>
+  proof (rule tendsto_iff_uniformity[THEN iffD2, rule_format])
+    fix E :: \<open>('c \<times> 'c) \<Rightarrow> bool\<close>
+    assume \<open>eventually E uniformity\<close>
+    then obtain D where D_uni: \<open>eventually D uniformity\<close> and DDE': \<open>\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)\<close>
+      by (metis (no_types, lifting) \<open>eventually E uniformity\<close> uniformity_transE)
+    from sum_S obtain G where \<open>finite G\<close> and \<open>G \<subseteq> Sigma A B\<close>
+      and G_sum: \<open>G \<subseteq> H \<Longrightarrow> H \<subseteq> Sigma A B \<Longrightarrow> finite H \<Longrightarrow> D (sum f H, a)\<close> for H
+      unfolding tendsto_iff_uniformity
+      by (metis (mono_tags, lifting) D_uni F_def eventually_finite_subsets_at_top)
+    have \<open>finite (fst ` G)\<close> and \<open>fst ` G \<subseteq> A\<close>
+      using \<open>finite G\<close> \<open>G \<subseteq> Sigma A B\<close> by auto
+    thm uniformity_prod_def
+    define Ga where \<open>Ga a = {b. (a,b) \<in> G}\<close> for a
+    have Ga_fin: \<open>finite (Ga a)\<close> and Ga_B: \<open>Ga a \<subseteq> B a\<close> for a
+      using \<open>finite G\<close> \<open>G \<subseteq> Sigma A B\<close> finite_proj by (auto simp: Ga_def finite_proj)
+
+    have \<open>E (sum b M, a)\<close> if \<open>M \<supseteq> fst ` G\<close> and \<open>finite M\<close> and \<open>M \<subseteq> A\<close> for M
+    proof -
+      define FMB where \<open>FMB = finite_subsets_at_top (Sigma M B)\<close>
+      have \<open>eventually (\<lambda>H. D (\<Sum>a\<in>M. b a, \<Sum>(a,b)\<in>H. f (a,b))) FMB\<close>
+      proof -
+        obtain D' where D'_uni: \<open>eventually D' uniformity\<close> 
+          and \<open>card M' \<le> card M \<and> (\<forall>m\<in>M'. D' (g m, g' m)) \<Longrightarrow> D (sum g M', sum g' M')\<close>
+            for M' :: \<open>'a set\<close> and g g'
+          apply (rule sum_uniformity[OF plus_cont \<open>eventually D uniformity\<close>, where n=\<open>card M\<close>])
+          by auto
+        then have D'_sum_D: \<open>(\<forall>m\<in>M. D' (g m, g' m)) \<Longrightarrow> D (sum g M, sum g' M)\<close> for g g'
+          by auto
+
+        obtain Ha where \<open>Ha a \<supseteq> Ga a\<close> and Ha_fin: \<open>finite (Ha a)\<close> and Ha_B: \<open>Ha a \<subseteq> B a\<close>
+          and D'_sum_Ha: \<open>Ha a \<subseteq> L \<Longrightarrow> L \<subseteq> B a \<Longrightarrow> finite L \<Longrightarrow> D' (b a, sum (\<lambda>b. f (a,b)) L)\<close> if \<open>a \<in> A\<close> for a L
+        proof -
+          from sum_b[unfolded tendsto_iff_uniformity, rule_format, OF _ D'_uni[THEN uniformity_sym]]
+          obtain Ha0 where \<open>finite (Ha0 a)\<close> and \<open>Ha0 a \<subseteq> B a\<close>
+            and \<open>Ha0 a \<subseteq> L \<Longrightarrow> L \<subseteq> B a \<Longrightarrow> finite L \<Longrightarrow> D' (b a, sum (\<lambda>b. f (a,b)) L)\<close> if \<open>a \<in> A\<close> for a L
+            unfolding FB_def eventually_finite_subsets_at_top apply auto by metis
+          moreover define Ha where \<open>Ha a = Ha0 a \<union> Ga a\<close> for a
+          ultimately show ?thesis
+            using that[where Ha=Ha]
+            using Ga_fin Ga_B by auto
+        qed
+
+        have \<open>D (\<Sum>a\<in>M. b a, \<Sum>(a,b)\<in>H. f (a,b))\<close> if \<open>finite H\<close> and \<open>H \<subseteq> Sigma M B\<close> and \<open>H \<supseteq> Sigma M Ha\<close> for H
+        proof -
+          define Ha' where \<open>Ha' a = {b| b. (a,b) \<in> H}\<close> for a
+          have [simp]: \<open>finite (Ha' a)\<close> and [simp]: \<open>Ha' a \<supseteq> Ha a\<close> and [simp]: \<open>Ha' a \<subseteq> B a\<close> if \<open>a \<in> M\<close> for a
+            unfolding Ha'_def using \<open>finite H\<close> \<open>H \<subseteq> Sigma M B\<close> \<open>Sigma M Ha \<subseteq> H\<close> that finite_proj by auto
+          have \<open>Sigma M Ha' = H\<close>
+            using that by (auto simp: Ha'_def)
+          then have *: \<open>(\<Sum>(a,b)\<in>H. f (a,b)) = (\<Sum>a\<in>M. \<Sum>b\<in>Ha' a. f (a,b))\<close>
+            apply (subst sum.Sigma)
+            using \<open>finite M\<close> by auto
+          have \<open>D' (b a, sum (\<lambda>b. f (a,b)) (Ha' a))\<close> if \<open>a \<in> M\<close> for a
+            apply (rule D'_sum_Ha)
+            using that \<open>M \<subseteq> A\<close> by auto
+          then have \<open>D (\<Sum>a\<in>M. b a, \<Sum>a\<in>M. sum (\<lambda>b. f (a,b)) (Ha' a))\<close>
+            by (rule_tac D'_sum_D, auto)
+          with * show ?thesis
+            by auto
+        qed
+        moreover have \<open>Sigma M Ha \<subseteq> Sigma M B\<close>
+          using Ha_B \<open>M \<subseteq> A\<close> by auto
+        ultimately show ?thesis
+          apply (simp add: FMB_def eventually_finite_subsets_at_top)
+          by (metis Ha_fin finite_SigmaI subsetD that(2) that(3))
+      qed
+      moreover have \<open>eventually (\<lambda>H. D (\<Sum>(a,b)\<in>H. f (a,b), a)) FMB\<close>
+        unfolding FMB_def eventually_finite_subsets_at_top
+        apply (rule exI[of _ G])
+        using \<open>G \<subseteq> Sigma A B\<close> \<open>finite G\<close> that G_sum apply auto
+        by (smt (z3) Sigma_Un_distrib1 dual_order.trans subset_Un_eq)
+      ultimately have \<open>\<forall>\<^sub>F x in FMB. E (sum b M, a)\<close>
+        by (smt (verit, best) DDE' eventually_elim2)
+      then show \<open>E (sum b M, a)\<close>
+        apply (rule eventually_const[THEN iffD1, rotated])
+        using FMB_def by force
+    qed
+    then show \<open>\<forall>\<^sub>F x in FA. E (sum b x, a)\<close>
+      using \<open>finite (fst ` G)\<close> and \<open>fst ` G \<subseteq> A\<close>
+      by (auto intro!: exI[of _ \<open>fst ` G\<close>] simp add: FA_def eventually_finite_subsets_at_top)
+  qed
+  then show ?thesis
+    by (simp add: FA_def has_sum_def)
+qed
+
+lemma summable_on_Sigma:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+  assumes summableAB: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+  assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (f x) summable_on (B x)\<close>
+  shows \<open>(\<lambda>x. infsum (f x) (B x)) summable_on A\<close>
+proof -
+  from summableAB obtain a where a: \<open>has_sum (\<lambda>(x,y). f x y) (Sigma A B) a\<close>
+    using has_sum_infsum by blast
+  from summableB have b: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (f x) (B x) (infsum (f x) (B x))\<close>
+    by (auto intro!: has_sum_infsum)
+  show ?thesis
+    using plus_cont a b 
+    by (auto intro: has_sum_Sigma[where f=\<open>\<lambda>(x,y). f x y\<close>, simplified] simp: summable_on_def)
+qed
+
+lemma infsum_Sigma:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+  assumes summableAB: "f summable_on (Sigma A B)"
+  assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (\<lambda>y. f (x, y)) summable_on (B x)\<close>
+  shows "infsum f (Sigma A B) = infsum (\<lambda>x. infsum (\<lambda>y. f (x, y)) (B x)) A"
+proof -
+  from summableAB have a: \<open>has_sum f (Sigma A B) (infsum f (Sigma A B))\<close>
+    using has_sum_infsum by blast
+  from summableB have b: \<open>\<And>x. x\<in>A \<Longrightarrow> has_sum (\<lambda>y. f (x, y)) (B x) (infsum (\<lambda>y. f (x, y)) (B x))\<close>
+    by (auto intro!: has_sum_infsum)
+  show ?thesis
+    using plus_cont a b by (auto intro: infsumI[symmetric] has_sum_Sigma simp: summable_on_def)
+qed
+
+lemma infsum_Sigma':
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add, t2_space, uniform_space}\<close>
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+  assumes summableAB: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+  assumes summableB: \<open>\<And>x. x\<in>A \<Longrightarrow> (f x) summable_on (B x)\<close>
+  shows \<open>infsum (\<lambda>x. infsum (f x) (B x)) A = infsum (\<lambda>(x,y). f x y) (Sigma A B)\<close>
+  using infsum_Sigma[of \<open>\<lambda>(x,y). f x y\<close> A B]
+  using assms by auto
+
+text \<open>A special case of @{thm [source] infsum_Sigma} etc. for Banach spaces. It has less premises.\<close>
+lemma
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<Rightarrow> 'b \<Rightarrow> 'c::banach\<close>
+  assumes [simp]: "(\<lambda>(x,y). f x y) summable_on (Sigma A B)"
+  shows infsum_Sigma'_banach: \<open>infsum (\<lambda>x. infsum (f x) (B x)) A = infsum (\<lambda>(x,y). f x y) (Sigma A B)\<close> (is ?thesis1)
+    and summable_on_Sigma_banach: \<open>(\<lambda>x. infsum (f x) (B x)) summable_on A\<close> (is ?thesis2)
+proof -
+  have [simp]: \<open>(f x) summable_on (B x)\<close> if \<open>x \<in> A\<close> for x
+  proof -
+    from assms
+    have \<open>(\<lambda>(x,y). f x y) summable_on (Pair x ` B x)\<close>
+      by (meson image_subset_iff summable_on_subset_banach mem_Sigma_iff that)
+    then have \<open>((\<lambda>(x,y). f x y) o Pair x) summable_on (B x)\<close>
+      apply (rule_tac summable_on_reindex[THEN iffD1])
+      by (simp add: inj_on_def)
+    then show ?thesis
+      by (auto simp: o_def)
+  qed
+  show ?thesis1
+    apply (rule infsum_Sigma')
+    by auto
+  show ?thesis2
+    apply (rule summable_on_Sigma)
+    by auto
+qed
+
+lemma infsum_Sigma_banach:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+    and f :: \<open>'a \<times> 'b \<Rightarrow> 'c::banach\<close>
+  assumes [simp]: "f summable_on (Sigma A B)"
+  shows \<open>infsum (\<lambda>x. infsum (\<lambda>y. f (x,y)) (B x)) A = infsum f (Sigma A B)\<close>
+  by (smt (verit, best) SigmaE assms infsum_Sigma'_banach infsum_cong summable_on_cong old.prod.case)
+
+lemma infsum_swap:
+  fixes A :: "'a set" and B :: "'b set"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{comm_monoid_add,t2_space,uniform_space}"
+  assumes plus_cont: \<open>uniformly_continuous_on UNIV (\<lambda>(x::'c,y). x+y)\<close>
+  assumes \<open>(\<lambda>(x, y). f x y) summable_on (A \<times> B)\<close>
+  assumes \<open>\<And>a. a\<in>A \<Longrightarrow> (f a) summable_on B\<close>
+  assumes \<open>\<And>b. b\<in>B \<Longrightarrow> (\<lambda>a. f a b) summable_on A\<close>
+  shows \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+proof -
+  have [simp]: \<open>(\<lambda>(x, y). f y x) summable_on (B \<times> A)\<close>
+    apply (subst product_swap[symmetric])
+    apply (subst summable_on_reindex)
+    using assms by (auto simp: o_def)
+  have \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>(x,y). f x y) (A \<times> B)\<close>
+    apply (subst infsum_Sigma)
+    using assms by auto
+  also have \<open>\<dots> = infsum (\<lambda>(x,y). f y x) (B \<times> A)\<close>
+    apply (subst product_swap[symmetric])
+    apply (subst infsum_reindex)
+    using assms by (auto simp: o_def)
+  also have \<open>\<dots> = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+    apply (subst infsum_Sigma)
+    using assms by auto
+  finally show ?thesis
+    by -
+qed
+
+lemma infsum_swap_banach:
+  fixes A :: "'a set" and B :: "'b set"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::banach"
+  assumes \<open>(\<lambda>(x, y). f x y) summable_on (A \<times> B)\<close>
+  shows "infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B"
+proof -
+  have [simp]: \<open>(\<lambda>(x, y). f y x) summable_on (B \<times> A)\<close>
+    apply (subst product_swap[symmetric])
+    apply (subst summable_on_reindex)
+    using assms by (auto simp: o_def)
+  have \<open>infsum (\<lambda>x. infsum (\<lambda>y. f x y) B) A = infsum (\<lambda>(x,y). f x y) (A \<times> B)\<close>
+    apply (subst infsum_Sigma'_banach)
+    using assms by auto
+  also have \<open>\<dots> = infsum (\<lambda>(x,y). f y x) (B \<times> A)\<close>
+    apply (subst product_swap[symmetric])
+    apply (subst infsum_reindex)
+    using assms by (auto simp: o_def)
+  also have \<open>\<dots> = infsum (\<lambda>y. infsum (\<lambda>x. f x y) A) B\<close>
+    apply (subst infsum_Sigma'_banach)
+    using assms by auto
+  finally show ?thesis
+    by -
+qed
+
+lemma infsum_0D:
+  fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
+  assumes "infsum f A \<le> 0"
+    and abs_sum: "f summable_on A"
+    and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+    and "x \<in> A"
+  shows "f x = 0"
+proof (rule ccontr)
+  assume \<open>f x \<noteq> 0\<close>
+  have ex: \<open>f summable_on (A-{x})\<close>
+    apply (rule summable_on_cofin_subset)
+    using assms by auto
+  then have pos: \<open>infsum f (A - {x}) \<ge> 0\<close>
+    apply (rule infsum_nonneg)
+    using nneg by auto
+
+  have [trans]: \<open>x \<ge> y \<Longrightarrow> y > z \<Longrightarrow> x > z\<close> for x y z :: 'b by auto
+
+  have \<open>infsum f A = infsum f (A-{x}) + infsum f {x}\<close>
+    apply (subst infsum_Un_disjoint[symmetric])
+    using assms ex apply auto by (metis insert_absorb) 
+  also have \<open>\<dots> \<ge> infsum f {x}\<close> (is \<open>_ \<ge> \<dots>\<close>)
+    using pos apply (rule add_increasing) by simp
+  also have \<open>\<dots> = f x\<close> (is \<open>_ = \<dots>\<close>)
+    apply (subst infsum_finite) by auto
+  also have \<open>\<dots> > 0\<close>
+    using \<open>f x \<noteq> 0\<close> assms(4) nneg by fastforce
+  finally show False
+    using assms by auto
+qed
+
+lemma has_sum_0D:
+  fixes f :: "'a \<Rightarrow> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
+  assumes "has_sum f A a" \<open>a \<le> 0\<close>
+    and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+    and "x \<in> A"
+  shows "f x = 0"
+  by (metis assms(1) assms(2) assms(4) infsumI infsum_0D summable_on_def nneg)
+
+lemma has_sum_cmult_left:
+  fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
+  assumes \<open>has_sum f A a\<close>
+  shows "has_sum (\<lambda>x. f x * c) A (a * c)"
+proof -
+  from assms have \<open>(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)\<close>
+    using has_sum_def by blast
+  then have \<open>((\<lambda>F. sum f F * c) \<longlongrightarrow> a * c) (finite_subsets_at_top A)\<close>
+    by (simp add: tendsto_mult_right)
+  then have \<open>(sum (\<lambda>x. f x * c) \<longlongrightarrow> a * c) (finite_subsets_at_top A)\<close>
+    apply (rule tendsto_cong[THEN iffD1, rotated])
+    apply (rule eventually_finite_subsets_at_top_weakI)
+    using sum_distrib_right by blast
+  then show ?thesis
+    using infsumI has_sum_def by blast
+qed
+
+lemma infsum_cmult_left:
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+  assumes \<open>c \<noteq> 0 \<Longrightarrow> f summable_on A\<close>
+  shows "infsum (\<lambda>x. f x * c) A = infsum f A * c"
+proof (cases \<open>c=0\<close>)
+  case True
+  then show ?thesis by auto
+next
+  case False
+  then have \<open>has_sum f A (infsum f A)\<close>
+    by (simp add: assms)
+  then show ?thesis
+    by (auto intro!: infsumI has_sum_cmult_left)
+qed
+
+lemma summable_on_cmult_left:
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+  assumes \<open>f summable_on A\<close>
+  shows "(\<lambda>x. f x * c) summable_on A"
+  using assms summable_on_def has_sum_cmult_left by blast
+
+lemma has_sum_cmult_right:
+  fixes f :: "'a \<Rightarrow> 'b :: {topological_semigroup_mult, semiring_0}"
+  assumes \<open>has_sum f A a\<close>
+  shows "has_sum (\<lambda>x. c * f x) A (c * a)"
+proof -
+  from assms have \<open>(sum f \<longlongrightarrow> a) (finite_subsets_at_top A)\<close>
+    using has_sum_def by blast
+  then have \<open>((\<lambda>F. c * sum f F) \<longlongrightarrow> c * a) (finite_subsets_at_top A)\<close>
+    by (simp add: tendsto_mult_left)
+  then have \<open>(sum (\<lambda>x. c * f x) \<longlongrightarrow> c * a) (finite_subsets_at_top A)\<close>
+    apply (rule tendsto_cong[THEN iffD1, rotated])
+    apply (rule eventually_finite_subsets_at_top_weakI)
+    using sum_distrib_left by blast
+  then show ?thesis
+    using infsumI has_sum_def by blast
+qed
+
+lemma infsum_cmult_right:
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+  assumes \<open>c \<noteq> 0 \<Longrightarrow> f summable_on A\<close>
+  shows \<open>infsum (\<lambda>x. c * f x) A = c * infsum f A\<close>
+proof (cases \<open>c=0\<close>)
+  case True
+  then show ?thesis by auto
+next
+  case False
+  then have \<open>has_sum f A (infsum f A)\<close>
+    by (simp add: assms)
+  then show ?thesis
+    by (auto intro!: infsumI has_sum_cmult_right)
+qed
+
+lemma summable_on_cmult_right:
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
+  assumes \<open>f summable_on A\<close>
+  shows "(\<lambda>x. c * f x) summable_on A"
+  using assms summable_on_def has_sum_cmult_right by blast
+
+lemma summable_on_cmult_left':
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+  assumes \<open>c \<noteq> 0\<close>
+  shows "(\<lambda>x. f x * c) summable_on A \<longleftrightarrow> f summable_on A"
+proof
+  assume \<open>f summable_on A\<close>
+  then show \<open>(\<lambda>x. f x * c) summable_on A\<close>
+    by (rule summable_on_cmult_left)
+next
+  assume \<open>(\<lambda>x. f x * c) summable_on A\<close>
+  then have \<open>(\<lambda>x. f x * c * inverse c) summable_on A\<close>
+    by (rule summable_on_cmult_left)
+  then show \<open>f summable_on A\<close>
+    by (metis (no_types, lifting) assms summable_on_cong mult.assoc mult.right_neutral right_inverse)
+qed
+
+lemma summable_on_cmult_right':
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+  assumes \<open>c \<noteq> 0\<close>
+  shows "(\<lambda>x. c * f x) summable_on A \<longleftrightarrow> f summable_on A"
+proof
+  assume \<open>f summable_on A\<close>
+  then show \<open>(\<lambda>x. c * f x) summable_on A\<close>
+    by (rule summable_on_cmult_right)
+next
+  assume \<open>(\<lambda>x. c * f x) summable_on A\<close>
+  then have \<open>(\<lambda>x. inverse c * (c * f x)) summable_on A\<close>
+    by (rule summable_on_cmult_right)
+  then show \<open>f summable_on A\<close>
+    by (metis (no_types, lifting) assms summable_on_cong left_inverse mult.assoc mult.left_neutral)
+qed
+
+lemma infsum_cmult_left':
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
+  shows "infsum (\<lambda>x. f x * c) A = infsum f A * c"
+proof (cases \<open>c \<noteq> 0 \<longrightarrow> f summable_on A\<close>)
+  case True
+  then show ?thesis
+    apply (rule_tac infsum_cmult_left) by auto
+next
+  case False
+  note asm = False
+  then show ?thesis
+  proof (cases \<open>c=0\<close>)
+    case True
+    then show ?thesis by auto
+  next
+    case False
+    with asm have nex: \<open>\<not> f summable_on A\<close>
+      by simp
+    moreover have nex': \<open>\<not> (\<lambda>x. f x * c) summable_on A\<close>
+      using asm False apply (subst summable_on_cmult_left') by auto
+    ultimately show ?thesis
+      unfolding infsum_def by simp
+  qed
+qed
+
+lemma infsum_cmult_right':
+  fixes f :: "'a \<Rightarrow> 'b :: {t2_space,topological_semigroup_mult,division_ring}"
+  shows "infsum (\<lambda>x. c * f x) A = c * infsum f A"
+proof (cases \<open>c \<noteq> 0 \<longrightarrow> f summable_on A\<close>)
+  case True
+  then show ?thesis
+    apply (rule_tac infsum_cmult_right) by auto
+next
+  case False
+  note asm = False
+  then show ?thesis
+  proof (cases \<open>c=0\<close>)
+    case True
+    then show ?thesis by auto
+  next
+    case False
+    with asm have nex: \<open>\<not> f summable_on A\<close>
+      by simp
+    moreover have nex': \<open>\<not> (\<lambda>x. c * f x) summable_on A\<close>
+      using asm False apply (subst summable_on_cmult_right') by auto
+    ultimately show ?thesis
+      unfolding infsum_def by simp
+  qed
+qed
+
+
+lemma has_sum_constant[simp]:
+  assumes \<open>finite F\<close>
+  shows \<open>has_sum (\<lambda>_. c) F (of_nat (card F) * c)\<close>
+  by (metis assms has_sum_finite sum_constant)
+
+lemma infsum_constant[simp]:
+  assumes \<open>finite F\<close>
+  shows \<open>infsum (\<lambda>_. c) F = of_nat (card F) * c\<close>
+  apply (subst infsum_finite[OF assms]) by simp
+
+lemma infsum_diverge_constant:
+  \<comment> \<open>This probably does not really need all of \<^class>\<open>archimedean_field\<close> but Isabelle/HOL
+       has no type class such as, e.g., "archimedean ring".\<close>
+  fixes c :: \<open>'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}\<close>
+  assumes \<open>infinite A\<close> and \<open>c \<noteq> 0\<close>
+  shows \<open>\<not> (\<lambda>_. c) summable_on A\<close>
+proof (rule notI)
+  assume \<open>(\<lambda>_. c) summable_on A\<close>
+  then have \<open>(\<lambda>_. inverse c * c) summable_on A\<close>
+    by (rule summable_on_cmult_right)
+  then have [simp]: \<open>(\<lambda>_. 1::'a) summable_on A\<close>
+    using assms by auto
+  have \<open>infsum (\<lambda>_. 1) A \<ge> d\<close> for d :: 'a
+  proof -
+    obtain n :: nat where \<open>of_nat n \<ge> d\<close>
+      by (meson real_arch_simple)
+    from assms
+    obtain F where \<open>F \<subseteq> A\<close> and \<open>finite F\<close> and \<open>card F = n\<close>
+      by (meson infinite_arbitrarily_large)
+    note \<open>d \<le> of_nat n\<close>
+    also have \<open>of_nat n = infsum (\<lambda>_. 1::'a) F\<close>
+      by (simp add: \<open>card F = n\<close> \<open>finite F\<close>)
+    also have \<open>\<dots> \<le> infsum (\<lambda>_. 1::'a) A\<close>
+      apply (rule infsum_mono_neutral)
+      using \<open>finite F\<close> \<open>F \<subseteq> A\<close> by auto
+    finally show ?thesis
+      by -
+  qed
+  then show False
+    by (meson linordered_field_no_ub not_less)
+qed
+
+lemma has_sum_constant_archimedean[simp]:
+  \<comment> \<open>This probably does not really need all of \<^class>\<open>archimedean_field\<close> but Isabelle/HOL
+       has no type class such as, e.g., "archimedean ring".\<close>
+  fixes c :: \<open>'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}\<close>
+  shows \<open>infsum (\<lambda>_. c) A = of_nat (card A) * c\<close>
+  apply (cases \<open>finite A\<close>)
+   apply simp
+  apply (cases \<open>c = 0\<close>)
+   apply simp
+  by (simp add: infsum_diverge_constant infsum_not_exists)
+
+lemma has_sum_uminus:
+  fixes f :: \<open>'a \<Rightarrow> 'b::topological_ab_group_add\<close>
+  shows \<open>has_sum (\<lambda>x. - f x) A a \<longleftrightarrow> has_sum f A (- a)\<close>
+  by (auto simp add: sum_negf[abs_def] tendsto_minus_cancel_left has_sum_def)
+
+lemma summable_on_uminus:
+  fixes f :: \<open>'a \<Rightarrow> 'b::topological_ab_group_add\<close>
+  shows\<open>(\<lambda>x. - f x) summable_on A \<longleftrightarrow> f summable_on A\<close>
+  by (metis summable_on_def has_sum_uminus verit_minus_simplify(4))
+
+lemma infsum_uminus:
+  fixes f :: \<open>'a \<Rightarrow> 'b::{topological_ab_group_add, t2_space}\<close>
+  shows \<open>infsum (\<lambda>x. - f x) A = - infsum f A\<close>
+  by (metis (full_types) add.inverse_inverse add.inverse_neutral infsumI infsum_def has_sum_infsum has_sum_uminus)
+
+subsection \<open>Extended reals and nats\<close>
+
+lemma summable_on_ennreal[simp]: \<open>(f::_ \<Rightarrow> ennreal) summable_on S\<close>
+  apply (rule pos_summable_on_complete) by simp
+
+lemma summable_on_enat[simp]: \<open>(f::_ \<Rightarrow> enat) summable_on S\<close>
+  apply (rule pos_summable_on_complete) by simp
+
+lemma has_sum_superconst_infinite_ennreal:
+  fixes f :: \<open>'a \<Rightarrow> ennreal\<close>
+  assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes b: \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "has_sum f S \<infinity>"
+proof -
+  have \<open>(sum f \<longlongrightarrow> \<infinity>) (finite_subsets_at_top S)\<close>
+  proof (rule order_tendstoI[rotated], simp)
+    fix y :: ennreal assume \<open>y < \<infinity>\<close>
+    then have \<open>y / b < \<infinity>\<close>
+      by (metis b ennreal_divide_eq_top_iff gr_implies_not_zero infinity_ennreal_def top.not_eq_extremum)
+    then obtain F where \<open>finite F\<close> and \<open>F \<subseteq> S\<close> and cardF: \<open>card F > y / b\<close>
+      using \<open>infinite S\<close>
+      by (metis ennreal_Ex_less_of_nat infinite_arbitrarily_large infinity_ennreal_def)
+    moreover have \<open>sum f Y > y\<close> if \<open>finite Y\<close> and \<open>F \<subseteq> Y\<close> and \<open>Y \<subseteq> S\<close> for Y
+    proof -
+      have \<open>y < b * card F\<close>
+        by (metis \<open>y < \<infinity>\<close> b cardF divide_less_ennreal ennreal_mult_eq_top_iff gr_implies_not_zero infinity_ennreal_def mult.commute top.not_eq_extremum)
+      also have \<open>\<dots> \<le> b * card Y\<close>
+        by (meson b card_mono less_imp_le mult_left_mono of_nat_le_iff that(1) that(2))
+      also have \<open>\<dots> = sum (\<lambda>_. b) Y\<close>
+        by (simp add: mult.commute)
+      also have \<open>\<dots> \<le> sum f Y\<close>
+        using geqb by (meson subset_eq sum_mono that(3))
+      finally show ?thesis
+        by -
+    qed
+    ultimately show \<open>\<forall>\<^sub>F x in finite_subsets_at_top S. y < sum f x\<close>
+      unfolding eventually_finite_subsets_at_top 
+      by auto
+  qed
+  then show ?thesis
+    by (simp add: has_sum_def)
+qed
+
+lemma infsum_superconst_infinite_ennreal:
+  fixes f :: \<open>'a \<Rightarrow> ennreal\<close>
+  assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "infsum f S = \<infinity>"
+  using assms infsumI has_sum_superconst_infinite_ennreal by blast
+
+lemma infsum_superconst_infinite_ereal:
+  fixes f :: \<open>'a \<Rightarrow> ereal\<close>
+  assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes b: \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "infsum f S = \<infinity>"
+proof -
+  obtain b' where b': \<open>e2ennreal b' = b\<close> and \<open>b' > 0\<close>
+    using b by blast
+  have *: \<open>infsum (e2ennreal o f) S = \<infinity>\<close>
+    apply (rule infsum_superconst_infinite_ennreal[where b=b'])
+    using assms \<open>b' > 0\<close> b' e2ennreal_mono apply auto
+    by (metis dual_order.strict_iff_order enn2ereal_e2ennreal le_less_linear zero_ennreal_def)
+  have \<open>infsum f S = infsum (enn2ereal o (e2ennreal o f)) S\<close>
+    by (smt (verit, best) b comp_apply dual_order.trans enn2ereal_e2ennreal geqb infsum_cong less_imp_le)
+  also have \<open>\<dots> = enn2ereal \<infinity>\<close>
+    apply (subst infsum_comm_additive_general)
+    using * by (auto simp: continuous_at_enn2ereal)
+  also have \<open>\<dots> = \<infinity>\<close>
+    by simp
+  finally show ?thesis
+    by -
+qed
+
+lemma has_sum_superconst_infinite_ereal:
+  fixes f :: \<open>'a \<Rightarrow> ereal\<close>
+  assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "has_sum f S \<infinity>"
+  by (metis Infty_neq_0(1) assms infsum_def has_sum_infsum infsum_superconst_infinite_ereal)
+
+lemma infsum_superconst_infinite_enat:
+  fixes f :: \<open>'a \<Rightarrow> enat\<close>
+  assumes geqb: \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes b: \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "infsum f S = \<infinity>"
+proof -
+  have \<open>ennreal_of_enat (infsum f S) = infsum (ennreal_of_enat o f) S\<close>
+    apply (rule infsum_comm_additive_general[symmetric])
+    by auto
+  also have \<open>\<dots> = \<infinity>\<close>
+    by (metis assms(3) b comp_apply ennreal_of_enat_0 ennreal_of_enat_inj ennreal_of_enat_le_iff geqb infsum_superconst_infinite_ennreal not_gr_zero)
+  also have \<open>\<dots> = ennreal_of_enat \<infinity>\<close>
+    by simp
+  finally show ?thesis
+    by (rule ennreal_of_enat_inj[THEN iffD1])
+qed
+
+lemma has_sum_superconst_infinite_enat:
+  fixes f :: \<open>'a \<Rightarrow> enat\<close>
+  assumes \<open>\<And>x. x \<in> S \<Longrightarrow> f x \<ge> b\<close>
+  assumes \<open>b > 0\<close>
+  assumes \<open>infinite S\<close>
+  shows "has_sum f S \<infinity>"
+  by (metis assms i0_lb has_sum_infsum infsum_superconst_infinite_enat pos_summable_on_complete)
+
+text \<open>This lemma helps to relate a real-valued infsum to a supremum over extended nonnegative reals.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_ennreal:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes summable: "f summable_on A"
+    and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "ennreal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))"
+proof -
+  have \<open>ennreal (infsum f A) = infsum (ennreal o f) A\<close>
+    apply (rule infsum_comm_additive_general[symmetric])
+    apply (subst sum_ennreal[symmetric])
+    using assms by auto
+  also have \<open>\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ennreal (sum f F)))\<close>
+    apply (subst pos_infsum_complete, simp)
+    apply (rule SUP_cong, blast)
+    apply (subst sum_ennreal[symmetric])
+    using fnn by auto
+  finally show ?thesis
+    by -
+qed
+
+text \<open>This lemma helps to related a real-valued infsum to a supremum over extended reals.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_ereal:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes summable: "f summable_on A"
+    and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "ereal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+proof -
+  have \<open>ereal (infsum f A) = infsum (ereal o f) A\<close>
+    apply (rule infsum_comm_additive_general[symmetric])
+    using assms by auto
+  also have \<open>\<dots> = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))\<close>
+    apply (subst pos_infsum_complete)
+    by (simp_all add: assms)[2]
+  finally show ?thesis
+    by -
+qed
+
+
+subsection \<open>Real numbers\<close>
+
+text \<open>Most lemmas in the general property section already apply to real numbers.
+      A few ones that are specific to reals are given here.\<close>
+
+lemma infsum_nonneg_is_SUPREMUM_real:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes summable: "f summable_on A"
+    and fnn: "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "infsum f A = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+proof -
+  have "ereal (infsum f A) = (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (ereal (sum f F)))"
+    using assms by (rule infsum_nonneg_is_SUPREMUM_ereal)
+  also have "\<dots> = ereal (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+  proof (subst ereal_SUP)
+    show "\<bar>SUP a\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f a)\<bar> \<noteq> \<infinity>"
+      using calculation by fastforce      
+    show "(SUP F\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f F)) = (SUP a\<in>{F. finite F \<and> F \<subseteq> A}. ereal (sum f a))"
+      by simp      
+  qed
+  finally show ?thesis by simp
+qed
+
+
+lemma has_sum_nonneg_SUPREMUM_real:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "f summable_on A" and "\<And>x. x\<in>A \<Longrightarrow> f x \<ge> 0"
+  shows "has_sum f A (SUP F\<in>{F. finite F \<and> F \<subseteq> A}. (sum f F))"
+  by (metis (mono_tags, lifting) assms has_sum_infsum infsum_nonneg_is_SUPREMUM_real)
+
+
+lemma summable_on_iff_abs_summable_on_real:
+  fixes f :: \<open>'a \<Rightarrow> real\<close>
+  shows \<open>f summable_on A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+  assume \<open>f summable_on A\<close>
+  define n A\<^sub>p A\<^sub>n
+    where \<open>n x = norm (f x)\<close> and \<open>A\<^sub>p = {x\<in>A. f x \<ge> 0}\<close> and \<open>A\<^sub>n = {x\<in>A. f x < 0}\<close> for x
+  have [simp]: \<open>A\<^sub>p \<union> A\<^sub>n = A\<close> \<open>A\<^sub>p \<inter> A\<^sub>n = {}\<close>
+    by (auto simp: A\<^sub>p_def A\<^sub>n_def)
+  from \<open>f summable_on A\<close> have [simp]: \<open>f summable_on A\<^sub>p\<close> \<open>f summable_on A\<^sub>n\<close>
+    using A\<^sub>p_def A\<^sub>n_def summable_on_subset_banach by fastforce+
+  then have [simp]: \<open>n summable_on A\<^sub>p\<close>
+    apply (subst summable_on_cong[where g=f])
+    by (simp_all add: A\<^sub>p_def n_def)
+  moreover have [simp]: \<open>n summable_on A\<^sub>n\<close>
+    apply (subst summable_on_cong[where g=\<open>\<lambda>x. - f x\<close>])
+     apply (simp add: A\<^sub>n_def n_def[abs_def])
+    by (simp add: summable_on_uminus)
+  ultimately have [simp]: \<open>n summable_on (A\<^sub>p \<union> A\<^sub>n)\<close>
+    apply (rule summable_on_Un_disjoint) by simp
+  then show \<open>n summable_on A\<close>
+    by simp
+next
+  show \<open>f abs_summable_on A \<Longrightarrow> f summable_on A\<close>
+    using abs_summable_summable by blast
+qed
+
+subsection \<open>Complex numbers\<close>
+
+lemma has_sum_cnj_iff[simp]: 
+  fixes f :: \<open>'a \<Rightarrow> complex\<close>
+  shows \<open>has_sum (\<lambda>x. cnj (f x)) M (cnj a) \<longleftrightarrow> has_sum f M a\<close>
+  by (simp add: has_sum_def lim_cnj del: cnj_sum add: cnj_sum[symmetric, abs_def, of f])
+
+lemma summable_on_cnj_iff[simp]:
+  "(\<lambda>i. cnj (f i)) summable_on A \<longleftrightarrow> f summable_on A"
+  by (metis complex_cnj_cnj summable_on_def has_sum_cnj_iff)
+
+lemma infsum_cnj[simp]: \<open>infsum (\<lambda>x. cnj (f x)) M = cnj (infsum f M)\<close>
+  by (metis complex_cnj_zero infsumI has_sum_cnj_iff infsum_def summable_on_cnj_iff has_sum_infsum)
+
+lemma infsum_Re:
+  assumes "f summable_on M"
+  shows "infsum (\<lambda>x. Re (f x)) M = Re (infsum f M)"
+  apply (rule infsum_comm_additive[where f=Re, unfolded o_def])
+  using assms by (auto intro!: additive.intro)
+
+lemma has_sum_Re:
+  assumes "has_sum f M a"
+  shows "has_sum (\<lambda>x. Re (f x)) M (Re a)"
+  apply (rule has_sum_comm_additive[where f=Re, unfolded o_def])
+  using assms by (auto intro!: additive.intro tendsto_Re)
+
+lemma summable_on_Re: 
+  assumes "f summable_on M"
+  shows "(\<lambda>x. Re (f x)) summable_on M"
+  apply (rule summable_on_comm_additive[where f=Re, unfolded o_def])
+  using assms by (auto intro!: additive.intro)
+
+lemma infsum_Im: 
+  assumes "f summable_on M"
+  shows "infsum (\<lambda>x. Im (f x)) M = Im (infsum f M)"
+  apply (rule infsum_comm_additive[where f=Im, unfolded o_def])
+  using assms by (auto intro!: additive.intro)
+
+lemma has_sum_Im:
+  assumes "has_sum f M a"
+  shows "has_sum (\<lambda>x. Im (f x)) M (Im a)"
+  apply (rule has_sum_comm_additive[where f=Im, unfolded o_def])
+  using assms by (auto intro!: additive.intro tendsto_Im)
+
+lemma summable_on_Im: 
+  assumes "f summable_on M"
+  shows "(\<lambda>x. Im (f x)) summable_on M"
+  apply (rule summable_on_comm_additive[where f=Im, unfolded o_def])
+  using assms by (auto intro!: additive.intro)
+
+lemma infsum_0D_complex:
+  fixes f :: "'a \<Rightarrow> complex"
+  assumes "infsum f A \<le> 0"
+    and abs_sum: "f summable_on A"
+    and nneg: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
+    and "x \<in> A"
+  shows "f x = 0"
+proof -
+  have \<open>Im (f x) = 0\<close>
+    apply (rule infsum_0D[where A=A])
+    using assms
+    by (auto simp add: infsum_Im summable_on_Im less_eq_complex_def)
+  moreover have \<open>Re (f x) = 0\<close>
+    apply (rule infsum_0D[where A=A])
+    using assms by (auto simp add: summable_on_Re infsum_Re less_eq_complex_def)
+  ultimately show ?thesis
+    by (simp add: complex_eqI)
+qed
+
+lemma has_sum_0D_complex:
+  fixes f :: "'a \<Rightarrow> complex"
+  assumes "has_sum f A a" and \<open>a \<le> 0\<close>
+    and "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0" and "x \<in> A"
+  shows "f x = 0"
+  by (metis assms infsumI infsum_0D_complex summable_on_def)
+
+text \<open>The lemma @{thm [source] infsum_mono_neutral} above applies to various linear ordered monoids such as the reals but not to the complex numbers.
+      Thus we have a separate corollary for those:\<close>
+
+lemma infsum_mono_neutral_complex:
+  fixes f :: "'a \<Rightarrow> complex"
+  assumes [simp]: "f summable_on A"
+    and [simp]: "g summable_on B"
+  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
+  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
+  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
+  shows \<open>infsum f A \<le> infsum g B\<close>
+proof -
+  have \<open>infsum (\<lambda>x. Re (f x)) A \<le> infsum (\<lambda>x. Re (g x)) B\<close>
+    apply (rule infsum_mono_neutral)
+    using assms(3-5) by (auto simp add: summable_on_Re less_eq_complex_def)
+  then have Re: \<open>Re (infsum f A) \<le> Re (infsum g B)\<close>
+    by (metis assms(1-2) infsum_Re)
+  have \<open>infsum (\<lambda>x. Im (f x)) A = infsum (\<lambda>x. Im (g x)) B\<close>
+    apply (rule infsum_cong_neutral)
+    using assms(3-5) by (auto simp add: summable_on_Re less_eq_complex_def)
+  then have Im: \<open>Im (infsum f A) = Im (infsum g B)\<close>
+    by (metis assms(1-2) infsum_Im)
+  from Re Im show ?thesis
+    by (auto simp: less_eq_complex_def)
+qed
+
+lemma infsum_mono_complex:
+  \<comment> \<open>For \<^typ>\<open>real\<close>, @{thm [source] infsum_mono} can be used. 
+      But \<^typ>\<open>complex\<close> does not have the right typeclass.\<close>
+  fixes f g :: "'a \<Rightarrow> complex"
+  assumes f_sum: "f summable_on A" and g_sum: "g summable_on A"
+  assumes leq: "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  shows   "infsum f A \<le> infsum g A"
+  by (metis DiffE IntD1 f_sum g_sum infsum_mono_neutral_complex leq)
+
+
+lemma infsum_nonneg_complex:
+  fixes f :: "'a \<Rightarrow> complex"
+  assumes "f summable_on M"
+    and "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+  shows "infsum f M \<ge> 0" (is "?lhs \<ge> _")
+  by (metis assms(1) assms(2) infsum_0_simp summable_on_0_simp infsum_mono_complex)
+
+lemma infsum_cmod:
+  assumes "f summable_on M"
+    and fnn: "\<And>x. x \<in> M \<Longrightarrow> 0 \<le> f x"
+  shows "infsum (\<lambda>x. cmod (f x)) M = cmod (infsum f M)"
+proof -
+  have \<open>complex_of_real (infsum (\<lambda>x. cmod (f x)) M) = infsum (\<lambda>x. complex_of_real (cmod (f x))) M\<close>
+    apply (rule infsum_comm_additive[symmetric, unfolded o_def])
+    apply auto
+    apply (simp add: additive.intro)
+    by (smt (verit, best) assms(1) cmod_eq_Re fnn summable_on_Re summable_on_cong less_eq_complex_def zero_complex.simps(1) zero_complex.simps(2))
+  also have \<open>\<dots> = infsum f M\<close>
+    apply (rule infsum_cong)
+    using fnn
+    using cmod_eq_Re complex_is_Real_iff less_eq_complex_def by force
+  finally show ?thesis
+    by (metis abs_of_nonneg infsum_def le_less_trans norm_ge_zero norm_infsum_bound norm_of_real not_le order_refl)
+qed
+
+
+lemma summable_on_iff_abs_summable_on_complex:
+  fixes f :: \<open>'a \<Rightarrow> complex\<close>
+  shows \<open>f summable_on A \<longleftrightarrow> f abs_summable_on A\<close>
+proof (rule iffI)
+  assume \<open>f summable_on A\<close>
+  define i r ni nr n where \<open>i x = Im (f x)\<close> and \<open>r x = Re (f x)\<close>
+    and \<open>ni x = norm (i x)\<close> and \<open>nr x = norm (r x)\<close> and \<open>n x = norm (f x)\<close> for x
+  from \<open>f summable_on A\<close> have \<open>i summable_on A\<close>
+    by (simp add: i_def[abs_def] summable_on_Im)
+  then have [simp]: \<open>ni summable_on A\<close>
+    using ni_def[abs_def] summable_on_iff_abs_summable_on_real by force
+
+  from \<open>f summable_on A\<close> have \<open>r summable_on A\<close>
+    by (simp add: r_def[abs_def] summable_on_Re)
+  then have [simp]: \<open>nr summable_on A\<close>
+    by (metis nr_def summable_on_cong summable_on_iff_abs_summable_on_real)
+
+  have n_sum: \<open>n x \<le> nr x + ni x\<close> for x
+    by (simp add: n_def nr_def ni_def r_def i_def cmod_le)
+
+  have *: \<open>(\<lambda>x. nr x + ni x) summable_on A\<close>
+    apply (rule summable_on_add) by auto
+  show \<open>n summable_on A\<close>
+    apply (rule pos_summable_on)
+     apply (simp add: n_def)
+    apply (rule bdd_aboveI[where M=\<open>infsum (\<lambda>x. nr x + ni x) A\<close>])
+    using * n_sum by (auto simp flip: infsum_finite simp: ni_def[abs_def] nr_def[abs_def] intro!: infsum_mono_neutral)
+next
+  show \<open>f abs_summable_on A \<Longrightarrow> f summable_on A\<close>
+    using abs_summable_summable by blast
+qed
+
+end
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Analysis/Product_Vector.thy
     Author:     Brian Huffman
+                Dominique Unruh, University of Tartu
 *)
 
 section \<open>Cartesian Products as Vector Spaces\<close>
@@ -122,15 +123,149 @@
 instance ..
 end
 
-instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist
-begin
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniformity, uniformity) uniformity begin
+
+definition [code del]: \<open>(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) = 
+        filtermap (\<lambda>((x1,x2),(y1,y2)). ((x1,y1),(x2,y2))) (uniformity \<times>\<^sub>F uniformity)\<close>
+
+instance..
+end
 
-definition [code del]:
-  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
-    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space begin
+instance 
+proof standard
+  fix U :: \<open>('a \<times> 'b) set\<close>
+  show \<open>open U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)\<close>
+  proof (intro iffI ballI)
+    fix x assume \<open>open U\<close> and \<open>x \<in> U\<close>
+    then obtain A B where \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A\<times>B\<close> \<open>A\<times>B \<subseteq> U\<close>
+      by (metis open_prod_elim)
+    define UA where \<open>UA = (\<lambda>(x'::'a,y). x' = fst x \<longrightarrow> y \<in> A)\<close>
+    from \<open>open A\<close> \<open>x \<in> A\<times>B\<close>
+    have \<open>eventually UA uniformity\<close>
+      unfolding open_uniformity UA_def by auto
+    define UB where \<open>UB = (\<lambda>(x'::'b,y). x' = snd x \<longrightarrow> y \<in> B)\<close>
+    from \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A\<times>B\<close>
+    have \<open>eventually UA uniformity\<close> \<open>eventually UB uniformity\<close>
+      unfolding open_uniformity UA_def UB_def by auto
+    then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
+      apply (auto intro!: exI[of _ UA] exI[of _ UB] simp add: eventually_prod_filter)
+      using \<open>A\<times>B \<subseteq> U\<close> by (auto simp: UA_def UB_def)
+    then show \<open>\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+      by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
+  next
+    assume asm: \<open>\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+    show \<open>open U\<close>
+    proof (unfold open_prod_def, intro ballI)
+      fix x assume \<open>x \<in> U\<close>
+      with asm have \<open>\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U\<close>
+        by auto
+      then have \<open>\<forall>\<^sub>F ((x'1, y1), (x'2, y2)) in uniformity \<times>\<^sub>F uniformity. (x'1,x'2) = x \<longrightarrow> (y1,y2) \<in> U\<close>
+        by (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold)
+      then obtain UA UB where \<open>eventually UA uniformity\<close> and \<open>eventually UB uniformity\<close>
+               and UA_UB_U: \<open>UA (a1, a2) \<Longrightarrow> UB (b1, b2) \<Longrightarrow> (a1, b1) = x \<Longrightarrow> (a2, b2) \<in> U\<close> for a1 a2 b1 b2
+        apply atomize_elim by (simp add: case_prod_beta eventually_prod_filter)
+      have \<open>eventually (\<lambda>a. UA (fst x, a)) (nhds (fst x))\<close>
+        using \<open>eventually UA uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
+      then obtain A where \<open>open A\<close> and A_UA: \<open>A \<subseteq> {a. UA (fst x, a)}\<close> and \<open>fst x \<in> A\<close>
+        by (metis (mono_tags, lifting) eventually_nhds mem_Collect_eq subsetI)
+      have \<open>eventually (\<lambda>b. UB (snd x, b)) (nhds (snd x))\<close>
+        using \<open>eventually UB uniformity\<close> eventually_mono eventually_nhds_uniformity by fastforce
+      then obtain B where \<open>open B\<close> and B_UB: \<open>B \<subseteq> {b. UB (snd x, b)}\<close> and \<open>snd x \<in> B\<close>
+        by (metis (mono_tags, lifting) eventually_nhds mem_Collect_eq subsetI)
+      have \<open>x \<in> A \<times> B\<close>
+        by (simp add: \<open>fst x \<in> A\<close> \<open>snd x \<in> B\<close> mem_Times_iff)
+      have \<open>A \<times> B \<subseteq> U\<close>
+        using A_UA B_UB UA_UB_U by fastforce
+      show \<open>\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> U\<close>
+        using \<open>A \<times> B \<subseteq> U\<close> \<open>open A\<close> \<open>open B\<close> \<open>x \<in> A \<times> B\<close> by auto
+    qed
+  qed
+next
+  show \<open>eventually E uniformity \<Longrightarrow> E (x, x)\<close> for E and x :: \<open>'a \<times> 'b\<close> 
+    apply (simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+    by (metis surj_pair uniformity_refl)
+next
+  show \<open>eventually E uniformity \<Longrightarrow> \<forall>\<^sub>F (x::'a\<times>'b, y) in uniformity. E (y, x)\<close> for E
+    apply (simp only: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+    apply (erule exE, erule exE, rename_tac Pf Pg)
+    apply (rule_tac x=\<open>\<lambda>(x,y). Pf (y,x)\<close> in exI)
+    apply (rule_tac x=\<open>\<lambda>(x,y). Pg (y,x)\<close> in exI)
+    by (auto simp add: uniformity_sym)
+next
+  show \<open>\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x::'a\<times>'b, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))\<close> 
+    if \<open>eventually E uniformity\<close> for E
+  proof -
+    from that
+    obtain EA EB where \<open>eventually EA uniformity\<close> and \<open>eventually EB uniformity\<close>
+               and EA_EB_E: \<open>EA (a1, a2) \<Longrightarrow> EB (b1, b2) \<Longrightarrow> E ((a1, b1), (a2, b2))\<close> for a1 a2 b1 b2
+      by (auto simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter)
+    obtain DA where \<open>eventually DA uniformity\<close> and DA_EA: \<open>DA (x,y) \<Longrightarrow> DA (y,z) \<Longrightarrow> EA (x,z)\<close> for x y z
+      using \<open>eventually EA uniformity\<close> uniformity_transE by blast
+    obtain DB where \<open>eventually DB uniformity\<close> and DB_EB: \<open>DB (x,y) \<Longrightarrow> DB (y,z) \<Longrightarrow> EB (x,z)\<close> for x y z
+      using \<open>eventually EB uniformity\<close> uniformity_transE by blast
+    define D where \<open>D = (\<lambda>((a1,b1),(a2,b2)). DA (a1,a2) \<and> DB (b1,b2))\<close>
+    have \<open>eventually D uniformity\<close>
+      using \<open>eventually DA uniformity\<close> \<open>eventually DB uniformity\<close>
+      by (auto simp add: uniformity_prod_def eventually_filtermap case_prod_unfold eventually_prod_filter D_def)
+    moreover have \<open>D ((a1, b1), (a2, b2)) \<Longrightarrow> D ((a2, b2), (a3, b3)) \<Longrightarrow> E ((a1, b1), (a3, b3))\<close> for a1 b1 a2 b2 a3 b3
+      using DA_EA DB_EB D_def EA_EB_E by blast
+    ultimately show ?thesis
+      by auto
+  qed
+qed
+end
 
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist begin
 instance
-  by standard (rule uniformity_prod_def)
+proof
+  show \<open>uniformity = (INF e\<in>{0 <..}. principal {(x::'a\<times>'b, y). dist x y < e})\<close>
+  proof (subst filter_eq_iff, intro allI iffI)
+    fix P :: \<open>('a \<times> 'b) \<times> ('a \<times> 'b) \<Rightarrow> bool\<close>
+
+    have 1: \<open>\<exists>e\<in>{0<..}.
+              {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < a} \<and>
+              {(x,y). dist x y < e} \<subseteq> {(x,y). dist x y < b}\<close> if \<open>a>0\<close> \<open>b>0\<close> for a b
+      apply (rule bexI[of _ \<open>min a b\<close>])
+      using that by auto
+    have 2: \<open>mono (\<lambda>P. eventually (\<lambda>x. P (Q x)) F)\<close> for F :: \<open>'z filter\<close> and Q :: \<open>'z \<Rightarrow> 'y\<close>
+      unfolding mono_def using eventually_mono le_funD by fastforce
+    have \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist x1 y1 < e/2 \<and> dist x2 y2 < e/2\<close> if \<open>e>0\<close> for e
+      by (auto intro!: eventually_prodI exI[of _ \<open>e/2\<close>] simp: case_prod_unfold eventually_uniformity_metric that)
+    then have 3: \<open>\<forall>\<^sub>F ((x1::'a,y1),(x2::'b,y2)) in uniformity \<times>\<^sub>F uniformity. dist (x1,x2) (y1,y2) < e\<close> if \<open>e>0\<close> for e
+      apply (rule eventually_rev_mp)
+      by (auto intro!: that eventuallyI simp: case_prod_unfold dist_prod_def sqrt_sum_squares_half_less)
+    show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e}) \<Longrightarrow> eventually P uniformity\<close>
+      apply (subst (asm) eventually_INF_base)
+      using 1 3 apply (auto simp: uniformity_prod_def case_prod_unfold eventually_filtermap 2 eventually_principal)
+      by (smt (verit, best) eventually_mono)
+  next
+    fix P :: \<open>('a \<times> 'b) \<times> ('a \<times> 'b) \<Rightarrow> bool\<close>
+    assume \<open>eventually P uniformity\<close>
+    then obtain P1 P2 where \<open>eventually P1 uniformity\<close> \<open>eventually P2 uniformity\<close>
+      and P1P2P: \<open>P1 (x1, y1) \<Longrightarrow> P2 (x2, y2) \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
+      by (auto simp: eventually_filtermap case_prod_beta eventually_prod_filter uniformity_prod_def)
+    from \<open>eventually P1 uniformity\<close> obtain e1 where \<open>e1>0\<close> and e1P1: \<open>dist x y < e1 \<Longrightarrow> P1 (x,y)\<close> for x y
+      using eventually_uniformity_metric by blast
+    from \<open>eventually P2 uniformity\<close> obtain e2 where \<open>e2>0\<close> and e2P2: \<open>dist x y < e2 \<Longrightarrow> P2 (x,y)\<close> for x y
+      using eventually_uniformity_metric by blast
+    define e where \<open>e = min e1 e2\<close>
+    have \<open>e > 0\<close>
+      using \<open>0 < e1\<close> \<open>0 < e2\<close> e_def by auto
+    have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x1 y1 < e1\<close> for x1 y1 :: 'a and x2 y2 :: 'b
+      unfolding dist_prod_def e_def apply auto
+      by (smt (verit, best) real_sqrt_sum_squares_ge1)
+    moreover have \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> dist x2 y2 < e2\<close> for x1 y1 :: 'a and x2 y2 :: 'b
+      unfolding dist_prod_def e_def apply auto
+      by (smt (verit, best) real_sqrt_sum_squares_ge1)
+    ultimately have *: \<open>dist (x1,x2) (y1,y2) < e \<Longrightarrow> P ((x1, x2), (y1, y2))\<close> for x1 y1 x2 y2
+      using e1P1 e2P2 P1P2P by auto
+
+    show \<open>eventually P (INF e\<in>{0<..}. principal {(x, y). dist x y < e})\<close>
+       apply (rule eventually_INF1[where i=e])
+      using \<open>e > 0\<close> * by (auto simp: eventually_principal)
+  qed
+qed
 end
 
 declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
@@ -221,24 +356,21 @@
       ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
     qed
   qed
-  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
-    unfolding * eventually_uniformity_metric
-    by (simp del: split_paired_All add: dist_prod_def dist_commute)
 qed
 
 end
 
 declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
 
-lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
+lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n :: 'a::metric_space \<times> 'b::metric_space))"
   unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
 
-lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
+lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n :: 'a::metric_space \<times> 'b::metric_space))"
   unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
 
 lemma Cauchy_Pair:
   assumes "Cauchy X" and "Cauchy Y"
-  shows "Cauchy (\<lambda>n. (X n, Y n))"
+  shows "Cauchy (\<lambda>n. (X n :: 'a::metric_space, Y n :: 'a::metric_space))"
 proof (rule metric_CauchyI)
   fix r :: real assume "0 < r"
   hence "0 < r / sqrt 2" (is "0 < ?s") by simp
@@ -251,6 +383,56 @@
   then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
 qed
 
+text \<open>Analogue to @{thm [source] uniformly_continuous_on_def} for two-argument functions.\<close>
+lemma uniformly_continuous_on_prod_metric:
+  fixes f :: \<open>('a::metric_space \<times> 'b::metric_space) \<Rightarrow> 'c::metric_space\<close>
+  shows \<open>uniformly_continuous_on (S\<times>T) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e)\<close>
+proof (unfold uniformly_continuous_on_def, intro iffI impI allI)
+  fix e :: real 
+  assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+  then obtain d where \<open>d > 0\<close>
+    and d: \<open>\<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+    by auto
+  show \<open>\<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>y\<in>S\<times>T. dist y x < d \<longrightarrow> dist (f y) (f x) < e\<close>
+    apply (rule exI[of _ d])
+    using \<open>d>0\<close> d[rule_format] apply auto
+    by (smt (verit, del_insts) dist_fst_le dist_snd_le fst_conv snd_conv)
+next
+  fix e :: real 
+  assume \<open>e > 0\<close> and \<open>\<forall>e>0. \<exists>d>0. \<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
+  then obtain d where \<open>d > 0\<close> and d: \<open>\<forall>x\<in>S\<times>T. \<forall>x'\<in>S\<times>T. dist x' x < d \<longrightarrow> dist (f x') (f x) < e\<close>
+    by auto
+  show \<open>\<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>S. \<forall>x'\<in>T. \<forall>y'\<in>T. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e\<close>
+  proof (intro exI conjI impI ballI)
+    from \<open>d > 0\<close> show \<open>d / 2 > 0\<close> by auto
+    fix x y x' y'
+    assume [simp]: \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>x' \<in> T\<close> \<open>y' \<in> T\<close>
+    assume \<open>dist x y < d / 2\<close> and \<open>dist x' y' < d / 2\<close>
+    then have \<open>dist (x, x') (y, y') < d\<close>
+      by (simp add: dist_Pair_Pair sqrt_sum_squares_half_less)
+    with d show \<open>dist (f (x, x')) (f (y, y')) < e\<close>
+      by auto
+  qed
+qed
+
+text \<open>Analogue to @{thm [source] isUCont_def} for two-argument functions.\<close>
+lemma isUCont_prod_metric:
+  fixes f :: \<open>('a::metric_space \<times> 'b::metric_space) \<Rightarrow> 'c::metric_space\<close>
+  shows \<open>isUCont f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x. \<forall>y. \<forall>x'. \<forall>y'. dist x y < d \<longrightarrow> dist x' y' < d \<longrightarrow> dist (f (x, x')) (f (y, y')) < e)\<close>
+  using uniformly_continuous_on_prod_metric[of UNIV UNIV]
+  by auto
+
+text \<open>This logically belong with the real vector spaces by we only have the necessary lemmas now.\<close>
+lemma isUCont_plus[simp]:
+  shows \<open>isUCont (\<lambda>(x::'a::real_normed_vector,y). x+y)\<close>
+proof (rule isUCont_prod_metric[THEN iffD2], intro allI impI, simp)
+  fix e :: real assume \<open>0 < e\<close>
+  show \<open>\<exists>d>0. \<forall>x y :: 'a. dist x y < d \<longrightarrow> (\<forall>x' y'. dist x' y' < d \<longrightarrow> dist (x + x') (y + y') < e)\<close>
+    apply (rule exI[of _ \<open>e/2\<close>])
+    using \<open>0 < e\<close> apply auto
+    by (smt (verit, ccfv_SIG) dist_add_cancel dist_add_cancel2 dist_commute dist_triangle_lt)
+qed
+
 subsection \<open>Product is a Complete Metric Space\<close>
 
 instance\<^marker>\<open>tag important\<close> prod :: (complete_space, complete_space) complete_space
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Analysis/document/root.bib
--- a/src/HOL/Analysis/document/root.bib	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Analysis/document/root.bib	Thu Oct 07 16:28:17 2021 +0200
@@ -23,4 +23,12 @@
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@book{conway2013course,
+  title={A course in functional analysis},
+  author={Conway, John B},
+  volume={96},
+  year={2013},
+  publisher={Springer Science \& Business Media}
+}
+
 @misc{dummy}
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Complex_Analysis/Winding_Numbers.thy
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -529,7 +529,7 @@
   fixes z::complex
   assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and 1: "Re (winding_number \<gamma> z) \<ge> 1"
       and w: "w \<noteq> z"
-  shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+  shows "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image \<gamma>"
 proof -
   have [simp]: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<gamma> x \<noteq> z"
     using z by (auto simp: path_image_def)
@@ -582,7 +582,7 @@
   fixes z::complex
   assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "\<bar>Re (winding_number \<gamma> z)\<bar> \<ge> 1"
       and w: "w \<noteq> z"
-  shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
+  shows "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image \<gamma>"
 proof -
   { assume "Re (winding_number \<gamma> z) \<le> - 1"
     then have "Re (winding_number (reversepath \<gamma>) z) \<ge> 1"
@@ -591,7 +591,7 @@
       using \<gamma> valid_path_imp_reverse by auto
     moreover have "z \<notin> path_image (reversepath \<gamma>)"
       by (simp add: z)
-    ultimately have "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image (reversepath \<gamma>)"
+    ultimately have "\<exists>a::real. 0 < a \<and> z + of_real a * (w - z) \<in> path_image (reversepath \<gamma>)"
       using winding_number_pos_meets w by blast
     then have ?thesis
       by simp
@@ -605,7 +605,7 @@
   fixes z::complex
   shows
   "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
-    \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
+    \<And>a::real. 0 < a \<Longrightarrow> z + of_real a * (w - z) \<notin> path_image \<gamma>\<rbrakk>
    \<Longrightarrow> Re(winding_number \<gamma> z) < 1"
    by (auto simp: not_less dest: winding_number_big_meets)
 
@@ -1736,7 +1736,7 @@
   ultimately
   have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}"
     by (auto simp: path_image_join assms)
-  have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if x: "x \<in> closed_segment (a + kde) (a + e)" for x
+  have ge_kde1: "\<exists>y. x = a + of_real y \<and> y \<ge> kde" if x: "x \<in> closed_segment (a + kde) (a + e)" for x
   proof -
     obtain u where "0 \<le> u" "u \<le> 1" and u: "x = (1 - u) *\<^sub>R (a + kde) + u *\<^sub>R (a + e)"
       using x by (auto simp: in_segment)
@@ -1747,7 +1747,7 @@
     ultimately
     show ?thesis by blast
   qed
-  have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if x: "x \<in> closed_segment (a - d) (a - kde)" for x
+  have ge_kde2: "\<exists>y. x = a + of_real y \<and> y \<le> -kde" if x: "x \<in> closed_segment (a - d) (a - kde)" for x
   proof -
     obtain u where "0 \<le> u" "u \<le> 1" and u: "x = (1 - u) *\<^sub>R (a - d) + u *\<^sub>R (a - kde)"
       using x by (auto simp: in_segment)
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Library/Complex_Order.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Complex_Order.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -0,0 +1,39 @@
+(*
+  Title:    HOL/Library/Complex_Order.thy
+  Author:   Dominique Unruh, University of Tartu
+
+  Instantiation of complex numbers as an ordered set.
+*)
+
+theory Complex_Order
+  imports Complex_Main
+begin
+
+instantiation complex :: order begin
+
+definition \<open>x < y \<longleftrightarrow> Re x < Re y \<and> Im x = Im y\<close>
+definition \<open>x \<le> y \<longleftrightarrow> Re x \<le> Re y \<and> Im x = Im y\<close>
+
+instance
+  apply standard
+  by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff)
+end
+
+lemma nonnegative_complex_is_real: \<open>(x::complex) \<ge> 0 \<Longrightarrow> x \<in> \<real>\<close>
+  by (simp add: complex_is_Real_iff less_eq_complex_def)
+
+lemma complex_is_real_iff_compare0: \<open>(x::complex) \<in> \<real> \<longleftrightarrow> x \<le> 0 \<or> x \<ge> 0\<close>
+  using complex_is_Real_iff less_eq_complex_def by auto
+
+instance complex :: ordered_comm_ring
+  apply standard
+  by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff mult_left_mono mult_right_mono)
+
+instance complex :: ordered_real_vector
+  apply standard
+  by (auto simp: less_complex_def less_eq_complex_def mult_left_mono mult_right_mono)
+
+instance complex :: ordered_cancel_comm_semiring
+  by standard
+
+end
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -1173,6 +1173,17 @@
 lemma ennreal_of_enat_eSuc[simp]: "ennreal_of_enat (eSuc x) = 1 + ennreal_of_enat x"
   by (cases x) (auto simp: eSuc_enat)
 
+(* Contributed by Dominique Unruh *)
+lemma ennreal_of_enat_plus[simp]: \<open>ennreal_of_enat (a+b) = ennreal_of_enat a + ennreal_of_enat b\<close>
+  apply (induction a)
+  apply auto
+  by (smt (z3) add.commute add.right_neutral enat.exhaust enat.simps(4) enat.simps(5) ennreal_add_left_cancel ennreal_of_enat_def infinity_ennreal_def of_nat_add of_nat_eq_enat plus_enat_simps(2))
+
+(* Contributed by Dominique Unruh *)
+lemma sum_ennreal_of_enat[simp]: "(\<Sum>i\<in>I. ennreal_of_enat (f i)) = ennreal_of_enat (sum f I)"
+  apply (induction I rule: infinite_finite_induct) 
+  by (auto simp: sum_nonneg)
+
 subsection \<open>Topology on \<^typ>\<open>ennreal\<close>\<close>
 
 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
@@ -1657,6 +1668,60 @@
   apply (auto simp del: sup_ereal_def simp add: sup_INF)
   done
 
+(* Contributed by Dominique Unruh *)
+lemma isCont_ennreal[simp]: \<open>isCont ennreal x\<close>
+  apply (auto intro!: sequentially_imp_eventually_within simp: continuous_within tendsto_def)
+  by (metis tendsto_def tendsto_ennrealI)
+
+(* Contributed by Dominique Unruh *)
+lemma isCont_ennreal_of_enat[simp]: \<open>isCont ennreal_of_enat x\<close>
+proof -
+  have continuous_at_open:
+    \<comment> \<open>Copied lemma from \<^session>\<open>HOL-Analysis\<close> to avoid dependency.\<close>
+      "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" for f :: \<open>enat \<Rightarrow> 'z::topological_space\<close>
+    unfolding continuous_within_topological [of x UNIV f]
+    unfolding imp_conjL
+    by (intro all_cong imp_cong ex_cong conj_cong refl) auto
+  show ?thesis
+  proof (subst continuous_at_open, intro allI impI, cases \<open>x = \<infinity>\<close>)
+    case True
+
+    fix t assume \<open>open t \<and> ennreal_of_enat x \<in> t\<close>
+    then have \<open>\<exists>y<\<infinity>. {y <.. \<infinity>} \<subseteq> t\<close>
+      apply (rule_tac open_left[where y=0])
+      by (auto simp: True)
+    then obtain y where \<open>{y<..} \<subseteq> t\<close> and \<open>y \<noteq> \<infinity>\<close>
+      apply atomize_elim
+      apply (auto simp: greaterThanAtMost_def)
+      by (metis atMost_iff inf.orderE subsetI top.not_eq_extremum top_greatest)
+
+    from \<open>y \<noteq> \<infinity>\<close>
+    obtain x' where x'y: \<open>ennreal_of_enat x' > y\<close> and \<open>x' \<noteq> \<infinity>\<close>
+      by (metis enat.simps(3) ennreal_Ex_less_of_nat ennreal_of_enat_enat infinity_ennreal_def top.not_eq_extremum)
+    define s where \<open>s = {x'<..}\<close>
+    have \<open>open s\<close>
+      by (simp add: s_def)
+    moreover have \<open>x \<in> s\<close>
+      by (simp add: \<open>x' \<noteq> \<infinity>\<close> s_def True)
+    moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
+      by (metis x'y \<open>{y<..} \<subseteq> t\<close> ennreal_of_enat_le_iff greaterThan_iff le_less_trans less_imp_le not_less s_def subsetD that)
+    ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+      by auto
+  next
+    case False
+    fix t assume asm: \<open>open t \<and> ennreal_of_enat x \<in> t\<close>
+    define s where \<open>s = {x}\<close>
+    have \<open>open s\<close>
+      using False open_enat_iff s_def by blast
+    moreover have \<open>x \<in> s\<close>
+      using s_def by auto
+    moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
+      using asm s_def that by blast
+    ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+      by auto
+  qed
+qed
+
 subsection \<open>Approximation lemmas\<close>
 
 lemma INF_approx_ennreal:
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Limits.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -1000,7 +1000,7 @@
   unfolding tendsto_iff by simp
 
 lemma tendsto_add_const_iff:
-  "((\<lambda>x. c + f x :: 'a::real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
+  "((\<lambda>x. c + f x :: 'a::topological_group_add) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
   using tendsto_add[OF tendsto_const[of c], of f d]
     and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
 
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/ROOT	Thu Oct 07 16:28:17 2021 +0200
@@ -76,6 +76,7 @@
     Code_Real_Approx_By_Float
     Code_Target_Numeral
     Code_Target_Numeral_Float
+    Complex_Order
     DAList
     DAList_Multiset
     RBT_Mapping
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -1781,6 +1781,38 @@
     by auto
 qed (auto intro!: exI[of _ "{y. dist x y < e}" for e] open_ball simp: dist_commute)
 
+(* Contributed by Dominique Unruh *)
+lemma tendsto_iff_uniformity:
+    \<comment> \<open>More general analogus of \<open>tendsto_iff\<close> below. Applies to all uniform spaces, not just metric ones.\<close>
+  fixes l :: \<open>'b :: uniform_space\<close>
+  shows \<open>(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>E. eventually E uniformity \<longrightarrow> (\<forall>\<^sub>F x in F. E (f x, l)))\<close>
+proof (intro iffI allI impI)
+  fix E :: \<open>('b \<times> 'b) \<Rightarrow> bool\<close>
+  assume \<open>(f \<longlongrightarrow> l) F\<close> and \<open>eventually E uniformity\<close>
+  from \<open>eventually E uniformity\<close>
+  have \<open>eventually (\<lambda>(x, y). E (y, x)) uniformity\<close>
+    by (simp add: uniformity_sym)
+  then have \<open>\<forall>\<^sub>F (y, x) in uniformity. y = l \<longrightarrow> E (x, y)\<close>
+    using eventually_mono by fastforce
+  with \<open>(f \<longlongrightarrow> l) F\<close> have \<open>eventually (\<lambda>x. E (x ,l)) (filtermap f F)\<close>
+    by (simp add: filterlim_def le_filter_def eventually_nhds_uniformity)
+  then show \<open>\<forall>\<^sub>F x in F. E (f x, l)\<close>
+    by (simp add: eventually_filtermap)
+next
+  assume assm: \<open>\<forall>E. eventually E uniformity \<longrightarrow> (\<forall>\<^sub>F x in F. E (f x, l))\<close>
+  have \<open>eventually P (filtermap f F)\<close> if \<open>\<forall>\<^sub>F (x, y) in uniformity. x = l \<longrightarrow> P y\<close> for P
+  proof -
+    from that have \<open>\<forall>\<^sub>F (y, x) in uniformity. x = l \<longrightarrow> P y\<close> 
+      using uniformity_sym[where E=\<open>\<lambda>(x,y). x=l \<longrightarrow> P y\<close>] by auto
+    with assm have \<open>\<forall>\<^sub>F x in F. P (f x)\<close>
+      by auto
+    then show ?thesis
+      by (auto simp: eventually_filtermap)
+  qed
+  then show \<open>(f \<longlongrightarrow> l) F\<close>
+    by (simp add: filterlim_def le_filter_def eventually_nhds_uniformity)
+qed
+
 lemma (in metric_space) tendsto_iff: "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   unfolding nhds_metric filterlim_INF filterlim_principal by auto
 
@@ -2186,6 +2218,52 @@
   done
 
 
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::dist \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
+
+(* Contributed by Dominique Unruh *)
+lemma cauchy_filter_metric:
+  fixes F :: "'a::{uniformity_dist,uniform_space} filter"
+  shows "cauchy_filter F \<longleftrightarrow> (\<forall>e. e>0 \<longrightarrow> (\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)))"
+proof (unfold cauchy_filter_def le_filter_def, auto)
+  assume assm: \<open>\<forall>e>0. \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+  then show \<open>eventually P uniformity \<Longrightarrow> eventually P (F \<times>\<^sub>F F)\<close> for P
+    apply (auto simp: eventually_uniformity_metric)
+    using eventually_prod_same by blast
+next
+  fix e :: real
+  assume \<open>e > 0\<close>
+  assume asm: \<open>\<forall>P. eventually P uniformity \<longrightarrow> eventually P (F \<times>\<^sub>F F)\<close>
+
+  define P where \<open>P \<equiv> \<lambda>(x,y :: 'a). dist x y < e\<close>
+  with asm \<open>e > 0\<close> have \<open>eventually P (F \<times>\<^sub>F F)\<close>
+    by (metis case_prod_conv eventually_uniformity_metric)
+  then
+  show \<open>\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+    by (auto simp add: eventually_prod_same P_def)
+qed
+
+(* Contributed by Dominique Unruh *)
+lemma cauchy_filter_metric_filtermap:
+  fixes f :: "'a \<Rightarrow> 'b::{uniformity_dist,uniform_space}"
+  shows "cauchy_filter (filtermap f F) \<longleftrightarrow> (\<forall>e. e>0 \<longrightarrow> (\<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)))"
+proof (subst cauchy_filter_metric, intro iffI allI impI)
+  assume \<open>\<forall>e>0. \<exists>P. eventually P (filtermap f F) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+  then show \<open>e>0 \<Longrightarrow> \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)\<close> for e
+    unfolding eventually_filtermap by blast
+next
+  assume asm: \<open>\<forall>e>0. \<exists>P. eventually P F \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist (f x) (f y) < e)\<close>
+  fix e::real assume \<open>e > 0\<close>
+  then obtain P where \<open>eventually P F\<close> and PPe: \<open>P x \<and> P y \<longrightarrow> dist (f x) (f y) < e\<close> for x y
+    using asm by blast
+
+  show \<open>\<exists>P. eventually P (filtermap f F) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> dist x y < e)\<close>
+    apply (rule exI[of _ \<open>\<lambda>x. \<exists>y. P y \<and> x = f y\<close>])
+    using PPe \<open>eventually P F\<close> apply (auto simp: eventually_filtermap)
+    by (smt (verit, ccfv_SIG) eventually_elim2)
+qed
+
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::metric_space \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
+
 subsubsection \<open>Cauchy Sequences are Convergent\<close>
 
 (* TODO: update to uniform_space *)
diff -r 6424c54157d9 -r fd5f62176987 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Oct 07 10:16:52 2021 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Oct 07 16:28:17 2021 +0200
@@ -788,6 +788,11 @@
 lemma tendsto_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> ((\<lambda>x. f x) \<longlongrightarrow> l) net"
   by (rule topological_tendstoI) (auto elim: eventually_mono)
 
+(* Contributed by Dominique Unruh *)
+lemma tendsto_principal_singleton[simp]:
+  shows "(f \<longlongrightarrow> f x) (principal {x})"
+  unfolding tendsto_def eventually_principal by simp
+
 end
 
 lemma (in topological_space) filterlim_within_subset:
@@ -3438,7 +3443,6 @@
 
 end
 
-
 subsubsection \<open>Uniformly continuous functions\<close>
 
 definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool"