Theory HOL-Analysis.Infinite_Set_Sum

(*
  Title:    HOL/Analysis/Infinite_Set_Sum.thy
  Author:   Manuel Eberl, TU München

  A theory of sums over possible infinite sets. (Only works for absolute summability)
*)
section ‹Sums over Infinite Sets›

theory Infinite_Set_Sum
  imports Set_Integral Infinite_Sum
begin

(*
  WARNING! This file is considered obsolete and will, in the long run, be replaced with
  the more general "Infinite_Sum".
*)

text ‹Conflicting notation from theoryHOL-Analysis.Infinite_Sum
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)

(* TODO Move *)
lemma sets_eq_countable:
  assumes "countable A" "space M = A" "x. x  A  {x}  sets M"
  shows   "sets M = Pow A"
proof (intro equalityI subsetI)
  fix X assume "X  Pow A"
  hence "(xX. {x})  sets M"
    by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
  also have "(xX. {x}) = X" by auto
  finally show "X  sets M" .
next
  fix X assume "X  sets M"
  from sets.sets_into_space[OF this] and assms
    show "X  Pow A" by simp
qed

lemma measure_eqI_countable':
  assumes spaces: "space M = A" "space N = A"
  assumes sets: "x. x  A  {x}  sets M" "x. x  A  {x}  sets N"
  assumes A: "countable A"
  assumes eq: "a. a  A  emeasure M {a} = emeasure N {a}"
  shows "M = N"
proof (rule measure_eqI_countable)
  show "sets M = Pow A"
    by (intro sets_eq_countable assms)
  show "sets N = Pow A"
    by (intro sets_eq_countable assms)
qed fact+

lemma count_space_PiM_finite:
  fixes B :: "'a  'b set"
  assumes "finite A" "i. countable (B i)"
  shows   "PiM A (λi. count_space (B i)) = count_space (PiE A B)"
