Theory Infinite_Sum

(*
  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
latex‹\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 \cite{conway2013course}.
This definition is quite general: it is well-defined whenever $f$ takes values in some
commutative monoid endowed with a Hausdorff topology.
(Examples are reals, complex numbers, normed vector spaces, and more.)

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

subsection Definition and syntax

definition has_sum :: ('a  'b :: {comm_monoid_add, topological_space})  'a set  'b  bool where
  has_sum f A x  (sum f  x) (finite_subsets_at_top A)

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

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"  ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10)
syntax
  "_infsum" :: "pttrn  'a set  'b  'b::topological_comm_monoid_add"  ("(2(_/_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!
  "iA. b"  "CONST infsum (λi. b) A"

syntax (ASCII)
  "_univinfsum" :: "pttrn  'a  'a"  ("(3INFSUM _./ _)" [0, 10] 10)
syntax
  "_univinfsum" :: "pttrn  'a  'a"  ("(2_./ _)" [0, 10] 10)
translations
  "x. t"  "CONST infsum (λx. t) (CONST UNIV)"

syntax (ASCII)
  "_qinfsum" :: "pttrn  bool  'a  'a"  ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
  "_qinfsum" :: "pttrn  bool  'a  'a"  ("(2_ | (_)./ _)" [0, 0, 10] 10)
translations
  "x|P. t" => "CONST infsum (λx. t) {x. P}"

print_translation 
let
  fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
        if x <> y then raise Match
        else
          let
            val x' = Syntax_Trans.mark_bound_body (x, Tx);
            val t' = subst_bound (x', t);
            val P' = subst_bound (x', P);
          in
            Syntax.const @{syntax_const "_qinfsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
          end
    | sum_tr' _ = raise Match;
in [(@{const_syntax infsum}, K sum_tr')] end


subsection General properties

lemma infsumI:
  fixes f g :: 'a  'b::{comm_monoid_add, t2_space}
  assumes has_sum f A x
  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 has_sum f A x
  assumes has_sum g B y
  shows infsum f A = infsum g B
  by (metis assms(1) assms(2) assms(3) finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)

lemma infsum_eqI':
  fixes f g :: 'a  'b::{comm_monoid_add, t2_space}
  assumes x. has_sum f A x  has_sum g B x
  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 summable_iff_has_sum_infsum: "f summable_on A  has_sum f A (infsum f A)"
  using infsumI summable_on_def by blast

lemma has_sum_infsum[simp]:
  assumes f summable_on S
  shows has_sum f S (infsum f S)
  using assms by (auto simp: summable_on_def infsum_def has_sum_def tendsto_Lim)

lemma has_sum_cong_neutral:
  fixes f g :: 'a  'b::{comm_monoid_add, topological_space}
  assumes x. xT-S  g x = 0
  assumes x. xS-T  f x = 0
  assumes x. xST  f x = g x
  shows "has_sum f S x  has_sum g T x"
proof -
  have eventually P (filtermap (sum f) (finite_subsets_at_top S))
      = eventually P (filtermap (sum g) (finite_subsets_at_top T)) for P
  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 ((FS)  (F0S)))
        apply (rule F0_P)
        using F0  S  finite F0 that by auto
      also have sum f ((FS)  (F0S)) = sum g F
        apply (rule sum.mono_neutral_cong)
        using that finite F0 F0'_def assms by 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 ((FT)  (F0T)))
        apply (rule F0_P)
        using F0  T  finite F0 that by auto
      also have sum g ((FT)  (F0T)) = sum f F
        apply (rule sum.mono_neutral_cong)
        using that finite F0 F0'_def assms by 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. xT-S  g x = 0
  assumes x. xS-T  f x = 0
  assumes x. xST  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. xT-S  g x = 0
  assumes x. xS-T  f x = 0
  assumes x. xST  f x = g x
  shows infsum f S = infsum g T
  apply (rule infsum_eqI')
  using assms by (rule has_sum_cong_neutral)

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

lemma summable_on_cong:
  assumes "x. xA  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. xA  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' = FA"
  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 has_sum f B b and has_sum f A a and AB: "A  B"
  shows has_sum_Diff: "has_sum f (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="YX"] 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 (FA))  a) (finite_subsets_at_top B)"
  proof (subst asm_rl [of "(λF. sum f (FA)) = sum f o (λF. FA)"])
    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 (FA))  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 [THEN iffD1 , rotated]
      ((λF. sum f F - sum f (F  A))  b - a) (finite_subsets_at_top B) 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)
  hence limBA: "(sum f  b - a) (finite_subsets_at_top (B-A))"
    apply (rule tendsto_mono[rotated])
    by (rule finite_subsets1)
  thus ?thesis
    by (simp add: has_sum_def)
qed


lemma
  fixes f :: "'a  '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 has_sum f A a and "has_sum g B b"
  assumes x. x  AB  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 has_sum f' (AB) a
    apply (subst has_sum_cong_neutral[where g=f and T=A])
    by (auto simp: f'_def assms(1))
  then have f'_lim: (sum f'  a) (finite_subsets_at_top (AB))
    by (meson has_sum_def)
  have has_sum g' (AB) b
    apply (subst has_sum_cong_neutral[where g=g and T=B])
    by (auto simp: g'_def assms(2))
  then have g'_lim: (sum g'  b) (finite_subsets_at_top (AB))
    using has_sum_def by blast

  have *: F x in finite_subsets_at_top (A  B). sum f' x  sum g' x
    apply (rule eventually_finite_subsets_at_top_weakI)
    apply (rule sum_mono)
    using assms by (auto simp: f'_def g'_def)
  show ?thesis
    apply (rule tendsto_le)
    using * g'_lim f'_lim by auto
qed

lemma infsum_mono_neutral:
  fixes f :: "'a'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "f summable_on A" and "g summable_on B"
  assumes x. x  AB  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 (rule has_sum_mono_neutral[of f A _ g B _]) (use assms in auto intro: has_sum_infsum)

lemma has_sum_mono:
  fixes f :: "'a'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "has_sum f A x" and "has_sum g A y"
  assumes x. x  A  f x  g x
  shows "x  y"
  apply (rule has_sum_mono_neutral)
  using assms by auto

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"
  apply (rule infsum_mono_neutral)
  using assms by auto

lemma has_sum_finite[simp]:
  assumes "finite F"
  shows "has_sum f F (sum f F)"
  using assms
  by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def has_sum_def principal_eq_bot_iff)

