Quelle  Infinite_Sum.thy

(*
  Title: HOL/Analysis/Infinite_Sum.thy
  Author: Dominique Unruh, University of Tartu
  Manuel Eberl, University of Innsbruck
 
  A theory of sums over possibly infinite sets.
*)

section ‹Infinite sums›
🍋‹\label{section:Infinite_Sum}›

text ‹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 🍋‹"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.)›

theory Infinite_Sum
  imports
    Elementary_Topology
    "HOL-Library.Extended_Nonnegative_Real"
    "HOL-Library.Complex_Order"
    "HOL-Computational_Algebra.Formal_Power_Series"
begin

subsection ‹Definition and syntax›

definition HAS_SUM :: ‹('a ==> 'b :: {comm_monoid_add, topological_space}) ==> 'a set ==> 'b ==> bool›
    where has_sum_def: ‹HAS_SUM f A x ≡ (sum f ---> x) (finite_subsets_at_top A)›

abbreviation has_sum (infixr ‹has'_sum› 46) where
  "(f has_sum S) A ≡ HAS_SUM f A S"

definition summable_on :: "('a ==> 'b::{comm_monoid_add, topological_space}) ==> 'a set ==> bool" (infixr ‹summable'_on› 46) where
  "f summable_on A ≡ (∃x. (f has_sum x) A)"

definition infsum :: "('a ==> 'b::{comm_monoid_add,t2_space}) ==> 'a set ==> '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 ==> 'b::real_normed_vector) ==> 'a set ==> bool" (infixr ‹abs'_summable'_on› 46) where
  "f abs_summable_on A ≡ (λx. norm (f x)) summable_on A"

syntax (ASCII)
  "_infsum" :: "pttrn ==> 'a set ==> 'b ==> 'b::topological_comm_monoid_add"
    (‹(‹indent=3 notation=‹binder INFSUM›\›INFSUM (_/:_)./ _)› [0, 51, 10] 10)
syntax
  "_infsum" :: "pttrn ==> 'a set ==> 'b ==> 'b::topological_comm_monoid_add"
    (‹(‹indent=2 notation=‹binder ∑🪙∞›\›\∑🪙∞(_/∈_)./ _)› [0, 51, 10] 10)
syntax_consts
  "_infsum" ⇌ infsum
translations 🍋 ‹Beware of argument permutation!›
  "∑🪙∞i∈A. b" ⇌ "CONST infsum (λi. b) A"

syntax (ASCII)
  "_univinfsum" :: "pttrn ==> 'a ==> 'a"  (‹(‹indent=3 notation=‹binder INFSUM›\›INFSUM _./ _)› [0, 10] 10)
syntax
  "_univinfsum" :: "pttrn ==> 'a ==> 'a"  (‹(‹indent=2 notation=‹binder ∑🪙∞›\›\∑🪙∞_./ _)› [0, 10] 10)
syntax_consts
  "_univinfsum" ⇌ infsum
translations
  "∑🪙∞x. t" ⇌ "CONST infsum (λx. t) (CONST UNIV)"

syntax (ASCII)
  "_qinfsum" :: "pttrn ==> bool ==> 'a ==> 'a"  (‹(‹indent=3 notation=‹binder INFSUM›\›INFSUM _ |/ _./ _)› [0, 0, 10] 10)
syntax
  "_qinfsum" :: "pttrn ==> bool ==> 'a ==> 'a"  (‹(‹indent=2 notation=‹binder ∑🪙∞›\›\∑🪙∞_ | (_)./ _)› [0, 0, 10] 10)
syntax_consts
  "_qinfsum" ⇌ infsum
translations
  "∑🪙∞x|P. t" => "CONST infsum (λx. t) {x. P}"
print_translation ‹
  [(🍋‹infsum›, K (Collect_binder_tr' 🍋‹_qinfsum›))]
 ›

subsection ‹General properties›

lemma infsumI:
  fixes f g :: ‹'a ==> 'b::{comm_monoid_add, t2_space}›
  assumes ‹(f has_sum x) A›
  shows ‹infsum f A = x›
  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 :: ‹'a ==> 'b::{comm_monoid_add, t2_space}›
  assumes ‹x = y›
  assumes ‹(f has_sum x) A›
  assumes ‹(g has_sum y) B›
  shows ‹infsum f A = infsum g B›
  using assms infsumI by blast

lemma infsum_eqI':
  fixes f g :: ‹'a ==> 'b::{comm_monoid_add, t2_space}›
  assumes ‹∧x. (f has_sum x) A ⟷ (g has_sum x) B›
  shows ‹infsum f A = infsum g B›
  by (metis assms infsum_def infsum_eqI summable_on_def)

lemma infsum_not_exists:
  fixes f :: ‹'a ==> 'b::{comm_monoid_add, t2_space}›
  assumes ‹¬ f summable_on A›
  shows ‹infsum f A = 0›
  by (simp add: assms infsum_def)

lemma has_sum_unique:
  fixes f :: "_ ==> 'a :: {topological_comm_monoid_add, t2_space}"
  assumes "(f has_sum x) A" "(f has_sum y) A"
  shows "x = y"
  using assms infsumI by blast

lemma summable_iff_has_sum_infsum: "f summable_on A ⟷ (f has_sum (infsum f A)) A"
  using infsumI summable_on_def by blast

lemma has_sum_iff: "(f has_sum S) A ⟷ f summable_on A ∧ infsum f A = S"
  using infsumI summable_iff_has_sum_infsum by blast

lemma has_sum_infsum[simp]:
  assumes ‹f summable_on S›
  shows ‹(f has_sum (infsum f S)) S›
  using assms summable_iff_has_sum_infsum by blast

lemma has_sum_cong_neutral:
  fixes f g :: ‹'a ==> 'b::{comm_monoid_add, topological_space}›
  assumes ‹∧x. x∈T-S ==> g x = 0›
  assumes ‹∧x. x∈S-T ==> f x = 0›
  assumes ‹∧x. x∈S∩T ==> f x = g x›
  shows "(f has_sum x) S ⟷ (g has_sum x) T"
proof -
  have ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))
  = eventually P (filtermap (sum g) (finite_subsets_at_top T))›
  proof 
    assume ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))›
    then obtain F0 where ‹finite F0› and ‹F0 ⊆ S› and F0_P: ‹∧F. finite F ==> F ⊆ S ==> F ?? F0 ==> P (sum f F)›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where ‹F0' = F0 ∩ T›
    have [simp]: ‹finite F0'› ‹F0' ⊆ T›
      by (simp_all add: F0'_def ‹finite F0›)
    have ‹P (sum g F)› if ‹finite F› ‹F ⊆ T› ‹F 🪙 F0'› for F
    proof -
      have ‹P (sum f ((F∩S) ∪ (F0∩S)))›
        by (intro F0_P) (use ‹F0 ⊆ S› ‹finite F0› that in auto)
      also have ‹sum f ((F∩S) ∪ (F0∩S)) = sum g F›
        by (intro sum.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
      finally show ?thesis .
    qed
    with ‹F0' ⊆ T› ‹finite F0'› show ‹eventually P (filtermap (sum g) (finite_subsets_at_top T))›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  next
    assume ‹eventually P (filtermap (sum g) (finite_subsets_at_top T))›
    then obtain F0 where ‹finite F0› and ‹F0 ⊆ T› and F0_P: ‹∧F. finite F ==> F ⊆ T ==> F ?? F0 ==> P (sum g F)›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where ‹F0' = F0 ∩ S›
    have [simp]: ‹finite F0'› ‹F0' ⊆ S›
      by (simp_all add: F0'_def ‹finite F0›)
    have ‹P (sum f F)› if ‹finite F› ‹F ⊆ S› ‹F 🪙 F0'› for F
    proof -
      have ‹P (sum g ((F∩T) ∪ (F0∩T)))›
        by (intro F0_P) (use ‹F0 ⊆ T› ‹finite F0› that in auto)
      also have ‹sum g ((F∩T) ∪ (F0∩T)) = sum f F›
        by (intro sum.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
      finally show ?thesis .
    qed
    with ‹F0' ⊆ S› ‹finite F0'› show ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  qed

  then have tendsto_x: "(sum f ---> x) (finite_subsets_at_top S) ⟷ (sum g ---> 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 :: ‹'a ==> 'b::{comm_monoid_add, topological_space}›
  assumes ‹∧x. x∈T-S ==> g x = 0›
  assumes ‹∧x. x∈S-T ==> f x = 0›
  assumes ‹∧x. x∈S∩T ==> f x = g x›
  shows "f summable_on S ⟷ 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 :: ‹'a ==> 'b::{comm_monoid_add, t2_space}›
  assumes ‹∧x. x∈T-S ==> g x = 0›
  assumes ‹∧x. x∈S-T ==> f x = 0›
  assumes ‹∧x. x∈S∩T ==> f x = g x›
  shows ‹infsum f S = infsum g T›
  by (smt (verit, best) assms has_sum_cong_neutral infsum_eqI')

lemma has_sum_cong: 
  assumes "∧x. x∈A ==> f x = g x"
  shows "(f has_sum x) A ⟷ (g has_sum x) A"
  using assms by (intro has_sum_cong_neutral) auto

lemma summable_on_cong:
  assumes "∧x. x∈A ==> f x = g x"
  shows "f summable_on A ⟷ g summable_on A"
  by (metis assms summable_on_def has_sum_cong)

lemma infsum_cong:
  assumes "∧x. x∈A ==> 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 ==> '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 ---> x) (finite_subsets_at_top A)"
    unfolding summable_on_def has_sum_def by auto
  define F' where "F' = F∩A"
  with assms have "finite F'" and "A-F = A-F'"
    by auto
  have "filtermap ((∪)F') (finite_subsets_at_top (A-F))
      ≤ 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 ⊆ A" 
      and P: "∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ P Y"
      unfolding eventually_finite_subsets_at_top by auto
    define X' where "X' = X-F"
    hence [simp]: "finite X'" and [simp]: "X' ⊆ A-F"
      using XA by auto
    hence "finite Y ∧ X' ⊆ Y ∧ Y ⊆ A - F ⟶ P (F' ∪ Y)" for Y
      using P XA unfolding X'_def using F'_def ‹finite F'› by blast
    thus "eventually P (filtermap ((∪) 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 ---> x) (filtermap ((∪)F') (finite_subsets_at_top (A-F)))"
    using tendsto_mono by blast
  have "((λG. sum f (F' ∪ G)) ---> x) (finite_subsets_at_top (A - F))"
    if "((sum f ∘ (∪) F') ---> x) (finite_subsets_at_top (A - F))"
    using that unfolding o_def by auto
  hence "((λG. sum f (F' ∪ G)) ---> x) (finite_subsets_at_top (A-F))"
    using tendsto_compose_filtermap [symmetric]
    by (simp add: ‹(sum f ---> x) (filtermap ((∪) F') (finite_subsets_at_top (A - F)))›
        tendsto_compose_filtermap)
  have "∀Y. finite Y ∧ Y ⊆ A - F ⟶ sum f (F' ∪ Y) = sum f F' + sum f Y"
    by (metis Diff_disjoint Int_Diff ‹A - F = A - F'› ‹finite F'› inf.orderE sum.union_disjoint)
  hence "∀🪙F x in finite_subsets_at_top (A - F). sum f (F' ∪ x) = sum f F' + sum f x"
    unfolding eventually_finite_subsets_at_top
    using exI [where x = "{}"]
    by (simp add: ‹∧P. P {} ==> ∃x. P x›) 
  hence "((λG. sum f F' + sum f G) ---> x) (finite_subsets_at_top (A-F))"
    using tendsto_cong [THEN iffD1 , rotated]
      ‹((λG. sum f (F' ∪ G)) ---> x) (finite_subsets_at_top (A - F))› by fastforce
  hence "((λG. sum f F' + sum f G) ---> sum f F' + (x-sum f F')) (finite_subsets_at_top (A-F))"
    by simp
  hence "(sum f ---> 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 ==> 'b::{topological_ab_group_add}"
  assumes ‹(f has_sum b) B› and ‹(f has_sum a) A› and AB: "A ⊆ B"
  shows has_sum_Diff: "(f has_sum (b - a)) (B - A)"
proof -
  have finite_subsets1:
    "finite_subsets_at_top (B - A) ≤ filtermap (λF. F - A) (finite_subsets_at_top B)"
  proof (rule filter_leI)
    fix P assume "eventually P (filtermap (λF. F - A) (finite_subsets_at_top B))"
    then obtain X where "finite X" and "X ⊆ B" 
      and P: "finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P (Y - A)" for Y
      unfolding eventually_filtermap eventually_finite_subsets_at_top by auto

    hence "finite (X-A)" and "X-A ⊆ B - A"
      by auto
    moreover have "finite Y ∧ X-A ⊆ Y ∧ Y ⊆ B - A ⟶ P Y" for Y
      using P[where Y="Y∪X"] ‹finite X› ‹X ⊆ B›
      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 (λF. F ∩ A) (finite_subsets_at_top B) ≤ 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 ---> b) (finite_subsets_at_top B)"
    using has_sum_def by auto
  from assms(2) have limA: "(sum f ---> a) (finite_subsets_at_top A)"
    using has_sum_def by blast
  have "((λF. sum f (F∩A)) ---> a) (finite_subsets_at_top B)"
  proof (subst asm_rl [of "(λF. sum f (F∩A)) = sum f ∘ (λF. F∩A)"])
    show "(λF. sum f (F ∩ A)) = sum f ∘ (λF. F ∩ A)"
      unfolding o_def by auto
    show "((sum f ∘ (λF. F ∩ A)) ---> a) (finite_subsets_at_top B)"
      unfolding o_def 
      using tendsto_compose_filtermap finite_subsets2 limA tendsto_mono
        ‹(λF. sum f (F ∩ A)) = sum f ∘ (λF. F ∩ A)› by fastforce
  qed

  with limB have 🍋: "((λF. sum f F - sum f (F∩A)) ---> b - a) (finite_subsets_at_top B)"
    using tendsto_diff by blast
  have "sum f X - sum f (X ∩ A) = sum f (X - A)" if "finite X" and "X ⊆ B" for X :: "'a set"
    using that by (metis add_diff_cancel_left' sum.Int_Diff)
  hence "∀🪙F x in finite_subsets_at_top B. sum f x - sum f (x ∩ A) = sum f (x - A)"
    by (rule eventually_finite_subsets_at_top_weakI)  
  hence "((λF. sum f (F-A)) ---> b - a) (finite_subsets_at_top B)"
    using 🍋 tendsto_cong by fastforce
  hence "(sum f ---> b - a) (filtermap (λF. F-A) (finite_subsets_at_top B))"
    by (subst tendsto_compose_filtermap[symmetric], simp add: o_def)
  thus ?thesis
    using finite_subsets1 has_sum_def tendsto_mono by blast
qed


lemma
  fixes f :: "'a ==> 'b::{topological_ab_group_add}"
  assumes "f summable_on B" and "f summable_on A" and "A ⊆ B"
  shows summable_on_Diff: "f summable_on (B-A)"
  by (meson assms summable_on_def has_sum_Diff)

lemma
  fixes f :: "'a ==> 'b::{topological_ab_group_add,t2_space}"
  assumes "f summable_on B" and "f summable_on A" and AB: "A ⊆ B"
  shows infsum_Diff: "infsum f (B - A) = infsum f B - infsum f A"
  by (metis AB assms has_sum_Diff infsumI summable_on_def)

lemma has_sum_mono_neutral:
  fixes f :: "'a==>'b::{ordered_comm_monoid_add,linorder_topology}"
  (* Does this really require a linorder topology? (Instead of order topology.) *)
  assumes ‹(f has_sum a) A› and "(g has_sum b) B"
  assumes ‹∧x. x ∈ A∩B ==> f x ≤ g x›
  assumes ‹∧x. x ∈ A-B ==> f x ≤ 0›
  assumes ‹∧x. x ∈ B-A ==> g x ≥ 0›
  shows "a ≤ b"
proof -
  define f' g' where ‹f' x = (if x ∈ A then f x else 0)› and ‹g' x = (if x ∈ B then g x else 0)› for x
  have [simp]: ‹f summable_on A› ‹g summable_on B›
    using assms(1,2) summable_on_def by auto
  have ‹(f' has_sum a) (A∪B)›
    by (smt (verit, best) DiffE IntE Un_iff f'_def assms(1) has_sum_cong_neutral)
  then have f'_lim: ‹(sum f' ---> a) (finite_subsets_at_top (A∪B))›
    by (meson has_sum_def)
  have ‹(g' has_sum b) (A∪B)›
  by (smt (verit, best) DiffD1 DiffD2 IntE UnCI g'_def assms(2) has_sum_cong_neutral)
  then have g'_lim: ‹(sum g' ---> b) (finite_subsets_at_top (A∪B))›
    using has_sum_def by blast

  have "∧X i. [X ⊆ A ∪ B; i ∈ X] ==> f' i ≤ g' i"
    using assms by (auto simp: f'_def g'_def)
  then have ‹∀🪙F x in finite_subsets_at_top (A ∪ B). sum f' x ≤ sum g' x›
    by (intro eventually_finite_subsets_at_top_weakI sum_mono)
  then show ?thesis
    using f'_lim finite_subsets_at_top_neq_bot g'_lim tendsto_le by blast
qed

lemma infsum_mono_neutral:
  fixes f :: "'a==>'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" and "g summable_on B"
  assumes ‹∧x. x ∈ A∩B ==> f x ≤ g x›
  assumes ‹∧x. x ∈ A-B ==> f x ≤ 0›
  assumes ‹∧x. x ∈ B-A ==> g x ≥ 0›
  shows "infsum f A ≤ infsum g B"
  by (smt (verit, best) assms has_sum_infsum has_sum_mono_neutral)

lemma has_sum_mono:
  fixes f :: "'a==>'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum x) A" and "(g has_sum y) A"
  assumes ‹∧x. x ∈ A ==> f x ≤ g x›
  shows "x ≤ y"
  using assms has_sum_mono_neutral by force

lemma infsum_mono:
  fixes f :: "'a==>'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" and "g summable_on A"
  assumes ‹∧x. x ∈ A ==> f x ≤ g x›
  shows "infsum f A ≤ infsum g A"
  by (meson assms has_sum_infsum has_sum_mono)

lemma has_sum_finite[simp]:
  assumes "finite F"
  shows "(f has_sum (sum f 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 :: ‹'a ==> 'b::{comm_monoid_add,topological_space}›
  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"
  by (simp add: assms infsumI)

lemma has_sum_finiteI: "finite A ==> S = sum f A ==> (f has_sum S) A"
  by simp

lemma has_sum_strict_mono_neutral:
  fixes f :: "'a ==> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
  assumes ‹(f has_sum a) A› and "(g has_sum b) B"
  assumes ‹∧x. x ∈ A∩B ==> f x ≤ g x›
  assumes ‹∧x. x ∈ A-B ==> f x ≤ 0›
  assumes ‹∧x. x ∈ B-A ==> g x ≥ 0›
  assumes ‹x ∈ B› ‹if x ∈ A then f x 🚫 x else 0 🚫 x›
  shows "a < b"
proof -
  define y where "y = (if x ∈ A then f x else 0)"
  have "a - y ≤ b - g x"
  proof (rule has_sum_mono_neutral)
    show "(f has_sum (a - y)) (A - (if x ∈ A then {x} else {}))"
      by (intro has_sum_Diff assms has_sum_finiteI) (auto simp: y_def)
    show "(g has_sum (b - g x)) (B - {x})"
      by (intro has_sum_Diff assms has_sum_finiteI) (use assms in auto)
  qed (use assms in ‹auto split: if_splits›)
  moreover have "y < g x"
    using assms(3,4,5)[of x] assms(6-) by (auto simp: y_def split: if_splits)
  ultimately show ?thesis
    by (metis diff_strict_left_mono diff_strict_mono leD neqE)
qed

lemma has_sum_strict_mono:
  fixes f :: "'a ==> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
  assumes ‹(f has_sum a) A› and "(g has_sum b) A"
  assumes ‹∧x. x ∈ A ==> f x ≤ g x›
  assumes ‹x ∈ A› ‹f x 🚫 x›
  shows "a < b"
  using assms has_sum_strict_mono_neutral by force

lemma has_sum_finite_approximation:
  fixes f :: "'a ==> 'b::{comm_monoid_add,metric_space}"
  assumes "(f has_sum x) A" and "ε > 0"
  shows "∃F. finite F ∧ F ⊆ A ∧ dist (sum f F) x ≤ ε"
proof -
  have "(sum f ---> x) (finite_subsets_at_top A)"
    by (meson assms(1) has_sum_def)
  hence *: "∀🪙F F in (finite_subsets_at_top A). dist (sum f F) x < ε"
    using assms(2) by (rule tendstoD)
  thus ?thesis
    unfolding eventually_finite_subsets_at_top by fastforce
qed

lemma infsum_finite_approximation:
  fixes f :: "'a ==> 'b::{comm_monoid_add,metric_space}"
  assumes "f summable_on A" and "ε > 0"
  shows "∃F. finite F ∧ F ⊆ A ∧ dist (sum f F) (infsum f A) ≤ ε"
proof -
  from assms have "(f has_sum (infsum f A)) A"
    by (simp add: summable_iff_has_sum_infsum)
  from this and ‹ε > 0› show ?thesis
    by (rule has_sum_finite_approximation)
qed

lemma abs_summable_summable:
  fixes f :: ‹'a ==> 'b :: banach›
  assumes ‹f abs_summable_on A›
  shows ‹f summable_on A›
proof -
  from assms obtain L where lim: ‹(sum (λx. norm (f x)) ---> L) (finite_subsets_at_top A)›
    unfolding has_sum_def summable_on_def by blast
  then have *: ‹cauchy_filter (filtermap (sum (λx. norm (f x))) (finite_subsets_at_top A))›
    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)
  have ‹∃P. eventually P (finite_subsets_at_top A) ∧
  (∀F F'. P F ∧ P F' ⟶ dist (sum f F) (sum f F') 🚫)›
  proof -
    define d P where ‹d = e/4› and ‹P F ⟷ finite F ∧ F ⊆ A ∧ dist (sum (λx. norm (f x)) F) L 🚫› for F
    then have ‹d > 0›
      by (simp add: d_def that)
    have ev_P: ‹eventually P (finite_subsets_at_top A)›
      using lim
      by (auto simp add: P_def[abs_def] ‹0 🚫› eventually_conj_iff eventually_finite_subsets_at_top_weakI tendsto_iff)
    
    moreover have ‹dist (sum f F1) (sum f F2) 🚫› if ‹P F1› and ‹P F2› for F1 F2
    proof -
      from ev_P
      obtain F' where ‹finite F'› and ‹F' ⊆ A› and P_sup_F': ‹finite F ∧ F 🪙 F' ∧ F ⊆ A ==> P F› for F
        by atomize_elim (simp add: eventually_finite_subsets_at_top)
      define F where ‹F = F' ∪ F1 ∪ F2›
      have ‹finite F› and ‹F ⊆ A›
        using F_def P_def[abs_def] that ‹finite F'› ‹F' ⊆ A› by auto
      have dist_F: ‹dist (sum (λx. norm (f x)) F) L 🚫›
        by (metis F_def ‹F ⊆ A› P_def P_sup_F' ‹finite F› le_supE order_refl)

      have dist_F_subset: ‹dist (sum f F) (sum f F') 🚫*d› if F': ‹F' ⊆ F› ‹P F'› for F'
      proof -
        have ‹dist (sum f F) (sum f F') = norm (sum f (F-F'))›
          unfolding dist_norm using ‹finite F› F' by (subst sum_diff) auto
        also have ‹… ≤ norm (∑x∈F-F'. norm (f x))›
          by (rule order.trans[OF sum_norm_le[OF order.refl]]) auto
        also have ‹… = dist (∑x∈F. norm (f x)) (∑x∈F'. norm (f x))›
          unfolding dist_norm using ‹finite F› F' by (subst sum_diff) auto
        also have ‹… 🚫 * d›
          using dist_F F' unfolding P_def dist_norm real_norm_def by linarith
        finally show ‹dist (sum f F) (sum f F') 🚫*d› .
      qed

      have ‹dist (sum f F1) (sum f F2) ≤ dist (sum f F) (sum f F1) + dist (sum f F) (sum f F2)›
        by (rule dist_triangle3)
      also have ‹… 🚫 * d + 2 * d›
        by (intro add_strict_mono dist_F_subset that) (auto simp: F_def)
      also have ‹… ≤ e›
        by (auto simp: d_def)
      finally show ‹dist (sum f F1) (sum f F2) 🚫› .
    qed
    then show ?thesis
      using ev_P by blast
  qed
  then have ‹cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))›
    by (simp add: cauchy_filter_metric_filtermap)
  moreover have "complete (UNIV::'b set)"
    by (meson Cauchy_convergent UNIV_I complete_def convergent_def)
  ultimately obtain L' where ‹(sum f ---> L') (finite_subsets_at_top A)›
    using complete_uniform[where S=UNIV] by (force simp add: filterlim_def)
  then show ?thesis
    using summable_on_def has_sum_def by blast
qed

text ‹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 🍋‹¬ f abs_summable_on UNIV› b
  and thus the sum over $\lVert f(i)\rVert$ diverges. On the other hand, we have 🍋‹f summable_on UNIV›;
  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.)›

lemma norm_has_sum_bound:
  fixes f :: "'b ==> 'a::real_normed_vector"
    and A :: "'b set"
  assumes "((λx. norm (f x)) has_sum n) A"
  assumes "(f has_sum a) A"
  shows "norm a ≤ n"
proof -
  have "norm a ≤ n + ε" if "ε>0" for ε
  proof-
    have "∃F. norm (a - sum f F) ≤ ε ∧ finite F ∧ F ⊆ A"
      using has_sum_finite_approximation[where A=A and f=f and ε="ε"] assms ‹0 🚫ε›
      by (metis dist_commute dist_norm)
    then obtain F where "norm (a - sum f F) ≤ ε"
      and "finite F" and "F ⊆ A"
      by (simp add: atomize_elim)
    hence "norm a ≤ norm (sum f F) + ε"
      by (metis add.commute diff_add_cancel dual_order.refl norm_triangle_mono)
    also have "… ≤ sum (λx. norm (f x)) F + ε"
      using norm_sum by auto
    also have "… ≤ n + ε"
    proof (intro add_right_mono [OF has_sum_mono_neutral])
      show "((λx. norm (f x)) has_sum (∑x∈F. norm (f x))) F"
        by (simp add: ‹finite F›)
    qed (use ‹F ⊆ A› assms in 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 ==> 'a::real_normed_vector"
    and A :: "'b set"
  assumes "f abs_summable_on A"
  shows "norm (infsum f A) ≤ infsum (λx. norm (f x)) A"
proof (cases "f summable_on A")
  case True
  have "((λx. norm (f x)) has_sum (∑🪙∞x∈A. norm (f x))) A"
    by (simp add: assms)
  then show ?thesis
    by (metis True has_sum_infsum norm_has_sum_bound)
next
  case False
  obtain t where t_def: "(sum (λx. norm (f x)) ---> t) (finite_subsets_at_top A)"
    using assms unfolding summable_on_def has_sum_def by blast
  have sumpos: "sum (λx. norm (f x)) X ≥ 0"
    for X
    by (simp add: sum_nonneg)
  have tgeq0:"t ≥ 0"
  proof(rule ccontr)
    define S::"real set" where "S = {s. s < 0}"
    assume "¬ 0 ≤ t"
    hence "t < 0" by simp
    hence "t ∈ S"
      unfolding S_def by blast
    moreover have "open S"
      by (metis S_def lessThan_def open_real_lessThan)
    ultimately have "∀🪙F X in finite_subsets_at_top A. (∑x∈X. norm (f x)) ∈ S"
      using t_def unfolding tendsto_def by blast
    hence "∃X. (∑x∈X. norm (f x)) ∈ S"
      by (metis (no_types, lifting) eventually_mono filterlim_iff finite_subsets_at_top_neq_bot tendsto_Lim)
    then obtain X where "(∑x∈X. norm (f x)) ∈ S"
      by blast
    hence "(∑x∈X. norm (f x)) < 0"
      unfolding S_def by auto      
    thus False by (simp add: leD sumpos)
  qed
  have "∃!h. (sum (λx. norm (f x)) ---> 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 (λx. norm (f x))))"
    using t_def unfolding Topological_Spaces.Lim_def
    by (metis the_equality)     
  hence "Lim (finite_subsets_at_top A) (sum (λx. norm (f x))) ≥ 0"
    using tgeq0 by blast
  thus ?thesis unfolding infsum_def 
    using False by auto
qed

lemma infsum_tendsto:
  assumes ‹f summable_on S›
  shows ‹((λF. sum f F) ---> infsum f S) (finite_subsets_at_top S)›
  using assms has_sum_def has_sum_infsum by blast

lemma has_sum_0: 
  assumes ‹∧x. x∈M ==> f x = 0›
  shows ‹(f has_sum 0) M›
  by (metis assms finite.intros(1) has_sum_cong has_sum_cong_neutral has_sum_finite sum.neutral_const)

lemma summable_on_0:
  assumes ‹∧x. x∈M ==> f x = 0›
  shows ‹f summable_on M›
  using assms summable_on_def has_sum_0 by blast

lemma infsum_0:
  assumes ‹∧x. x∈M ==> f x = 0›
  shows ‹infsum f M = 0›
  by (metis assms finite_subsets_at_top_neq_bot infsum_def has_sum_0 has_sum_def tendsto_Lim)

text ‹Variants of @{thm [source] infsum_0} etc. suitable as simp-rules›
lemma infsum_0_simp[simp]: ‹infsum (λ_. 0) M = 0›
  by (simp_all add: infsum_0)

lemma summable_on_0_simp[simp]: ‹(λ_. 0) summable_on M›
  by (simp_all add: summable_on_0)

lemma has_sum_0_simp[simp]: ‹((λ_. 0) has_sum 0) M›
  by (simp_all add: has_sum_0)


lemma has_sum_add:
  fixes f g :: "'a ==> 'b::{topological_comm_monoid_add}"
  assumes ‹(f has_sum a) A›
  assumes ‹(g has_sum b) A›
  shows ‹((λx. f x + g x) has_sum (a + b)) A›
proof -
  from assms have lim_f: ‹(sum f ---> a) (finite_subsets_at_top A)›
    and lim_g: ‹(sum g ---> b) (finite_subsets_at_top A)›
    by (simp_all add: has_sum_def)
  then have lim: ‹(sum (λx. f x + g x) ---> a + b) (finite_subsets_at_top A)›
    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 ==> 'b::{topological_comm_monoid_add}"
  assumes ‹f summable_on A›
  assumes ‹g summable_on A›
  shows ‹(λx. f x + g x) summable_on A›
  by (metis (full_types) assms summable_on_def has_sum_add)

lemma infsum_add:
  fixes f g :: "'a ==> 'b::{topological_comm_monoid_add, t2_space}"
  assumes ‹f summable_on A›
  assumes ‹g summable_on A›
  shows ‹infsum (λx. f x + g x) A = infsum f A + infsum g A›
proof -
  have ‹((λx. f x + g x) has_sum (infsum f A + infsum g A)) A›
    by (simp add: assms has_sum_add)
  then show ?thesis
    using infsumI by blast
qed


lemma has_sum_Un_disjoint:
  fixes f :: "'a ==> 'b::topological_comm_monoid_add"
  assumes "(f has_sum a) A"
  assumes "(f has_sum b) B"
  assumes disj: "A ∩ B = {}"
  shows ‹(f has_sum (a + b)) (A ∪ B)›
proof -
  define fA fB where ‹fA x = (if x ∈ A then f x else 0)›
    and ‹fB x = (if x ∉ A then f x else 0)› for x
  have fA: ‹(fA has_sum a) (A ∪ B)›
    by (smt (verit, ccfv_SIG) DiffD1 DiffD2 UnCI fA_def assms(1) has_sum_cong_neutral inf_sup_absorb)
  have fB: ‹(fB has_sum b) (A ∪ B)›
    by (smt (verit, best) DiffD1 DiffD2 IntE Un_iff fB_def assms(2) disj disjoint_iff has_sum_cong_neutral)
  have fAB: ‹f x = fA x + fB x› 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 ==> 'b::topological_comm_monoid_add"
  assumes "f summable_on A"
  assumes "f summable_on B"
  assumes disj: "A ∩ B = {}"
  shows ‹f summable_on (A ∪ B)›
  by (meson assms disj summable_on_def has_sum_Un_disjoint)

lemma infsum_Un_disjoint:
  fixes f :: "'a ==> 'b::{topological_comm_monoid_add, t2_space}"
  assumes "f summable_on A"
  assumes "f summable_on B"
  assumes disj: "A ∩ B = {}"
  shows ‹infsum f (A ∪ B) = infsum f A + infsum f B›
  by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)  

lemma norm_summable_imp_has_sum:
  fixes f :: "nat ==> 'a :: banach"
  assumes "summable (λn. norm (f n))" and "f sums S"
  shows   "(f has_sum S) (UNIV :: nat set)"
  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
proof clarsimp
  fix ε::real 
  assume "ε > 0"
  from assms obtain S' where S': "(λn. norm (f n)) sums S'"
    by (auto simp: summable_def)
  with ‹ε > 0› obtain N where N: "∧n. n ≥ N ==> ∣S' - (∑i∣ < ε"
    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
  have "dist (sum f Y) S < ε" if "finite Y" "{..⊆ Y" for Y
  proof -
    from that have "(λn. if n ∈ Y then 0 else f n) sums (S - sum f Y)"
      by (intro sums_If_finite_set'[OF ‹f sums S›]) (auto simp: sum_negf)
    hence "S - sum f Y = (∑n. if n ∈ Y then 0 else f n)"
      by (simp add: sums_iff)
    also have "norm … ≤ (∑n. norm (if n ∈ Y then 0 else f n))"
      by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
    also have "… ≤ (∑n. if n < N then 0 else norm (f n))"
      using that by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
    also have "(λn. if n ∈ {..∑i 
      by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
    hence "(∑n. if n < N then 0 else norm (f n)) = S' - (∑i
      by (simp add: sums_iff)
    also have "S' - (∑i≤ ∣S' - (∑i∣" by simp
    also have "… < ε" by (rule N) auto
    finally show ?thesis by (simp add: dist_norm norm_minus_commute)
  qed
  then show "∃X. finite X ∧ (∀Y. finite Y ∧ X ⊆ Y ⟶ dist (sum f Y) S < ε)"
    by (meson finite_lessThan subset_UNIV)
qed

lemma norm_summable_imp_summable_on:
  fixes f :: "nat ==> 'a :: banach"
  assumes "summable (λn. norm (f n))"
  shows   "f summable_on UNIV"
  using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
  by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)

lemma sums_nonneg_imp_has_sum_strong:
  assumes "f sums (S::real)" "eventually (λn. f n ≥ 0) sequentially"
  shows   "(f has_sum S) UNIV"
proof -
  from assms(2) obtain N where N: "∧n. n ≥ N ==> f n ≥ 0"
    by (auto simp: eventually_at_top_linorder)
  from assms(1) have "summable f"
    by (simp add: sums_iff)
  hence "summable (λn. f (n + N))"
    by (rule summable_ignore_initial_segment)
  hence "summable (λn. norm (f (n + N)))"
    using N by simp
  hence "summable (λn. norm (f n))"
    using summable_iff_shift by blast
  with assms(1) show ?thesis
    using norm_summable_imp_has_sum by blast
qed

lemma sums_nonneg_imp_has_sum:
  assumes "f sums (S::real)" and "∧n. f n ≥ 0"
  shows   "(f has_sum S) UNIV"
  by (rule sums_nonneg_imp_has_sum_strong) (use assms in auto)

lemma summable_nonneg_imp_summable_on_strong:
  assumes "summable f" "eventually (λn. f n ≥ (0::real)) sequentially"
  shows   "f summable_on UNIV"
  using assms has_sum_iff sums_nonneg_imp_has_sum_strong by blast

lemma summable_nonneg_imp_summable_on:
  assumes "summable f" "∧n. f n ≥ (0::real)"
  shows   "f summable_on UNIV"
  by (rule summable_nonneg_imp_summable_on_strong) (use assms in auto)

text ‹The following lemma indeed needs a complete space (as formalized by the premise 🍋‹complete UNIV›).
  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.›

lemma summable_on_subset_aux:
  fixes A B and f :: ‹'a ==> 'b::{ab_group_add, uniform_space}›
  assumes ‹complete (UNIV :: 'b set)›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'b,y). x+y)›
  assumes ‹f summable_on A›
  assumes ‹B ⊆ A›
  shows ‹f summable_on B›
proof -
  let ?filter_fB = ‹filtermap (sum f) (finite_subsets_at_top B)›
  from ‹f summable_on A›
  obtain S where ‹(sum f ---> S) (finite_subsets_at_top A)› (is ‹(sum f ---> S) ?filter_A›)
    using summable_on_def has_sum_def by blast
  then have cauchy_fA: ‹cauchy_filter (filtermap (sum f) (finite_subsets_at_top A))› (is ‹cauchy_filter ?filter_fA›)
    by (auto intro!: nhds_imp_cauchy_filter simp: filterlim_def)

  have ‹cauchy_filter (filtermap (sum f) (finite_subsets_at_top B))›
  proof (unfold cauchy_filter_def, rule filter_leI)
    fix E :: ‹('b×'b) ==> bool› assume ‹eventually E uniformity›
    then obtain E' where ‹eventually E' uniformity› and E'E'E: ‹E' (x, y) ⟶ E' (y, z) ⟶ E (x, z)› for x y z
      using uniformity_trans by blast
    obtain D where ‹eventually D uniformity› and DE: ‹D (x, y) ==> E' (x+c, y+c)› for x y c
      using plus_cont ‹eventually E' uniformity›
      unfolding uniformly_continuous_on_uniformity filterlim_def le_filter_def uniformity_prod_def
      by (auto simp: case_prod_beta eventually_filtermap eventually_prod_same uniformity_refl)
    have DE': "E' (x, y)" if "D (x + c, y + c)" for x y c
      using DE[of "x + c" "y + c" "-c"] that by simp

    from ‹eventually D uniformity› and cauchy_fA have ‹eventually D (?filter_fA ×🪙F ?filter_fA)›
      unfolding cauchy_filter_def le_filter_def by simp
    then obtain P1 P2
      where ev_P1: ‹eventually (λF. P1 (sum f F)) ?filter_A›
        and ev_P2: ‹eventually (λF. P2 (sum f F)) ?filter_A›
        and P1P2E: ‹P1 x ==> P2 y ==> D (x, y)› for x y
      unfolding eventually_prod_filter eventually_filtermap
      by auto
    from ev_P1 obtain F1 where F1: ‹finite F1› ‹F1 ⊆ A› ‹∧F. F🪙F1 ==> finite F ==> F⊆A ==> P1 (sum f F)›
      by (metis eventually_finite_subsets_at_top)
    from ev_P2 obtain F2 where F2: ‹finite F2› ‹F2 ⊆ A› ‹∧F. F🪙F2 ==> finite F ==> F⊆A ==> P2 (sum f F)›
      by (metis eventually_finite_subsets_at_top)
    define F0 F0A F0B where ‹F0 ≡ F1 ∪ F2› and ‹F0A ≡ F0 - B› and ‹F0B ≡ F0 ∩ B›
    have [simp]: ‹finite F0›  ‹F0 ⊆ A›
      using ‹F1 ⊆ A› ‹F2 ⊆ A› ‹finite F1› ‹finite F2› unfolding F0_def by blast+
 
    have *: "E' (sum f F1', sum f F2')"
      if "F1'🪙F0B" "F2'🪙F0B" "finite F1'" "finite F2'" "F1'⊆B" "F2'⊆B" for F1' F2'
    proof (intro DE'[where c = "sum f F0A"] P1P2E)
      have "P1 (sum f (F1' ∪ F0A))"
        using that assms F1(1,2) F2(1,2) by (intro F1) (auto simp: F0A_def F0B_def F0_def)
      thus "P1 (sum f F1' + sum f F0A)"
        by (subst (asm) sum.union_disjoint) (use that in ‹auto simp: F0A_def›)
    next
      have "P2 (sum f (F2' ∪ F0A))"
        using that assms F1(1,2) F2(1,2) by (intro F2) (auto simp: F0A_def F0B_def F0_def)
      thus "P2 (sum f F2' + sum f F0A)"
        by (subst (asm) sum.union_disjoint) (use that in ‹auto simp: F0A_def›)      
    qed

    have "eventually (λx. E' (x, sum f F0B)) (filtermap (sum f) (finite_subsets_at_top B))"
     and "eventually (λx. E' (sum f F0B, x)) (filtermap (sum f) (finite_subsets_at_top B))"
        unfolding eventually_filtermap eventually_finite_subsets_at_top
        by (rule exI[of _ F0B]; use * in ‹force simp: F0B_def›)+
      then 
    show ‹eventually E (?filter_fB ×🪙F ?filter_fB)›
      unfolding eventually_prod_filter
      using E'E'E by blast
  qed

  then obtain x where ‹?filter_fB ≤ nhds x›
    using cauchy_filter_complete_converges[of ?filter_fB UNIV] ‹complete (UNIV :: _)›
    by (auto simp: filtermap_bot_iff)
  then have ‹(sum f ---> x) (finite_subsets_at_top B)›
    by (auto simp: filterlim_def)
  then show ?thesis
    by (auto simp: summable_on_def has_sum_def)
qed

text ‹A special case of @{thm [source] summable_on_subset_aux} for Banach spaces with fewer premises.›

lemma summable_on_subset_banach:
  fixes A B and f :: ‹'a ==> 'b::banach›
  assumes ‹f summable_on A›
  assumes ‹B ⊆ A›
  shows ‹f summable_on B›
  by (meson Cauchy_convergent UNIV_I assms complete_def convergent_def isUCont_plus summable_on_subset_aux)

lemma has_sum_empty[simp]: ‹(f has_sum 0) {}›
  by (meson ex_in_conv has_sum_0)

lemma summable_on_empty[simp]: ‹f summable_on {}›
  by auto

lemma infsum_empty[simp]: ‹infsum f {} = 0›
  by simp

lemma sum_has_sum:
  fixes f :: "'a ==> 'b::topological_comm_monoid_add"
  assumes ‹finite A›
  assumes ‹∧a. a ∈ A ==> (f has_sum (s a)) (B a)›
  assumes ‹∧a a'. a∈A ==> a'∈A ==> a≠a' ==> B a ∩ B a' = {}›
  shows ‹(f has_sum (sum s A)) (∪a∈A. B a)›
  using assms 
proof (induction)
  case empty
  then show ?case 
    by simp
next
  case (insert x A)
  have ‹(f has_sum (s x)) (B x)›
    by (simp add: insert.prems)
  moreover have IH: ‹(f has_sum (sum s A)) (∪a∈A. B a)›
    using insert by simp
  ultimately have ‹(f has_sum (s x + sum s A)) (B x ∪ (∪a∈A. B a))›
    using insert by (intro has_sum_Un_disjoint) auto
  then show ?case
    using insert.hyps by auto
qed


lemma summable_on_finite_union_disjoint:
  fixes f :: "'a ==> 'b::topological_comm_monoid_add"
  assumes finite: ‹finite A›
  assumes conv: ‹∧a. a ∈ A ==> f summable_on (B a)›
  assumes disj: ‹∧a a'. a∈A ==> a'∈A ==> a≠a' ==> B a ∩ B a' = {}›
  shows ‹f summable_on (∪a∈A. B a)›
  using sum_has_sum [of A f B] assms unfolding summable_on_def by metis

lemma sum_infsum:
  fixes f :: "'a ==> 'b::{topological_comm_monoid_add, t2_space}"
  assumes finite: ‹finite A›
  assumes conv: ‹∧a. a ∈ A ==> f summable_on (B a)›
  assumes disj: ‹∧a a'. a∈A ==> a'∈A ==> a≠a' ==> B a ∩ B a' = {}›
  shows ‹sum (λa. infsum f (B a)) A = infsum f (∪a∈A. B a)›
  by (metis (no_types, lifting) assms has_sum_infsum infsumI sum_has_sum)

text ‹The lemmas ‹infsum_comm_additive_general› and ‹infsum_comm_additive› (and variants) below both state that the infinite sum commutes with
  a continuous additive function. ‹infsum_comm_additive_general› 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 🍋‹additive› which introduces an additional sort constraint
  (group instead of monoid). For example, extended reals (🍋‹ereal›, 🍋‹ennreal›) are not covered
  by ‹infsum_comm_additive›.›


lemma has_sum_comm_additive_general: 
  fixes f :: ‹'b :: {comm_monoid_add,topological_space} ==> 'c :: {comm_monoid_add,topological_space}›
  assumes f_sum: ‹∧F. finite F ==> F ⊆ S ==> sum (f ∘ g) F = f (sum g F)›
      🍋 ‹Not using 🍋‹additive› because it would add sort constraint 🍋‹ab_group_add›\<close>
  assumes cont: ‹f ←-x→ f x›
    🍋 ‹For 🍋‹t2_space›, this is equivalent to ‹isCont f x› by @{thm [source] isCont_def}.›
  assumes infsum: ‹(g has_sum x) S›
  shows ‹((f ∘ g) has_sum (f x)) S›
proof -
  have ‹(sum g ---> x) (finite_subsets_at_top S)›
    using infsum has_sum_def by blast
  then have ‹((f ∘ sum g) ---> f x) (finite_subsets_at_top S)›
    by (meson cont filterlim_def tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap tendsto_mono)
  then have ‹(sum (f ∘ g) ---> f x) (finite_subsets_at_top S)›
    using tendsto_cong f_sum
    by (simp add: Lim_transform_eventually eventually_finite_subsets_at_top_weakI)
  then show ‹((f ∘ g) has_sum (f x)) S›
    using has_sum_def by blast 
qed

lemma summable_on_comm_additive_general:
  fixes f :: ‹'b :: {comm_monoid_add,topological_space} ==> 'c :: {comm_monoid_add,topological_space}›
  assumes ‹∧F. finite F ==> F ⊆ S ==> sum (f ∘ g) F = f (sum g F)›
    🍋 ‹Not using 🍋‹additive› because it would add sort constraint 🍋‹ab_group_add›\›
  assumes ‹∧x. (g has_sum x) S ==> f ←-x→ f x›
    🍋 ‹For 🍋‹t2_space›, this is equivalent to ‹isCont f x› by @{thm [source] isCont_def}.›
  assumes ‹g summable_on S›
  shows ‹(f ∘ g) summable_on S›
  by (meson assms summable_on_def has_sum_comm_additive_general has_sum_def infsum_tendsto)

lemma infsum_comm_additive_general:
  fixes f :: ‹'b :: {comm_monoid_add,t2_space} ==> 'c :: {comm_monoid_add,t2_space}›
  assumes f_sum: ‹∧F. finite F ==> F ⊆ S ==> sum (f ∘ g) F = f (sum g F)›
      🍋 ‹Not using 🍋‹additive› because it would add sort constraint 🍋‹ab_group_add›\›
  assumes ‹isCont f (infsum g S)›
  assumes ‹g summable_on S›
  shows ‹infsum (f ∘ g) S = f (infsum g S)›
  using assms
  by (intro infsumI has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def)

lemma has_sum_comm_additive: 
  fixes f :: ‹'b :: {ab_group_add,topological_space} ==> 'c :: {ab_group_add,topological_space}›
  assumes ‹additive f›
  assumes ‹f ←-x→ f x›
    🍋 ‹For 🍋‹t2_space›, this is equivalent to ‹isCont f x› by @{thm [source] isCont_def}.›
  assumes infsum: ‹(g has_sum x) S›
  shows ‹((f ∘ g) has_sum (f x)) S›
  using assms
  by (intro has_sum_comm_additive_general has_sum_infsum) (auto simp: isCont_def additive.sum) 

lemma summable_on_comm_additive:
  fixes f :: ‹'b :: {ab_group_add,t2_space} ==> 'c :: {ab_group_add,topological_space}›
  assumes ‹additive f›
  assumes ‹isCont f (infsum g S)›
  assumes ‹g summable_on S›
  shows ‹(f ∘ g) summable_on S›
  by (meson assms summable_on_def has_sum_comm_additive has_sum_infsum isContD)

lemma infsum_comm_additive:
  fixes f :: ‹'b :: {ab_group_add,t2_space} ==> 'c :: {ab_group_add,t2_space}›
  assumes ‹additive f›
  assumes ‹isCont f (infsum g S)›
  assumes ‹g summable_on S›
  shows ‹infsum (f ∘ g) S = f (infsum g S)›
  by (rule infsum_comm_additive_general; auto simp: assms additive.sum)

lemma nonneg_bdd_above_has_sum:
  fixes f :: ‹'a ==> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  assumes ‹bdd_above (sum f ` {F. F⊆A ∧ finite F})›
  shows ‹(f has_sum (SUP F∈{F. finite F ∧ F⊆A}. sum f F)) A›
proof -
  have ‹(sum f ---> (SUP F∈{F. finite F ∧ F⊆A}. sum f F)) (finite_subsets_at_top A)›
  proof (rule order_tendstoI)
    fix a assume ‹a 🚫SUP F∈{F. finite F ∧ F⊆A}. sum f F)›
    then obtain F where ‹a 🚫 f F› and ‹finite F› and ‹F ⊆ A›
      by (metis (mono_tags, lifting) Collect_cong Collect_empty_eq assms(2) empty_subsetI finite.emptyI less_cSUP_iff mem_Collect_eq)
    have "∧Y. [finite Y; F ⊆ Y; Y ⊆ A] ==> a < sum f Y"
      by (meson DiffE ‹a 🚫 f F› assms(1) less_le_trans subset_iff sum_mono2)
    then show ‹∀🪙F x in finite_subsets_at_top A. a 🚫 f x›
      by (metis ‹F ⊆ A› ‹finite F› eventually_finite_subsets_at_top)
  next
    fix a assume *: ‹(SUP F∈{F. finite F ∧ F⊆A}. sum f F) 🚫›
    have "sum f F ≤ (SUP F∈{F. finite F ∧ F⊆A}. sum f F)" if ‹F⊆A› and ‹finite F› for F
        by (rule cSUP_upper) (use that assms(2) in ‹auto simp: conj_commute›)
    then show ‹∀🪙F x in finite_subsets_at_top A. sum f x 🚫›
      by (metis (no_types, lifting) "*" eventually_finite_subsets_at_top_weakI order_le_less_trans)
  qed
  then show ?thesis
    using has_sum_def by blast
qed

lemma nonneg_bdd_above_summable_on:
  fixes f :: ‹'a ==> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  assumes ‹bdd_above (sum f ` {F. F⊆A ∧ finite F})›
  shows ‹f summable_on A›
  using assms summable_on_def nonneg_bdd_above_has_sum by blast

lemma nonneg_bdd_above_infsum:
  fixes f :: ‹'a ==> 'b :: {conditionally_complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  assumes ‹bdd_above (sum f ` {F. F⊆A ∧ finite F})›
  shows ‹infsum f A = (SUP F∈{F. finite F ∧ F⊆A}. sum f F)›
  using assms by (auto intro!: infsumI nonneg_bdd_above_has_sum)

lemma nonneg_has_sum_complete:
  fixes f :: ‹'a ==> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  shows ‹(f has_sum (SUP F∈{F. finite F ∧ F⊆A}. sum f F)) A›
  using assms nonneg_bdd_above_has_sum by blast

lemma nonneg_summable_on_complete:
  fixes f :: ‹'a ==> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  shows ‹f summable_on A›
  using assms nonneg_bdd_above_summable_on by blast

lemma nonneg_infsum_complete:
  fixes f :: ‹'a ==> 'b :: {complete_linorder, ordered_comm_monoid_add, linorder_topology}›
  assumes ‹∧x. x∈A ==> f x ≥ 0›
  shows ‹infsum f A = (SUP F∈{F. finite F ∧ F⊆A}. sum f F)›
  using assms nonneg_bdd_above_infsum by blast

lemma has_sum_nonneg:
  fixes f :: "'a ==> 'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum a) M"
    and "∧x. x ∈ M ==> 0 ≤ f x"
  shows "a ≥ 0"
  by (metis (no_types, lifting) DiffD1 assms empty_iff has_sum_0 has_sum_mono_neutral order_refl)

lemma infsum_nonneg:
  fixes f :: "'a ==> 'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "∧x. x ∈ M ==> 0 ≤ f x"
  shows "infsum f M ≥ 0" (is "?lhs ≥ _")
  by (metis assms has_sum_infsum has_sum_nonneg infsum_not_exists linorder_linear)

lemma has_sum_mono2:
  fixes f :: "'a ==> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum S) A" "(f has_sum S') B" "A ⊆ B"
  assumes "∧x. x ∈ B - A ==> f x ≥ 0"
  shows   "S ≤ S'"
  by (metis add_0 add_right_mono assms diff_add_cancel has_sum_Diff has_sum_nonneg)

lemma infsum_mono2:
  fixes f :: "'a ==> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" "f summable_on B" "A ⊆ B"
  assumes "∧x. x ∈ B - A ==> f x ≥ 0"
  shows   "infsum f A ≤ infsum f B"
  by (rule has_sum_mono2[OF has_sum_infsum has_sum_infsum]) (use assms in auto)

lemma finite_sum_le_has_sum:
  fixes f :: "'a ==> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "(f has_sum S) A" "finite B" "B ⊆ A"
  assumes "∧x. x ∈ A - B ==> f x ≥ 0"
  shows   "sum f B ≤ S"
  by (meson assms has_sum_finite has_sum_mono2)

lemma finite_sum_le_infsum:
  fixes f :: "'a ==> 'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" "finite B" "B ⊆ A"
  assumes "∧x. x ∈ A - B ==> f x ≥ 0"
  shows   "sum f B ≤ infsum f A"
  by (rule finite_sum_le_has_sum[OF has_sum_infsum]) (use assms in auto)

lemma has_sum_reindex:
  assumes ‹inj_on h A›
  shows ‹(g has_sum x) (h ` A) ⟷ ((g ∘ h) has_sum x) A›
proof -
  have ‹(g has_sum x) (h ` A) ⟷ (sum g ---> x) (finite_subsets_at_top (h ` A))›
    by (simp add: has_sum_def)
  also have ‹… ⟷ ((λF. sum g (h ` F)) ---> x) (finite_subsets_at_top A)›
    by (metis assms filterlim_filtermap filtermap_image_finite_subsets_at_top)
  also have ‹… ⟷ (sum (g ∘ h) ---> x) (finite_subsets_at_top A)›
  proof (intro tendsto_cong eventually_finite_subsets_at_top_weakI sum.reindex)
    show "∧X. [finite X; X ⊆ A] ==> inj_on h X"
      using assms inj_on_subset by blast
  qed
  also have ‹… ⟷ ((g ∘ h) has_sum x) A›
    by (simp add: has_sum_def)
  finally show ?thesis .
qed

lemma summable_on_reindex:
  assumes ‹inj_on h A›
  shows ‹g summable_on (h ` A) ⟷ (g ∘ h) summable_on A›
  by (simp add: assms summable_on_def has_sum_reindex)

lemma infsum_reindex:
  assumes ‹inj_on h A›
  shows ‹infsum g (h ` A) = infsum (g ∘ h) A›
  by (metis assms has_sum_infsum has_sum_reindex infsumI infsum_def)

lemma summable_on_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "(λx. f (g x)) summable_on A ⟷ f summable_on B"
  by (smt (verit) assms bij_betw_def o_apply summable_on_cong summable_on_reindex) 

lemma infsum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "infsum (λx. f (g x)) A = infsum f B"
  by (metis (mono_tags, lifting) assms bij_betw_def infsum_cong infsum_reindex o_def)

lemma sum_uniformity:
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'b::{uniform_space,comm_monoid_add},y). x+y)›
  assumes EE: ‹eventually E uniformity›
  obtains D where ‹eventually D uniformity›
    and ‹∧M::'a set. ∧f f' :: 'a ==> 'b. card M ≤ n ∧ (∀m∈M. D (f m, f' m)) ==> E (sum f M, sum f' M)›
proof (atomize_elim, insert EE, 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 ‹eventually D1 uniformity› and ‹eventually D2 uniformity›
    and D1D2E: ‹D1 (x, y) ==> D2 (x', y') ==> E (x + x', y + y')› 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 ‹eventually D2 uniformity›]
  obtain D3 where ‹eventually D3 uniformity› and D3: ‹card M ≤ n ==> (∀m∈M. D3 (f m, f' m)) ==> D2 (sum f M, sum f' M)›
    for M :: ‹'a set› and f f'
    by metis

  define D where ‹D x ≡ D1 x ∧ D3 x› for x
  have ‹eventually D uniformity›
    using D_def ‹eventually D1 uniformity› ‹eventually D3 uniformity› eventually_elim2 by blast

  have ‹E (sum f M, sum f' M)›
    if ‹card M ≤ Suc n› and DM: ‹∀m∈M. D (f m, f' m)›
    for M :: ‹'a set› and f f'
  proof (cases ‹card M = 0›)
    case True
    then show ?thesis
      by (metis Suc.prems card_eq_0_iff sum.empty sum.infinite uniformity_refl) 
  next
    case False
    with ‹card M ≤ Suc n› obtain N x where ‹card N ≤ n› and ‹x ∉ N› and ‹M = insert x N›
      by (metis card_Suc_eq less_Suc_eq_0_disj less_Suc_eq_le)

    from DM have ‹∧m. m∈N ==> D (f m, f' m)›
      using ‹M = insert x N› by blast
    with D3[OF ‹card N ≤ n›]
    have D2_N: ‹D2 (sum f N, sum f' N)›
      using D_def by blast

    from DM 
    have ‹D (f x, f' x)›
      using ‹M = insert x N› by blast
    then have ‹D1 (f x, f' x)›
      by (simp add: D_def)

    with D2_N
    have ‹E (f x + sum f N, f' x + sum f' N)›
      using D1D2E by presburger

    then show ‹E (sum f M, sum f' M)›
      by (metis False ‹M = insert x N› ‹x ∉ N› card.infinite finite_insert sum.insert)
  qed
  with ‹eventually D uniformity› show ?case 
    by auto
qed

lemma has_sum_Sigma:
  fixes A :: "'a set" and B :: "'a ==> 'b set"
    and f :: ‹'a × 'b ==> 'c::{comm_monoid_add,uniform_space}›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes summableAB: "(f has_sum a) (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> ((λy. f (x, y)) has_sum b x) (B x)›
  shows "(b has_sum a) A"
proof -
  define F FB FA where ‹F = finite_subsets_at_top (Sigma A B)› and ‹FB x = finite_subsets_at_top (B x)›
    and ‹FA = finite_subsets_at_top A› for x

  from summableB
  have sum_b: ‹(sum (λy. f (x, y)) ---> b x) (FB x)› if ‹x ∈ A› for x
    using FB_def[abs_def] has_sum_def that by auto
  from summableAB
  have sum_S: ‹(sum f ---> a) F›
    using F_def has_sum_def by blast

  have finite_proj: ‹finite {b| b. (a,b) ∈ H}› if ‹finite H› for H :: ‹('a×'b) set› and a
    by (metis (no_types, lifting) finite_imageI finite_subset image_eqI mem_Collect_eq snd_conv subsetI that)

  have ‹(sum b ---> a) FA›
  proof (rule tendsto_iff_uniformity[THEN iffD2, rule_format])
    fix E :: ‹('c × 'c) ==> bool›
    assume ‹eventually E uniformity›
    then obtain D where D_uni: ‹eventually D uniformity› and DDE': ‹∧x y z. D (x, y) ==> D (y, z) ==> E (x, z)›
      by (metis (no_types, lifting) ‹eventually E uniformity› uniformity_transE)
    from sum_S obtain G where ‹finite G› and ‹G ⊆ Sigma A B›
      and G_sum: ‹G ⊆ H ==> H ⊆ Sigma A B ==> finite H ==> D (sum f H, a)› for H
      unfolding tendsto_iff_uniformity
      by (metis (mono_tags, lifting) D_uni F_def eventually_finite_subsets_at_top)
    have ‹finite (fst ` G)› and ‹fst ` G ⊆ A›
      using ‹finite G› ‹G ⊆ Sigma A B› by auto
    thm uniformity_prod_def
    define Ga where ‹Ga a = {b. (a,b) ∈ G}› for a
    have Ga_fin: ‹finite (Ga a)› and Ga_B: ‹Ga a ⊆ B a› for a
      using ‹finite G› ‹G ⊆ Sigma A B› finite_proj by (auto simp: Ga_def finite_proj)

    have ‹E (sum b M, a)› if ‹M 🪙 fst ` G› and ‹finite M› and ‹M ⊆ A› for M
    proof -
      define FMB where ‹FMB = finite_subsets_at_top (Sigma M B)›
      have ‹eventually (λH. D (∑a∈M. b a, ∑(a,b)∈H. f (a,b))) FMB›
      proof -
        obtain D' where D'_uni: ‹eventually D' uniformity›
          and ‹card M' ≤ card M ∧ (∀m∈M'. D' (g m, g' m)) ==> D (sum g M', sum g' M')›
        for M' :: ‹'a set› and g g'
          using sum_uniformity[OF plus_cont ‹eventually D uniformity›] by blast
        then have D'_sum_D: ‹(∀m∈M. D' (g m, g' m)) ==> D (sum g M, sum g' M)› for g g'
          by auto

        obtain Ha where ‹Ha a 🪙 Ga a› and Ha_fin: ‹finite (Ha a)› and Ha_B: ‹Ha a ⊆ B a›
          and D'_sum_Ha: ‹Ha a ⊆ L ==> L ⊆ B a ==> finite L ==> D' (b a, sum (λb. f (a,b)) L)› if ‹a ∈ A› for a L
        proof -
          from sum_b[unfolded tendsto_iff_uniformity, rule_format, OF _ D'_uni[THEN uniformity_sym]]
          obtain Ha0 where ‹finite (Ha0 a)› and ‹Ha0 a ⊆ B a›
            and ‹Ha0 a ⊆ L ==> L ⊆ B a ==> finite L ==> D' (b a, sum (λb. f (a,b)) L)› if ‹a ∈ A› for a L
            unfolding FB_def eventually_finite_subsets_at_top unfolding prod.case by metis
          moreover define Ha where ‹Ha a = Ha0 a ∪ Ga a› for a
          ultimately show ?thesis
            using that[where Ha=Ha]
            using Ga_fin Ga_B by auto
        qed

        have ‹D (∑a∈M. b a, ∑(a,b)∈H. f (a,b))› if ‹finite H› and ‹H ⊆ Sigma M B› and ‹H 🪙 Sigma M Ha› for H
        proof -
          define Ha' where ‹Ha' a = {b| b. (a,b) ∈ H}› for a
          have [simp]: ‹finite (Ha' a)› and [simp]: ‹Ha' a 🪙 Ha a› and [simp]: ‹Ha' a ⊆ B a› if ‹a ∈ M› for a
            unfolding Ha'_def using ‹finite H› ‹H ⊆ Sigma M B› ‹Sigma M Ha ⊆ H› that finite_proj by auto
          have ‹Sigma M Ha' = H›
            using that by (auto simp: Ha'_def)
          then have *: ‹(∑(a,b)∈H. f (a,b)) = (∑a∈M. ∑b∈Ha' a. f (a,b))›
            by (simp add: ‹finite M› sum.Sigma)
          have ‹D' (b a, sum (λb. f (a,b)) (Ha' a))› if ‹a ∈ M› for a
            using D'_sum_Ha ‹M ⊆ A› that by auto
          then have ‹D (∑a∈M. b a, ∑a∈M. sum (λb. f (a,b)) (Ha' a))›
            by (rule_tac D'_sum_D, auto)
          with * show ?thesis
            by auto
        qed
        moreover have ‹Sigma M Ha ⊆ Sigma M B›
          using Ha_B ‹M ⊆ A› by auto
        ultimately show ?thesis
          unfolding FMB_def eventually_finite_subsets_at_top
          by (metis (no_types, lifting) Ha_fin finite_SigmaI subsetD that(2) that(3))
      qed
      moreover have ‹eventually (λH. D (∑(a,b)∈H. f (a,b), a)) FMB›
        unfolding FMB_def eventually_finite_subsets_at_top
      proof (rule exI[of _ G], safe)
        fix Y assume Y: "finite Y" "G ⊆ Y" "Y ⊆ Sigma M B"
        thus "D (∑(a,b)∈Y. f (a, b), a)"
          using G_sum[of Y] Y using that(3) by fastforce
      qed (use ‹finite G› ‹G ⊆ Sigma A B› that in auto)
      ultimately have ‹∀🪙F x in FMB. E (sum b M, a)›
        by eventually_elim (use DDE' in auto)
      then show ‹E (sum b M, a)›
        using FMB_def by force
    qed
    then show ‹∀🪙F x in FA. E (sum b x, a)›
      using ‹finite (fst ` G)› and ‹fst ` G ⊆ A›
      by (metis (mono_tags, lifting) 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 ==> 'b set"
    and f :: ‹'a ==> 'b ==> 'c::{comm_monoid_add, t2_space, uniform_space}›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes summableAB: "(λ(x,y). f x y) summable_on (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> (f x) summable_on (B x)›
  shows ‹(λx. infsum (f x) (B x)) summable_on A›
proof -
  from summableAB obtain a where a: ‹((λ(x,y). f x y) has_sum a) (Sigma A B)›
    using has_sum_infsum by blast
  from summableB have b: ‹∧x. x∈A ==> (f x has_sum infsum (f x) (B x)) (B x)›
    by (auto intro!: has_sum_infsum)
  show ?thesis
    using plus_cont a b
    by (smt (verit) has_sum_Sigma[where f=‹λ(x,y). f x y›] has_sum_cong old.prod.case summable_on_def) 
qed

lemma infsum_Sigma:
  fixes A :: "'a set" and B :: "'a ==> 'b set"
    and f :: ‹'a × 'b ==> 'c::{comm_monoid_add, t2_space, uniform_space}›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes summableAB: "f summable_on (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> (λy. f (x, y)) summable_on (B x)›
  shows "infsum f (Sigma A B) = infsum (λx. infsum (λy. f (x, y)) (B x)) A"
proof -
  from summableAB have a: ‹(f has_sum infsum f (Sigma A B)) (Sigma A B)›
    using has_sum_infsum by blast
  from summableB have b: ‹∧x. x∈A ==> ((λy. f (x, y)) has_sum infsum (λy. f (x, y)) (B x)) (B x)›
    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 ==> 'b set"
    and f :: ‹'a ==> 'b ==> 'c::{comm_monoid_add, t2_space, uniform_space}›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes summableAB: "(λ(x,y). f x y) summable_on (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> (f x) summable_on (B x)›
  shows ‹infsum (λx. infsum (f x) (B x)) A = infsum (λ(x,y). f x y) (Sigma A B)›
  using infsum_Sigma[of ‹λ(x,y). f x y› A B]
  using assms by auto

text ‹A special case of @{thm [source] infsum_Sigma} etc. for Banach spaces. It has less premises.›
lemma
  fixes A :: "'a set" and B :: "'a ==> 'b set"
    and f :: ‹'a ==> 'b ==> 'c::banach›
  assumes [simp]: "(λ(x,y). f x y) summable_on (Sigma A B)"
  shows infsum_Sigma'_banach: ‹infsum (λx. infsum (f x) (B x)) A = infsum (λ(x,y). f x y) (Sigma A B)› (is ?thesis1)
    and summable_on_Sigma_banach: ‹(λx. infsum (f x) (B x)) summable_on A› (is ?thesis2)
proof -
  have fsum: ‹(f x) summable_on (B x)› if ‹x ∈ A› for x
  proof -
    from assms
    have ‹(λ(x,y). f x y) summable_on (Pair x ` B x)›
      by (meson image_subset_iff summable_on_subset_banach mem_Sigma_iff that)
    then have ‹((λ(x,y). f x y) ∘ Pair x) summable_on (B x)›
      by (metis summable_on_reindex inj_on_def prod.inject)
    then show ?thesis
      by (auto simp: o_def)
  qed
  show ?thesis1
    using fsum assms infsum_Sigma' isUCont_plus by blast
  show ?thesis2
    using fsum assms isUCont_plus summable_on_Sigma by blast
qed

lemma infsum_Sigma_banach:
  fixes A :: "'a set" and B :: "'a ==> 'b set"
    and f :: ‹'a × 'b ==> 'c::banach›
  assumes [simp]: "f summable_on (Sigma A B)"
  shows ‹infsum (λx. infsum (λy. f (x,y)) (B x)) A = infsum f (Sigma A B)›
  using assms by (simp add: infsum_Sigma'_banach)

lemma infsum_swap:
  fixes A :: "'a set" and B :: "'b set"
  fixes f :: "'a ==> 'b ==> 'c::{comm_monoid_add,t2_space,uniform_space}"
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes ‹(λ(x, y). f x y) summable_on (A × B)›
  assumes ‹∧a. a∈A ==> (f a) summable_on B›
  assumes ‹∧b. b∈B ==> (λa. f a b) summable_on A›
  shows ‹infsum (λx. infsum (λy. f x y) B) A = infsum (λy. infsum (λx. f x y) A) B›
proof -
  have "(λ(x, y). f y x) ∘ prod.swap summable_on A × B"
    by (simp add: assms(2) summable_on_cong)
  then have fyx: ‹(λ(x, y). f y x) summable_on (B × A)›
    by (metis has_sum_reindex infsum_reindex inj_swap product_swap summable_iff_has_sum_infsum)
  have ‹infsum (λx. infsum (λy. f x y) B) A = infsum (λ(x,y). f x y) (A × B)›
    using assms infsum_Sigma' by blast
  also have ‹… = infsum (λ(x,y). f y x) (B × A)›
    apply (subst product_swap[symmetric])
    apply (subst infsum_reindex)
    using assms by (auto simp: o_def)
  also have ‹… = infsum (λy. infsum (λx. f x y) A) B›
    by (smt (verit) fyx assms(1) assms(4) infsum_Sigma' infsum_cong)
  finally show ?thesis .
qed

lemma infsum_swap_banach:
  fixes A :: "'a set" and B :: "'b set"
  fixes f :: "'a ==> 'b ==> 'c::banach"
  assumes ‹(λ(x, y). f x y) summable_on (A × B)›
  shows "infsum (λx. infsum (λy. f x y) B) A = infsum (λy. infsum (λx. f x y) A) B"
proof -
  have 🍋: ‹(λ(x, y). f y x) summable_on (B × A)›
    by (metis (mono_tags, lifting) assms case_swap inj_swap o_apply product_swap summable_on_cong summable_on_reindex)
  have ‹infsum (λx. infsum (λy. f x y) B) A = infsum (λ(x,y). f x y) (A × B)›
    using assms infsum_Sigma'_banach by blast
  also have ‹… = infsum (λ(x,y). f y x) (B × A)›
    apply (subst product_swap[symmetric])
    apply (subst infsum_reindex)
    using assms by (auto simp: o_def)
  also have ‹… = infsum (λy. infsum (λx. f x y) A) B›
    by (metis (mono_tags, lifting) 🍋 infsum_Sigma'_banach infsum_cong)
  finally show ?thesis .
qed

lemma nonneg_infsum_le_0D:
  fixes f :: "'a ==> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
  assumes "infsum f A ≤ 0"
    and abs_sum: "f summable_on A"
    and nneg: "∧x. x ∈ A ==> f x ≥ 0"
    and "x ∈ A"
  shows "f x = 0"
proof (rule ccontr)
  assume ‹f x ≠ 0›
  have ex: ‹f summable_on (A-{x})›
    by (rule summable_on_cofin_subset) (use assms in auto)
  have pos: ‹infsum f (A - {x}) ≥ 0›
    by (rule infsum_nonneg) (use nneg in auto)

  have [trans]: ‹x ≥ y ==> y > z ==> x > z› for x y z :: 'b by auto

  have ‹infsum f A = infsum f (A-{x}) + infsum f {x}›
    by (subst infsum_Un_disjoint[symmetric]) (use assms ex in ‹auto simp: insert_absorb›)
  also have ‹… ≥ infsum f {x}› (is ‹_ ≥ …›)
    using pos by (rule add_increasing) simp
  also have ‹… = f x› (is ‹_ = …›)
    by (subst infsum_finite) auto
  also have ‹… > 0›
    using ‹f x ≠ 0› assms(4) nneg by fastforce
  finally show False
    using assms by auto
qed

lemma nonneg_has_sum_le_0D:
  fixes f :: "'a ==> 'b::{topological_ab_group_add,ordered_ab_group_add,linorder_topology}"
  assumes "(f has_sum a) A" ‹a ≤ 0›
    and "∧x. x ∈ A ==> f x ≥ 0"
    and "x ∈ A"
  shows "f x = 0"
  by (metis assms infsumI nonneg_infsum_le_0D summable_on_def)

lemma has_sum_cmult_left:
  fixes f :: "'a ==> 'b :: {topological_semigroup_mult, semiring_0}"
  assumes ‹(f has_sum a) A›
  shows "((λx. f x * c) has_sum (a * c)) A"
  using assms tendsto_mult_right 
  by (force simp add: has_sum_def sum_distrib_right)

lemma infsum_cmult_left:
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
  assumes ‹c ≠ 0 ==> f summable_on A›
  shows "infsum (λx. f x * c) A = infsum f A * c"
  using assms has_sum_cmult_left infsumI summable_iff_has_sum_infsum by fastforce

lemma summable_on_cmult_left:
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
  assumes ‹f summable_on A›
  shows "(λ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 ==> 'b :: {topological_semigroup_mult, semiring_0}"
  assumes ‹(f has_sum a) A›
  shows "((λx. c * f x) has_sum (c * a)) A"
  using assms tendsto_mult_left 
  by (force simp add: has_sum_def sum_distrib_left)

lemma infsum_cmult_right:
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
  assumes ‹c ≠ 0 ==> f summable_on A›
  shows ‹infsum (λx. c * f x) A = c * infsum f A›
  using assms has_sum_cmult_right infsumI summable_iff_has_sum_infsum by fastforce

lemma summable_on_cmult_right:
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, semiring_0}"
  assumes ‹f summable_on A›
  shows "(λ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 ==> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
  assumes ‹c ≠ 0›
  shows "(λx. f x * c) summable_on A ⟷ f summable_on A"
proof
  assume ‹f summable_on A›
  then show ‹(λx. f x * c) summable_on A›
    by (rule summable_on_cmult_left)
next
  assume ‹(λx. f x * c) summable_on A›
  then have ‹(λx. f x * c * inverse c) summable_on A›
    by (rule summable_on_cmult_left)
  then show ‹f summable_on A›
    by (smt (verit, del_insts) assms divide_inverse nonzero_divide_eq_eq summable_on_cong)
qed

lemma summable_on_cmult_right':
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
  assumes ‹c ≠ 0›
  shows "(λx. c * f x) summable_on A ⟷ f summable_on A"
    by (metis (no_types, lifting) assms left_inverse mult.assoc mult_1 summable_on_cmult_right summable_on_cong)

lemma infsum_cmult_left':
  fixes f :: "'a ==> 'b :: {t2_space, topological_semigroup_mult, division_ring}"
  shows "infsum (λx. f x * c) A = infsum f A * c"
  by (metis (full_types) infsum_cmult_left infsum_not_exists mult_eq_0_iff summable_on_cmult_left')

lemma infsum_cmult_right':
  fixes f :: "'a ==> 'b :: {t2_space,topological_semigroup_mult,division_ring}"
  shows "infsum (λx. c * f x) A = c * infsum f A"
  by (metis (full_types) infsum_cmult_right infsum_not_exists mult_eq_0_iff summable_on_cmult_right')

lemma has_sum_constant[simp]:
  assumes ‹finite F›
  shows ‹((λ_. c) has_sum of_nat (card F) * c) F›
  by (metis assms has_sum_finite sum_constant)

lemma infsum_constant[simp]:
  assumes ‹finite F›
  shows ‹infsum (λ_. c) F = of_nat (card F) * c›
  by (simp add: assms)

lemma infsum_diverge_constant:
  🍋 ‹This probably does not really need all of 🍋‹archimedean_field› but Isabelle/HOL
  has no type class such as, e.g., "archimedean ring".›
  fixes c :: ‹'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}›
  assumes ‹infinite A› and ‹c ≠ 0›
  shows ‹¬ (λ_. c) summable_on A›
proof (rule notI)
  assume ‹(λ_. c) summable_on A›
  then have ‹(λ_. inverse c * c) summable_on A›
    by (rule summable_on_cmult_right)
  then have [simp]: ‹(λ_. 1::'a) summable_on A›
    using assms by auto
  have ‹infsum (λ_. 1) A ≥ d› for d :: 'a
  proof -
    obtain n :: nat where ‹of_nat n ≥ d›
      by (meson real_arch_simple)
    from assms
    obtain F where ‹F ⊆ A› and ‹finite F› and ‹card F = n›
      by (meson infinite_arbitrarily_large)
    note ‹d ≤ of_nat n›
    also have ‹of_nat n = infsum (λ_. 1::'a) F›
      by (simp add: ‹card F = n› ‹finite F›)
    also have ‹… ≤ infsum (λ_. 1::'a) A›
      apply (rule infsum_mono_neutral)
      using ‹finite F› ‹F ⊆ A› by auto
    finally show ?thesis .
  qed                                                        
  then show False
    by (meson linordered_field_no_ub not_less)
qed

lemma has_sum_constant_archimedean[simp]:
  🍋 ‹This probably does not really need all of 🍋‹archimedean_field› but Isabelle/HOL
  has no type class such as, e.g., "archimedean ring".›
  fixes c :: ‹'a::{archimedean_field, comm_monoid_add, linorder_topology, topological_semigroup_mult}›
  shows ‹infsum (λ_. c) A = of_nat (card A) * c›
  by (metis infsum_0 infsum_constant infsum_diverge_constant infsum_not_exists sum.infinite sum_constant)

lemma has_sum_uminus:
  fixes f :: ‹'a ==> 'b::topological_ab_group_add›
  shows ‹((λx. - f x) has_sum a) A ⟷ (f has_sum (- a)) A›
  by (auto simp add: sum_negf[abs_def] tendsto_minus_cancel_left has_sum_def)

lemma summable_on_uminus:
  fixes f :: ‹'a ==> 'b::topological_ab_group_add›
  shows‹(λx. - f x) summable_on A ⟷ f summable_on A›
  by (metis summable_on_def has_sum_uminus verit_minus_simplify(4))

lemma infsum_uminus:
  fixes f :: ‹'a ==> 'b::{topological_ab_group_add, t2_space}›
  shows ‹infsum (λx. - f x) A = - infsum f A›
  by (metis (full_types) add.inverse_inverse add.inverse_neutral infsumI infsum_def has_sum_infsum has_sum_uminus)

lemma has_sum_le_finite_sums:
  fixes a :: ‹'a::{comm_monoid_add,topological_space,linorder_topology}›
  assumes ‹(f has_sum a) A›
  assumes ‹∧F. finite F ==> F ⊆ A ==> sum f F ≤ b›
  shows ‹a ≤ b›
  by (metis assms eventually_finite_subsets_at_top_weakI finite_subsets_at_top_neq_bot has_sum_def tendsto_upperbound)

lemma infsum_le_finite_sums:
  fixes b :: ‹'a::{comm_monoid_add,topological_space,linorder_topology}›
  assumes ‹f summable_on A›
  assumes ‹∧F. finite F ==> F ⊆ A ==> sum f F ≤ b›
  shows ‹infsum f A ≤ b›
  by (meson assms has_sum_infsum has_sum_le_finite_sums)


lemma summable_on_scaleR_left [intro]:
  fixes c :: ‹'a :: real_normed_vector›
  assumes "c ≠ 0 ==> f summable_on A"
  shows   "(λx. f x *🪙R c) summable_on A"
proof (cases ‹c = 0›)
  case False
  then have "(λy. y *🪙R c) ∘ f summable_on A"
    using assms by (auto simp add: scaleR_left.additive_axioms summable_on_comm_additive)
  then show ?thesis
    by (metis (mono_tags, lifting) comp_apply summable_on_cong)
qed auto


lemma summable_on_scaleR_right [intro]:
  fixes f :: ‹'a ==> 'b :: real_normed_vector›
  assumes "c ≠ 0 ==> f summable_on A"
  shows   "(λx. c *🪙R f x) summable_on A"
proof (cases ‹c = 0›)
  case False
  then have "(*\<^sub>R) c \ f summable_on A"
  using assms by (auto simp add: scaleR_right.additive_axioms summable_on_comm_additive)
  then show ?thesis
    by (metis (mono_tags, lifting) comp_apply summable_on_cong)
qed auto

lemma infsum_scaleR_left:
  fixes c :: ‹'a :: real_normed_vector›
  assumes "c ≠ 0 ==> f summable_on A"
  shows   "infsum (λx. f x *🪙R c) A = infsum f A *🪙R c"
proof (cases ‹c = 0›)
  case False
  then have "infsum ((λy. y *🪙R c) ∘ f) A = infsum f A *🪙R c"
  using assms by (auto simp add: scaleR_left.additive_axioms infsum_comm_additive)
  then show ?thesis
    by (metis (mono_tags, lifting) comp_apply infsum_cong)
qed auto

lemma infsum_scaleR_right:
  fixes f :: ‹'a ==> 'b :: real_normed_vector›
  shows   "infsum (λx. c *🪙R f x) A = c *🪙R infsum f A"
proof -
  consider (summable) ‹f summable_on A› | (c0) ‹c = 0› | (not_summable) ‹¬ f summable_on A› ‹c ≠ 0›
    by auto
  then show ?thesis
  proof cases
    case summable
    then have "infsum ((*🪙R) c ∘ f) A = c *🪙R infsum f A"
      by (auto simp add: scaleR_right.additive_axioms infsum_comm_additive)
    then show ?thesis
      by (metis (mono_tags, lifting) comp_apply infsum_cong)
  next
    case c0
    then show ?thesis by auto
  next
    case not_summable
    have ‹¬ (λx. c *🪙R f x) summable_on A›
    proof (rule notI)
      assume ‹(λx. c *🪙R f x) summable_on A›
      then have ‹(λx. inverse c *🪙R c *🪙R f x) summable_on A›
        using summable_on_scaleR_right by blast
      with not_summable show False
        by simp
    qed
    then show ?thesis
      by (simp add: infsum_not_exists not_summable(1)) 
  qed
qed


lemma infsum_Un_Int:
  fixes f :: "'a ==> 'b::{topological_ab_group_add, t2_space}"
  assumes "f summable_on A - B" "f summable_on B - A" ‹f summable_on A ∩ B›
  shows   "infsum f (A ∪ B) = infsum f A + infsum f B - infsum f (A ∩ B)"
proof -
  obtain ‹f summable_on A› ‹f summable_on B›
    using assms by (metis Int_Diff_Un Int_Diff_disjoint inf_commute summable_on_Un_disjoint)
  then have ‹infsum f (A ∪ B) = infsum f A + infsum f (B - A)›
    using assms(2) infsum_Un_disjoint by fastforce
  moreover have ‹infsum f (B - A) = infsum f B - infsum f (A ∩ B)›
    using assms by (metis Diff_Int2 Un_Int_eq(2) ‹f summable_on B› inf_le2 infsum_Diff)
  ultimately show ?thesis
    by auto
qed

lemma inj_combinator':
  assumes "x ∉ F"
  shows ‹inj_on (λ(g, y). g(x := y)) (Pi🪙E F B × B x)›
proof -
  have "inj_on ((λ(y, g). g(x := y)) ∘ prod.swap) (Pi🪙E F B × B x)"
    using inj_combinator[of x F B] assms by (intro comp_inj_on) (auto simp: product_swap)
  thus ?thesis
    by (simp add: o_def)
qed

lemma infsum_prod_PiE:
  🍋 ‹See also ‹infsum_prod_PiE_abs› below with incomparable premises.›
  fixes f :: "'a ==> 'b ==> 'c :: {comm_monoid_mult, topological_semigroup_mult, division_ring, banach}"
  assumes finite: "finite A"
  assumes "∧x. x ∈ A ==> f x summable_on B x"
  assumes "(λg. ∏x∈A. f x (g x)) summable_on (PiE A B)"
  shows   "infsum (λg. ∏x∈A. f x (g x)) (PiE A B) = (∏x∈A. infsum (f x) (B x))"
proof (use finite assms(2-) in induction)
  case empty
  then show ?case 
    by auto
next
  case (insert x F)
  have pi: ‹Pi🪙E (insert x F) B = (λ(g,y). g(x:=y)) ` (Pi🪙E F B × B x)›
    unfolding PiE_insert_eq 
    by (subst swap_product [symmetric]) (simp add: image_image case_prod_unfold)
  have prod: ‹(∏x'∈F. f x' ((p(x:=y)) x')) = (∏x'∈F. f x' (p x'))› for p y
    by (rule prod.cong) (use insert.hyps in auto)
  have inj: ‹inj_on (λ(g, y). g(x := y)) (Pi🪙E F B × B x)›
    using ‹x ∉ F› by (rule inj_combinator')

  have summable1: ‹(λg. ∏x∈insert x F. f x (g x)) summable_on Pi🪙E (insert x F) B›
    using insert.prems(2) .
  also have ‹Pi🪙E (insert x F) B = (λ(g,y). g(x:=y)) ` (Pi🪙E F B × B x)›
    by (simp only: pi)
  also have "(λg. ∏x∈insert x F. f x (g x)) summable_on … ⟷
               ((λg. ∏x∈insert x F. f x (g x)) ∘ (λ(g,y). g(x:=y))) summable_on (Pi🪙E F B × B x)"
    using inj by (rule summable_on_reindex)
  also have "(∏z∈F. f z ((g(x := y)) z)) = (∏z∈F. f z (g z))" for g y
    using insert.hyps by (intro prod.cong) auto
  hence "((λg. ∏x∈insert x F. f x (g x)) ∘ (λ(g,y). g(x:=y))) =
             (λ(p, y). f x y * (∏x'∈F. f x' (p x')))"
    using insert.hyps by (auto simp: fun_eq_iff cong: prod.cong_simp)
  finally have summable2: ‹(λ(p, y). f x y * (∏x'∈F. f x' (p x'))) summable_on Pi🪙E F B × B x› .

  then have ‹(λp. ∑🪙∞y∈B x. f x y * (∏x'∈F. f x' (p x'))) summable_on Pi🪙E F B›
    by (rule summable_on_Sigma_banach)
  then have ‹(λp. (∑🪙∞y∈B x. f x y) * (∏x'∈F. f x' (p x'))) summable_on Pi🪙E F B›
    by (metis (mono_tags, lifting) infsum_cmult_left' infsum_cong summable_on_cong)
  then have summable3: ‹(λp. (∏x'∈F. f x' (p x'))) summable_on Pi🪙E F B› if ‹(∑🪙∞y∈B x. f x y) ≠ 0›
    using summable_on_cmult_right' that by blast

  have ‹(∑🪙∞g∈Pi🪙E (insert x F) B. ∏x∈insert x F. f x (g x))
  = (∑🪙∞(p,y)∈Pi🪙E F B × B x. ∏x'∈insert x F. f x' ((p(x:=y)) x'))›
    by (smt (verit, ccfv_SIG) comp_apply infsum_cong infsum_reindex inj pi prod.cong split_def)
  also have ‹… = (∑🪙∞(p, y)∈Pi🪙E F B × B x. f x y * (∏x'∈F. f x' ((p(x:=y)) x')))›
    using insert.hyps by auto
  also have ‹… = (∑🪙∞(p, y)∈Pi🪙E F B × B x. f x y * (∏x'∈F. f x' (p x')))›
    using prod by presburger
  also have ‹… = (∑🪙∞p∈Pi🪙E F B. ∑🪙∞y∈B x. f x y * (∏x'∈F. f x' (p x')))›
    using infsum_Sigma'_banach summable2 by force
  also have ‹… = (∑🪙∞y∈B x. f x y) * (∑🪙∞p∈Pi🪙E F B. ∏x'∈F. f x' (p x'))›
    by (smt (verit) infsum_cmult_left' infsum_cmult_right' infsum_cong)
  also have ‹… = (∏x∈insert x F. infsum (f x) (B x))›
    using insert summable3 by auto
  finally show ?case
    by simp
qed

lemma infsum_prod_PiE_abs:
  🍋 ‹See also @{thm [source] infsum_prod_PiE} above with incomparable premises.›
  fixes f :: "'a ==> 'b ==> 'c :: {banach, real_normed_div_algebra, comm_semiring_1}"
  assumes finite: "finite A"
  assumes "∧x. x ∈ A ==> f x abs_summable_on B x"
  shows   "infsum (λg. ∏x∈A. f x (g x)) (PiE A B) = (∏x∈A. infsum (f x) (B x))"
proof (use finite assms(2) in induction)
  case empty
  then show ?case 
    by auto
next
  case (insert x A)
  
  have pi: ‹Pi🪙E (insert x F) B = (λ(g,y). g(x:=y)) ` (Pi🪙E F B × B x)› for x F and B :: "'a ==> 'b set"
    unfolding PiE_insert_eq 
    by (subst swap_product [symmetric]) (simp add: image_image case_prod_unfold)
  have prod: ‹(∏x'∈A. f x' ((p(x:=y)) x')) = (∏x'∈A. f x' (p x'))› for p y
    by (rule prod.cong) (use insert.hyps in auto)
  have inj: ‹inj_on (λ(g, y). g(x := y)) (Pi🪙E A B × B x)›
    using ‹x ∉ A› by (rule inj_combinator')

  define s where ‹s x = infsum (λy. norm (f x y)) (B x)› for x

  have ‹(∑p∈P. norm (∏x∈F. f x (p x))) ≤ prod s F›
    if P: ‹P ⊆ Pi🪙E F B› and [simp]: ‹finite P› ‹finite F›
      and sum: ‹∧x. x ∈ F ==> f x abs_summable_on B x› for P F
  proof -
    define B' where ‹B' x = {p x| p. p∈P}› for x
    have fin_B'[simp]: ‹finite (B' x)› for x
      using that by (auto simp: B'_def)
    have [simp]: ‹finite (Pi🪙E F B')›
      by (simp add: finite_PiE)
    have [simp]: ‹P ⊆ Pi🪙E F B'›
      using that by (auto simp: B'_def)
    have B'B: ‹B' x ⊆ B x› if ‹x ∈ F› for x
      unfolding B'_def using P that 
      by auto
    have s_bound: ‹(∑y∈B' x. norm (f x y)) ≤ s x› if ‹x ∈ F› for x
      by (metis B'B fin_B' finite_sum_le_has_sum has_sum_infsum norm_ge_zero s_def sum that)
    have ‹(∑p∈P. norm (∏x∈F. f x (p x))) ≤ (∑p∈Pi🪙E F B'. norm (∏x∈F. f x (p x)))›
      by (simp add: sum_mono2)
    also have ‹… = (∑p∈Pi🪙E F B'. ∏x∈F. norm (f x (p x)))›
      by (simp add: prod_norm)
    also have ‹… = (∏x∈F. ∑y∈B' x. norm (f x y))›
    proof (use ‹finite F› in induction)
      case empty
      then show ?case by simp
    next
      case (insert x F)
      have inj: ‹inj_on (λ(g, y). g(x := y)) (Pi🪙E F B' × B' x)›
        by (simp add: inj_combinator' insert.hyps)
      then have ‹(∑p∈Pi🪙E (insert x F) B'. ∏x∈insert x F. norm (f x (p x)))
  = (∑(p,y)∈Pi🪙E F B' × B' x. ∏x'∈insert x F. norm (f x' ((p(x := y)) x')))›
        by (simp add: pi sum.reindex case_prod_unfold)
      also have ‹… = (∑(p, y)∈Pi🪙E F B' × B' x. norm (f x y) * (∏x'∈F. norm (f x' (p x'))))›
        by (smt (verit, del_insts) fun_upd_apply insert.hyps prod.cong prod.insert split_def sum.cong)
      also have ‹… = (∑y∈B' x. norm (f x y)) * (∑p∈Pi🪙E F B'. ∏x'∈F. norm (f x' (p x')))›
        by (simp add: sum_product sum.swap [of _ "Pi🪙E F B'"] sum.cartesian_product)
      also have ‹… = (∏x∈insert x F. ∑y∈B' x. norm (f x y))›
        using insert by force
      finally show ?case .
    qed
    also have ‹… ≤ (∏x∈F. s x)›
      using s_bound by (simp add: prod_mono sum_nonneg)
    finally show ?thesis .
  qed
  then have "bdd_above
     (sum (λg. norm (∏x∈insert x A. f x (g x))) ` {F. F ⊆ Pi🪙E (insert x A) B ∧ finite F})"
    using insert.hyps insert.prems by (intro bdd_aboveI) blast
  then have ‹(λg. ∏x∈insert x A. f x (g x)) abs_summable_on Pi🪙E (insert x A) B›
    using nonneg_bdd_above_summable_on
    by (metis (mono_tags, lifting) Collect_cong norm_ge_zero)
  also have ‹Pi🪙E (insert x A) B = (λ(g,y). g(x:=y)) ` (Pi🪙E A B × B x)›
    by (simp only: pi)
  also have "(λg. ∏x∈insert x A. f x (g x)) abs_summable_on … ⟷
               ((λg. ∏x∈insert x A. f x (g x)) ∘ (λ(g,y). g(x:=y))) abs_summable_on (Pi🪙E A B × B x)"
    using inj by (subst summable_on_reindex) (auto simp: o_def)
  also have "(∏z∈A. f z ((g(x := y)) z)) = (∏z∈A. f z (g z))" for g y
    using insert.hyps by (intro prod.cong) auto
  hence "((λg. ∏x∈insert x A. f x (g x)) ∘ (λ(g,y). g(x:=y))) =
             (λ(p, y). f x y * (∏x'∈A. f x' (p x')))"
    using insert.hyps by (auto simp: fun_eq_iff cong: prod.cong_simp)
  finally have summable2: ‹(λ(p, y). f x y * (∏x'∈A. f x' (p x'))) abs_summable_on Pi??E A B × B x› .

  have ‹(∑🪙∞g∈Pi🪙E (insert x A) B. ∏x∈insert x A. f x (g x))
  = (∑🪙∞(p,y)∈Pi🪙E A B × B x. ∏x'∈insert x A. f x' ((p(x:=y)) x'))›
    using inj by (simp add: pi infsum_reindex o_def case_prod_unfold)
  also have ‹… = (∑🪙∞(p,y) ∈ Pi🪙E A B × B x. f x y * (∏x'∈A. f x' (p x')))›
    using prod insert.hyps by auto
  also have ‹… = (∑🪙∞p∈Pi🪙E A B. ∑🪙∞y∈B x. f x y * (∏x'∈A. f x' (p x')))›
    using abs_summable_summable infsum_Sigma'_banach summable2 by fastforce
  also have ‹… = (∑🪙∞y∈B x. f x y) * (∑🪙∞p∈Pi🪙E A B. ∏x'∈A. f x' (p x'))›
    by (smt (verit, best) infsum_cmult_left' infsum_cmult_right' infsum_cong)
  finally show ?case
    by (simp add: insert)
qed



subsection ‹Absolute convergence›

lemma abs_summable_countable:
  assumes ‹f abs_summable_on A›
  shows ‹countable {x∈A. f x ≠ 0}›
proof -
  have fin: ‹finite {x∈A. norm (f x) ≥ t}› if ‹t > 0› for t
  proof (rule ccontr)
    assume *: ‹infinite {x ∈ A. t ≤ norm (f x)}›
    have ‹infsum (λx. norm (f x)) A ≥ b› for b
    proof -
      obtain b' where b': ‹of_nat b' ≥ b / t›
        by (meson real_arch_simple)
      from *
      obtain F where cardF: ‹card F ≥ b'› and ‹finite F› and F: ‹F ⊆ {x ∈ A. t ≤ norm (f x)}›
        by (meson finite_if_finite_subsets_card_bdd nle_le)
      have ‹b ≤ of_nat b' * t›
        using b' ‹t > 0› by (simp add: field_simps split: if_splits)
      also have ‹… ≤ of_nat (card F) * t›
        by (simp add: cardF that)
      also have ‹… = sum (λx. t) F›
        by simp
      also have ‹… ≤ sum (λx. norm (f x)) F›
        by (metis (mono_tags, lifting) F in_mono mem_Collect_eq sum_mono)
      also have ‹… = infsum (λx. norm (f x)) F›
        using ‹finite F› by (rule infsum_finite[symmetric])
      also have ‹… ≤ infsum (λx. norm (f x)) A›
        by (rule infsum_mono_neutral) (use ‹finite F› assms F in auto)
      finally show ?thesis .
    qed
    then show False
      by (meson gt_ex linorder_not_less)
  qed
  have ‹countable (∪i∈{1..}. {x∈A. norm (f x) ≥ 1/of_nat i})›
    by (rule countable_UN) (use fin in ‹auto intro!: countable_finite›)
  also have ‹… = {x∈A. f x ≠ 0}›
  proof safe
    fix x assume x: "x ∈ A" "f x ≠ 0"
    define i where "i = max 1 (nat (ceiling (1 / norm (f x))))"
    have "i ≥ 1"
      by (simp add: i_def)
    moreover have "real i ≥ 1 / norm (f x)"
      unfolding i_def by linarith
    hence "1 / real i ≤ norm (f x)" using ‹f x ≠ 0›
      by (auto simp: divide_simps mult_ac)
    ultimately show "x ∈ (∪i∈{1..}. {x ∈ A. 1 / real i ≤ norm (f x)})"
      using ‹x ∈ A› by auto
  qed auto
  finally show ?thesis .
qed

(* Logically belongs in the section about reals, but needed as a dependency here *)
lemma summable_on_iff_abs_summable_on_real:
  fixes f :: ‹'a ==> real›
  shows ‹f summable_on A ⟷ f abs_summable_on A›
proof (rule iffI)
  assume ‹f summable_on A›
  define n A🪙p A🪙n
    where ‹n ≡ λx. norm (f x)› and ‹A🪙p = {x∈A. f x ≥ 0}› and ‹A🪙n = {x∈A. f x 🚫}› for x
  have A: ‹A🪙p ∪ A🪙n = A› ‹A🪙p ∩ A🪙n = {}›
    by (auto simp: A🪙p_def A🪙n_def)
  from ‹f summable_on A› have ‹f summable_on A🪙p› ‹f summable_on A🪙n›
    using A🪙p_def A🪙n_def summable_on_subset_banach by fastforce+
  then have ‹n summable_on A🪙p›
    by (smt (verit) A🪙p_def n_def mem_Collect_eq real_norm_def summable_on_cong)
  moreover have ‹n summable_on A🪙n›
    by (smt (verit, best) ‹f summable_on A🪙n›  summable_on_uminus A🪙n_def n_def summable_on_cong mem_Collect_eq real_norm_def)
  ultimately show ‹n summable_on A›
    using A summable_on_Un_disjoint by blast
next
  show ‹f abs_summable_on A ==> f summable_on A›
    using abs_summable_summable by blast
qed

lemma abs_summable_on_Sigma_iff:
  shows   "f abs_summable_on Sigma A B ⟷
             (∀x∈A. (λy. f (x, y)) abs_summable_on B x) ∧
             ((λx. infsum (λy. norm (f (x, y))) (B x)) abs_summable_on A)"
proof (intro iffI conjI ballI)
  assume asm: ‹f abs_summable_on Sigma A B›
  then have ‹(λx. infsum (λy. norm (f (x,y))) (B x)) summable_on A›
    by (simp add: cond_case_prod_eta summable_on_Sigma_banach)
  then show ‹(λx. ∑🪙∞y∈B x. norm (f (x, y))) abs_summable_on A›
    using summable_on_iff_abs_summable_on_real by force

  show ‹(λy. f (x, y)) abs_summable_on B x› if ‹x ∈ A› for x
  proof -
    from asm have ‹f abs_summable_on Pair x ` B x›
      by (simp add: image_subset_iff summable_on_subset_banach that)
    then show ?thesis
      by (metis (mono_tags, lifting) o_def inj_on_def summable_on_reindex prod.inject summable_on_cong)
  qed
next
  assume asm: ‹(∀x∈A. (λxa. f (x, xa)) abs_summable_on B x) ∧
  (λx. ∑🪙∞y∈B x. norm (f (x, y))) abs_summable_on A›
  have ‹(∑xy∈F. norm (f xy)) ≤ (∑🪙∞x∈A. ∑🪙∞y∈B x. norm (f (x, y)))›
    if ‹F ⊆ Sigma A B› and [simp]: ‹finite F› for F
  proof -
    have [simp]: ‹(SIGMA x:fst ` F. {y. (x, y) ∈ F}) = F›
      by (auto intro!: set_eqI simp add: Domain.DomainI fst_eq_Domain)
    have [simp]: ‹finite {y. (x, y) ∈ F}› for x
      by (metis ‹finite F› Range.intros finite_Range finite_subset mem_Collect_eq subsetI)
    have ‹(∑xy∈F. norm (f xy)) = (∑x∈fst ` F. ∑y∈{y. (x,y)∈F}. norm (f (x,y)))›
      by (simp add: sum.Sigma)
    also have ‹… = (∑🪙∞x∈fst ` F. ∑🪙∞y∈{y. (x,y)∈F}. norm (f (x,y)))›
      by auto
    also have ‹… ≤ (∑🪙∞x∈fst ` F. ∑🪙∞y∈B x. norm (f (x,y)))›
      using asm that(1) by (intro infsum_mono infsum_mono_neutral) auto
    also have ‹… ≤ (∑🪙∞x∈A. ∑🪙∞y∈B x. norm (f (x,y)))›
      by (rule infsum_mono_neutral) (use asm that(1) in ‹auto simp add: infsum_nonneg›)
    finally show ?thesis .
  qed
  then show ‹f abs_summable_on Sigma A B›
    by (intro nonneg_bdd_above_summable_on) (auto simp: bdd_above_def)
qed

lemma abs_summable_on_comparison_test:
  assumes "g abs_summable_on A"
  assumes "∧x. x ∈ A ==> norm (f x) ≤ norm (g x)"
  shows   "f abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on)
  show "bdd_above (sum (λx. norm (f x)) ` {F. F ⊆ A ∧ finite F})"
  proof (rule bdd_aboveI2)
    fix F assume F: "F ∈ {F. F ⊆ A ∧ finite F}"
    have ‹sum (λx. norm (f x)) F ≤ sum (λx. norm (g x)) F›
      using assms F by (intro sum_mono) auto
    also have ‹… = infsum (λx. norm (g x)) F›
      using F by simp
    also have ‹… ≤ infsum (λx. norm (g x)) A›
      by (smt (verit) F assms(1) infsum_mono2 mem_Collect_eq norm_ge_zero summable_on_subset_banach)
    finally show "(∑x∈F. norm (f x)) ≤ (∑🪙∞x∈A. norm (g x))" .
  qed
qed auto

lemma abs_summable_iff_bdd_above:
  fixes f :: ‹'a ==> 'b::real_normed_vector›
  shows ‹f abs_summable_on A ⟷ bdd_above (sum (λx. norm (f x)) ` {F. F⊆A ∧ finite F})›
proof (rule iffI)
  assume ‹f abs_summable_on A›
  show ‹bdd_above (sum (λx. norm (f x)) ` {F. F ⊆ A ∧ finite F})›
  proof (rule bdd_aboveI2)
    fix F assume F: "F ∈ {F. F ⊆ A ∧ finite F}"
    show "(∑x∈F. norm (f x)) ≤ (∑🪙∞x∈A. norm (f x))"
      by (rule finite_sum_le_infsum) (use ‹f abs_summable_on A› F in auto)
  qed
next
  assume ‹bdd_above (sum (λx. norm (f x)) ` {F. F⊆A ∧ finite F})›
  then show ‹f abs_summable_on A›
    by (simp add: nonneg_bdd_above_summable_on)
qed

lemma abs_summable_product:
  fixes x :: "'a ==> 'b::{real_normed_div_algebra,banach,second_countable_topology}"
  assumes x2_sum: "(λi. (x i) * (x i)) abs_summable_on A"
    and y2_sum: "(λi. (y i) * (y i)) abs_summable_on A"
  shows "(λi. x i * y i) abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on)
  show "bdd_above (sum (λxa. norm (x xa * y xa)) ` {F. F ⊆ A ∧ finite F})"
  proof (rule bdd_aboveI2)
    fix F assume F: ‹F ∈ {F. F ⊆ A ∧ finite F}›
    then have r1: "finite F" and b4: "F ⊆ A"
      by auto
  
    have a1: "(∑🪙∞i∈F. norm (x i * x i)) ≤ (∑🪙∞i∈A. norm (x i * x i))"
      by (metis (no_types, lifting) b4 infsum_mono2 norm_ge_zero summable_on_subset_banach x2_sum)

    have "norm (x i * y i) ≤ norm (x i * x i) + norm (y i * y i)" for i
      unfolding norm_mult by (smt (verit, best) abs_norm_cancel mult_mono not_sum_squares_lt_zero)
    hence "(∑i∈F. norm (x i * y i)) ≤ (∑i∈F. norm (x i * x i) + norm (y i * y i))"
      by (simp add: sum_mono)
    also have "… = (∑i∈F. norm (x i * x i)) + (∑i∈F. norm (y i * y i))"
      by (simp add: sum.distrib)
    also have "… = (∑🪙∞i∈F. norm (x i * x i)) + (∑🪙∞i∈F. norm (y i * y i))"
      by (simp add: ‹finite F›)
    also have "… ≤ (∑🪙∞i∈A. norm (x i * x i)) + (∑🪙∞i∈A. norm (y i * y i))"
      using F assms
      by (intro add_mono infsum_mono2) auto
    finally show ‹(∑xa∈F. norm (x xa * y xa)) ≤ (∑🪙∞i∈A. norm (x i * x i)) + (∑🪙∞i∈A. norm (y i * y i))›
      by simp
  qed
qed auto

subsection ‹Extended reals and nats›

lemma summable_on_ennreal[simp]: ‹(f::_ ==> ennreal) summable_on S› and summable_on_enat[simp]: ‹(f::_ ==> enat) summable_on S›
  by (simp_all add: nonneg_summable_on_complete)

lemma has_sum_superconst_infinite_ennreal:
  fixes f :: ‹'a ==> ennreal›
  assumes geqb: ‹∧x. x ∈ S ==> f x ≥ b›
  assumes b: ‹b > 0›
  assumes ‹infinite S›
  shows "(f has_sum ∞) S"
proof -
  have ‹(sum f ---> ∞) (finite_subsets_at_top S)›
  proof (rule order_tendstoI)
    fix y :: ennreal assume ‹y 🚫∞›
    then have ‹y / b 🚫∞› ‹y 🚫›
      using b ennreal_divide_eq_top_iff top.not_eq_extremum by force+
    then obtain F where ‹finite F› and ‹F ⊆ S› and cardF: ‹card F > y / b›
      using ‹infinite S›
      by (metis ennreal_Ex_less_of_nat infinite_arbitrarily_large infinity_ennreal_def)
    moreover have ‹sum f Y > y› if ‹finite Y› and ‹F ⊆ Y› and ‹Y ⊆ S› for Y
    proof -
      have ‹y 🚫 * card F›
        by (metis b ‹y 🚫› cardF divide_less_ennreal ennreal_mult_eq_top_iff gr_implies_not_zero mult.commute top.not_eq_extremum)
      also have ‹… ≤ b * card Y›
        by (meson b card_mono less_imp_le mult_left_mono of_nat_le_iff that)
      also have ‹… = sum (λ_. b) Y›
        by (simp add: mult.commute)
      also have ‹… ≤ sum f Y›
        using geqb by (meson subset_eq sum_mono that(3))
      finally show ?thesis .
    qed
    ultimately show ‹∀🪙F x in finite_subsets_at_top S. y 🚫 f x›
      unfolding eventually_finite_subsets_at_top by auto
  qed auto
  then show ?thesis
    by (simp add: has_sum_def)
qed

lemma infsum_superconst_infinite_ennreal:
  fixes f :: ‹'a ==> ennreal›
  assumes ‹∧x. x ∈ S ==> f x ≥ b›
  assumes ‹b > 0›
  assumes ‹infinite S›
  shows "infsum f S = ∞"
  using assms infsumI has_sum_superconst_infinite_ennreal by blast

lemma infsum_superconst_infinite_ereal:
  fixes f :: ‹'a ==> ereal›
  assumes geqb: ‹∧x. x ∈ S ==> f x ≥ b›
  assumes b: ‹b > 0›
  assumes ‹infinite S›
  shows "infsum f S = ∞"
proof -
  obtain b' where b': ‹e2ennreal b' = b› and ‹b' > 0›
    using b by blast
  have "0 < e2ennreal b"
    using b' b
    by (metis dual_order.refl enn2ereal_e2ennreal gr_zeroI order_less_le zero_ennreal.abs_eq)
  hence *: ‹infsum (e2ennreal ∘ f) S = ∞›
    using assms b'
    by (intro infsum_superconst_infinite_ennreal[where b=b']) (auto intro!: e2ennreal_mono)
  have ‹infsum f S = infsum (enn2ereal ∘ (e2ennreal ∘ f)) S›
    using geqb b by (intro infsum_cong) (fastforce simp: enn2ereal_e2ennreal)
  also have ‹… = enn2ereal ∞›
    using * by (simp add: infsum_comm_additive_general continuous_at_enn2ereal nonneg_summable_on_complete)
  also have ‹… = ∞›
    by simp
  finally show ?thesis .
qed

lemma has_sum_superconst_infinite_ereal:
  fixes f :: ‹'a ==> ereal›
  assumes ‹∧x. x ∈ S ==> f x ≥ b›
  assumes ‹b > 0›
  assumes ‹infinite S›
  shows "(f has_sum ∞) S"
  by (metis Infty_neq_0(1) assms infsum_def has_sum_infsum infsum_superconst_infinite_ereal)

lemma infsum_superconst_infinite_enat:
  fixes f :: ‹'a ==> enat›
  assumes geqb: ‹∧x. x ∈ S ==> f x ≥ b›
  assumes b: ‹b > 0›
  assumes ‹infinite S›
  shows "infsum f S = ∞"
proof -
  have ‹ennreal_of_enat (infsum f S) = infsum (ennreal_of_enat ∘ f) S›
    by (simp flip: infsum_comm_additive_general)
  also have ‹… = ∞›
    by (metis assms(3) b comp_def ennreal_of_enat_0 ennreal_of_enat_le_iff geqb infsum_superconst_infinite_ennreal leD leI)
  also have ‹… = ennreal_of_enat ∞›
    by simp
  finally show ?thesis
    by (rule ennreal_of_enat_inj[THEN iffD1])
qed

lemma has_sum_superconst_infinite_enat:
  fixes f :: ‹'a ==> enat›
  assumes ‹∧x. x ∈ S ==> f x ≥ b›
  assumes ‹b > 0›
  assumes ‹infinite S›
  shows "(f has_sum ∞) S"
  by (metis assms i0_lb has_sum_infsum infsum_superconst_infinite_enat nonneg_summable_on_complete)

text ‹This lemma helps to relate a real-valued infsum to a supremum over extended nonnegative reals.›

lemma infsum_nonneg_is_SUPREMUM_ennreal:
  fixes f :: "'a ==> real"
  assumes summable: "f summable_on A"
    and fnn: "∧x. x∈A ==> f x ≥ 0"
  shows "ennreal (infsum f A) = (SUP F∈{F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))"
proof -
  have 🍋: "∧F. [finite F; F ⊆ A] ==> sum (ennreal ∘ f) F = ennreal (sum f F)"
    by (metis (mono_tags, lifting) comp_def fnn subsetD sum.cong sum_ennreal)
  then have ‹ennreal (infsum f A) = infsum (ennreal ∘ f) A›
    by (simp add: infsum_comm_additive_general local.summable)
  also have ‹… = (SUP F∈{F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))›
    by (metis (mono_tags, lifting) 🍋 image_cong mem_Collect_eq nonneg_infsum_complete zero_le)
  finally show ?thesis .
qed

text ‹This lemma helps to related a real-valued infsum to a supremum over extended reals.›

lemma infsum_nonneg_is_SUPREMUM_ereal:
  fixes f :: "'a ==> real"
  assumes summable: "f summable_on A"
    and fnn: "∧x. x∈A ==> f x ≥ 0"
  shows "ereal (infsum f A) = (SUP F∈{F. finite F ∧ F ⊆ A}. (ereal (sum f F)))"
proof -
  have "∧F. [finite F; F ⊆ A] ==> sum (ereal ∘ f) F = ereal (sum f F)"
    by auto
  then have ‹ereal (infsum f A) = infsum (ereal ∘ f) A›
    by (simp add: infsum_comm_additive_general local.summable)
  also have ‹… = (SUP F∈{F. finite F ∧ F ⊆ A}. (ereal (sum f F)))›
    by (subst nonneg_infsum_complete) (simp_all add: assms)
  finally show ?thesis .
qed


subsection ‹Real numbers›

text ‹Most lemmas in the general property section already apply to real numbers.
  A few ones that are specific to reals are given here.›

lemma infsum_nonneg_is_SUPREMUM_real:
  fixes f :: "'a ==> real"
  assumes summable: "f summable_on A"
    and fnn: "∧x. x∈A ==> f x ≥ 0"
  shows "infsum f A = (SUP F∈{F. finite F ∧ F ⊆ A}. (sum f F))"
proof -
  have *: "ereal (infsum f A) = (SUP F∈{F. finite F ∧ F ⊆ A}. (ereal (sum f F)))"
    using assms by (rule infsum_nonneg_is_SUPREMUM_ereal)
  also have "… = ereal (SUP F∈{F. finite F ∧ F ⊆ A}. (sum f F))"
    by (metis (no_types, lifting) * MInfty_neq_ereal(2) PInfty_neq_ereal(2) SUP_cong abs_eq_infinity_cases ereal_SUP)
  finally show ?thesis by simp
qed


lemma has_sum_nonneg_SUPREMUM_real:
  fixes f :: "'a ==> real"
  assumes "f summable_on A" and "∧x. x∈A ==> f x ≥ 0"
  shows "(f has_sum (SUP F∈{F. finite F ∧ F ⊆ A}. (sum f F))) A"
  by (metis (mono_tags, lifting) assms has_sum_infsum infsum_nonneg_is_SUPREMUM_real)

lemma summable_countable_real:
  fixes f :: ‹'a ==> real›
  assumes ‹f summable_on A›
  shows ‹countable {x∈A. f x ≠ 0}›
  using abs_summable_countable assms summable_on_iff_abs_summable_on_real by blast

subsection ‹Complex numbers›

lemma has_sum_cnj_iff[simp]: 
  fixes f :: ‹'a ==> complex›
  shows ‹((λx. cnj (f x)) has_sum cnj a) M ⟷ (f has_sum a) M›
  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]:
  "(λi. cnj (f i)) summable_on A ⟷ f summable_on A"
  by (metis complex_cnj_cnj summable_on_def has_sum_cnj_iff)

lemma infsum_cnj[simp]: ‹infsum (λx. cnj (f x)) M = cnj (infsum f M)›
  by (metis complex_cnj_zero infsumI has_sum_cnj_iff infsum_def summable_on_cnj_iff has_sum_infsum)

lemma has_sum_Re:
  assumes "(f has_sum a) M"
  shows "((λx. Re (f x)) has_sum Re a) M"
  using has_sum_comm_additive[where f=Re]
  using  assms tendsto_Re by (fastforce simp add: o_def additive_def)

lemma infsum_Re:
  assumes "f summable_on M"
  shows "infsum (λx. Re (f x)) M = Re (infsum f M)"
  by (simp add: assms has_sum_Re infsumI)

lemma summable_on_Re: 
  assumes "f summable_on M"
  shows "(λx. Re (f x)) summable_on M"
  by (metis assms has_sum_Re summable_on_def)

lemma has_sum_Im:
  assumes "(f has_sum a) M"
  shows "((λx. Im (f x)) has_sum Im a) M"
  using has_sum_comm_additive[where f=Im]
  using  assms tendsto_Im by (fastforce simp add: o_def additive_def)

lemma infsum_Im: 
  assumes "f summable_on M"
  shows "infsum (λx. Im (f x)) M = Im (infsum f M)"
  by (simp add: assms has_sum_Im infsumI)

lemma summable_on_Im: 
  assumes "f summable_on M"
  shows "(λx. Im (f x)) summable_on M"
  by (metis assms has_sum_Im summable_on_def)

lemma nonneg_infsum_le_0D_complex:
  fixes f :: "'a ==> complex"
  assumes "infsum f A ≤ 0"
    and abs_sum: "f summable_on A"
    and nneg: "∧x. x ∈ A ==> f x ≥ 0"
    and "x ∈ A"
  shows "f x = 0"
proof -
  have ‹Im (f x) = 0›
    using assms(4) less_eq_complex_def nneg by auto
  moreover have ‹Re (f x) = 0›
    using assms by (auto simp add: summable_on_Re infsum_Re less_eq_complex_def intro: nonneg_infsum_le_0D[where A=A])
  ultimately show ?thesis
    by (simp add: complex_eqI)
qed

lemma nonneg_has_sum_le_0D_complex:
  fixes f :: "'a ==> complex"
  assumes "(f has_sum a) A" and ‹a ≤ 0›
    and "∧x. x ∈ A ==> f x ≥ 0" and "x ∈ A"
  shows "f x = 0"
  by (metis assms infsumI nonneg_infsum_le_0D_complex summable_on_def)

text ‹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:›

lemma infsum_mono_neutral_complex:
  fixes f :: "'a ==> complex"
  assumes [simp]: "f summable_on A"
    and [simp]: "g summable_on B"
  assumes ‹∧x. x ∈ A∩B ==> f x ≤ g x›
  assumes ‹∧x. x ∈ A-B ==> f x ≤ 0›
  assumes ‹∧x. x ∈ B-A ==> g x ≥ 0›
  shows ‹infsum f A ≤ infsum g B›
proof -
  have ‹infsum (λx. Re (f x)) A ≤ infsum (λx. Re (g x)) B›
    by (smt (verit) assms infsum_cong infsum_mono_neutral less_eq_complex_def summable_on_Re zero_complex.simps(1))
  then have Re: ‹Re (infsum f A) ≤ Re (infsum g B)›
    by (metis assms(1-2) infsum_Re)
  have ‹infsum (λx. Im (f x)) A = infsum (λx. Im (g x)) B›
    by (smt (verit, best) assms(3-5) infsum_cong_neutral less_eq_complex_def zero_complex.simps(2))
  then have Im: ‹Im (infsum f A) = Im (infsum g B)›
    by (metis assms(1-2) infsum_Im)
  from Re Im show ?thesis
    by (auto simp: less_eq_complex_def)
qed

lemma infsum_mono_complex:
  🍋 ‹For 🍋‹real›, @{thm [source] infsum_mono} can be used. 
      But 🍋‹complex› does not have the right typeclass.›
  fixes f g :: "'a ==> complex"
  assumes f_sum: "f summable_on A" and g_sum: "g summable_on A"
  assumes leq: "∧x. x ∈ A ==> f x ≤ g x"
  shows   "infsum f A ≤ infsum g A"
  by (metis DiffE IntD1 f_sum g_sum infsum_mono_neutral_complex leq)


lemma infsum_nonneg_complex:
  fixes f :: "'a ==> complex"
  assumes "f summable_on M"
    and "∧x. x ∈ M ==> 0 ≤ f x"
  shows "infsum f M ≥ 0" (is "?lhs ≥ _")
  by (metis assms infsum_0_simp summable_on_0_simp infsum_mono_complex)

lemma infsum_cmod:
  assumes "f summable_on M"
    and fnn: "∧x. x ∈ M ==> 0 ≤ f x"
  shows "infsum (λx. cmod (f x)) M = cmod (infsum f M)"
proof -
  have ‹complex_of_real (infsum (λx. cmod (f x)) M) = infsum (λx. complex_of_real (cmod (f x))) M›
  proof (rule infsum_comm_additive[symmetric, unfolded o_def])
    have "(λz. Re (f z)) summable_on M"
      using assms summable_on_Re by blast
    also have "?this ⟷ f abs_summable_on M"
      using fnn by (intro summable_on_cong) (auto simp: less_eq_complex_def cmod_def)
    finally show … .
  qed (auto simp: additive_def)
  also have ‹… = infsum f M›
    using fnn cmod_eq_Re complex_is_Real_iff less_eq_complex_def by (force cong: infsum_cong)
  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 :: ‹'a ==> complex›
  shows ‹f summable_on A ⟷ f abs_summable_on A›
proof (rule iffI)
  assume ‹f summable_on A›
  define i r ni nr n where ‹i x = Im (f x)› and ‹r x = Re (f x)›
    and ‹ni x = norm (i x)› and ‹nr x = norm (r x)› and ‹n x = norm (f x)› for x
  from ‹f summable_on A› have ‹i summable_on A›
    by (simp add: i_def[abs_def] summable_on_Im)
  then have [simp]: ‹ni summable_on A›
    using ni_def[abs_def] summable_on_iff_abs_summable_on_real by force

  from ‹f summable_on A› have ‹r summable_on A›
    by (simp add: r_def[abs_def] summable_on_Re)
  then have [simp]: ‹nr summable_on A›
    by (metis nr_def summable_on_cong summable_on_iff_abs_summable_on_real)

  have n_sum: ‹n x ≤ nr x + ni x› for x
    by (simp add: n_def nr_def ni_def r_def i_def cmod_le)

  have *: ‹(λx. nr x + ni x) summable_on A›
    by (simp add: summable_on_add)
  have "bdd_above (sum n ` {F. F ⊆ A ∧ finite F})"
    apply (rule bdd_aboveI[where M=‹infsum (λx. nr x + ni x) A›])
    using * n_sum by (auto simp flip: infsum_finite simp: ni_def nr_def intro!: infsum_mono_neutral)
  then show ‹n summable_on A›
    by (simp add: n_def nonneg_bdd_above_summable_on)
next
  show ‹f abs_summable_on A ==> f summable_on A›
    using abs_summable_summable by blast
qed

lemma summable_countable_complex:
  fixes f :: ‹'a ==> complex›
  assumes ‹f summable_on A›
  shows ‹countable {x∈A. f x ≠ 0}›
  using abs_summable_countable assms summable_on_iff_abs_summable_on_complex by blast


(* TODO: figure all this out *)
inductive (in topological_space) convergent_filter :: "'a filter ==> bool" where
  "F ≤ nhds x ==> convergent_filter F"

lemma (in topological_space) convergent_filter_iff: "convergent_filter F ⟷ (∃x. F ≤ nhds x)"
  by (auto simp: convergent_filter.simps)

lemma (in uniform_space) cauchy_filter_mono:
  "cauchy_filter F ==> F' ≤ F ==> cauchy_filter F'"
  unfolding cauchy_filter_def by (meson dual_order.trans prod_filter_mono)

lemma (in uniform_space) convergent_filter_cauchy: 
  assumes "convergent_filter F"
  shows   "cauchy_filter F"
  using assms cauchy_filter_mono nhds_imp_cauchy_filter[OF order.refl]
  by (auto simp: convergent_filter_iff)

lemma (in topological_space) convergent_filter_bot [simp, intro]: "convergent_filter bot"
  by (simp add: convergent_filter_iff)



class complete_uniform_space = uniform_space +
  assumes cauchy_filter_convergent': "cauchy_filter (F :: 'a filter) ==> F ≠ bot ==> convergent_filter F"

lemma (in complete_uniform_space)
  cauchy_filter_convergent: "cauchy_filter (F :: 'a filter) ==> convergent_filter F"
  using cauchy_filter_convergent'[of F] by (cases "F = bot") auto

lemma (in complete_uniform_space) convergent_filter_iff_cauchy:
  "convergent_filter F ⟷ cauchy_filter F"
  using convergent_filter_cauchy cauchy_filter_convergent by blast

definition countably_generated_filter :: "'a filter ==> bool" where
  "countably_generated_filter F ⟷ (∃U :: nat ==> 'a set. F = (INF (n::nat). principal (U n)))"

lemma countably_generated_filter_has_antimono_basis:
  assumes "countably_generated_filter F"
  obtains B :: "nat ==> 'a set"
  where "antimono B" and "F = (INF n. principal (B n))" and
        "∧P. eventually P F ⟷ (∃i. ∀x∈B i. P x)"
proof -
  from assms obtain B where B: "F = (INF (n::nat). principal (B n))"
    unfolding countably_generated_filter_def by blast

  define B' where "B' = (λn. ∩k≤n. B k)"
  have "antimono B'"
    unfolding decseq_def B'_def by force

  have "(INF n. principal (B' n)) = (INF n. INF k∈{..n}. principal (B k))"
    unfolding B'_def by (intro INF_cong refl INF_principal_finite [symmetric]) auto
  also have "… = (INF (n::nat). principal (B n))"
    apply (intro antisym)
    apply (meson INF_lower INF_mono atMost_iff order_refl)
    apply (meson INF_greatest INF_lower UNIV_I)
    done
  also have "… = F"
    by (simp add: B)
  finally have F: "F = (INF n. principal (B' n))" ..

  moreover have "eventually P F ⟷ (∃i. eventually P (principal (B' i)))" for P
    unfolding F using ‹antimono B'›
    apply (subst eventually_INF_base)
      apply (auto simp: decseq_def)
    by (meson nat_le_linear)
  ultimately show ?thesis
    using ‹antimono B'› that[of B'] unfolding eventually_principal by blast
qed

lemma (in uniform_space) cauchy_filter_iff:
  "cauchy_filter F ⟷ (∀P. eventually P uniformity ⟶ (∃X. eventually (λx. x ∈ X) F ∧ (∀z∈X×X. P z)))" 
  unfolding cauchy_filter_def le_filter_def
  apply (auto simp: eventually_prod_same)
   apply (metis (full_types) eventually_mono mem_Collect_eq)
  apply blast
  done

lemma (in uniform_space) controlled_sequences_convergent_imp_complete_aux_sequence:
  fixes U :: "nat ==> ('a × 'a) set"
  fixes F :: "'a filter"
  assumes "cauchy_filter F" "F ≠ bot"
  assumes "∧n. eventually (λz. z ∈ U n) uniformity"
  obtains g G where
    "antimono G" "∧n. g n ∈ G n"
    "∧n. eventually (λx. x ∈ G n) F" "∧n. G n × G n ⊆ U n"
proof -
  have "∃C. eventually (λx. x ∈ C) F ∧ C × C ⊆ U n" for n
    using assms(1) assms(3)[of n] unfolding cauchy_filter_iff by blast
  then obtain G where G: "∧n. eventually (λx. x ∈ G n) F" "∧n. G n × G n ⊆ U n"
    by metis
  define G' where "G' = (λn. ∩k≤n. G k)"
  have 1: "eventually (λx. x ∈ G' n) F" for n
    using G by (auto simp: G'_def intro: eventually_ball_finite)
  have 2: "G' n × G' n ⊆ U n" for n
    using G unfolding G'_def by fast
  have 3: "antimono G'"
    unfolding G'_def decseq_def by force

  have "∃g. g ∈ G' n" for n
    using 1 assms(2) eventually_happens' by auto
  then obtain g where g: "∧n. g n ∈ G' n"
    by metis
  from g 1 2 3 that[of G' g] show ?thesis
    by metis
qed

definition lift_filter :: "('a set ==> 'b filter) ==> 'a filter ==> 'b filter" where
  "lift_filter f F = (INF X∈{X. eventually (λx. x ∈ X) F}. f X)"

lemma lift_filter_top [simp]: "lift_filter g top = g UNIV"
proof -
  have "{X. ∀x::'b. x ∈ X} = {UNIV}"
    by auto
  thus ?thesis
    by (simp add: lift_filter_def)
qed

lemma eventually_lift_filter_iff:
  assumes "mono g"
  shows   "eventually P (lift_filter g F) ⟷ (∃X. eventually (λx. x ∈ X) F ∧ eventually P (g X))"
  unfolding lift_filter_def
proof (subst eventually_INF_base, goal_cases)
  case 1
  thus ?case by (auto intro: exI[of _ UNIV])
next
  case (2 X Y)
  thus ?case
    by (auto intro!: exI[of _ "X ∩ Y"] eventually_conj monoD[OF assms])
qed auto

lemma lift_filter_le:
  assumes "eventually (λx. x ∈ X) F" "g X ≤ F'"
  shows   "lift_filter g F ≤ F'"
  unfolding lift_filter_def
  by (metis INF_lower2 assms mem_Collect_eq)

definition lift_filter' :: "('a set ==> 'b set) ==> 'a filter ==> 'b filter" where
  "lift_filter' f F = lift_filter (principal ∘ f) F"

lemma lift_filter'_top [simp]: "lift_filter' g top = principal (g UNIV)"
  by (simp add: lift_filter'_def)

lemma eventually_lift_filter'_iff:
  assumes "mono g"
  shows   "eventually P (lift_filter' g F) ⟷ (∃X. eventually (λx. x ∈ X) F ∧ (∀x∈g X. P x))"
  unfolding lift_filter'_def using assms
  by (subst eventually_lift_filter_iff) (auto simp: mono_def eventually_principal)

lemma lift_filter'_le:
  assumes "eventually (λx. x ∈ X) F" "principal (g X) ≤ F'"
  shows   "lift_filter' g F ≤ F'"
  unfolding lift_filter'_def using assms
  by (intro lift_filter_le[where X = X]) auto


lemma (in uniform_space) comp_uniformity_le_uniformity:
  "lift_filter' (λX. X O X) uniformity ≤ uniformity"
  unfolding le_filter_def
proof safe
  fix P assume P: "eventually P uniformity"
  have [simp]: "mono (λX::('a × 'a) set. X O X)"
    by (intro monoI) auto
  from P obtain P' where P': "eventually P' uniformity " "(∧x y z. P' (x, y) ==> P' (y, z) ==> P (x, z))"
    using uniformity_transE by blast
  show "eventually P (lift_filter' (λX. X O X) uniformity)"
    by (auto simp: eventually_lift_filter'_iff intro!: exI[of _ "{x. P' x}"] P')
qed

lemma (in uniform_space) comp_mem_uniformity_sets:
  assumes "eventually (λz. z ∈ X) uniformity"
  obtains Y where "eventually (λz. z ∈ Y) uniformity" "Y O Y ⊆ X"
proof -
  have [simp]: "mono (λX::('a × 'a) set. X O X)"
    by (intro monoI) auto
  have "eventually (λz. z ∈ X) (lift_filter' (λX. X O X) uniformity)"
    using assms comp_uniformity_le_uniformity using filter_leD by blast
  thus ?thesis using that
    by (auto simp: eventually_lift_filter'_iff)
qed

lemma (in uniform_space) le_nhds_of_cauchy_adhp_aux:
  assumes "∧P. eventually P uniformity ==> (∃X. eventually (λy. y ∈ X) F ∧ (∀z∈X × X. P z) ∧ (∃y. P (x, y) ∧ y ∈ X))"
  shows   "F ≤ nhds x"
  unfolding le_filter_def
proof safe
  fix P assume "eventually P (nhds x)"
  hence "∀🪙F z in uniformity. z ∈ {z. fst z = x ⟶ P (snd z)}"
    by (simp add: eventually_nhds_uniformity case_prod_unfold)
  then obtain Y where Y: "∀🪙F z in uniformity. z ∈ Y" "Y O Y ⊆ {z. fst z = x ⟶ P (snd z)}"
    using comp_mem_uniformity_sets by blast
  obtain X y where Xy: "eventually (λy. y ∈ X) F" "X×X ⊆ Y" "(x, y) ∈ Y" "y ∈ X"
    using assms[OF Y(1)] by blast
  have *: "P x" if "x ∈ X" for x
    using Y(2) Xy(2-4) that unfolding relcomp_unfold by force  
  show "eventually P F"
    by (rule eventually_mono[OF Xy(1)]) (use * in auto)
qed

lemma (in uniform_space) eventually_uniformity_imp_nhds:
  assumes "eventually P uniformity"
  shows   "eventually (λy. P (x, y)) (nhds x)"
  using assms unfolding eventually_nhds_uniformity by (elim eventually_mono) auto

lemma (in uniform_space) controlled_sequences_convergent_imp_complete_aux:
  fixes U :: "nat ==> ('a × 'a) set"
  assumes gen: "countably_generated_filter (uniformity :: ('a × 'a) filter)"
  assumes U: "∧n. eventually (λz. z ∈ U n) uniformity"
  assumes conv: "∧(u :: nat ==> 'a). (∧N m n. N ≤ m ==> N ≤ n ==> (u m, u n) ∈ U N) ==> convergent u"
  assumes "cauchy_filter F"
  shows   "convergent_filter F"
proof (cases "F = bot")
  case False
  note F = ‹cauchy_filter F› ‹F ≠ bot›
  from gen obtain B :: "nat ==> ('a × 'a) set" where B:
    "antimono B" "uniformity = (INF n. principal (B n))"
    "∧P. eventually P uniformity ⟷ (∃i. ∀x∈B i. P x)"
    using countably_generated_filter_has_antimono_basis by blast

  have ev_B: "eventually (λz. z ∈ B n) uniformity" for n
    by (subst B(3)) auto
  hence ev_B': "eventually (λz. z ∈ B n ∩ U n) uniformity" for n
    using U by (auto intro: eventually_conj)

  obtain g G where gG: "antimono G" "∧n. g n ∈ G n"
    "∧n. eventually (λx. x ∈ G n) F" "∧n. G n × G n ⊆ B n ∩ U n"
    using controlled_sequences_convergent_imp_complete_aux_sequence[of F "λn. B n ∩ U n", OF F ev_B']
    by metis

  have "convergent g"
  proof (rule conv)
    fix N m n :: nat
    assume mn: "N ≤ m" "N ≤ n"
    have "(g m, g n) ∈ G m × G n"
      using gG by auto
    also from mn have "… ⊆ G N × G N"
      by (intro Sigma_mono gG antimonoD[OF gG(1)])
    also have "… ⊆ U N"
      using gG by blast
    finally show "(g m, g n) ∈ U N" .
  qed
  then obtain L where G: "g <---- L"
    unfolding convergent_def by blast

  have "F ≤ nhds L"
  proof (rule le_nhds_of_cauchy_adhp_aux)
    fix P :: "'a × 'a ==> bool"
    assume P: "eventually P uniformity"
    hence "eventually (λn. ∀x∈B n. P x) sequentially"
      using ‹antimono B› unfolding B(3) eventually_sequentially decseq_def by blast
    moreover have "eventually (λn. P (L, g n)) sequentially"
      using P eventually_compose_filterlim eventually_uniformity_imp_nhds G by blast
    ultimately have "eventually (λn. (∀x∈B n. P x) ∧ P (L, g n)) sequentially"
      by eventually_elim auto
    then obtain n where "∀x∈B n. P x" "P (L, g n)"
      unfolding eventually_at_top_linorder by blast
    then show "∃X. (∀🪙F y in F. y ∈ X) ∧ (∀z∈X × X. P z) ∧ (∃y. P (L, y) ∧ y ∈ X)"
      using gG by blast+
  qed
  thus "convergent_filter F"
    by (auto simp: convergent_filter_iff)
qed auto

theorem (in uniform_space) controlled_sequences_convergent_imp_complete:
  fixes U :: "nat ==> ('a × 'a) set"
  assumes gen: "countably_generated_filter (uniformity :: ('a × 'a) filter)"
  assumes U: "∧n. eventually (λz. z ∈ U n) uniformity"
  assumes conv: "∧(u :: nat ==> 'a). (∧N m n. N ≤ m ==> N ≤ n ==> (u m, u n) ∈ U N) ==> convergent u"
  shows "class.complete_uniform_space open uniformity"
  by unfold_locales (use assms controlled_sequences_convergent_imp_complete_aux in blast)

lemma filtermap_prod_filter: "filtermap (map_prod f g) (F ×🪙F G) = filtermap f F ×🪙F filtermap g G"
proof (intro antisym)
  show "filtermap (map_prod f g) (F ×🪙F G) ≤ filtermap f F ×🪙F filtermap g G"
    by (auto simp: le_filter_def eventually_filtermap eventually_prod_filter)
next
  show "filtermap f F ×🪙F filtermap g G ≤ filtermap (map_prod f g) (F ×🪙F G)"
    unfolding le_filter_def
  proof safe
    fix P assume P: "eventually P (filtermap (map_prod f g) (F ×🪙F G))"
    then obtain Pf Pg where *: "eventually Pf F" "eventually Pg G" "∀x. Pf x ⟶ (∀y. Pg y ⟶ P (f x, g y))"
      by (auto simp: eventually_filtermap eventually_prod_filter)

    define Pf' where "Pf' = (λx. ∃y. x = f y ∧ Pf y)"
    define Pg' where "Pg' = (λx. ∃y. x = g y ∧ Pg y)"

    from *(1) have "∀🪙F x in F. Pf' (f x)"
      by eventually_elim (auto simp: Pf'_def)
    moreover from *(2) have "∀🪙F x in G. Pg' (g x)"
      by eventually_elim (auto simp: Pg'_def)
    moreover have "(∀x y. Pf' x ⟶ Pg' y ⟶ P (x, y))"
      using *(3) by (auto simp: Pf'_def Pg'_def)
    ultimately show "eventually P (filtermap f F ×🪙F filtermap g G)"
      unfolding eventually_prod_filter eventually_filtermap
      by blast
  qed
qed
      

lemma (in uniform_space) Cauchy_seq_iff_tendsto:
  "Cauchy f ⟷ filterlim (map_prod f f) uniformity (at_top ×🪙F at_top)"
  unfolding Cauchy_uniform cauchy_filter_def filterlim_def filtermap_prod_filter ..

theorem (in uniform_space) controlled_seq_imp_Cauchy_seq:
  fixes U :: "nat ==> ('a × 'a) set"
  assumes U: "∧P. eventually P uniformity ==> (∃n. ∀x∈U n. P x)"
  assumes controlled: "∧N m n. N ≤ m ==> N ≤ n ==> (f m, f n) ∈ U N"
  shows   "Cauchy f"
  unfolding Cauchy_seq_iff_tendsto
proof -
  show "filterlim (map_prod f f) uniformity (sequentially ×🪙F sequentially)"
    unfolding filterlim_def le_filter_def
  proof safe
    fix P :: "'a × 'a ==> bool"
    assume P: "eventually P uniformity"
    from U[OF this] obtain N where "∀x∈U N. P x"
      by blast
    then show "eventually P (filtermap (map_prod f f) (sequentially ×🪙F sequentially))"
      unfolding eventually_filtermap eventually_prod_sequentially
      by (metis controlled map_prod_simp)
  qed
qed

lemma (in uniform_space) Cauchy_seq_convergent_imp_complete_aux:
  fixes U :: "nat ==> ('a × 'a) set"
  assumes gen: "countably_generated_filter (uniformity :: ('a × 'a) filter)"
  assumes conv: "∧(u :: nat ==> 'a). Cauchy u ==> convergent u"
  assumes "cauchy_filter F"
  shows   "convergent_filter F"
proof -
  from gen obtain B :: "nat ==> ('a × 'a) set" where B:
    "antimono B" "uniformity = (INF n. principal (B n))"
    "∧P. eventually P uniformity ⟷ (∃i. ∀x∈B i. P x)"
    using countably_generated_filter_has_antimono_basis by blast

  show ?thesis
  proof (rule controlled_sequences_convergent_imp_complete_aux[where U = B])
    show "∀🪙F z in uniformity. z ∈ B n" for n
      unfolding B(3) by blast
  next
    fix f :: "nat ==> 'a"
    assume f: "∧N m n. N ≤ m ==> N ≤ n ==> (f m, f n) ∈ B N"
    have "Cauchy f" using f B
      by (intro controlled_seq_imp_Cauchy_seq[where U = B]) auto
    with conv show "convergent f"
      by simp
  qed fact+
qed

theorem (in uniform_space) Cauchy_seq_convergent_imp_complete:
  fixes U :: "nat ==> ('a × 'a) set"
  assumes gen: "countably_generated_filter (uniformity :: ('a × 'a) filter)"
  assumes conv: "∧(u :: nat ==> 'a). Cauchy u ==> convergent u"
  shows   "class.complete_uniform_space open uniformity"
  by unfold_locales (use assms Cauchy_seq_convergent_imp_complete_aux in blast)

lemma (in metric_space) countably_generated_uniformity:
  "countably_generated_filter uniformity"
proof -
  have "(INF e∈{0<..}. principal {(x, y). dist (x::'a) y < e}) =
        (INF n∈UNIV. principal {(x, y). dist x y < 1 / real (Suc n)})" (is "?F = ?G")
    unfolding uniformity_dist
  proof (intro antisym)
    have "?G = (INF e∈(λn. 1 / real (Suc n)) ` UNIV. principal {(x, y). dist x y < e})"
      by (simp add: image_image)
    also have "… ≥ ?F"
      by (intro INF_superset_mono) auto
    finally show "?F ≤ ?G" .
  next
    show "?G ≤ ?F"
      unfolding le_filter_def
    proof safe
      fix P assume "eventually P ?F"
      then obtain ε where ε: "ε > 0" "eventually P (principal {(x, y). dist x y < ε})"
      proof (subst (asm) eventually_INF_base, goal_cases)
        case (2 ε1 ε2)
        thus ?case
          by (intro bexI[of _ "min ε1 ε2"]) auto
      qed auto
      from ‹ε > 0› obtain n where "1 / real (Suc n) < ε"
        using nat_approx_posE by blast
      then have "eventually P (principal {(x, y). dist x y < 1 / real (Suc n)})"
        using ε(2) by (auto simp: eventually_principal)
      thus "eventually P ?G"
        by (intro eventually_INF1) auto
    qed
  qed
  thus "countably_generated_filter uniformity"
    unfolding countably_generated_filter_def uniformity_dist by fast
qed

subclass (in complete_space) complete_uniform_space
proof (rule Cauchy_seq_convergent_imp_complete)
  show "convergent f" if "Cauchy f" for f
    using Cauchy_convergent that by blast
qed (fact countably_generated_uniformity)

lemma (in complete_uniform_space) complete_UNIV_cuspace [intro]: "complete UNIV"
  unfolding complete_uniform using cauchy_filter_convergent
  by (auto simp: convergent_filter.simps)



lemma norm_infsum_le:
  assumes "(f has_sum S) X"
  assumes "(g has_sum T) X"
  assumes "∧x. x ∈ X ==> norm (f x) ≤ g x"
  shows   "norm S ≤ T"
proof (rule tendsto_le)
  show "((λY. norm (∑x∈Y. f x)) ---> norm S) (finite_subsets_at_top X)"
    using assms(1) unfolding has_sum_def by (intro tendsto_norm)
  show "((λY. ∑x∈Y. g x) ---> T) (finite_subsets_at_top X)"
    using assms(2) unfolding has_sum_def .
  show "∀🪙F x in finite_subsets_at_top X. norm (sum f x) ≤ (∑x∈x. g x)"
    by (simp add: assms(3) eventually_finite_subsets_at_top_weakI subsetD sum_norm_le)
qed auto

(*
 lemma summable_on_Sigma:
  fixes A :: "'a set" and B :: "'a ==> 'b set"
  and f :: ‹'a ==> 'b ==> 'c::{comm_monoid_add, t2_space, uniform_space}›
  assumes plus_cont: ‹uniformly_continuous_on UNIV (λ(x::'c,y). x+y)›
  assumes summableAB: "(λ(x,y). f x y) summable_on (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> (f x) summable_on (B x)›
  shows ‹(λx. infsum (f x) (B x)) summable_on A›
*)

lemma has_sum_imp_summable: "(f has_sum S) A ==> f summable_on A"
  by (auto simp: summable_on_def)

lemma has_sum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "((λx. f (g x)) has_sum S) A = (f has_sum S) B"
proof -
  have "((λx. f (g x)) has_sum S) A ⟷ (f has_sum S) (g ` A)"
    by (subst has_sum_reindex) (use assms in ‹auto dest: bij_betw_imp_inj_on simp: o_def›)
  then show ?thesis
    using assms bij_betw_imp_surj_on by blast 
qed

lemma has_sum_reindex_bij_witness:
  assumes "∧a. a ∈ S ==> i (j a) = a"
  assumes "∧a. a ∈ S ==> j a ∈ T"
  assumes "∧b. b ∈ T ==> j (i b) = b"
  assumes "∧b. b ∈ T ==> i b ∈ S"
  assumes "∧a. a ∈ S ==> h (j a) = g a"
  assumes "s = s'"
  shows   "(g has_sum s) S = (h has_sum s') T"
  by (smt (verit, del_insts) assms bij_betwI' has_sum_cong has_sum_reindex_bij_betw)

lemma summable_on_reindex_bij_witness:
  assumes "∧a. a ∈ S ==> i (j a) = a"
  assumes "∧a. a ∈ S ==> j a ∈ T"
  assumes "∧b. b ∈ T ==> j (i b) = b"
  assumes "∧b. b ∈ T ==> i b ∈ S"
  assumes "∧a. a ∈ S ==> h (j a) = g a"
  shows   "g summable_on S ⟷ h summable_on T"
  using has_sum_reindex_bij_witness[of S i j T h g, OF assms]
  by (simp add: summable_on_def)

lemma infsum_reindex_bij_witness:
  assumes "∧a. a ∈ S ==> i (j a) = a"
  assumes "∧a. a ∈ S ==> j a ∈ T"
  assumes "∧b. b ∈ T ==> j (i b) = b"
  assumes "∧b. b ∈ T ==> i b ∈ S"
  assumes "∧a. a ∈ S ==> h (j a) = g a"
  shows   "infsum g S = infsum h T"
proof (cases "g summable_on S")
  case True
  then obtain s where s: "(g has_sum s) S"
    by (auto simp: summable_on_def)
  also have "?this ⟷ (h has_sum s) T"
    by (rule has_sum_reindex_bij_witness[of _ i j]) (use assms in auto)
  finally have s': "(h has_sum s) T" .
  show ?thesis
    using infsumI[OF s] infsumI[OF s'] by simp
next
  case False
  note ‹¬g summable_on S›
  also have "g summable_on S ⟷ h summable_on T"
    by (rule summable_on_reindex_bij_witness[of _ i j]) (use assms in auto)
  finally show ?thesis
    using False by (simp add: infsum_not_exists)
qed

lemma has_sum_homomorphism:
  assumes "(f has_sum S) A" "h 0 = 0" "∧a b. h (a + b) = h a + h b" "continuous_on UNIV h"
  shows   "((λx. h (f x)) has_sum (h S)) A"
proof -
  have "sum (h ∘ f) X = h (sum f X)" for X
    by (induction X rule: infinite_finite_induct) (simp_all add: assms)
  hence sum_h: "sum (h ∘ f) = h ∘ sum f"
    by (intro ext) auto
  then have "((h ∘ f) has_sum h S) A"
    using assms
    by (metis UNIV_I continuous_on_def has_sum_comm_additive_general o_apply)
  thus ?thesis
    by (simp add: o_def)
qed

lemma summable_on_homomorphism:
  assumes "f summable_on A" "h 0 = 0" "∧a b. h (a + b) = h a + h b" "continuous_on UNIV h"
  shows   "(λx. h (f x)) summable_on A"
proof -
  from assms(1) obtain S where "(f has_sum S) A"
    by (auto simp: summable_on_def)
  hence "((λx. h (f x)) has_sum h S) A"
    by (rule has_sum_homomorphism) (use assms in auto)
  thus ?thesis
    by (auto simp: summable_on_def)
qed

lemma infsum_homomorphism_strong:
  fixes h :: "'a :: {t2_space, topological_comm_monoid_add} ==>
                'b :: {t2_space, topological_comm_monoid_add}"
  assumes "(λx. h (f x)) summable_on A ⟷ f summable_on A"
  assumes "h 0 = 0" 
  assumes "∧S. (f has_sum S) A ==> ((λx. h (f x)) has_sum (h S)) A"
  shows   "infsum (λx. h (f x)) A = h (infsum f A)"
  by (metis assms has_sum_infsum infsumI infsum_not_exists)

lemma has_sum_bounded_linear:
  assumes "bounded_linear h" and "(f has_sum S) A"
  shows "((λx. h (f x)) has_sum h S) A"
proof -
  interpret bounded_linear h by fact
  from assms(2) show ?thesis
    by (rule has_sum_homomorphism) (auto simp: add intro!: continuous_on)
qed

lemma summable_on_bounded_linear:
  assumes "bounded_linear h" and "f summable_on A"
  shows "(λx. h (f x)) summable_on A"
  by (metis assms has_sum_bounded_linear summable_on_def)

lemma summable_on_bounded_linear_iff:
  assumes "bounded_linear h" and "bounded_linear h'" and "∧x. h' (h x) = x"
  shows "(λx. h (f x)) summable_on A ⟷ f summable_on A"
  by (metis (full_types) assms summable_on_bounded_linear summable_on_cong)

lemma infsum_bounded_linear_strong:
  fixes h :: "'a :: real_normed_vector ==> 'b :: real_normed_vector"
  assumes "(λx. h (f x)) summable_on A ⟷ f summable_on A"
  assumes "bounded_linear h"
  shows   "infsum (λx. h (f x)) A = h (infsum f A)"
proof -
  interpret bounded_linear h by fact
  show ?thesis
    by (rule infsum_homomorphism_strong)
       (insert assms, auto intro: add continuous_on has_sum_bounded_linear)
qed

lemma infsum_bounded_linear_strong':
  fixes mult :: "'c :: zero ==> 'a :: real_normed_vector ==> 'b :: real_normed_vector"
  assumes "c ≠ 0 ==> (λx. mult c (f x)) summable_on A ⟷ f summable_on A"
  assumes "bounded_linear (mult c)"
  assumes [simp]: "∧x. mult 0 x = 0"
  shows   "infsum (λx. mult c (f x)) A = mult c (infsum f A)"
  by (metis assms infsum_0 infsum_bounded_linear_strong)

lemma has_sum_scaleR:
  fixes f :: "'a ==> 'b :: real_normed_vector"
  assumes "(f has_sum S) A"
  shows   "((λx. c *🪙R f x) has_sum (c *🪙R S)) A"
  using has_sum_bounded_linear[OF bounded_linear_scaleR_right[of c], of f A S] assms by simp

lemma has_sum_scaleR_iff:
  fixes f :: "'a ==> 'b :: real_normed_vector"
  assumes "c ≠ 0"
  shows   "((λx. c *🪙R f x) has_sum S) A ⟷ (f has_sum (S /🪙R c)) A"
  using has_sum_scaleR[of f A "S /🪙R c" c] has_sum_scaleR[of "λx. c *🪙R f x" A S "inverse c"] assms
  by auto

lemma has_sum_of_nat: "(f has_sum S) A ==> ((λx. of_nat (f x)) has_sum of_nat S) A"
  by (erule has_sum_homomorphism) (auto intro!: continuous_intros)

lemma has_sum_of_int: "(f has_sum S) A ==> ((λx. of_int (f x)) has_sum of_int S) A"
  by (erule has_sum_homomorphism) (auto intro!: continuous_intros)

lemma summable_on_of_nat: "f summable_on A ==> (λx. of_nat (f x)) summable_on A"
  by (erule summable_on_homomorphism) (auto intro!: continuous_intros)

lemma summable_on_of_int: "f summable_on A ==> (λx. of_int (f x)) summable_on A"
  by (erule summable_on_homomorphism) (auto intro!: continuous_intros)

lemma summable_on_of_real:
  "f summable_on A ==> (λx. of_real (f x) :: 'a :: real_normed_algebra_1) summable_on A"
  using summable_on_bounded_linear[of "of_real :: real ==> 'a", OF bounded_linear_of_real, of f A]
  by simp

lemma has_sum_of_real_iff:
  "((λx. of_real (f x) :: 'a :: real_normed_div_algebra) has_sum (of_real c)) A ⟷
   (f has_sum c) A"
proof -
  have "((λx. of_real (f x) :: 'a) has_sum (of_real c)) A ⟷
        (sum (λx. of_real (f x) :: 'a) ---> of_real c) (finite_subsets_at_top A)"
    by (simp add: has_sum_def)
  also have "sum (λx. of_real (f x) :: 'a) = (λX. of_real (sum f X))"
    by simp
  also have "((λX. of_real (sum f X) :: 'a) ---> of_real c) (finite_subsets_at_top A) ⟷
             (f has_sum c) A"
    unfolding has_sum_def tendsto_of_real_iff ..
  finally show ?thesis .
qed

lemma has_sum_of_real:
  "(f has_sum S) A ==> ((λx. of_real (f x) :: 'a :: real_normed_algebra_1) has_sum of_real S) A"
  using has_sum_bounded_linear[of "of_real :: real ==> 'a", OF bounded_linear_of_real, of f A S]
  by simp

lemma summable_on_discrete_iff:
  fixes f :: "'a ==> 'b :: {discrete_topology, topological_comm_monoid_add, cancel_comm_monoid_add}"
  shows "f summable_on A ⟷ finite {x∈A. f x ≠ 0}"
proof
  assume *: "finite {x∈A. f x ≠ 0}"
  hence "f summable_on {x∈A. f x ≠ 0}"
    by (rule summable_on_finite)
  then show "f summable_on A"
    by (smt (verit) DiffE mem_Collect_eq summable_on_cong_neutral) 
next
  assume "f summable_on A"
  then obtain S where "(f has_sum S) A"
    by (auto simp: summable_on_def)
  hence "∀🪙F x in finite_subsets_at_top A. sum f x = S"
    unfolding has_sum_def tendsto_discrete .
  then obtain X where X: "finite X" "X ⊆ A" "∧Y. finite Y ==> X ⊆ Y ==> Y ⊆ A ==> sum f Y = S"
    unfolding eventually_finite_subsets_at_top by metis
  have "{x∈A. f x ≠ 0} ⊆ X"
  proof
    fix x assume x: "x ∈ {x∈A. f x ≠ 0}"
    show "x ∈ X"
    proof (rule ccontr)
      assume [simp]: "x ∉ X"
      have "sum f (insert x X) = S"
        using X x by (intro X) auto
      then have "f x = 0"
        using X by auto
      with x show False
        by auto
    qed
  qed
  thus "finite {x∈A. f x ≠ 0}"
    using X(1) finite_subset by blast
qed

lemma has_sum_imp_sums: "(f has_sum S) (UNIV :: nat set) ==> f sums S"
  unfolding sums_def has_sum_def by (rule filterlim_compose[OF _ filterlim_lessThan_at_top])

lemma summable_on_imp_summable: "f summable_on (UNIV :: nat set) ==> summable f"
  unfolding summable_on_def summable_def by (auto dest: has_sum_imp_sums)

lemma summable_on_UNIV_nonneg_real_iff:
  assumes "∧n. f n ≥ (0 :: real)"
  shows   "f summable_on UNIV ⟷ summable f"
  using assms by (auto intro: norm_summable_imp_summable_on summable_on_imp_summable)

lemma summable_on_imp_bounded_partial_sums:
  fixes f :: "_ ==> 'a :: {topological_comm_monoid_add, linorder_topology}"
  assumes f: "f summable_on A"
  shows   "∃C. eventually (λX. sum f X ≤ C) (finite_subsets_at_top A)"
proof -
  from assms obtain S where S: "(sum f ---> S) (finite_subsets_at_top A)"
    unfolding summable_on_def has_sum_def by blast
  show ?thesis
  proof (cases "∃C. C > S")
    case True
    then obtain C where C: "C > S"
      by blast
    have "∀🪙F X in finite_subsets_at_top A. sum f X < C"
      using S C by (rule order_tendstoD(2))
    thus ?thesis
      by (meson eventually_mono nless_le)
  next
    case False thus ?thesis
      by (meson not_eventuallyD not_le_imp_less)
  qed
qed

lemma has_sum_mono':
  fixes S S' :: "'a :: {linorder_topology, ordered_comm_monoid_add, topological_comm_monoid_add}"
  assumes f: "(f has_sum S) A" "(f has_sum S') B" 
     and AB: "A ⊆ B" "∧x. x ∈ B - A ==> f x ≥ 0"
  shows   "S ≤ S'"
  using AB has_sum_mono_neutral[OF f] by fastforce


context
  assumes "SORT_CONSTRAINT('a :: {topological_comm_monoid_add, order_topology,
             ordered_comm_monoid_add, conditionally_complete_linorder})"
begin

text ‹
  Any family of non-negative numbers with bounded partial sums is summable, and the sum
  is simply the supremum of the partial sums.
 ›
lemma nonneg_bounded_partial_sums_imp_has_sum_SUP:
  assumes nonneg: "∧x. x ∈ A ==> f x ≥ (0::'a)"
      and bound:  "eventually (λX. sum f X ≤ C) (finite_subsets_at_top A)"
  shows   "(f has_sum (SUP X∈{X. X ⊆ A ∧ finite X}. sum f X)) A"
proof -
  from bound obtain X0
    where X0: "X0 ⊆ A" "finite X0" "∧X. X0 ⊆ X ==> X ⊆ A ==> finite X ==> sum f X ≤ C"
    by (force simp: eventually_finite_subsets_at_top)
  have bound': "sum f X ≤ C" if "X ⊆ A" "finite X" for X
  proof -
    have "sum f X ≤ sum f (X ∪ X0)"
      using that X0 assms(1) by (intro sum_mono2) auto
    also have "… ≤ C"
      by (simp add: X0 that)
    finally show ?thesis .
  qed
  hence bdd: "bdd_above (sum f ` {X. X ⊆ A ∧ finite X})"
    by (auto simp: bdd_above_def)

  show ?thesis unfolding has_sum_def
  proof (rule increasing_tendsto)
    show "∀🪙F X in finite_subsets_at_top A. sum f X ≤ Sup (sum f ` {X. X ⊆ A ∧ finite X})"
      by (intro eventually_finite_subsets_at_top_weakI cSUP_upper[OF _ bdd]) auto
  next
    fix y assume "y < Sup (sum f ` {X. X ⊆ A ∧ finite X})"
    then obtain X where X: "X ⊆ A" "finite X" "y < sum f X"
      by (subst (asm) less_cSUP_iff[OF _ bdd]) auto
    from X have "eventually (λX'. X ⊆ X' ∧ X' ⊆ A ∧ finite X') (finite_subsets_at_top A)"
      by (auto simp: eventually_finite_subsets_at_top)
    thus "eventually (λX'. y < sum f X') (finite_subsets_at_top A)"
    proof eventually_elim
      case (elim X')
      note ‹y 🚫 f X›
      also have "sum f X ≤ sum f X'"
        using nonneg elim by (intro sum_mono2) auto
      finally show ?case .
    qed
  qed
qed

lemma nonneg_bounded_partial_sums_imp_summable_on:
  assumes nonneg: "∧x. x ∈ A ==> f x ≥ (0::'a)"
      and bound:  "eventually (λX. sum f X ≤ C) (finite_subsets_at_top A)"
  shows   "f summable_on A"
  using nonneg_bounded_partial_sums_imp_has_sum_SUP[OF assms] by (auto simp: summable_on_def)

end

context
  assumes "SORT_CONSTRAINT('a :: {topological_comm_monoid_add, linorder_topology,
             ordered_comm_monoid_add, conditionally_complete_linorder})"
begin

lemma summable_on_comparison_test:
  assumes "f summable_on A" and "∧x. x ∈ A ==> g x ≤ f x" and "∧x. x ∈ A ==> (0::'a) ≤ g x"
  shows   "g summable_on A"
proof -
  obtain C where C: "∀🪙F X in finite_subsets_at_top A. sum f X ≤ C"
    using assms(1) summable_on_imp_bounded_partial_sums by blast
  show ?thesis
  proof (rule nonneg_bounded_partial_sums_imp_summable_on)
    show "∀🪙F X in finite_subsets_at_top A. sum g X ≤ C"
      using C assms 
      unfolding eventually_finite_subsets_at_top
      by (smt (verit, ccfv_SIG) order_trans subsetD sum_mono)
  qed (use assms in auto)
qed

end



lemma summable_on_subset:
  fixes f :: "_ ==> 'a :: {uniform_topological_group_add, topological_comm_monoid_add, ab_group_add, complete_uniform_space}"
  assumes "f summable_on A" "B ⊆ A"
  shows "f summable_on B"
  by (rule summable_on_subset_aux[OF _ _ assms]) (auto simp: uniformly_continuous_add)

lemma summable_on_union:
  fixes f :: "_ ==> 'a :: {uniform_topological_group_add, topological_comm_monoid_add, ab_group_add, complete_uniform_space}"
  assumes "f summable_on A" "f summable_on B"
  shows "f summable_on (A ∪ B)"
proof -
  have "f summable_on (A ∪ (B - A))"
    by (meson Diff_disjoint Diff_subset assms summable_on_Un_disjoint summable_on_subset)
  also have "A ∪ (B - A) = A ∪ B"
    by blast
  finally show ?thesis .
qed

lemma summable_on_insert_iff:
  fixes f :: "_ ==> 'a :: {uniform_topological_group_add, topological_comm_monoid_add, ab_group_add, complete_uniform_space}"
  shows "f summable_on insert x A ⟷ f summable_on A"
  using summable_on_union[of f A "{x}"] by (auto intro: summable_on_subset)

lemma has_sum_insert:
  fixes f :: "'a ==> 'b :: topological_comm_monoid_add"
  assumes "x ∉ A" and "(f has_sum S) A"
  shows   "(f has_sum (f x + S)) (insert x A)"
proof -
  have "(f has_sum (f x + S)) ({x} ∪ A)"
    using assms by (intro has_sum_Un_disjoint) (auto intro: has_sum_finiteI)
  thus ?thesis by simp
qed

lemma infsum_insert:
  fixes f :: "_ ==> 'a :: {topological_comm_monoid_add, t2_space}"
  assumes "f summable_on A" "a ∉ A"
  shows   "infsum f (insert a A) = f a + infsum f A"
  by (meson assms has_sum_insert infsumI summable_iff_has_sum_infsum)

lemma has_sum_SigmaD:
  fixes f :: "'b × 'c ==> 'a :: {topological_comm_monoid_add,t3_space}"
  assumes sum1: "(f has_sum S) (Sigma A B)"
  assumes sum2: "∧x. x ∈ A ==> ((λy. f (x, y)) has_sum g x) (B x)"
  shows   "(g has_sum S) A"
  unfolding has_sum_def tendsto_def eventually_finite_subsets_at_top
proof (safe, goal_cases)
  case (1 X)
  with nhds_closed[of S X] obtain X'
    where X': "S ∈ X'" "closed X'" "X' ⊆ X" "eventually (λy. y ∈ X') (nhds S)" by blast
  from X'(4) obtain X'' where X'': "S ∈ X''" "open X''" "X'' ⊆ X'"
    by (auto simp: eventually_nhds)
  with sum1 obtain Y :: "('b × 'c) set"
    where Y: "Y ⊆ Sigma A B" "finite Y"
             "∧Z. Y ⊆ Z ==> Z ⊆ Sigma A B ==> finite Z ==> sum f Z ∈ X''"
    unfolding has_sum_def tendsto_def eventually_finite_subsets_at_top by force
  define Y1 :: "'b set" where "Y1 = fst ` Y"
  from Y have Y1: "Y1 ⊆ A" by (auto simp: Y1_def)
  define Y2 :: "'b ==> 'c set" where "Y2 = (λx. {y. (x, y) ∈ Y})"
  have Y2: "finite (Y2 x)" "Y2 x ⊆ B x" if "x ∈ A" for x
    using that Y(1,2) unfolding Y2_def
    by (force simp: image_iff intro: finite_subset[of _ "snd ` Y"])+

  show ?case
  proof (rule exI[of _ Y1], safe, goal_cases)
    case (3 Z)
    define H where "H = (INF x∈Z. filtercomap (λp. p x) (finite_subsets_at_top (B x)))"
    
    have "sum g Z ∈ X'"
    proof (rule Lim_in_closed_set)
      show "closed X'" by fact
    next
      show "((λB'. sum (λx. sum (λy. f (x, y)) (B' x)) Z) ---> sum g Z) H"
        unfolding H_def
      proof (intro tendsto_sum filterlim_INF')
        fix x assume x: "x ∈ Z"
        with 3 have "x ∈ A" by auto
        from sum2[OF this] have "(sum (λy. f (x, y)) ---> g x) (finite_subsets_at_top (B x))"
          by (simp add: has_sum_def)
        thus "((λB'. sum (λy. f (x, y)) (B' x)) ---> g x)
                 (filtercomap (λp. p x) (finite_subsets_at_top (B x)))"
          by (rule filterlim_compose[OF _ filterlim_filtercomap])
      qed auto
    next
      show "∀🪙F h in H. sum (λx. sum (λy. f (x, y)) (h x)) Z ∈ X'"
        unfolding H_def
      proof (subst eventually_INF_finite[OF ‹finite Z›], rule exI, safe)
        fix x assume x: "x ∈ Z"
        hence x': "x ∈ A" using 3 by auto
        show "eventually (λh. finite (h x) ∧ Y2 x ⊆ h x ∧ h x ⊆ B x)
                (filtercomap (λp. p x) (finite_subsets_at_top (B x)))" using 3 Y2[OF x']
          by (intro eventually_filtercomapI)
             (auto simp: eventually_finite_subsets_at_top intro: exI[of _ "Y2 x"])
      next
        fix h
        assume *: "∀x∈Z. finite (h x) ∧ Y2 x ⊆ h x ∧ h x ⊆ B x"
        hence "sum (λx. sum (λy. f (x, y)) (h x)) Z = sum f (Sigma Z h)"
          using ‹finite Z› by (subst sum.Sigma) auto
        also have "… ∈ X''"
          using * 3 Y(1,2) by (intro Y; force simp: Y1_def Y2_def)
        also have "X'' ⊆ X'" by fact
        finally show "sum (λx. sum (λy. f (x, y)) (h x)) Z ∈ X'" .
      qed
    next
      have "H = (INF x∈SIGMA x:Z. {X. finite X ∧ X ⊆ B x}.
                  principal {y. finite (y (fst x)) ∧ snd x ⊆ y (fst x) ∧ y (fst x) ⊆ B (fst x)})"
        unfolding H_def finite_subsets_at_top_def filtercomap_INF filtercomap_principal
        by (simp add: INF_Sigma)
      also have "… ≠ bot"
      proof (rule INF_filter_not_bot, subst INF_principal_finite, goal_cases)
        case (2 X)
        define H' where
          "H' = (∩x∈X. {y. finite (y (fst x)) ∧ snd x ⊆ y (fst x) ∧ y (fst x) ⊆ B (fst x)})"
        from 2 have "(λx. ∪(y,Y)∈X. if x = y then Y else {}) ∈ H'"
          by (force split: if_splits simp: H'_def)
        hence "H' ≠ {}" by blast
        thus "principal H' ≠ bot" by (simp add: principal_eq_bot_iff)
      qed
      finally show "H ≠ bot" .
    qed
    also have "X' ⊆ X" by fact
    finally show "sum g Z ∈ X" .
  qed (insert Y(1,2), auto simp: Y1_def)
qed

lemma has_sum_finite_iff: 
  fixes S :: "'a :: {topological_comm_monoid_add,t2_space}"
  assumes "finite A"
  shows   "(f has_sum S) A ⟷ S = (∑x∈A. f x)"
proof
  assume "S = (∑x∈A. f x)"
  thus "(f has_sum S) A"
    by (intro has_sum_finiteI assms)
next
  assume "(f has_sum S) A"
  moreover have "(f has_sum (∑x∈A. f x)) A"
    by (intro has_sum_finiteI assms) auto
  ultimately show "S = (∑x∈A. f x)"
    using has_sum_unique by blast
qed

lemma has_sum_finite_neutralI:
  assumes "finite B" "B ⊆ A" "∧x. x ∈ A - B ==> f x = 0" "c = (∑x∈B. f x)"
  shows   "(f has_sum c) A"
proof -
  have "(f has_sum c) B"
    by (rule has_sum_finiteI) (use assms in auto)
  also have "?this ⟷ (f has_sum c) A"
    by (intro has_sum_cong_neutral) (use assms in auto)
  finally show ?thesis .
qed

lemma has_sum_SigmaI:
  fixes f :: "_ ==> 'a :: {topological_comm_monoid_add, t3_space}"
  assumes f: "∧x. x ∈ A ==> ((λy. f (x, y)) has_sum g x) (B x)"
  assumes g: "(g has_sum S) A"
  assumes summable: "f summable_on Sigma A B"
  shows   "(f has_sum S) (Sigma A B)"
  by (metis f g has_sum_SigmaD has_sum_infsum has_sum_unique local.summable)

lemma summable_on_SigmaD1:
  fixes f :: "_ ==> _ ==> 'a :: {complete_uniform_space, uniform_topological_group_add, ab_group_add, topological_comm_monoid_add}"
  assumes f: "(λ(x,y). f x y) summable_on Sigma A B"
  assumes x: "x ∈ A"
  shows   "f x summable_on B x"
proof -
  have "(λ(x,y). f x y) summable_on Sigma {x} B"
    using f by (rule summable_on_subset) (use x in auto)
  also have "?this ⟷ ((λy. f x y) ∘ snd) summable_on Sigma {x} B"
    by (intro summable_on_cong) auto
  also have "… ⟷ (λy. f x y) summable_on snd ` Sigma {x} B"
    by (intro summable_on_reindex [symmetric] inj_onI) auto
  also have "snd ` Sigma {x} B = B x"
    by (force simp: Sigma_def)
  finally show ?thesis .
qed

lemma has_sum_swap:
  "(f has_sum S) (A × B) ⟷ ((λ(x,y). f (y,x)) has_sum S) (B × A)"
proof -
  have "bij_betw (λ(x,y). (y,x)) (B × A) (A × B)"
    by (rule bij_betwI[of _ _ _ "λ(x,y). (y,x)"]) auto
  from has_sum_reindex_bij_betw[OF this, where f = f] show ?thesis
    by (simp add: case_prod_unfold)
qed


lemma summable_on_swap:
  "f summable_on (A × B) ⟷ (λ(x,y). f (y,x)) summable_on (B × A)"
  by (metis has_sum_swap summable_on_def)

lemma has_sum_cmult_right_iff:
  fixes c :: "'a :: {topological_semigroup_mult, field}"
  assumes "c ≠ 0"
  shows   "((λx. c * f x) has_sum S) A ⟷ (f has_sum (S / c)) A"
  using has_sum_cmult_right[of f A "S/c" c]
        has_sum_cmult_right[of "λx. c * f x" A S "inverse c"] assms
  by (auto simp: field_simps)

lemma has_sum_cmult_left_iff:
  fixes c :: "'a :: {topological_semigroup_mult, field}"
  assumes "c ≠ 0"
  shows   "((λx. f x * c) has_sum S) A ⟷ (f has_sum (S / c)) A"
  by (smt (verit, best) assms has_sum_cmult_right_iff has_sum_cong mult.commute)

lemma finite_nonzero_values_imp_summable_on:
  assumes "finite {x∈X. f x ≠ 0}"
  shows   "f summable_on X"
  by (smt (verit, del_insts) Diff_iff assms mem_Collect_eq summable_on_cong_neutral summable_on_finite)

lemma summable_on_of_int_iff:
  "(λx::'a. of_int (f x) :: 'b :: real_normed_algebra_1) summable_on A ⟷ f summable_on A"
proof
  assume "f summable_on A"
  thus "(λx. of_int (f x)) summable_on A"
    by (rule summable_on_homomorphism) auto
next
  assume "(λx. of_int (f x) :: 'b) summable_on A"
  then obtain S where "((λx. of_int (f x) :: 'b) has_sum S) A"
    by (auto simp: summable_on_def)
  hence "(sum (λx. of_int (f x) :: 'b) ---> S) (finite_subsets_at_top A)"
    unfolding has_sum_def .
  moreover have "1/2 > (0 :: real)"
    by auto
  ultimately have "eventually (λX. dist (sum (λx. of_int (f x) :: 'b) X) S < 1/2)
                     (finite_subsets_at_top A)"
    unfolding tendsto_iff by blast
  then obtain X where X: "finite X" "X ⊆ A"
     "∧Y. finite Y ==> X ⊆ Y ==> Y ⊆ A ==> dist (sum (λx. of_int (f x)) Y) S < 1/2"
    unfolding eventually_finite_subsets_at_top by metis

  have "sum f Y = sum f X" if "finite Y" "X ⊆ Y" "Y ⊆ A" for Y
  proof -
    have "dist (sum (λx. of_int (f x)) X) S < 1/2"
      by (intro X) auto
    moreover have "dist (sum (λx. of_int (f x)) Y) S < 1/2"
      by (intro X that)
    ultimately have "dist (sum (λx. of_int (f x)) X) (sum (λx. of_int (f x) :: 'b) Y) <
                       1/2 + 1/2"
      using dist_triangle_less_add by blast
    thus ?thesis
      by (simp add: dist_norm flip: of_int_sum of_int_diff)
  qed
  then have "{x∈A. f x ≠ 0} ⊆ X"
    by (smt (verit) X finite_insert insert_iff mem_Collect_eq subset_eq sum.insert)
  with ‹finite X› have "finite {x∈A. f x ≠ 0}"
    using finite_subset by blast
  thus "f summable_on A"
    by (rule finite_nonzero_values_imp_summable_on)
qed

lemma summable_on_of_nat_iff:
  "(λx::'a. of_nat (f x) :: 'b :: real_normed_algebra_1) summable_on A ⟷ f summable_on A"
proof
  assume "f summable_on A"
  thus "(λx. of_nat (f x) :: 'b) summable_on A"
    by (rule summable_on_homomorphism) auto
next
  assume "(λx. of_nat (f x) :: 'b) summable_on A"
  hence "(λx. of_int (int (f x)) :: 'b) summable_on A"
    by simp
  also have "?this ⟷ (λx. int (f x)) summable_on A"
    by (rule summable_on_of_int_iff)
  also have "… ⟷ f summable_on A"
    by (simp add: summable_on_discrete_iff)
  finally show "f summable_on A" .
qed

lemma infsum_of_nat:
  "infsum (λx::'a. of_nat (f x) :: 'b :: {real_normed_algebra_1}) A = of_nat (infsum f A)"
  by (metis has_sum_infsum has_sum_of_nat infsumI infsum_def of_nat_0 summable_on_of_nat_iff)

lemma infsum_of_int:
  "infsum (λx::'a. of_int (f x) :: 'b :: {real_normed_algebra_1}) A = of_int (infsum f A)"
  by (metis has_sum_infsum has_sum_of_int infsumI infsum_not_exists of_int_0 summable_on_of_int_iff)


lemma summable_on_SigmaI:
  fixes f :: "_ ==> 'a :: {linorder_topology, ordered_comm_monoid_add, topological_comm_monoid_add,
                          conditionally_complete_linorder}"
  assumes f: "∧x. x ∈ A ==> ((λy. f (x, y)) has_sum g x) (B x)"
  assumes g: "g summable_on A"
  assumes f_nonneg: "∧x y. x ∈ A ==> y ∈ B x ==> f (x, y) ≥ (0 :: 'a)"
  shows   "f summable_on Sigma A B"
proof -
  have g_nonneg: "g x ≥ 0" if "x ∈ A" for x
    using f by (rule has_sum_nonneg) (use f_nonneg that in auto)
  obtain C where C: "eventually (λX. sum g X ≤ C) (finite_subsets_at_top A)"
    using summable_on_imp_bounded_partial_sums[OF g] by blast

  have sum_g_le: "sum g X ≤ C" if X: "finite X" "X ⊆ A" for X
  proof -
    from C obtain X' where X':
      "finite X'" "X' ⊆ A" "∧Y. finite Y ==> X' ⊆ Y ==> Y ⊆ A ==> sum g Y ≤ C"
      unfolding eventually_finite_subsets_at_top by metis
    have "sum g X ≤ sum g (X ∪ X')"
      using X X' by (intro sum_mono2 g_nonneg) auto
    also have "… ≤ C"
      using X X'(1,2) by (intro X'(3)) auto
    finally show ?thesis .
  qed

  have "sum f Y ≤ C" if Y: "finite Y" "Y ⊆ Sigma A B" for Y
  proof -
    define Y1 and Y2 where "Y1 = fst ` Y" and "Y2 = (λx. snd ` {z∈Y. fst z = x})"
    have Y12: "Y = Sigma Y1 Y2"
      unfolding Y1_def Y2_def by force
    have [intro]: "finite Y1" "∧x. x ∈ Y1 ==> finite (Y2 x)"
      using Y unfolding Y1_def Y2_def by auto
    have Y12_subset: "Y1 ⊆ A" "∧x. Y2 x ⊆ B x"
      using Y by (auto simp: Y1_def Y2_def)

    have "sum f Y = sum f (Sigma Y1 Y2)"
      by (simp add: Y12)
    also have "… = (∑x∈Y1. ∑y∈Y2 x. f (x, y))"
      by (subst sum.Sigma) auto
    also have "… ≤ (∑x∈Y1. g x)"
    proof (rule sum_mono)
      fix x assume x: "x ∈ Y1"
      show "(∑y∈Y2 x. f (x, y)) ≤ g x"
      proof (rule has_sum_mono')
        show "((λy. f (x, y)) has_sum (∑y∈Y2 x. f (x, y))) (Y2 x)"
          using x by (intro has_sum_finite) auto
        show "((λy. f (x, y)) has_sum g x) (B x)"
          by (rule f) (use x Y12_subset in auto)
        show "f (x, y) ≥ 0" if "y ∈ B x - Y2 x" for y
          using x that Y12_subset by (intro f_nonneg) auto
      qed (use Y12_subset in auto)
    qed
    also have "… ≤ C"
      using Y12_subset by (intro sum_g_le) auto
    finally show ?thesis .
  qed

  hence "∀🪙F X in finite_subsets_at_top (Sigma A B). sum f X ≤ C"
    unfolding eventually_finite_subsets_at_top by auto
  thus ?thesis
    by (metis SigmaE f_nonneg nonneg_bounded_partial_sums_imp_summable_on)
qed

lemma summable_on_UnionI:
  fixes f :: "_ ==> 'a :: {linorder_topology, ordered_comm_monoid_add, topological_comm_monoid_add,
                          conditionally_complete_linorder}"
  assumes f: "∧x. x ∈ A ==> (f has_sum g x) (B x)"
  assumes g: "g summable_on A"
  assumes f_nonneg: "∧x y. x ∈ A ==> y ∈ B x ==> f y ≥ (0 :: 'a)"
  assumes disj: "disjoint_family_on B A"
  shows   "f summable_on (∪x∈A. B x)"
proof -
  have "f ∘ snd summable_on Sigma A B"
    using assms by (intro summable_on_SigmaI[where g = g]) auto
  also have "?this ⟷ f summable_on (snd ` Sigma A B)" using assms
    by (subst summable_on_reindex; force simp: disjoint_family_on_def inj_on_def)
  also have "snd ` (Sigma A B) = (∪x∈A. B x)"
    by force
  finally show ?thesis .
qed

lemma summable_on_SigmaD:
  fixes f :: "'a × 'b ==> 'c :: {topological_comm_monoid_add,t3_space}"
  assumes sum1: "f summable_on (Sigma A B)"
  assumes sum2: "∧x. x ∈ A ==> (λy. f (x, y)) summable_on (B x)"
  shows   "(λx. infsum (λy. f (x, y)) (B x)) summable_on A"
  using assms unfolding summable_on_def
  by (smt (verit, del_insts) assms has_sum_SigmaD has_sum_cong has_sum_infsum)

lemma summable_on_UnionD:
  fixes f :: "'a ==> 'c :: {topological_comm_monoid_add,t3_space}"
  assumes sum1: "f summable_on (∪x∈A. B x)"
  assumes sum2: "∧x. x ∈ A ==> f summable_on (B x)"
  assumes disj: "disjoint_family_on B A"
  shows   "(λx. infsum f (B x)) summable_on A"
proof -
  have "(∪x∈A. B x) = snd ` Sigma A B"
    by (force simp: Sigma_def)
  with sum1 have "f summable_on (snd ` Sigma A B)"
    by simp
  also have "?this ⟷ (f ∘ snd) summable_on (Sigma A B)"
    using disj by (intro summable_on_reindex inj_onI) (force simp: disjoint_family_on_def)
  finally show "(λx. infsum f (B x)) summable_on A"
    using summable_on_SigmaD[of "f ∘ snd" A B] sum2 by simp
qed

lemma summable_on_Union_iff:
  fixes f :: "_ ==> 'a :: {linorder_topology, ordered_comm_monoid_add, topological_comm_monoid_add,
                          conditionally_complete_linorder, t3_space}"
  assumes f: "∧x. x ∈ A ==> (f has_sum g x) (B x)"
  assumes f_nonneg: "∧x y. x ∈ A ==> y ∈ B x ==> f y ≥ 0"
  assumes disj: "disjoint_family_on B A"
  shows   "f summable_on (∪x∈A. B x) ⟷ g summable_on A"
proof
  assume "g summable_on A"
  thus "f summable_on (∪x∈A. B x)"
    using summable_on_UnionI[of A f B g] assms by auto
next
  assume "f summable_on (∪x∈A. B x)"
  hence "(λx. infsum f (B x)) summable_on A"
    using assms by (intro summable_on_UnionD) (auto dest: has_sum_imp_summable)
  also have "?this ⟷ g summable_on A"
    using assms by (intro summable_on_cong) (auto simp: infsumI)
  finally show "g summable_on A" .
qed

lemma has_sum_Sigma':
  fixes A :: "'a set" and B :: "'a ==> 'b set"
    and f :: ‹'a × 'b ==> 'c::{comm_monoid_add,uniform_space,uniform_topological_group_add}›
  assumes summableAB: "(f has_sum a) (Sigma A B)"
  assumes summableB: ‹∧x. x∈A ==> ((λy. f (x, y)) has_sum (b x)) (B x)›
  shows "(b has_sum a) A"
  by (intro has_sum_Sigma[OF _ assms] uniformly_continuous_add)

lemma abs_summable_on_comparison_test':
  assumes "g summable_on A"
  assumes "∧x. x ∈ A ==> norm (f x) ≤ g x"
  shows   "(λx. norm (f x)) summable_on A"
proof (rule Infinite_Sum.abs_summable_on_comparison_test)
  have "g summable_on A ⟷ (λx. norm (g x)) summable_on A"
    by (metis summable_on_iff_abs_summable_on_real)
  with assms show "(λx. norm (g x)) summable_on A" by blast
qed (use assms in fastforce)

lemma has_sum_geometric_from_1:
  fixes z :: "'a :: {real_normed_field, banach}"
  assumes "norm z < 1"
  shows   "((λn. z ^ n) has_sum (z / (1 - z))) {1..}"
proof -
  have [simp]: "z ≠ 1"
    using assms by auto
  have "(λn. z ^ Suc n) sums (1 / (1 - z) - 1)"
    using geometric_sums[of z] assms by (subst sums_Suc_iff) auto
  also have "1 / (1 - z) - 1 = z / (1 - z)"
    by (auto simp: field_simps)
  finally have "(λn. z ^ Suc n) sums (z / (1 - z))" .
  moreover have "summable (λn. norm (z ^ Suc n))"
    using assms
    by (subst summable_Suc_iff) (auto simp: norm_power intro!: summable_geometric)
  ultimately have "((λn. z ^ Suc n) has_sum (z / (1 - z))) UNIV"
    by (intro norm_summable_imp_has_sum)
  also have "?this ⟷ ?thesis"
    by (intro has_sum_reindex_bij_witness[of _ "λn. n-1" "λn. n+1"]) auto
  finally show ?thesis .
qed 

lemma has_sum_divide_const:
  fixes f :: "'a ==> 'b :: {topological_semigroup_mult, field, semiring_0}"
  shows "(f has_sum S) A ==> ((λx. f x / c) has_sum (S / c)) A"
  using has_sum_cmult_right[of f A S "inverse c"] by (simp add: field_simps)

lemma has_sum_uminusI:
  fixes f :: "'a ==> 'b :: {topological_semigroup_mult, ring_1}"
  shows "(f has_sum S) A ==> ((λx. -f x) has_sum (-S)) A"
  using has_sum_cmult_right[of f A S "-1"] by simp


subsection ‹Infinite sums of formal power series›

text ‹
  Consequently, a family $(f_x)_{x\in A}$ of formal power series sums to a series $s$ iff for
  any $n\geq 0$, the set $A_n = \{x\in A \mid [X^n]\,f_x \neq 0\}$ is finite and
  $[X^n]\,s = \sum_{x\in A_n} [X^n]\,f_x$.
 
  The first condition can be rephrased as follows: for any $n\geq 0$, for all but finitely many
  $x$, the series $f_x$ has subdegree ${>}\,n$.
 ›
lemma has_sum_fpsI:
  assumes "∧n. finite {x∈A. fps_nth (F x) n ≠ 0}"
  assumes "∧n. fps_nth S n = (∑x | x ∈ A ∧ fps_nth (F x) n ≠ 0. fps_nth (F x) n)"
  shows   "(F has_sum S) A"
  unfolding has_sum_def
proof (rule tendsto_fpsI)
  fix n :: nat
  define B where "B = {x∈A. fps_nth (F x) n ≠ 0}"
  from assms(1) have [intro]: "finite B"
    unfolding B_def by auto
  moreover have "B ⊆ A"
    by (auto simp: B_def)
  ultimately have "eventually (λX. finite X ∧ B ⊆ X ∧ X ⊆ A) (finite_subsets_at_top A)"
    by (subst eventually_finite_subsets_at_top) blast
  thus "eventually (λX. fps_nth (∑x∈X. F x) n = fps_nth S n) (finite_subsets_at_top A)"
  proof eventually_elim
    case (elim X)
    have "fps_nth (∑x∈X. F x) n = (∑x∈X. fps_nth (F x) n)"
      by (simp add: fps_sum_nth)
    also have "… = (∑x∈B. fps_nth (F x) n)"
      by (rule sum.mono_neutral_right)  (use ‹finite B› ‹B ⊆ A› elim in ‹auto simp: B_def›)
    also have "… = fps_nth S n"
      using assms(2)[of n] by (simp add: B_def)
    finally show "fps_nth (∑x∈X. F x) n = fps_nth S n" .
  qed
qed

lemma has_sum_fpsD:
  fixes F :: "'a ==> 'b :: ab_group_add fps"
  assumes "(F has_sum S) A"
  shows   "finite {x∈A. fps_nth (F x) n ≠ 0}"
          "fps_nth S n = (∑x | x ∈ A ∧ fps_nth (F x) n ≠ 0. fps_nth (F x) n)"
proof -
  from assms have "∀🪙F X in finite_subsets_at_top A. fps_nth (sum F X) k = fps_nth S k" for k
    unfolding has_sum_def tendsto_fps_iff by blast
  hence "∀🪙F X in finite_subsets_at_top A. fps_nth (sum F X) n = fps_nth S n"
    by eventually_elim force
  then obtain B where [intro, simp]: "finite B" and B: "B ⊆ A"
     "∧X. finite X ==> B ⊆ X ==> X ⊆ A ==> fps_nth (sum F X) n = fps_nth S n"
    unfolding eventually_finite_subsets_at_top by metis

  have subset: "{x∈A. fps_nth (F x) n ≠ 0} ⊆ B"
  proof safe
    fix x assume x: "x ∈ A" "fps_nth (F x) n ≠ 0"
    have "fps_nth (sum F B) n = fps_nth S n"
      by (rule B(2)) (use B(1) in auto)
    moreover have "fps_nth (sum F (insert x B)) n = fps_nth S n"
      by (rule B(2)) (use B(1) x in auto)
    ultimately show "x ∈ B"
      using x by (auto simp: sum.insert_if split: if_splits)
  qed
  thus finite: "finite {x∈A. fps_nth (F x) n ≠ 0}"
    by (rule finite_subset) auto

  have "fps_nth S n = fps_nth (∑x∈B. F x) n"
    by (rule sym, rule B(2)) (use B(1) in auto)
  also have "… = (∑x∈B. fps_nth (F x) n)"
    by (simp add: fps_sum_nth)
  also have "… = (∑x | x ∈ A ∧ fps_nth (F x) n ≠ 0. fps_nth (F x) n)"
    by (rule sum.mono_neutral_right) (use subset B(1) in auto)
  finally show "fps_nth S n = (∑x | x ∈ A ∧ fps_nth (F x) n ≠ 0. fps_nth (F x) n)" .
qed

end