proof (rule measure_eqI_countable')
  show "space (PiM A (λi. count_space (B i))) = PiE A B"
    by (simp add: space_PiM)
  show "space (count_space (PiE A B)) = PiE A B" by simp
next
  fix f assume f: "f  PiE A B"
  hence "PiE A (λx. {f x})  sets (PiM A (λi. count_space (B i)))"
    by (intro sets_PiM_I_finite assms) auto
  also from f have "PiE A (λx. {f x}) = {f}"
    by (intro PiE_singleton) (auto simp: PiE_def)
  finally show "{f}  sets (PiM A (λi. count_space (B i)))" .
next
  interpret product_sigma_finite "(λi. count_space (B i))"
    by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
  thm sigma_finite_measure_count_space
  fix f assume f: "f  PiE A B"
  hence "{f} = PiE A (λx. {f x})"
    by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
  also have "emeasure (PiM A (λi. count_space (B i)))  =
               (iA. emeasure (count_space (B i)) {f i})"
    using f assms by (subst emeasure_PiM) auto
  also have " = (iA. 1)"
    by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
  also have " = emeasure (count_space (PiE A B)) {f}"
    using f by (subst emeasure_count_space_finite) auto
  finally show "emeasure (PiM A (λi. count_space (B i))) {f} =
                  emeasure (count_space (PiE A B)) {f}" .
qed (simp_all add: countable_PiE assms)



definitiontag important› abs_summable_on ::
    "('a  'b :: {banach, second_countable_topology})  'a set  bool"
    (infix "abs'_summable'_on" 50)
 where
   "f abs_summable_on A  integrable (count_space A) f"


definitiontag important› infsetsum ::
    "('a  'b :: {banach, second_countable_topology})  'a set  'b"
 where
   "infsetsum f A = lebesgue_integral (count_space A) f"

syntax (ASCII)
  "_infsetsum" :: "pttrn  'a set  'b  'b::{banach, second_countable_topology}"
  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
syntax
  "_infsetsum" :: "pttrn  'a set  'b  'b::{banach, second_countable_topology}"
  ("(2a__./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
  "aiA. b"  "CONST infsetsum (λi. b) A"

syntax (ASCII)
  "_uinfsetsum" :: "pttrn  'a set  'b  'b::{banach, second_countable_topology}"
  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
syntax
  "_uinfsetsum" :: "pttrn  'b  'b::{banach, second_countable_topology}"
  ("(2a_./ _)" [0, 10] 10)
translations ― ‹Beware of argument permutation!›
  "ai. b"  "CONST infsetsum (λi. b) (CONST UNIV)"

syntax (ASCII)
  "_qinfsetsum" :: "pttrn  bool  'a  'a::{banach, second_countable_topology}"
  ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
  "_qinfsetsum" :: "pttrn  bool  'a  'a::{banach, second_countable_topology}"
  ("(2a_ | (_)./ _)" [0, 0, 10] 10)
translations
  "ax|P. t" => "CONST infsetsum (λx. t) {x. P}"

print_translation let
  fun sum_tr' [Abs (x, Tx, t), Const (const_syntaxCollect, _) $ 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‹_qinfsetsum› $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
          end
    | sum_tr' _ = raise Match;
in [(const_syntaxinfsetsum, K sum_tr')] end


lemma restrict_count_space_subset:
  "A  B  restrict_space (count_space B) A = count_space A"
  by (subst restrict_count_space) (simp_all add: Int_absorb2)

lemma abs_summable_on_restrict:
  fixes f :: "'a  'b :: {banach, second_countable_topology}"
  assumes "A  B"
  shows   "f abs_summable_on A  (λx. indicator A x *R f x) abs_summable_on B"
proof -
  have "count_space A = restrict_space (count_space B) A"
    by (rule restrict_count_space_subset [symmetric]) fact+
  also have "integrable  f  set_integrable (count_space B) A f"
    by (simp add: integrable_restrict_space set_integrable_def)
  finally show ?thesis
    unfolding abs_summable_on_def set_integrable_def .
qed

lemma abs_summable_on_altdef: "f abs_summable_on A  set_integrable (count_space UNIV) A f"
  unfolding abs_summable_on_def set_integrable_def
  by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV)

lemma abs_summable_on_altdef':
  "A  B  f abs_summable_on A  set_integrable (count_space B) A f"
  unfolding abs_summable_on_def set_integrable_def
  by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset sets_count_space space_count_space)

lemma abs_summable_on_norm_iff [simp]:
  "(λx. norm (f x)) abs_summable_on A  f abs_summable_on A"
  by (simp add: abs_summable_on_def integrable_norm_iff)

lemma abs_summable_on_normI: "f abs_summable_on A  (λx. norm (f x)) abs_summable_on A"
  by simp

lemma abs_summable_complex_of_real [simp]: "(λn. complex_of_real (f n)) abs_summable_on A  f abs_summable_on A"
  by (simp add: abs_summable_on_def complex_of_real_integrable_eq)

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"
  using assms Bochner_Integration.integrable_bound[of "count_space A" g f]
  unfolding abs_summable_on_def by (auto simp: AE_count_space)

lemma abs_summable_on_comparison_test':
  assumes "g abs_summable_on A"
  assumes "x. x  A  norm (f x)  g x"
  shows   "f abs_summable_on A"
proof (rule abs_summable_on_comparison_test[OF assms(1), of f])
  fix x assume "x  A"
  with assms(2) have "norm (f x)  g x" .
  also have "  norm (g x)" by simp
  finally show "norm (f x)  norm (g x)" .
qed

lemma abs_summable_on_cong [cong]:
  "(x. x  A  f x = g x)  A = B  (f abs_summable_on A)  (g abs_summable_on B)"
  unfolding abs_summable_on_def by (intro integrable_cong) auto

lemma abs_summable_on_cong_neutral:
  assumes "x. x  A - B  f x = 0"
  assumes "x. x  B - A  g x = 0"
  assumes "x. x  A  B  f x = g x"
  shows   "f abs_summable_on A  g abs_summable_on B"
  unfolding abs_summable_on_altdef set_integrable_def using assms
  by (intro Bochner_Integration.integrable_cong refl)
     (auto simp: indicator_def split: if_splits)

lemma abs_summable_on_restrict':
  fixes f :: "'a  'b :: {banach, second_countable_topology}"
  assumes "A  B"
  shows   "f abs_summable_on A  (λx. if x  A then f x else 0) abs_summable_on B"
  by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)

lemma abs_summable_on_nat_iff:
  "f abs_summable_on (A :: nat set)  summable (λn. if n  A then norm (f n) else 0)"
proof -
  have "f abs_summable_on A  summable (λx. norm (if x  A then f x else 0))"
    by (subst abs_summable_on_restrict'[of _ UNIV])
       (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
  also have "(λx. norm (if x  A then f x else 0)) = (λx. if x  A then norm (f x) else 0)"
    by auto
  finally show ?thesis .
qed

lemma abs_summable_on_nat_iff':
  "f abs_summable_on (UNIV :: nat set)  summable (λn. norm (f n))"
  by (subst abs_summable_on_nat_iff) auto

lemma nat_abs_summable_on_comparison_test:
  fixes f :: "nat  'a :: {banach, second_countable_topology}"
  assumes "g abs_summable_on I"
  assumes "n. nN; n  I  norm (f n)  g n"
  shows   "f abs_summable_on I"
  using assms by (fastforce simp add: abs_summable_on_nat_iff intro: summable_comparison_test')

lemma abs_summable_comparison_test_ev:
  assumes "g abs_summable_on I"
  assumes "eventually (λx. x  I  norm (f x)  g x) sequentially"
  shows   "f abs_summable_on I"
  by (metis (no_types, lifting) nat_abs_summable_on_comparison_test eventually_at_top_linorder assms)

lemma abs_summable_on_Cauchy:
  "f abs_summable_on (UNIV :: nat set)  (e>0. N. mN. n. (x = m..<n. norm (f x)) < e)"
  by (simp add: abs_summable_on_nat_iff' summable_Cauchy sum_nonneg)

lemma abs_summable_on_finite [simp]: "finite A  f abs_summable_on A"
  unfolding abs_summable_on_def by (rule integrable_count_space)

lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
  by simp

lemma abs_summable_on_subset:
  assumes "f abs_summable_on B" and "A  B"
  shows   "f abs_summable_on A"
  unfolding abs_summable_on_altdef
  by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)

lemma abs_summable_on_union [intro]:
  assumes "f abs_summable_on A" and "f abs_summable_on B"
  shows   "f abs_summable_on (A  B)"
  using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto

lemma abs_summable_on_insert_iff [simp]:
  "f abs_summable_on insert x A  f abs_summable_on A"
proof safe
  assume "f abs_summable_on insert x A"
  thus "f abs_summable_on A"
    by (rule abs_summable_on_subset) auto
next
  assume "f abs_summable_on A"
  from abs_summable_on_union[OF this, of "{x}"]
    show "f abs_summable_on insert x A" by simp
qed

lemma abs_summable_sum:
  assumes "x. x  A  f x abs_summable_on B"
  shows   "(λy. xA. f x y) abs_summable_on B"
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)

lemma abs_summable_Re: "f abs_summable_on A  (λx. Re (f x)) abs_summable_on A"
  by (simp add: abs_summable_on_def)

lemma abs_summable_Im: "f abs_summable_on A  (λx. Im (f x)) abs_summable_on A"
  by (simp add: abs_summable_on_def)

lemma abs_summable_on_finite_diff:
  assumes "f abs_summable_on A" "A  B" "finite (B - A)"
  shows   "f abs_summable_on B"
proof -
  have "f abs_summable_on (A  (B - A))"
    by (intro abs_summable_on_union assms abs_summable_on_finite)
  also from assms have "A  (B - A) = B" by blast
  finally show ?thesis .
qed

lemma abs_summable_on_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "(λx. f (g x)) abs_summable_on A  f abs_summable_on B"
proof -
  have *: "count_space B = distr (count_space A) (count_space B) g"
    by (rule distr_bij_count_space [symmetric]) fact
  show ?thesis unfolding abs_summable_on_def
    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"])
       (insert assms, auto simp: bij_betw_def)
qed

lemma abs_summable_on_reindex:
  assumes "(λx. f (g x)) abs_summable_on A"
  shows   "f abs_summable_on (g ` A)"
proof -
  define g' where "g' = inv_into A g"
  from assms have "(λx. f (g x)) abs_summable_on (g' ` g ` A)"
    by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
  also have "?this  (λx. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
    by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
  also have "  f abs_summable_on (g ` A)"
    by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
  finally show ?thesis .
qed

lemma abs_summable_on_reindex_iff:
  "inj_on g A  (λx. f (g x)) abs_summable_on A  f abs_summable_on (g ` A)"
  by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)

lemma abs_summable_on_Sigma_project2:
  fixes A :: "'a set" and B :: "'a  'b set"
  assumes "f abs_summable_on (Sigma A B)" "x  A"
  shows   "(λy. f (x, y)) abs_summable_on (B x)"
proof -
  from assms(2) have "f abs_summable_on (Sigma {x} B)"
    by (intro abs_summable_on_subset [OF assms(1)]) auto
  also have "?this  (λz. f (x, snd z)) abs_summable_on (Sigma {x} B)"
    by (rule abs_summable_on_cong) auto
  finally have "(λy. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
    by (rule abs_summable_on_reindex)
  also have "snd ` Sigma {x} B = B x"
    using assms by (auto simp: image_iff)
  finally show ?thesis .
qed

lemma abs_summable_on_Times_swap:
  "f abs_summable_on A × B  (λ(x,y). f (y,x)) abs_summable_on B × A"
proof -
  have bij: "bij_betw (λ(x,y). (y,x)) (B × A) (A × B)"
    by (auto simp: bij_betw_def inj_on_def)
  show ?thesis
    by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
       (simp_all add: case_prod_unfold)
qed

lemma abs_summable_on_0 [simp, intro]: "(λ_. 0) abs_summable_on A"
  by (simp add: abs_summable_on_def)

lemma abs_summable_on_uminus [intro]:
  "f abs_summable_on A  (λx. -f x) abs_summable_on A"
  unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)

lemma abs_summable_on_add [intro]:
  assumes "f abs_summable_on A" and "g abs_summable_on A"
  shows   "(λx. f x + g x) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)

lemma abs_summable_on_diff [intro]:
  assumes "f abs_summable_on A" and "g abs_summable_on A"
  shows   "(λx. f x - g x) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)

lemma abs_summable_on_scaleR_left [intro]:
  assumes "c  0  f abs_summable_on A"
  shows   "(λx. f x *R c) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)

lemma abs_summable_on_scaleR_right [intro]:
  assumes "c  0  f abs_summable_on A"
  shows   "(λx. c *R f x) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)

lemma abs_summable_on_cmult_right [intro]:
  fixes f :: "'a  'b :: {banach, real_normed_algebra, second_countable_topology}"
  assumes "c  0  f abs_summable_on A"
  shows   "(λx. c * f x) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)

lemma abs_summable_on_cmult_left [intro]:
  fixes f :: "'a  'b :: {banach, real_normed_algebra, second_countable_topology}"
  assumes "c  0  f abs_summable_on A"
  shows   "(λx. f x * c) abs_summable_on A"
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)

lemma abs_summable_on_prod_PiE:
  fixes f :: "'a  'b  'c :: {real_normed_field,banach,second_countable_topology}"
  assumes finite: "finite A" and countable: "x. x  A  countable (B x)"
  assumes summable: "x. x  A  f x abs_summable_on B x"
  shows   "(λg. xA. f x (g x)) abs_summable_on PiE A B"