lemma summable_on_finite[simp]:
  fixes f :: '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"
  using assms by (auto intro: tendsto_Lim simp: finite_subsets_at_top_finite infsum_def principal_eq_bot_iff)

lemma has_sum_finite_approximation:
  fixes f :: "'a  'b::{comm_monoid_add,metric_space}"
  assumes "has_sum f A x" 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 "has_sum f A (infsum f 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') < e) if e>0 for e
  proof -
    define d P where d = e/4 and P F  finite F  F  A  dist (sum (λx. norm (f x)) F) L < d 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 < d eventually_conj_iff eventually_finite_subsets_at_top_weakI tendsto_iff)
    
    moreover have dist (sum f F1) (sum f F2) < e 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 < d
        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') < 2*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 (xF-F'. norm (f x))
          by (rule order.trans[OF sum_norm_le[OF order.refl]]) auto
        also have  = dist (xF. norm (f x)) (xF'. norm (f x))
          unfolding dist_norm using finite F F' by (subst sum_diff) auto
        also have  < 2 * d
          using dist_F F' unfolding P_def dist_norm real_norm_def by linarith
        finally show dist (sum f F) (sum f F') < 2*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  < 2 * 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) < e .
    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)
  then obtain L' where (sum f  L') (finite_subsets_at_top A)
    apply atomize_elim unfolding filterlim_def
    apply (rule complete_uniform[where S=UNIV, simplified, THEN iffD1, rule_format])
      apply (auto simp add: filtermap_bot_iff)
    by (meson Cauchy_convergent UNIV_I complete_def convergent_def)
  then show ?thesis
    using summable_on_def has_sum_def by blast
qed

text The converse of @{thm [source] abs_summable_summable} does not hold:
  Consider the Hilbert space of square-summable sequences.
  Let $e_i$ denote the sequence with 1 in the $i$th position and 0 elsewhere.
  Let $f(i) := e_i/i$ for $i\geq1$. We have term¬ f abs_summable_on UNIV because $\lVert f(i)\rVert=1/i$
  and thus the sum over $\lVert f(i)\rVert$ diverges. On the other hand, we have termf 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 "has_sum (λx. norm (f x)) A n"
  assumes "has_sum f 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 + ε"
      apply (rule add_right_mono)
      apply (rule has_sum_mono_neutral[where A=F and B=A and f=λx. norm (f x) and g=λx. norm (f x)])
      using finite F F  A assms by auto
    finally show ?thesis 
      by assumption
  qed
  thus ?thesis
    using linordered_field_class.field_le_epsilon by blast
