Quelle Infinite_Set_Sum.thy Sprache: Isabelle

(*
  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 \<open>Sums over Infinite Sets\<close>

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 \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
no_notation Infinite_Sum.abs_summable_on (infixr \<open>abs'_summable'_on\<close> 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 "(\x\X. {x}) \ sets M"
    by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
  also have "(\x\X. {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 (Pi\<^sub>M 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 (Pi\<^sub>M 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 (Pi\<^sub>M A (\i. count_space (B i))) \ =
               (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
    using f assms by (subst emeasure_PiM) auto
  also have "\ = (\i\A. 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 (Pi\<^sub>M A (\i. count_space (B i))) {f} =
                  emeasure (count_space (Pi\<^sub>E A B)) {f}" .
qed (simp_all add: countable_PiE assms)

definition\<^marker>\<open>tag important\<close> abs_summable_on ::
    "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool"
    (infix \<open>abs'_summable'_on\<close> 50)
where
   "f abs_summable_on A \ integrable (count_space A) f"

definition\<^marker>\<open>tag important\<close> 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}"
  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
  "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}"
  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
syntax_consts
  "_infsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
  "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A"

syntax (ASCII)
  "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}"
  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
  "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}"
  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
syntax_consts
  "_uinfsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
  "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)"

syntax (ASCII)
  "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}"
  (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
  "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}"
  (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
  "_qinfsetsum" \<rightleftharpoons> infsetsum
translations
  "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}"
print_translation \<open>
  [(\<^const_syntax>\<open>infsetsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsetsum\<close>))]
\<close>

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 *\<^sub>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. \n\N; 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. \m\N. \n. (\x = m..
  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. \x\A. 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 *\<^sub>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 *\<^sub>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. \x\A. f x (g x)) abs_summable_on PiE A B"
proof -
  define B' where "B' = (\<lambda>x. if x \<in> 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. \x\A. 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   "(\x\A. \\<^sub>ay\B. f x y) = (\\<^sub>ay\B. \x\A. 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) = (\\<^sub>ax\A. Re (f x))"
  by (simp add: infsetsum_def abs_summable_on_def)

lemma Im_infsetsum: "f abs_summable_on A \ Im (infsetsum f A) = (\\<^sub>ax\A. 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 = (\x\A. 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 *\<^sub>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 *\<^sub>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 \<open>A \<subseteq> B\<close> 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 \<open>B \<subseteq> A\<close> 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' = (\<Union>i\<in>A. 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 *\<^sub>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 \\<^sub>M count_space B') (\(x, y). indicator (B x) y *\<^sub>R f (x, y))"
    by (intro Bochner_Integration.integrable_cong)
       (auto simp: pair_measure_countable indicator_def split: if_splits)
  finally have integrable: \<dots> .

  have "infsetsum (\x. infsetsum (\y. f (x, y)) (B x)) A =
          (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
    unfolding infsetsum_def by simp
  also have "\ = (\x. \y. indicator (B x) y *\<^sub>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) \
         (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>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 *\<^sub>R f (x, y) \(count_space A \\<^sub>M count_space B'))"
    by (subst integral_fst [OF integrable]) auto
  also have "\ = (\z. indicator (Sigma A B) z *\<^sub>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 \
             (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
             ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
proof safe
  define B' where "B' = (\<Union>x\<in>A. 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 \\<^sub>M count_space B'"
      by (simp add: pair_measure_countable)
    finally have "integrable (count_space A)
                    (\<lambda>x. lebesgue_integral (count_space B')
                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
      unfolding set_integrable_def by (rule integrable_fst')
    also have "?this \ integrable (count_space A)
                    (\<lambda>x. lebesgue_integral (count_space B')
                      (\<lambda>y. indicator (B x) y *\<^sub>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 \<dots> .
  }
  {
    assume *: "\x\A. (\y. f (x, y)) abs_summable_on B x"
    assume "(\x. \\<^sub>ay\B x. norm (f (x, y))) abs_summable_on A"
    also have "?this \ (\x. \y\B 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) *\<^sub>R norm (f (x, y)) \count_space B')
                        abs_summable_on A" (is "_ \<longleftrightarrow> ?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 **: \<dots> .

    have "integrable (count_space A \\<^sub>M count_space B') (\z. indicator (Sigma A B) z *\<^sub>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')
                      (\<lambda>y. indicator (B x) y *\<^sub>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 *\<^sub>R f (x, y)) =
                     (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
          using x by (auto simp: indicator_def)
        finally have "integrable (count_space B')
                        (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" .
      }
      thus ?case by (auto simp: AE_count_space)
    qed (insert **, auto simp: pair_measure_countable)
    moreover have "count_space A \\<^sub>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. \x\A. f x (g x)) (PiE A B) = (\x\A. infsetsum (f x) (B x))"
proof -
  define B' where "B' = (\<lambda>x. if x \<in> 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. \x\A. f x (g x)) (PiE A B) =
          (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>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. (\x\A. f x (g x)) \\) = (\x\A. 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 "\ = (\x\A. 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 *\<^sub>R c) A = infsetsum f A *\<^sub>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 *\<^sub>R f x) A = c *\<^sub>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 \ F\S \ 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 \ (\i\F. 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 \ F\S \ sum normf F \ ennreal B" for F
      using assms[THEN ennreal_leI]
      by auto
    have "integral\<^sup>S 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 \<open>g \<le> normf\<close> that unfolding gS_def le_fun_def normf_def apply auto
        using ennreal_less_top neq_top_trans top.not_eq_extremum by blast
      define B' where "B' r = (SUP F\<in>{F. finite F \<and> F\<subseteq>part r}. sum normf F)" for r
      have B'fin: "B' r < \<infinity>" for r
      proof -
        have "B' r \ (SUP F\{F. finite F \ F\part 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 \<le> ennreal B + \<epsilon>" if "\<epsilon>>0" for \<epsilon>
      proof -
        define N \<epsilon>N where "N = card gS" and "\<epsilon>N = \<epsilon> / N"
        have "N > 0"
          unfolding N_def using \<open>gS\<noteq>{}\<close> \<open>finite gS\<close>
          by (simp add: card_gt_0_iff)
        from \<epsilon>N_def that have "\<epsilon>N > 0"
          by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_zero_less_divide)
        have c1: "\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}) \
               \<exists>F. B' r - \<epsilon>N \<le> sum normf F \<and> finite F \<and> F \<subseteq> part r"
            by (metis (no_types, lifting) leD le_cases less_SUP_iff mem_Collect_eq)
          hence "B' r - \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 \<open>B' r - \<epsilon>N < B' r\<close> 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 \<and> y \<subseteq> 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: \<open>finite gS\<close>)
        have w2: "\i\gS. 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: "\i\gS. \j\gS. 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 \ (\r\gS. sum normf (F r) + \N)"
          using F by (simp add: sum_mono)
        also have "\ = (\r\gS. sum normf (F r)) + (\r\gS. \N)"
          by (simp add: sum.distrib)
        also have "\ = (\r\gS. sum normf (F r)) + (card gS * \N)"
          by auto
        also have "\ = (\r\gS. sum normf (F r)) + \"
          unfolding \<epsilon>N_def N_def[symmetric] using \<open>N>0\<close>
          by (simp add: ennreal_times_divide mult.commute mult_divide_eq_ennreal)
        also have "\ = sum normf (\ (F ` gS)) + \"
          using w1 w2 w3 w4
          by (subst sum.UNION_disjoint[symmetric])
        also have "\ \ B + \"
          using \<open>finite gS\<close> normf_B add_right_mono Ffin Fpartr unfolding part_def
          by (simp add: \<open>gS \<noteq> {}\<close> cSUP_least)
        finally show ?thesis
          by auto
      qed
      hence sumB': "sum B' gS \<le> B"
        using ennreal_le_epsilon ennreal_less_zero_iff by blast
      have "\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) \ r\0 \ 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 \<open>g \<le> normf\<close>
          by (simp add: le_fun_def sum_mono)

        have "r * of_nat (card (part r)) = r * (\x\part r. 1)" by simp
        also have "\ = (\x\part r. r)"
          using mult.commute by auto
        also have "\ = (\x\part r. g x)"
          unfolding part_def by auto
        also have "\ \ (SUP F\{F. finite F \ F\part 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 \<open>r : gS\<close>] obtain r' where r': "r = ennreal r'"
          using ennreal_cases by auto
        with infinite have "r' > 0"
          using ennreal_less_zero_iff not_gr_zero by blast
        obtain N::nat where N:"N > B / r'" and "real N > 0" apply atomize_elim
          using reals_Archimedean2
          by (metis less_trans linorder_neqE_linordered_idom)
        obtain F where "finite F" and "card F = N" and "F \ part r"
          using infinite(1) infinite_arbitrarily_large by blast
        from \<open>F \<subseteq> part r\<close> have "F \<subseteq> S" unfolding part_def by simp
        have "B < r * N"
          unfolding r' ennreal_of_nat_eq_real_of_nat
          using N \<open>0 < r'\<close> \<open>B \<ge> 0\<close> r'
          by (metis enn2real_ennreal enn2real_less_iff ennreal_less_top ennreal_mult' less_le mult_less_cancel_left_pos nonzero_mult_div_cancel_left times_divide_eq_right)
        also have "r * N = (\x\F. r)"
          using \<open>card F = N\<close> by (simp add: mult.commute)
        also have "(\x\F. r) = (\x\F. g x)"
          using \<open>F \<subseteq> part r\<close>  part_def sum.cong subsetD by fastforce
        also have "(\x\F. g x) \ (\x\F. ennreal (norm (f x)))"
          by (metis (mono_tags, lifting) \<open>g \<le> normf\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> le_fun_def
              sum_mono)
        also have "(\x\F. ennreal (norm (f x))) \ B"
          using \<open>F \<subseteq> S\<close> \<open>finite F\<close> \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> normf_B by blast
        finally have "B < B" by auto
        thus ?thesis by simp
      qed

      have "integral\<^sup>S M g = (\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: "integral\<^sup>N M normf \ B"
      unfolding nn_integral_def by (metis (no_types, lifting) SUP_least mem_Collect_eq)
    hence "integral\<^sup>N 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 "(\\<^sup>+ x. ennreal (norm (f x)) \count_space S) \ ennreal B"
      using M_def \<open>normf \<equiv> \<lambda>x. ennreal (norm (f x))\<close> int_leq_B by auto
    ultimately have "ennreal (\\<^sub>ax\S. norm (f x)) \ ennreal B"
      by (simp add: nn_integral_conv_infsetsum)
    hence v2: "(\\<^sub>ax\S. norm (f x)) \ B"
      by (subst ennreal_le_iff[symmetric], simp add: assms \<open>B \<ge> 0\<close>)
    show ?thesis
      using v1 v2 by auto
  qed
  then show "f abs_summable_on S"
    by (metis abs_summable_on_finite assms empty_subsetI finite.emptyI sum_clauses(1))
qed

lemma infsetsum_nonneg_is_SUPREMUM_ennreal:
  fixes f :: "'a \ real"
  assumes summable: "f abs_summable_on A"
    and fnn: "\x. x\A \ 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 \<open>finite F\<close> 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: \<open>finite F\<close>)
      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: \<open>F \<subseteq> A\<close>)
      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 = \\<^sup>+ 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}. integral\<^sup>S (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 \ integral\<^sup>S (count_space A) ` {g. finite (g ` A) \ g \ fe}"
    then obtain g where xg: "x = integral\<^sup>S (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 = integral\<^sup>S (count_space A) g" by (fact xg)
      also have "\ = integral\<^sup>N (count_space A) g"
        by (simp add: fin_gA nn_integral_eq_simple_integral)
      also have "\ \ integral\<^sup>N (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 = (\t\g`A-{0}. {z\A. g z = t})"
      unfolding F_def by auto
    hence "finite F"
      unfolding F using fin_gA fin by auto
    have "x = integral\<^sup>N (count_space A) g"
      unfolding xg
      by (simp add: fin_gA nn_integral_eq_simple_integral)
    also have "\ = 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 "(\\<^sup>+ a. g a * (if a \ A then 1 else 0) \count_space UNIV)
           = (\<integral>\<^sup>+ a. g a * (if a \<in> {a \<in> A. g a \<noteq> 0} then 1 else 0) \<partial>count_space UNIV)"
        by presburger
      thus ?thesis unfolding F_def indicator_def
        using mult.right_neutral mult_zero_right nn_integral_cong
        by (simp add: of_bool_def)
    qed
    also have "\ = integral\<^sup>N (count_space F) g"
      by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
    also have "\ = sum g F"
      using \<open>finite F\<close> 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 \<open>finite F\<close> \<open>F\<subseteq>A\<close>
      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 \ (\x\x. ennreal (f x)) = ennreal (sum f x)"
        for x
        by (metis fnn subsetCE sum_ennreal)
      thus "sum fe x = ennreal (sum f x)"
        if "x \ {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. x\A \ 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) =
                   (\<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x))" for y
    proof -
      have "(\x. (\y. finite y \ y \ A \ x = ennreal (sum f y)) \ y = enn2ereal x) \
            (\<exists>X x. finite X \<and> X \<subseteq> A \<and> x = ennreal (sum f X) \<and> 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. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
      by simp
    ultimately show "max 0 (Sup {y. \x. (\xa. finite xa \ xa \ A \ x
                                       = ennreal (sum f xa)) \<and> y = enn2ereal x})
         = Sup {y. \<exists>x. finite x \<and> x \<subseteq> A \<and> y = ereal (sum f x)}"
      by linarith
  qed
  finally show ?thesis
    by simp
qed

text \<open>The following theorem relates \<^const>\<open>Infinite_Set_Sum.abs_summable_on\<close> with \<^const>\<open>Infinite_Sum.abs_summable_on\<close>.
  Note that while this theorem expresses an equivalence, the notion on the lhs is more general
  nonetheless because it applies to a wider range of types. (The rhs requires second-countable
  Banach spaces while the lhs is well-defined on arbitrary real vector spaces.)\<close>

lemma abs_summable_equivalent: \<open>Infinite_Sum.abs_summable_on f A \<longleftrightarrow> f abs_summable_on A\<close>
proof (rule iffI)
  define n where \<open>n x = norm (f x)\<close> for x
  assume \<open>n summable_on A\<close>
  then have \<open>sum n F \<le> infsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
    using that by (auto simp flip: infsum_finite simp: n_def[abs_def] intro!: infsum_mono_neutral)

  then show \<open>f abs_summable_on A\<close>
    by (auto intro!: abs_summable_finite_sumsI simp: n_def)
next
  define n where \<open>n x = norm (f x)\<close> for x
  assume \<open>f abs_summable_on A\<close>
  then have \<open>n abs_summable_on A\<close>
    by (simp add: \<open>f abs_summable_on A\<close> n_def)
  then have \<open>sum n F \<le> infsetsum n A\<close> if \<open>finite F\<close> and \<open>F\<subseteq>A\<close> for F
    using that by (auto simp flip: infsetsum_finite simp: n_def[abs_def] intro!: infsetsum_mono_neutral)
  then show \<open>n summable_on A\<close>
    apply (rule_tac 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 \<delta> where "\<delta> = \<epsilon>/2"
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.