proof -
  define B' where "B' = (λx. if x  A then B x else {})"
  from assms have [simp]: "countable (B' x)" for x
    by (auto simp: B'_def)
  then interpret product_sigma_finite "count_space  B'"
    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
  from assms have "integrable (PiM A (count_space  B')) (λg. xA. f x (g x))"
    by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
  also have "PiM A (count_space  B') = count_space (PiE A B')"
    unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
  also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
  finally show ?thesis by (simp add: abs_summable_on_def)
qed



lemma not_summable_infsetsum_eq:
  "¬f abs_summable_on A  infsetsum f A = 0"
  by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)

lemma infsetsum_altdef:
  "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
  unfolding set_lebesgue_integral_def
  by (subst integral_restrict_space [symmetric])
     (auto simp: restrict_count_space_subset infsetsum_def)

lemma infsetsum_altdef':
  "A  B  infsetsum f A = set_lebesgue_integral (count_space B) A f"
  unfolding set_lebesgue_integral_def
  by (subst integral_restrict_space [symmetric])
     (auto simp: restrict_count_space_subset infsetsum_def)

lemma nn_integral_conv_infsetsum:
  assumes "f abs_summable_on A" "x. x  A  f x  0"
  shows   "nn_integral (count_space A) f = ennreal (infsetsum f A)"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (subst nn_integral_eq_integral) auto

lemma infsetsum_conv_nn_integral:
  assumes "nn_integral (count_space A) f  " "x. x  A  f x  0"
  shows   "infsetsum f A = enn2real (nn_integral (count_space A) f)"
  unfolding infsetsum_def using assms
  by (subst integral_eq_nn_integral) auto

lemma infsetsum_cong [cong]:
  "(x. x  A  f x = g x)  A = B  infsetsum f A = infsetsum g B"
  unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto

lemma infsetsum_0 [simp]: "infsetsum (λ_. 0) A = 0"
  by (simp add: infsetsum_def)

lemma infsetsum_all_0: "(x. x  A  f x = 0)  infsetsum f A = 0"
  by simp

lemma infsetsum_nonneg: "(x. x  A  f x  (0::real))  infsetsum f A  0"
  unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto

lemma sum_infsetsum:
  assumes "x. x  A  f x abs_summable_on B"
  shows   "(xA. ayB. f x y) = (ayB. xA. f x y)"
  using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)

lemma Re_infsetsum: "f abs_summable_on A  Re (infsetsum f A) = (axA. Re (f x))"
  by (simp add: infsetsum_def abs_summable_on_def)

lemma Im_infsetsum: "f abs_summable_on A  Im (infsetsum f A) = (axA. Im (f x))"
  by (simp add: infsetsum_def abs_summable_on_def)

lemma infsetsum_of_real:
  shows "infsetsum (λx. of_real (f x)
           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A =
             of_real (infsetsum f A)"
  unfolding infsetsum_def
  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto

lemma infsetsum_finite [simp]: "finite A  infsetsum f A = (xA. f x)"
  by (simp add: infsetsum_def lebesgue_integral_count_space_finite)

lemma infsetsum_nat:
  assumes "f abs_summable_on A"
  shows   "infsetsum f A = (n. if n  A then f n else 0)"
proof -
  from assms have "infsetsum f A = (n. indicator A n *R f n)"
    unfolding infsetsum_altdef abs_summable_on_altdef set_lebesgue_integral_def set_integrable_def
 by (subst integral_count_space_nat) auto
  also have "(λn. indicator A n *R f n) = (λn. if n  A then f n else 0)"
    by auto
  finally show ?thesis .
qed

lemma infsetsum_nat':
  assumes "f abs_summable_on UNIV"
  shows   "infsetsum f UNIV = (n. f n)"
  using assms by (subst infsetsum_nat) auto

lemma sums_infsetsum_nat:
  assumes "f abs_summable_on A"
  shows   "(λn. if n  A then f n else 0) sums infsetsum f A"
proof -
  from assms have "summable (λn. if n  A then norm (f n) else 0)"
    by (simp add: abs_summable_on_nat_iff)
  also have "(λn. if n  A then norm (f n) else 0) = (λn. norm (if n  A then f n else 0))"
    by auto
  finally have "summable (λn. if n  A then f n else 0)"
    by (rule summable_norm_cancel)
  with assms show ?thesis
    by (auto simp: sums_iff infsetsum_nat)
qed

lemma sums_infsetsum_nat':
  assumes "f abs_summable_on UNIV"
  shows   "f sums infsetsum f UNIV"
  using sums_infsetsum_nat [OF assms] by simp

lemma infsetsum_Un_disjoint:
  assumes "f abs_summable_on A" "f abs_summable_on B" "A  B = {}"
  shows   "infsetsum f (A  B) = infsetsum f A + infsetsum f B"
  using assms unfolding infsetsum_altdef abs_summable_on_altdef
  by (subst set_integral_Un) auto

lemma infsetsum_Diff:
  assumes "f abs_summable_on B" "A  B"
  shows   "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
proof -
  have "infsetsum f ((B - A)  A) = infsetsum f (B - A) + infsetsum f A"
    using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
  also from assms(2) have "(B - A)  A = B"
    by auto
  ultimately show ?thesis
    by (simp add: algebra_simps)
qed

lemma infsetsum_Un_Int:
  assumes "f abs_summable_on (A  B)"
  shows   "infsetsum f (A  B) = infsetsum f A + infsetsum f B - infsetsum f (A  B)"
proof -
  have "A  B = A  (B - A  B)"
    by auto
  also have "infsetsum f  = infsetsum f A + infsetsum f (B - A  B)"
    by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
  also have "infsetsum f (B - A  B) = infsetsum f B - infsetsum f (A  B)"
    by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
  finally show ?thesis
    by (simp add: algebra_simps)
qed

lemma infsetsum_reindex_bij_betw:
  assumes "bij_betw g A B"
  shows   "infsetsum (λx. f (g x)) A = infsetsum f B"
proof -
  have *: "count_space B = distr (count_space A) (count_space B) g"
    by (rule distr_bij_count_space [symmetric]) fact
  show ?thesis unfolding infsetsum_def
    by (subst *, subst integral_distr[of _ _ "count_space B"])
       (insert assms, auto simp: bij_betw_def)
qed

theorem infsetsum_reindex:
  assumes "inj_on g A"
  shows   "infsetsum f (g ` A) = infsetsum (λx. f (g x)) A"
  by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)

lemma infsetsum_cong_neutral:
  assumes "x. x  A - B  f x = 0"
  assumes "x. x  B - A  g x = 0"
  assumes "x. x  A  B  f x = g x"
  shows   "infsetsum f A = infsetsum g B"
  unfolding infsetsum_altdef set_lebesgue_integral_def using assms
  by (intro Bochner_Integration.integral_cong refl)
     (auto simp: indicator_def split: if_splits)

lemma infsetsum_mono_neutral:
  fixes f g :: "'a  real"
  assumes "f abs_summable_on A" and "g abs_summable_on B"
  assumes "x. x  A  f x  g x"
  assumes "x. x  A - B  f x  0"
  assumes "x. x  B - A  g x  0"
  shows   "infsetsum f A  infsetsum g B"
  using assms unfolding infsetsum_altdef set_lebesgue_integral_def abs_summable_on_altdef set_integrable_def
  by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)

lemma infsetsum_mono_neutral_left:
  fixes f g :: "'a  real"
  assumes "f abs_summable_on A" and "g abs_summable_on B"
  assumes "x. x  A  f x  g x"
  assumes "A  B"
  assumes "x. x  B - A  g x  0"
  shows   "infsetsum f A  infsetsum g B"
  using A  B by (intro infsetsum_mono_neutral assms) auto

lemma infsetsum_mono_neutral_right:
  fixes f g :: "'a  real"
  assumes "f abs_summable_on A" and "g abs_summable_on B"
  assumes "x. x  A  f x  g x"
  assumes "B  A"
  assumes "x. x  A - B  f x  0"
  shows   "infsetsum f A  infsetsum g B"
  using B  A by (intro infsetsum_mono_neutral assms) auto