qed

lemma norm_infsum_bound:
  fixes f :: "'b  '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
  show ?thesis
    apply (rule norm_has_sum_bound[where A=A and f=f and a=infsum f A and n=infsum (λx. norm (f x)) A])
    using assms True
    by (metis finite_subsets_at_top_neq_bot infsum_def summable_on_def has_sum_def tendsto_Lim)+
next
  case False
  obtain t where t_def: "(sum (λ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"
    proof-
      have "closed {s::real. s  0}"
        using Elementary_Topology.closed_sequential_limits[where S = "{s::real. s  0}"]
        by (metis Lim_bounded2 mem_Collect_eq)
      moreover have "{s::real. s  0} = UNIV - S"
        unfolding S_def by auto
      ultimately have "closed (UNIV - S)"
        by simp
      thus ?thesis
        by (simp add: Compl_eq_Diff_UNIV open_closed) 
    qed
    ultimately have "F X in finite_subsets_at_top A. (xX. norm (f x))  S"
      using t_def unfolding tendsto_def by blast
    hence "X. (xX. 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 "(xX. norm (f x))  S"
      by blast
    hence "(xX. 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 by (simp flip: has_sum_def)


lemma has_sum_0: 
  assumes x. xM  f x = 0
  shows has_sum f M 0
  unfolding has_sum_def
  apply (subst tendsto_cong[where g=λ_. 0])
   apply (rule eventually_finite_subsets_at_top_weakI)
  using assms by (auto simp add: subset_iff)

lemma summable_on_0:
  assumes x. xM  f x = 0
  shows f summable_on M
  using assms summable_on_def has_sum_0 by blast

lemma infsum_0:
  assumes x. xM  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]: has_sum (λ_. 0) M 0
  by (simp_all add: has_sum_0)