lemma infsetsum_mono:
  fixes f g :: "'a  real"
  assumes "f abs_summable_on A" and "g abs_summable_on A"
  assumes "x. x  A  f x  g x"
  shows   "infsetsum f A  infsetsum g A"
  by (intro infsetsum_mono_neutral assms) auto

lemma norm_infsetsum_bound:
  "norm (infsetsum f A)  infsetsum (λx. norm (f x)) A"
  unfolding abs_summable_on_def infsetsum_def
  by (rule Bochner_Integration.integral_norm_bound)

theorem infsetsum_Sigma:
  fixes A :: "'a set" and B :: "'a  'b set"
  assumes [simp]: "countable A" and "i. countable (B i)"
  assumes summable: "f abs_summable_on (Sigma A B)"
  shows   "infsetsum f (Sigma A B) = infsetsum (λx. infsetsum (λy. f (x, y)) (B x)) A"
proof -
  define B' where "B' = (iA. B i)"
  have [simp]: "countable B'"
    unfolding B'_def by (intro countable_UN assms)
  interpret pair_sigma_finite "count_space A" "count_space B'"
    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+

  have "integrable (count_space (A × B')) (λz. indicator (Sigma A B) z *R f z)"
    using summable
    by (metis (mono_tags, lifting) abs_summable_on_altdef abs_summable_on_def integrable_cong integrable_mult_indicator set_integrable_def sets_UNIV)
  also have "?this  integrable (count_space A M count_space B') (λ(x, y). indicator (B x) y *R f (x, y))"
    by (intro Bochner_Integration.integrable_cong)
       (auto simp: pair_measure_countable indicator_def split: if_splits)
  finally have integrable:  .

  have "infsetsum (λx. infsetsum (λy. f (x, y)) (B x)) A =
          (x. infsetsum (λy. f (x, y)) (B x) count_space A)"
    unfolding infsetsum_def by simp
  also have " = (x. y. indicator (B x) y *R f (x, y) count_space B' count_space A)"
  proof (rule Bochner_Integration.integral_cong [OF refl])
    show "x. x  space (count_space A) 
         (ayB x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *R f (x, y)"
      using infsetsum_altdef'[of _ B']
      unfolding set_lebesgue_integral_def B'_def
      by auto
  qed
  also have " = ((x,y). indicator (B x) y *R f (x, y) (count_space A M count_space B'))"
    by (subst integral_fst [OF integrable]) auto
  also have " = (z. indicator (Sigma A B) z *R f z count_space (A × B'))"
    by (intro Bochner_Integration.integral_cong)
       (auto simp: pair_measure_countable indicator_def split: if_splits)
  also have " = infsetsum f (Sigma A B)"
    unfolding set_lebesgue_integral_def [symmetric]
    by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
  finally show ?thesis ..
qed

lemma infsetsum_Sigma':
  fixes A :: "'a set" and B :: "'a  'b set"
  assumes [simp]: "countable A" and "i. countable (B i)"
  assumes summable: "(λ(x,y). f x y) abs_summable_on (Sigma A B)"
  shows   "infsetsum (λx. infsetsum (λy. f x y) (B x)) A = infsetsum (λ(x,y). f x y) (Sigma A B)"
  using assms by (subst infsetsum_Sigma) auto

lemma infsetsum_Times:
  fixes A :: "'a set" and B :: "'b set"
  assumes [simp]: "countable A" and "countable B"
  assumes summable: "f abs_summable_on (A × B)"
  shows   "infsetsum f (A × B) = infsetsum (λx. infsetsum (λy. f (x, y)) B) A"
  using assms by (subst infsetsum_Sigma) auto

lemma infsetsum_Times':
  fixes A :: "'a set" and B :: "'b set"
  fixes f :: "'a  'b  'c :: {banach, second_countable_topology}"
  assumes [simp]: "countable A" and [simp]: "countable B"
  assumes summable: "(λ(x,y). f x y) abs_summable_on (A × B)"
  shows   "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λ(x,y). f x y) (A × B)"
  using assms by (subst infsetsum_Times) auto

lemma infsetsum_swap:
  fixes A :: "'a set" and B :: "'b set"
  fixes f :: "'a  'b  'c :: {banach, second_countable_topology}"
  assumes [simp]: "countable A" and [simp]: "countable B"
  assumes summable: "(λ(x,y). f x y) abs_summable_on A × B"
  shows   "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λy. infsetsum (λx. f x y) A) B"
proof -
  from summable have summable': "(λ(x,y). f y x) abs_summable_on B × A"
    by (subst abs_summable_on_Times_swap) auto
  have bij: "bij_betw (λ(x, y). (y, x)) (B × A) (A × B)"
    by (auto simp: bij_betw_def inj_on_def)
  have "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λ(x,y). f x y) (A × B)"
    using summable by (subst infsetsum_Times) auto
  also have " = infsetsum (λ(x,y). f y x) (B × A)"
    by (subst infsetsum_reindex_bij_betw[OF bij, of "λ(x,y). f x y", symmetric])
       (simp_all add: case_prod_unfold)
  also have " = infsetsum (λy. infsetsum (λx. f x y) A) B"
    using summable' by (subst infsetsum_Times) auto
  finally show ?thesis .
qed

theorem abs_summable_on_Sigma_iff:
  assumes [simp]: "countable A" and "x. x  A  countable (B x)"
  shows   "f abs_summable_on Sigma A B 
             (xA. (λy. f (x, y)) abs_summable_on B x) 
             ((λx. infsetsum (λy. norm (f (x, y))) (B x)) abs_summable_on A)"
proof safe
  define B' where "B' = (xA. B x)"
  have [simp]: "countable B'"
    unfolding B'_def using assms by auto
  interpret pair_sigma_finite "count_space A" "count_space B'"
    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
  {
    assume *: "f abs_summable_on Sigma A B"
    thus "(λy. f (x, y)) abs_summable_on B x" if "x  A" for x
      using that by (rule abs_summable_on_Sigma_project2)

    have "set_integrable (count_space (A × B')) (Sigma A B) (λz. norm (f z))"
      using abs_summable_on_normI[OF *]
      by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
    also have "count_space (A × B') = count_space A M count_space B'"
      by (simp add: pair_measure_countable)
    finally have "integrable (count_space A)
                    (λx. lebesgue_integral (count_space B')
                      (λy. indicator (Sigma A B) (x, y) *R norm (f (x, y))))"
      unfolding set_integrable_def by (rule integrable_fst')
    also have "?this  integrable (count_space A)
                    (λx. lebesgue_integral (count_space B')
                      (λy. indicator (B x) y *R norm (f (x, y))))"
      by (intro integrable_cong refl) (simp_all add: indicator_def)
    also have "  integrable (count_space A) (λx. infsetsum (λy. norm (f (x, y))) (B x))"
      unfolding set_lebesgue_integral_def [symmetric]
      by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
    also have "  (λx. infsetsum (λy. norm (f (x, y))) (B x)) abs_summable_on A"
      by (simp add: abs_summable_on_def)
    finally show  .
  }
  {
    assume *: "xA. (λy. f (x, y)) abs_summable_on B x"
    assume "(λx. ayB x. norm (f (x, y))) abs_summable_on A"
    also have "?this  (λx. yB x. norm (f (x, y)) count_space B') abs_summable_on A"
      by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
    also have "  (λx. y. indicator (Sigma A B) (x, y) *R norm (f (x, y)) count_space B')
                        abs_summable_on A" (is "_  ?h abs_summable_on _")
      unfolding set_lebesgue_integral_def
      by (intro abs_summable_on_cong) (auto simp: indicator_def)
    also have "  integrable (count_space A) ?h"
      by (simp add: abs_summable_on_def)
    finally have **:  .

    have "integrable (count_space A M count_space B') (λz. indicator (Sigma A B) z *R f z)"
    proof (rule Fubini_integrable, goal_cases)
      case 3
      {
        fix x assume x: "x  A"
        with * have "(λy. f (x, y)) abs_summable_on B x"
          by blast
        also have "?this  integrable (count_space B')
                      (λy. indicator (B x) y *R f (x, y))"
          unfolding set_integrable_def [symmetric]
         using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
        also have "(λy. indicator (B x) y *R f (x, y)) =
                     (λy. indicator (Sigma A B) (x, y) *R f (x, y))"
          using x by (auto simp: indicator_def)
        finally have "integrable (count_space B')
                        (λy. indicator (Sigma A B) (x, y) *R f (x, y))" .
      }
      thus ?case by (auto simp: AE_count_space)
    qed (insert **, auto simp: pair_measure_countable)
    moreover have "count_space A M count_space B' = count_space (A × B')"
      by (simp add: pair_measure_countable)
    moreover have "set_integrable (count_space (A × B')) (Sigma A B) f 
                 f abs_summable_on Sigma A B"
      by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
    ultimately show "f abs_summable_on Sigma A B"
      by (simp add: set_integrable_def)
  }
qed

lemma abs_summable_on_Sigma_project1:
  assumes "(λ(x,y). f x y) abs_summable_on Sigma A B"
  assumes [simp]: "countable A" and "x. x  A  countable (B x)"
  shows   "(λx. infsetsum (λy. norm (f x y)) (B x)) abs_summable_on A"
  using assms by (subst (asm) abs_summable_on_Sigma_iff) auto

lemma abs_summable_on_Sigma_project1':
  assumes "(λ(x,y). f x y) abs_summable_on Sigma A B"
  assumes [simp]: "countable A" and "x. x  A  countable (B x)"
  shows   "(λx. infsetsum (λy. f x y) (B x)) abs_summable_on A"
  by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
        norm_infsetsum_bound)

theorem infsetsum_prod_PiE:
  fixes f :: "'a  'b  'c :: {real_normed_field,banach,second_countable_topology}"
  assumes finite: "finite A" and countable: "x. x  A  countable (B x)"
  assumes summable: "x. x  A  f x abs_summable_on B x"
  shows   "infsetsum (λg. xA. f x (g x)) (PiE A B) = (xA. infsetsum (f x) (B x))"
proof -
  define B' where "B' = (λx. if x  A then B x else {})"
  from assms have [simp]: "countable (B' x)" for x
    by (auto simp: B'_def)
  then interpret product_sigma_finite "count_space  B'"
    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
  have "infsetsum (λg. xA. f x (g x)) (PiE A B) =
          (g. (xA. f x (g x)) count_space (PiE A B))"
    by (simp add: infsetsum_def)
  also have "PiE A B = PiE A B'"
    by (intro PiE_cong) (simp_all add: B'_def)
  hence "count_space (PiE A B) = count_space (PiE A B')"
    by simp
  also have " = PiM A (count_space  B')"
    unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
  also have "(g. (xA. f x (g x)) ) = (xA. infsetsum (f x) (B' x))"
    by (subst product_integral_prod)
       (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
  also have " = (xA. infsetsum (f x) (B x))"
    by (intro prod.cong refl) (simp_all add: B'_def)
  finally show ?thesis .
qed

lemma infsetsum_uminus: "infsetsum (λx. -f x) A = -infsetsum f A"
  unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_minus)

lemma infsetsum_add:
  assumes "f abs_summable_on A" and "g abs_summable_on A"
  shows   "infsetsum (λx. f x + g x) A = infsetsum f A + infsetsum g A"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_add)

lemma infsetsum_diff:
  assumes "f abs_summable_on A" and "g abs_summable_on A"
  shows   "infsetsum (λx. f x - g x) A = infsetsum f A - infsetsum g A"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_diff)

lemma infsetsum_scaleR_left:
  assumes "c  0  f abs_summable_on A"
  shows   "infsetsum (λx. f x *R c) A = infsetsum f A *R c"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_scaleR_left)

lemma infsetsum_scaleR_right:
  "infsetsum (λx. c *R f x) A = c *R infsetsum f A"
  unfolding infsetsum_def abs_summable_on_def
  by (subst Bochner_Integration.integral_scaleR_right) auto

lemma infsetsum_cmult_left:
  fixes f :: "'a  'b :: {banach, real_normed_algebra, second_countable_topology}"
  assumes "c  0  f abs_summable_on A"
  shows   "infsetsum (λx. f x * c) A = infsetsum f A * c"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_mult_left)

lemma infsetsum_cmult_right:
  fixes f :: "'a  'b :: {banach, real_normed_algebra, second_countable_topology}"
  assumes "c  0  f abs_summable_on A"
  shows   "infsetsum (λx. c * f x) A = c * infsetsum f A"
  using assms unfolding infsetsum_def abs_summable_on_def
  by (rule Bochner_Integration.integral_mult_right)

lemma infsetsum_cdiv:
  fixes f :: "'a  'b :: {banach, real_normed_field, second_countable_topology}"
  assumes "c  0  f abs_summable_on A"
  shows   "infsetsum (λx. f x / c) A = infsetsum f A / c"
  using assms unfolding infsetsum_def abs_summable_on_def by auto


(* TODO Generalise with bounded_linear *)

lemma
  fixes f :: "'a  'c :: {banach, real_normed_field, second_countable_topology}"
  assumes [simp]: "countable A" and [simp]: "countable B"
  assumes "f abs_summable_on A" and "g abs_summable_on B"
  shows   abs_summable_on_product: "(λ(x,y). f x * g y) abs_summable_on A × B"
    and   infsetsum_product: "infsetsum (λ(x,y). f x * g y) (A × B) =
                                infsetsum f A * infsetsum g B"
proof -
  from assms show "(λ(x,y). f x * g y) abs_summable_on A × B"
    by (subst abs_summable_on_Sigma_iff)
       (auto intro!: abs_summable_on_cmult_right simp: norm_mult infsetsum_cmult_right)
  with assms show "infsetsum (λ(x,y). f x * g y) (A × B) = infsetsum f A * infsetsum g B"
    by (subst infsetsum_Sigma)
       (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
qed

lemma abs_summable_finite_sumsI:
  assumes "F. finite F  FS  sum (λx. norm (f x)) F  B"
  shows "f abs_summable_on S"
proof -
  have main: "f abs_summable_on S  infsetsum (λx. norm (f x)) S  B" if B  0 and S  {}
  proof -
    define M normf where "M = count_space S" and "normf x = ennreal (norm (f x))" for x
    have "sum normf F  ennreal B"
      if "finite F" and "F  S" and
        "F. finite F  F  S  (iF. ennreal (norm (f i)))  ennreal B" and
        "ennreal 0  ennreal B" for F
      using that unfolding normf_def[symmetric] by simp
    hence normf_B: "finite F  FS  sum normf F  ennreal B" for F
      using assms[THEN ennreal_leI]
      by auto
    have "integralS M g  B" if "simple_function M g" and "g  normf" for g 
    proof -
      define gS where "gS = g ` S"
      have "finite gS"
        using that unfolding gS_def M_def simple_function_count_space by simp
      have "gS  {}" unfolding gS_def using S  {} by auto
      define part where "part r = g -` {r}  S" for r
      have r_finite: "r < " if "r : gS" for r 
        using g  normf that unfolding gS_def le_fun_def normf_def apply auto
        using ennreal_less_top neq_top_trans top.not_eq_extremum by blast
      define B' where "B' r = (SUP F{F. finite F  Fpart r}. sum normf F)" for r
      have B'fin: "B' r < " for r
      proof -
        have "B' r  (SUP F{F. finite F  Fpart r}. sum normf F)"
          unfolding B'_def
          by (metis (mono_tags, lifting) SUP_least SUP_upper)
        also have "  B"
          using normf_B unfolding part_def
          by (metis (no_types, lifting) Int_subset_iff SUP_least mem_Collect_eq)
        also have " < "
          by simp
        finally show ?thesis by simp
      qed
      have sumB': "sum B' gS  ennreal B + ε" if "ε>0" for ε
      proof -
        define N εN where "N = card gS" and "εN = ε / N"
        have "N > 0" 
          unfolding N_def using gS{} finite gS
          by (simp add: card_gt_0_iff)
        from εN_def that have "εN > 0"
          by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_zero_less_divide)
        have c1: "y. B' r  sum normf y + εN  finite y  y  part r"
          if "B' r = 0" for r
          using that by auto
        have c2: "y. B' r  sum normf y + εN  finite y  y  part r" if "B' r  0" for r
        proof-
          have "B' r - εN < B' r"
            using B'fin 0 < εN ennreal_between that by fastforce
          have "B' r - εN < Sup (sum normf ` {F. finite F  F  part r}) 
               F. B' r - εN  sum normf F  finite F  F  part r"
            by (metis (no_types, lifting) leD le_cases less_SUP_iff mem_Collect_eq)
          hence "B' r - εN < B' r  F. B' r - εN  sum normf F  finite F  F  part r"
            by (subst (asm) (2) B'_def)
          then obtain F where "B' r - εN  sum normf F" and "finite F" and "F  part r"
            using B' r - εN < B' r by auto  
          thus "F. B' r  sum normf F + εN  finite F  F  part r"
            by (metis add.commute ennreal_minus_le_iff)
        qed
        have "x. y. B' x  sum normf y + εN 
            finite y  y  part x"
          using c1 c2
          by blast 
        hence "F. x. B' x  sum normf (F x) + εN  finite (F x)  F x  part x"
          by metis 
        then obtain F where F: "sum normf (F r) + εN  B' r" and Ffin: "finite (F r)" and Fpartr: "F r  part r" for r
          using atomize_elim by auto
        have w1: "finite gS"
          by (simp add: finite gS)          
        have w2: "igS. finite (F i)"
          by (simp add: Ffin)          
        have False
          if "r. F r  g -` {r}  F r  S"
            and "i  gS" and "j  gS" and "i  j" and "x  F i" and "x  F j"
          for i j x
          by (metis subsetD that(1) that(4) that(5) that(6) vimage_singleton_eq)          
        hence w3: "igS. jgS. i  j  F i  F j = {}"
          using Fpartr[unfolded part_def] by auto          
        have w4: "sum normf ( (F ` gS)) + ε = sum normf ( (F ` gS)) + ε"
          by simp
        have "sum B' gS  (rgS. sum normf (F r) + εN)"
          using F by (simp add: sum_mono)
        also have " = (rgS. sum normf (F r)) + (rgS. εN)"
          by (simp add: sum.distrib)
        also have " = (rgS. sum normf (F r)) + (card gS * εN)"
          by auto
        also have " = (rgS. sum normf (F r)) + ε"
          unfolding εN_def N_def[symmetric] using N>0 
          by (simp add: ennreal_times_divide mult.commute mult_divide_eq_ennreal)
        also have " = sum normf ( (F ` gS)) + ε" 
          using w1 w2 w3 w4
          by (subst sum.UNION_disjoint[symmetric])
        also have "  B + ε"
          using finite gS normf_B add_right_mono Ffin Fpartr unfolding part_def
          by (simp add: gS  {} cSUP_least)          
        finally show ?thesis
          by auto
      qed
      hence sumB': "sum B' gS  B"
        using ennreal_le_epsilon ennreal_less_zero_iff by blast
      have "r. y. r  gS  B' r = ennreal y"
        using B'fin less_top_ennreal by auto
      hence "B''. r. r  gS  B' r = ennreal (B'' r)"
        by (rule_tac choice) 
      then obtain B'' where B'': "B' r = ennreal (B'' r)" if "r  gS" for r
        by atomize_elim 
      have cases[case_names zero finite infinite]: "P" if "r=0  P" and "finite (part r)  P"
        and "infinite (part r)  r0  P" for P r
        using that by metis
      have emeasure_B': "r * emeasure M (part r)  B' r" if "r : gS" for r
      proof (cases rule:cases[of r])
        case zero
        thus ?thesis by simp
      next
        case finite
        have s1: "sum g F  sum normf F"
          if "F  {F. finite F  F  part r}"
          for F
          using g  normf 
          by (simp add: le_fun_def sum_mono)

        have "r * of_nat (card (part r)) = r * (xpart r. 1)" by simp
        also have " = (xpart r. r)"
          using mult.commute by auto
        also have " = (xpart r. g x)"
          unfolding part_def by auto
        also have "  (SUP F{F. finite F  Fpart r}. sum g F)"
          using finite
          by (simp add: Sup_upper)
        also have "  B' r"        
          unfolding B'_def
          using s1 SUP_subset_mono by blast
        finally have "r * of_nat (card (part r))  B' r" by assumption
        thus ?thesis
          unfolding M_def
          using part_def finite by auto
      next
        case infinite
        from r_finite[OF r : gS] obtain r' where r': "r = ennreal r'"
          using ennreal_cases by auto
        with infinite have "r' > 0"
          using ennreal_less_zero_iff not_gr_zero by blast
        obtain N::nat where N:"N > B / r'" and "real N > 0" apply atomize_elim
          using reals_Archimedean2
          by (metis less_trans linorder_neqE_linordered_idom)
        obtain F where "finite F" and "card F = N" and "F  part r"
          using infinite(1) infinite_arbitrarily_large by blast
        from F  part r have "F  S" unfolding part_def by simp
        have "B < r * N"
          unfolding r' ennreal_of_nat_eq_real_of_nat
          using N 0 < r' B  0 r'
          by (metis enn2real_ennreal enn2real_less_iff ennreal_less_top ennreal_mult' less_le mult_less_cancel_left_pos nonzero_mult_div_cancel_left times_divide_eq_right)
        also have "r * N = (xF. r)"
          using card F = N by (simp add: mult.commute)
        also have "(xF. r) = (xF. g x)"
          using F  part r  part_def sum.cong subsetD by fastforce
        also have "(xF. g x)  (xF. ennreal (norm (f x)))"
          by (metis (mono_tags, lifting) g  normf normf  λx. ennreal (norm (f x)) le_fun_def 
              sum_mono)
        also have "(xF. ennreal (norm (f x)))  B"
          using F  S finite F normf  λx. ennreal (norm (f x)) normf_B by blast 
        finally have "B < B" by auto
        thus ?thesis by simp
      qed

      have "integralS M g = (r  gS. r * emeasure M (part r))"
        unfolding simple_integral_def gS_def M_def part_def by simp
      also have "  (r  gS. B' r)"
        by (simp add: emeasure_B' sum_mono)
      also have "  B"
        using sumB' by blast
      finally show ?thesis by assumption
    qed
    hence int_leq_B: "integralN M normf  B"
      unfolding nn_integral_def by (metis (no_types, lifting) SUP_least mem_Collect_eq)
    hence "integralN M normf < "
      using le_less_trans by fastforce
    hence "integrable M f"
      unfolding M_def normf_def by (rule integrableI_bounded[rotated], simp)
    hence v1: "f abs_summable_on S"
      unfolding abs_summable_on_def M_def by simp  

    have "(λx. norm (f x)) abs_summable_on S"
      using v1 Infinite_Set_Sum.abs_summable_on_norm_iff[where A = S and f = f]
      by auto
    moreover have "0  norm (f x)"
      if "x  S" for x
      by simp    
    moreover have "(+ x. ennreal (norm (f x)) count_space S)  ennreal B"
      using M_def normf  λx. ennreal (norm (f x)) int_leq_B by auto    
    ultimately have "ennreal (axS. norm (f x))  ennreal B"
      by (simp add: nn_integral_conv_infsetsum)    
    hence v2: "(axS. norm (f x))  B"
      by (subst ennreal_le_iff[symmetric], simp add: assms B  0)
    show ?thesis
      using v1 v2 by auto
  qed
  then show "f abs_summable_on S"
    by (metis abs_summable_on_finite assms empty_subsetI finite.emptyI sum_clauses(1))
qed


lemma infsetsum_nonneg_is_SUPREMUM_ennreal:
  fixes f :: "'a  real"
  assumes summable: "f abs_summable_on A"
    and fnn: "x. xA  f x  0"
  shows "ennreal (infsetsum f A) = (SUP F{F. finite F  F  A}. (ennreal (sum f F)))"
proof -
  have sum_F_A: "sum f F  infsetsum f A" 
    if "F  {F. finite F  F  A}" 
    for F
  proof-
    from that have "finite F" and "F  A" by auto
    from finite F have "sum f F = infsetsum f F" by auto
    also have "  infsetsum f A"
    proof (rule infsetsum_mono_neutral_left)
      show "f abs_summable_on F"
        by (simp add: finite F)        
      show "f abs_summable_on A"
        by (simp add: local.summable)        
      show "f x  f x"
        if "x  F"
        for x :: 'a
        by simp 
      show "F  A"
        by (simp add: F  A)        
      show "0  f x"
        if "x  A - F"
        for x :: 'a
        using that fnn by auto 
    qed
    finally show ?thesis by assumption
  qed 
  hence geq: "ennreal (infsetsum f A)  (SUP F{G. finite G  G  A}. (ennreal (sum f F)))"
    by (meson SUP_least ennreal_leI)

  define fe where "fe x = ennreal (f x)" for x

  have sum_f_int: "infsetsum f A = + x. fe x (count_space A)"
    unfolding infsetsum_def fe_def
  proof (rule nn_integral_eq_integral [symmetric])
    show "integrable (count_space A) f"
      using abs_summable_on_def local.summable by blast      
    show "AE x in count_space A. 0  f x"
      using fnn by auto      
  qed
  also have " = (SUP g  {g. finite (g`A)  g  fe}. integralS (count_space A) g)"
    unfolding nn_integral_def simple_function_count_space by simp
  also have "  (SUP F{F. finite F  F  A}. (ennreal (sum f F)))"
  proof (rule Sup_least)
    fix x assume "x  integralS (count_space A) ` {g. finite (g ` A)  g  fe}"
    then obtain g where xg: "x = integralS (count_space A) g" and fin_gA: "finite (g`A)" 
      and g_fe: "g  fe" by auto
    define F where "F = {z:A. g z  0}"
    hence "F  A" by simp

    have fin: "finite {z:A. g z = t}" if "t  0" for t
    proof (rule ccontr)
      assume inf: "infinite {z:A. g z = t}"
      hence tgA: "t  g ` A"
        by (metis (mono_tags, lifting) image_eqI not_finite_existsD)
      have "x = (x  g ` A. x * emeasure (count_space A) (g -` {x}  A))"
        unfolding xg simple_integral_def space_count_space by simp
      also have "  (x  {t}. x * emeasure (count_space A) (g -` {x}  A))" (is "_  ")
      proof (rule sum_mono2)
        show "finite (g ` A)"
          by (simp add: fin_gA)          
        show "{t}  g ` A"
          by (simp add: tgA)          
        show "0  b * emeasure (count_space A) (g -` {b}  A)"
          if "b  g ` A - {t}"
          for b :: ennreal
          using that
          by simp
      qed
      also have " = t * emeasure (count_space A) (g -` {t}  A)"
        by auto
      also have " = t * "
      proof (subst emeasure_count_space_infinite)
        show "g -` {t}  A  A"
          by simp             
        have "{a  A. g a = t} = {a  g -` {t}. a  A}"
          by auto
        thus "infinite (g -` {t}  A)"
          by (metis (full_types) Int_def inf) 
        show "t *  = t * "
          by simp
      qed
      also have " = " using t  0
        by (simp add: ennreal_mult_eq_top_iff)
      finally have x_inf: "x = "
        using neq_top_trans by auto
      have "x = integralS (count_space A) g" by (fact xg)
      also have " = integralN (count_space A) g"
        by (simp add: fin_gA nn_integral_eq_simple_integral)
      also have "  integralN (count_space A) fe"
        using g_fe
        by (simp add: le_funD nn_integral_mono)
      also have " < "
        by (metis sum_f_int ennreal_less_top infinity_ennreal_def) 
      finally have x_fin: "x < " by simp
      from x_inf x_fin show False by simp
    qed
    have F: "F = (tg`A-{0}. {zA. g z = t})"
      unfolding F_def by auto
    hence "finite F"
      unfolding F using fin_gA fin by auto
    have "x = integralN (count_space A) g"
      unfolding xg
      by (simp add: fin_gA nn_integral_eq_simple_integral)
    also have " = set_nn_integral (count_space UNIV) A g"
      by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
    also have " = set_nn_integral (count_space UNIV) F g"
    proof -
      have "a. g a * (if a  {a  A. g a  0} then 1 else 0) = g a * (if a  A then 1 else 0)"
        by auto
      hence "(+ a. g a * (if a  A then 1 else 0) count_space UNIV)
           = (+ a. g a * (if a  {a  A. g a  0} then 1 else 0) count_space UNIV)"
        by presburger
      thus ?thesis unfolding F_def indicator_def
        using mult.right_neutral mult_zero_right nn_integral_cong
        by (simp add: of_bool_def) 
    qed
    also have " = integralN (count_space F) g"
      by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
    also have " = sum g F" 
      using finite F by (rule nn_integral_count_space_finite)
    also have "sum g F  sum fe F"
      using g_fe unfolding le_fun_def
      by (simp add: sum_mono) 
    also have "  (SUP F  {G. finite G  G  A}. (sum fe F))"
      using finite F FA
      by (simp add: SUP_upper)
    also have " = (SUP F  {F. finite F  F  A}. (ennreal (sum f F)))"
    proof (rule SUP_cong [OF refl])
      have "finite x  x  A  (xx. ennreal (f x)) = ennreal (sum f x)"
        for x
        by (metis fnn subsetCE sum_ennreal)
      thus "sum fe x = ennreal (sum f x)"
        if "x  {G. finite G  G  A}"
        for x :: "'a set"
        using that unfolding fe_def by auto      
    qed 
    finally show "x  " by simp
  qed
  finally have leq: "ennreal (infsetsum f A)  (SUP F{F. finite F  F  A}. (ennreal (sum f F)))"
    by assumption
  from leq geq show ?thesis by simp
qed

lemma infsetsum_nonneg_is_SUPREMUM_ereal:
  fixes f :: "'a  real"
  assumes summable: "f abs_summable_on A"
    and fnn: "x. xA  f x  0"
  shows "ereal (infsetsum f A) = (SUP F{F. finite F  F  A}. (ereal (sum f F)))"
proof -
  have "ereal (infsetsum f A) = enn2ereal (ennreal (infsetsum f A))"
    by (simp add: fnn infsetsum_nonneg)
  also have " = enn2ereal (SUP F{F. finite F  F  A}. ennreal (sum f F))"
    apply (subst infsetsum_nonneg_is_SUPREMUM_ennreal)
    using fnn by (auto simp add: local.summable)      
  also have " = (SUP F{F. finite F  F  A}. (ereal (sum f F)))"
  proof (simp add: image_def Sup_ennreal.rep_eq)
    have "0  Sup {y. x. (xa. finite xa  xa  A  x = ennreal (sum f xa)) 
                     y = enn2ereal x}"
      by (metis (mono_tags, lifting) Sup_upper empty_subsetI ennreal_0 finite.emptyI
          mem_Collect_eq sum.empty zero_ennreal.rep_eq)
    moreover have "(x. (y. finite y  y  A  x = ennreal (sum f y))  y = enn2ereal x) = 
                   (x. finite x  x  A  y = ereal (sum f x))" for y
    proof -
      have "(x. (y. finite y  y  A  x = ennreal (sum f y))  y = enn2ereal x) 
            (X x. finite X  X  A  x = ennreal (sum f X)  y = enn2ereal x)"
        by blast
      also have "  (X. finite X  X  A  y = ereal (sum f X))"
        by (rule arg_cong[of _ _ Ex])
           (auto simp: fun_eq_iff intro!: enn2ereal_ennreal sum_nonneg enn2ereal_ennreal[symmetric] fnn)
      finally show ?thesis .
    qed
    hence "Sup {y. x. (y. finite y  y  A  x = ennreal (sum f y))  y = enn2ereal x} =
           Sup {y. x. finite x  x  A  y = ereal (sum f x)}"
      by simp
    ultimately show "max 0 (Sup {y. x. (xa. finite xa  xa  A  x
                                       = ennreal (sum f xa))  y = enn2ereal x})
         = Sup {y. x. finite x  x  A  y = ereal (sum f x)}"
      by linarith
  qed   
  finally show ?thesis
    by simp