lemma has_sum_add:
  fixes f g :: "'a  'b::{topological_comm_monoid_add}"
  assumes has_sum f A a
  assumes has_sum g A b
  shows has_sum (λx. f x + g x) A (a + b)
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(1) assms(2) 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 has_sum (λx. f x + g x) A (infsum f A + infsum g A)
    by (simp add: assms(1) assms(2) 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 "has_sum f A a"
  assumes "has_sum f B b"
  assumes disj: "A  B = {}"
  shows has_sum f (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: has_sum fA (A  B) a
    apply (subst has_sum_cong_neutral[where T=A and g=f])
    using assms by (auto simp: fA_def)
  have fB: has_sum fB (A  B) b
    apply (subst has_sum_cong_neutral[where T=B and g=f])
    using assms by (auto simp: fB_def)
  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(1) assms(2) 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   "has_sum f (UNIV :: nat set) S"
  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
proof (safe, goal_cases)
  case (1 ε)
  from assms(1) obtain S' where S': "(λn. norm (f n)) sums S'"
    by (auto simp: summable_def)
  with 1 obtain N where N: "n. n  N  ¦S' - (i<n. norm (f i))¦ < ε"
    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
  
  show ?case
  proof (rule exI[of _ "{..<N}"], safe, goal_cases)
    case (2 Y)
    from 2 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 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
    also have "(λn. if n  {..<N} then 0 else norm (f n)) sums (S' - (i<N. norm (f 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<N. norm (f i))"
      by (simp add: sums_iff)
    also have "S' - (i<N. norm (f i))  ¦S' - (i<N. norm (f i))¦" by simp
    also have " < ε" by (rule N) auto
    finally show ?case by (simp add: dist_norm norm_minus_commute)
  qed auto
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)

text The following lemma indeed needs a complete space (as formalized by the premise termcomplete 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:
  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. FF1  finite F  FA  P1 (sum f F)
      by (metis eventually_finite_subsets_at_top)
    from ev_P2 obtain F2 where F2: finite F2 F2  A F. FF2  finite F  FA  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

    show eventually E (?filter_fB ×F ?filter_fB)
      unfolding eventually_prod_filter
    proof (safe intro!: exI)
      show "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)+
    next
      show "E (x, y)" if "E' (x, sum f F0B)" and "E' (sum f F0B, y)" for x y
        using E'E'E that by blast
    qed
  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} for Banach spaces with less 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 (rule summable_on_subset[OF _ _ assms])
     (auto simp: complete_def convergent_def dest!: Cauchy_convergent)

lemma has_sum_empty[simp]: has_sum f {} 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: finite A
  assumes conv: a. a  A  has_sum f (B a) (s a)
  assumes disj: a a'. aA  a'A  aa'  B a  B a' = {}
  shows has_sum f (aA. B a) (sum s A)
  using assms
proof (insert finite conv disj, induction)
  case empty
  then show ?case 
    by simp
next
  case (insert x A)
  have has_sum f (B x) (s x)
    by (simp add: insert.prems)
  moreover have IH: has_sum f (aA. B a) (sum s A)
    using insert by simp
  ultimately have has_sum f (B x  (aA. B a)) (s x + sum s A)
    apply (rule has_sum_Un_disjoint)
    using insert by auto
  then show ?case
    using insert.hyps by auto
qed


lemma summable_on_finite_union_disjoint:
  fixes f :: "'a  'b::topological_comm_monoid_add"
  assumes finite: finite A
  assumes conv: a. a  A  f summable_on (B a)
  assumes disj: a a'. aA  a'A  aa'  B a  B a' = {}
  shows f summable_on (aA. B a)
  using finite conv disj apply induction by (auto intro!: summable_on_Un_disjoint)

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'. aA  a'A  aa'  B a  B a' = {}
  shows sum (λa. infsum f (B a)) A = infsum f (aA. B a)
  by (rule sym, rule infsumI)
     (use sum_has_sum[of A f B λa. infsum f (B a)] assms in auto)

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 constadditive which introduces an additional sort constraint
  (group instead of monoid). For example, extended reals (typereal, typennreal) 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 o g) F = f (sum g F)
      ― ‹Not using constadditive because it would add sort constraint classab_group_add
  assumes cont: f x f x
    ― ‹For classt2_space, this is equivalent to isCont f x› by @{thm [source] isCont_def}.
  assumes infsum: has_sum g S x
  shows has_sum (f o g) S (f x) 
proof -
  have (sum g  x) (finite_subsets_at_top S)
    using infsum has_sum_def by blast
  then have ((f o sum g)  f x) (finite_subsets_at_top S)
    apply (rule tendsto_compose_at)
    using assms by auto
  then have (sum (f o g)  f x) (finite_subsets_at_top S)
    apply (rule tendsto_cong[THEN iffD1, rotated])
    using f_sum by fastforce
  then show has_sum (f o g) S (f x)
    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 o g) F = f (sum g F)
    ― ‹Not using constadditive because it would add sort constraint classab_group_add
  assumes x. has_sum g S x  f x f x
    ― ‹For classt2_space, this is equivalent to isCont f x› by @{thm [source] isCont_def}.
  assumes g summable_on S
  shows (f o 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 o g) F = f (sum g F)
      ― ‹Not using constadditive because it would add sort constraint classab_group_add
  assumes isCont f (infsum g S)
  assumes g summable_on S
  shows infsum (f o 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 classt2_space, this is equivalent to isCont f x› by @{thm [source] isCont_def}.
  assumes infsum: has_sum g S x
  shows has_sum (f o g) S (f x)
  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 o g) summable_on S
  by (meson assms(1) assms(2) assms(3) summable_on_def has_sum_comm_additive has_sum_infsum isContD)