qed


text ‹The following theorem relates constInfinite_Set_Sum.abs_summable_on with constInfinite_Sum.abs_summable_on.
  Note that while this theorem expresses an equivalence, the notion on the lhs is more general
  nonetheless because it applies to a wider range of types. (The rhs requires second-countable
  Banach spaces while the lhs is well-defined on arbitrary real vector spaces.)›

lemma abs_summable_equivalent: Infinite_Sum.abs_summable_on f A  f abs_summable_on A
proof (rule iffI)
  define n where n x = norm (f x) for x
  assume n summable_on A
  then have sum n F  infsum n A if finite F and FA for F
    using that by (auto simp flip: infsum_finite simp: n_def[abs_def] intro!: infsum_mono_neutral)
    
  then show f abs_summable_on A
    by (auto intro!: abs_summable_finite_sumsI simp: n_def)
next
  define n where n x = norm (f x) for x
  assume f abs_summable_on A
  then have n abs_summable_on A
    by (simp add: f abs_summable_on A n_def)
  then have sum n F  infsetsum n A if finite F and FA for F
    using that by (auto simp flip: infsetsum_finite simp: n_def[abs_def] intro!: infsetsum_mono_neutral)
  then show n summable_on A
    apply (rule_tac nonneg_bdd_above_summable_on)
    by (auto simp add: n_def bdd_above_def)