lemma infsum_comm_additive:
  fixes f :: '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 o 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. xA  f x  0
  assumes bdd_above (sum f ` {F. FA  finite F})
  shows has_sum f A (SUP F{F. finite F  FA}. sum f F)
proof -
  have (sum f  (SUP F{F. finite F  FA}. sum f F)) (finite_subsets_at_top A)
  proof (rule order_tendstoI)
    fix a assume a < (SUP F{F. finite F  FA}. sum f F)
    then obtain F where a < sum 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)
    show F x in finite_subsets_at_top A. a < sum f x
      unfolding eventually_finite_subsets_at_top
    proof (rule exI[of _ F], safe)
      fix Y assume Y: "finite Y" "F  Y" "Y  A"
      have "a < sum f F"
        by fact
      also have "  sum f Y"
        using assms Y by (intro sum_mono2) auto
      finally show "a < sum f Y" .
    qed (use finite F F  A in auto)
  next
    fix a assume *: (SUP F{F. finite F  FA}. sum f F) < a
    have sum f F < a if FA and finite F for F
    proof -
      have "sum f F  (SUP F{F. finite F  FA}. sum f F)"
        by (rule cSUP_upper) (use that assms(2) in auto simp: conj_commute)
      also have " < a"
        by fact
      finally show ?thesis .
    qed
    then show F x in finite_subsets_at_top A. sum f x < a
      by (rule eventually_finite_subsets_at_top_weakI)
  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. xA  f x  0
  assumes bdd_above (sum f ` {F. FA  finite F})
  shows f summable_on A
  using assms(1) assms(2) 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. xA  f x  0
  assumes bdd_above (sum f ` {F. FA  finite F})
  shows infsum f A = (SUP F{F. finite F  FA}. 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. xA  f x  0
  shows has_sum f A (SUP F{F. finite F  FA}. sum f F)
  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. xA  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. xA  f x  0
  shows infsum f A = (SUP F{F. finite F  FA}. 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 "has_sum f M a"
    and "x. x  M  0  f x"
  shows "a  0"
  by (metis (no_types, lifting) DiffD1 assms(1) assms(2) empty_iff has_sum_0 has_sum_mono_neutral order_refl)

lemma infsum_nonneg:
  fixes f :: "'a  'b::{ordered_comm_monoid_add,linorder_topology}"
  assumes "x. x  M  0  f x"
  shows "infsum f M  0" (is "?lhs  _")
  apply (cases f summable_on M)
   apply (metis assms infsum_0_simp summable_on_0_simp infsum_mono)
  using assms by (auto simp add: infsum_not_exists)

lemma has_sum_mono2:
  fixes f :: "'a  'b::{topological_ab_group_add, ordered_comm_monoid_add,linorder_topology}"
  assumes "has_sum f A S" "has_sum f B S'" "A  B"
  assumes "x. x  B - A  f x  0"
  shows   "S  S'"
proof -
  have "has_sum f (B - A) (S' - S)"
    by (rule has_sum_Diff) fact+
  hence "S' - S  0"
    by (rule has_sum_nonneg) (use assms(4) in auto)
  thus ?thesis
    by (metis add_0 add_mono_thms_linordered_semiring(3) diff_add_cancel)
qed

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 "has_sum f A S" "finite B" "B  A"
  assumes "x. x  A - B  f x  0"
  shows   "sum f B  S"
proof (rule has_sum_mono2)
  show "has_sum f A S"
    by fact
  show "has_sum f B (sum f B)"
    by (rule has_sum_finite) fact+
qed (use assms in auto)

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 has_sum g (h ` A) x  has_sum (g  h) A x
proof -
  have has_sum g (h ` A) x  (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)
    apply (subst filtermap_image_finite_subsets_at_top[symmetric])
    using assms by (auto simp: filterlim_def filtermap_filtermap)
  also have   (sum (g  h)  x) (finite_subsets_at_top A)
    apply (rule tendsto_cong)
    apply (rule eventually_finite_subsets_at_top_weakI)
    apply (rule sum.reindex)
    using assms subset_inj_on by blast
  also have   has_sum (g  h) A x
    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 (no_types, opaque_lifting) assms finite_subsets_at_top_neq_bot infsum_def 
        summable_on_reindex has_sum_def has_sum_infsum has_sum_reindex tendsto_Lim)

lemma summable_on_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "(λx. f (g x)) summable_on A  f summable_on B"
proof -
  thm summable_on_reindex
  have (λx. f (g x)) summable_on A  f summable_on g ` A
    apply (rule summable_on_reindex[symmetric, unfolded o_def])
    using assms bij_betw_imp_inj_on by blast
  also have   f summable_on B
    using assms bij_betw_imp_surj_on by blast
  finally show ?thesis .
qed

lemma infsum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "infsum (λx. f (g x)) A = infsum f B"
proof -
  have infsum (λx. f (g x)) A = infsum f (g ` A)
    by (metis (mono_tags, lifting) assms bij_betw_imp_inj_on infsum_cong infsum_reindex o_def)
  also have  = infsum f B
    using assms bij_betw_imp_surj_on by blast
  finally show ?thesis .
qed

lemma sum_uniformity:
  assumes plus_cont: uniformly_continuous_on UNIV (λ(x::'b::{uniform_space,comm_monoid_add},y). x+y)
  assumes eventually E uniformity
  obtains D where eventually D uniformity 
    and M::'a set. f f' :: 'a  'b. card M  n  (mM. D (f m, f' m))  E (sum f M, sum f' M)
proof (atomize_elim, insert eventually E uniformity, 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  (mM. 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: mM. 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. mN  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: "has_sum f (Sigma A B) a"
  assumes summableB: x. xA  has_sum (λy. f (x, y)) (B x) (b x)
  shows "has_sum b 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
    apply (subst asm_rl[of {b| b. (a,b)  H} = snd ` {ab. ab  H  fst ab = a}])
    by (auto simp: image_iff 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 (aM. b a, (a,b)H. f (a,b))) FMB
      proof -
        obtain D' where D'_uni: eventually D' uniformity 
          and card M'  card M  (mM'. D' (g m, g' m))  D (sum g M', sum g' M')
            for M' :: 'a set and g g'
          apply (rule sum_uniformity[OF plus_cont eventually D uniformity, where n=card M])
          by auto
        then have D'_sum_D: (mM. 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 (aM. 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)) = (aM. bHa' a. f (a,b))
            apply (subst sum.Sigma)
            using finite M by auto
          have D' (b a, sum (λb. f (a,b)) (Ha' a)) if a  M for a
            apply (rule D'_sum_Ha)
            using that M  A by auto
          then have D (aM. b a, aM. 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 (intro exI[of _ "Sigma M Ha"])
             (use Ha_fin that(2,3) in fastforce intro!: finite_SigmaI)
      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"
        have "Y  Sigma A B"
          using Y M  A by blast
        thus "D ((a,b)Y. f (a, b), a)"
          using G_sum[of Y] Y by auto
      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)
        by (rule eventually_const[THEN iffD1, rotated]) (force simp: FMB_def)
    qed
    then show F x in FA. E (sum b x, a)
      using finite (fst ` G) and fst ` G  A
      by (auto intro!: exI[of _ fst ` G] simp add: FA_def eventually_finite_subsets_at_top)
  qed
  then show ?thesis
    by (simp add: FA_def has_sum_def)
qed

lemma summable_on_Sigma:
  fixes A :: "'a set" and B :: "'a  '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. xA  (f x) summable_on (B x)
  shows (λx. infsum (f x) (B x)) summable_on A
proof -
  from summableAB obtain a where a: has_sum (λ(x,y). f x y) (Sigma A B) a
    using has_sum_infsum by blast
  from summableB have b: x. xA  has_sum (f x) (B x) (infsum (f x) (B x))
    by (auto intro!: has_sum_infsum)
  show ?thesis
    using plus_cont a b 
    by (auto intro: has_sum_Sigma[where f=λ(x,y). f x y, simplified] 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: "f summable_on (Sigma A B)"
  assumes summableB: x. xA  (λ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: has_sum f (Sigma A B) (infsum f (Sigma A B))
    using has_sum_infsum by blast
  from summableB have b: x. xA  has_sum (λy. f (x, y)) (B x) (infsum (λy. f (x, y)) (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. xA  (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 [simp]: (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) o Pair x) summable_on (B x)
      apply (rule_tac summable_on_reindex[THEN iffD1])
      by (simp add: inj_on_def)
    then show ?thesis
      by (auto simp: o_def)
  qed
  show ?thesis1
    apply (rule infsum_Sigma')
    by auto
  show ?thesis2
    apply (rule summable_on_Sigma)
    by auto
qed

lemma infsum_Sigma_banach:
  fixes A :: "'a set" and B :: "'a  '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 (subst infsum_Sigma'_banach) auto

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. aA  (f a) summable_on B
  assumes b. bB  (λ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 [simp]: (λ(x, y). f y x) summable_on (B × A)
    apply (subst product_swap[symmetric])
    apply (subst summable_on_reindex)
    using assms by (auto simp: o_def)
  have infsum (λx. infsum (λy. f x y) B) A = infsum (λ(x,y). f x y) (A × B)
    apply (subst infsum_Sigma)
    using assms by auto
  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
    apply (subst infsum_Sigma)
    using assms by auto
  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.