qed

lemma infsetsum_infsum:
  assumes "f abs_summable_on A"
  shows "infsetsum f A = infsum f A"
proof -
  have conv_sum_norm[simp]: "(λx. norm (f x)) summable_on A"
    using abs_summable_equivalent assms by blast
  have "norm (infsetsum f A - infsum f A)  ε" if "ε>0" for ε
  proof -
    define δ where "δ = ε/2"
    with that have [simp]: "δ > 0" by simp
    obtain F1 where F1A: "F1  A" and finF1: "finite F1" and leq_eps: "infsetsum (λx. norm (f x)) (A-F1)  δ"
    proof -
      have sum_SUP: "ereal (infsetsum (λx. norm (f x)) A) = (SUP F{F. finite F  F  A}. ereal (sum (λx. norm (f x)) F))"
        (is "_ = ?SUP")
        apply (rule infsetsum_nonneg_is_SUPREMUM_ereal)
        using assms by auto

      have "(SUP F{F. finite F  F  A}. ereal (xF. norm (f x))) - ereal δ
            < (SUP i{F. finite F  F  A}. ereal (xi. norm (f x)))"
        using δ>0
        by (metis diff_strict_left_mono diff_zero ereal_less_eq(3) ereal_minus(1) not_le sum_SUP)
      then obtain F where "F{F. finite F  F  A}" and "ereal (sum (λx. norm (f x)) F) > ?SUP - ereal (δ)"
        by (meson less_SUP_iff)
        
      hence "sum (λx. norm (f x)) F > infsetsum (λx. norm (f x)) A -  (δ)"
        unfolding sum_SUP[symmetric] by auto
      hence "δ > infsetsum (λx. norm (f x)) (A-F)"
      proof (subst infsetsum_Diff)
        show "(λx. norm (f x)) abs_summable_on A"
          if "(axA. norm (f x)) - δ < (xF. norm (f x))"
          using that
          by (simp add: assms) 
        show "F  A"
          if "(axA. norm (f x)) - δ < (xF. norm (f x))"
          using that F  {F. finite F  F  A} by blast 
        show "(axA. norm (f x)) - (axF. norm (f x)) < δ"
          if "(axA. norm (f x)) - δ < (xF. norm (f x))"
          using that F  {F. finite F  F  A} by auto 
      qed
      thus ?thesis using that 
        apply atomize_elim
        using F  {F. finite F  F  A} less_imp_le by blast
    qed
    obtain F2 where F2A: "F2  A" and finF2: "finite F2"
      and dist: "dist (sum (λx. norm (f x)) F2) (infsum (λx. norm (f x)) A)  δ"
      apply atomize_elim
      by (metis 0 < δ conv_sum_norm infsum_finite_approximation)
    have  leq_eps': "infsum (λx. norm (f x)) (A-F2)  δ"
      apply (subst infsum_Diff)
      using finF2 F2A dist by (auto simp: dist_norm)
    define F where "F = F1  F2"
    have FA: "F  A" and finF: "finite F" 
      unfolding F_def using F1A F2A finF1 finF2 by auto

    have "(axA - (F1  F2). norm (f x))  (axA - F1. norm (f x))"
      apply (rule infsetsum_mono_neutral_left)
      using abs_summable_on_subset assms by fastforce+
    hence leq_eps: "infsetsum (λx. norm (f x)) (A-F)  δ"
      unfolding F_def
      using leq_eps by linarith
    have "infsum (λx. norm (f x)) (A - (F1  F2))
           infsum (λx. norm (f x)) (A - F2)"
      apply (rule infsum_mono_neutral)
      using finF by (auto simp add: finF2 summable_on_cofin_subset F_def)
    hence leq_eps': "infsum (λx. norm (f x)) (A-F)  δ"
      unfolding F_def 
      by (rule order.trans[OF _ leq_eps'])
    have "norm (infsetsum f A - infsetsum f F) = norm (infsetsum f (A-F))"
      apply (subst infsetsum_Diff [symmetric])
      by (auto simp: FA assms)
    also have "  infsetsum (λx. norm (f x)) (A-F)"
      using norm_infsetsum_bound by blast
    also have "  δ"
      using leq_eps by simp
    finally have diff1: "norm (infsetsum f A - infsetsum f F)  δ"
      by assumption
    have "norm (infsum f A - infsum f F) = norm (infsum f (A-F))"
      apply (subst infsum_Diff [symmetric])
      by (auto simp: assms abs_summable_summable finF FA)
    also have "  infsum (λx. norm (f x)) (A-F)"
      by (simp add: finF summable_on_cofin_subset norm_infsum_bound)
    also have "  δ"
      using leq_eps' by simp
    finally have diff2: "norm (infsum f A - infsum f F)  δ"
      by assumption

    have x1: "infsetsum f F = infsum f F"
      using finF by simp
    have "norm (infsetsum f A - infsum f A)  norm (infsetsum f A - infsetsum f F) + norm (infsum f A - infsum f F)"
      apply (rule_tac norm_diff_triangle_le)
       apply auto
      by (simp_all add: x1 norm_minus_commute)
    also have "  ε"
      using diff1 diff2 δ_def by linarith
    finally show ?thesis
      by assumption
  qed
  hence "norm (infsetsum f A - infsum f A) = 0"
    by (meson antisym_conv1 dense_ge norm_not_less_zero)
  thus ?thesis
    by auto
qed

end