src/HOL/Analysis/Infinite_Set_Sum.thy
author Manuel Eberl <eberlm@in.tum.de>
Tue Dec 12 10:01:14 2017 +0100 (18 months ago)
changeset 67167 88d1c9d86f48
parent 66568 52b5cf533fd6
child 67268 bdf25939a550
permissions -rw-r--r--
Moved analysis material from AFP
     1 (*  
     2   Title:    HOL/Analysis/Infinite_Set_Sum.thy
     3   Author:   Manuel Eberl, TU M√ľnchen
     4 
     5   A theory of sums over possible infinite sets. (Only works for absolute summability)
     6 *)
     7 section \<open>Sums over infinite sets\<close>
     8 theory Infinite_Set_Sum
     9   imports Set_Integral
    10 begin
    11 
    12 (* TODO Move *)
    13 lemma sets_eq_countable:
    14   assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
    15   shows   "sets M = Pow A"
    16 proof (intro equalityI subsetI)
    17   fix X assume "X \<in> Pow A"
    18   hence "(\<Union>x\<in>X. {x}) \<in> sets M"
    19     by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
    20   also have "(\<Union>x\<in>X. {x}) = X" by auto
    21   finally show "X \<in> sets M" .
    22 next
    23   fix X assume "X \<in> sets M"
    24   from sets.sets_into_space[OF this] and assms 
    25     show "X \<in> Pow A" by simp
    26 qed
    27 
    28 lemma measure_eqI_countable':
    29   assumes spaces: "space M = A" "space N = A" 
    30   assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
    31   assumes A: "countable A"
    32   assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
    33   shows "M = N"
    34 proof (rule measure_eqI_countable)
    35   show "sets M = Pow A"
    36     by (intro sets_eq_countable assms)
    37   show "sets N = Pow A"
    38     by (intro sets_eq_countable assms)
    39 qed fact+
    40 
    41 lemma PiE_singleton: 
    42   assumes "f \<in> extensional A"
    43   shows   "PiE A (\<lambda>x. {f x}) = {f}"
    44 proof -
    45   {
    46     fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
    47     hence "g x = f x" for x
    48       using assms by (cases "x \<in> A") (auto simp: extensional_def)
    49     hence "g = f" by (simp add: fun_eq_iff)
    50   }
    51   thus ?thesis using assms by (auto simp: extensional_def)
    52 qed
    53 
    54 lemma count_space_PiM_finite:
    55   fixes B :: "'a \<Rightarrow> 'b set"
    56   assumes "finite A" "\<And>i. countable (B i)"
    57   shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
    58 proof (rule measure_eqI_countable')
    59   show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
    60     by (simp add: space_PiM)
    61   show "space (count_space (PiE A B)) = PiE A B" by simp
    62 next
    63   fix f assume f: "f \<in> PiE A B"
    64   hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
    65     by (intro sets_PiM_I_finite assms) auto
    66   also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
    67     by (intro PiE_singleton) (auto simp: PiE_def)
    68   finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
    69 next
    70   interpret product_sigma_finite "(\<lambda>i. count_space (B i))"
    71     by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
    72   thm sigma_finite_measure_count_space
    73   fix f assume f: "f \<in> PiE A B"
    74   hence "{f} = PiE A (\<lambda>x. {f x})"
    75     by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
    76   also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
    77                (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
    78     using f assms by (subst emeasure_PiM) auto
    79   also have "\<dots> = (\<Prod>i\<in>A. 1)"
    80     by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
    81   also have "\<dots> = emeasure (count_space (PiE A B)) {f}"
    82     using f by (subst emeasure_count_space_finite) auto
    83   finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} =
    84                   emeasure (count_space (Pi\<^sub>E A B)) {f}" .
    85 qed (simp_all add: countable_PiE assms)
    86 
    87 
    88 
    89 definition abs_summable_on ::
    90     "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
    91     (infix "abs'_summable'_on" 50)
    92  where
    93    "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
    94 
    95 
    96 definition infsetsum ::
    97     "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
    98  where
    99    "infsetsum f A = lebesgue_integral (count_space A) f"
   100 
   101 syntax (ASCII)
   102   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   103   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
   104 syntax
   105   "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   106   ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
   107 translations \<comment> \<open>Beware of argument permutation!\<close>
   108   "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
   109 
   110 syntax (ASCII)
   111   "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   112   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
   113 syntax
   114   "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   115   ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
   116 translations \<comment> \<open>Beware of argument permutation!\<close>
   117   "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
   118 
   119 syntax (ASCII)
   120   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
   121   ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
   122 syntax
   123   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
   124   ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
   125 translations
   126   "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
   127 
   128 print_translation \<open>
   129 let
   130   fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   131         if x <> y then raise Match
   132         else
   133           let
   134             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   135             val t' = subst_bound (x', t);
   136             val P' = subst_bound (x', P);
   137           in
   138             Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   139           end
   140     | sum_tr' _ = raise Match;
   141 in [(@{const_syntax infsetsum}, K sum_tr')] end
   142 \<close>
   143 
   144 
   145 
   146 
   147 lemma restrict_count_space_subset:
   148   "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
   149   by (subst restrict_count_space) (simp_all add: Int_absorb2)
   150 
   151 lemma abs_summable_on_restrict:
   152   fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
   153   assumes "A \<subseteq> B"
   154   shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B"
   155 proof -
   156   have "count_space A = restrict_space (count_space B) A"
   157     by (rule restrict_count_space_subset [symmetric]) fact+
   158   also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
   159     by (subst integrable_restrict_space) auto
   160   finally show ?thesis 
   161     unfolding abs_summable_on_def .
   162 qed
   163 
   164 lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
   165   by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def)
   166 
   167 lemma abs_summable_on_altdef': 
   168   "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
   169   by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
   170 
   171 lemma abs_summable_on_norm_iff [simp]: 
   172   "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
   173   by (simp add: abs_summable_on_def integrable_norm_iff)
   174 
   175 lemma abs_summable_on_normI: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
   176   by simp
   177 
   178 lemma abs_summable_on_comparison_test:
   179   assumes "g abs_summable_on A"
   180   assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
   181   shows   "f abs_summable_on A"
   182   using assms Bochner_Integration.integrable_bound[of "count_space A" g f] 
   183   unfolding abs_summable_on_def by (auto simp: AE_count_space)  
   184 
   185 lemma abs_summable_on_comparison_test':
   186   assumes "g abs_summable_on A"
   187   assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> g x"
   188   shows   "f abs_summable_on A"
   189 proof (rule abs_summable_on_comparison_test[OF assms(1), of f])
   190   fix x assume "x \<in> A"
   191   with assms(2) have "norm (f x) \<le> g x" .
   192   also have "\<dots> \<le> norm (g x)" by simp
   193   finally show "norm (f x) \<le> norm (g x)" .
   194 qed
   195 
   196 lemma abs_summable_on_cong [cong]:
   197   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> (f abs_summable_on A) \<longleftrightarrow> (g abs_summable_on B)"
   198   unfolding abs_summable_on_def by (intro integrable_cong) auto
   199 
   200 lemma abs_summable_on_cong_neutral:
   201   assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
   202   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   203   assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   204   shows   "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
   205   unfolding abs_summable_on_altdef using assms
   206   by (intro Bochner_Integration.integrable_cong refl)
   207      (auto simp: indicator_def split: if_splits)
   208 
   209 lemma abs_summable_on_restrict':
   210   fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
   211   assumes "A \<subseteq> B"
   212   shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B"
   213   by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)
   214 
   215 lemma abs_summable_on_nat_iff:
   216   "f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
   217 proof -
   218   have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))"
   219     by (subst abs_summable_on_restrict'[of _ UNIV]) 
   220        (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
   221   also have "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> A then norm (f x) else 0)"
   222     by auto
   223   finally show ?thesis .
   224 qed
   225 
   226 lemma abs_summable_on_nat_iff':
   227   "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
   228   by (subst abs_summable_on_nat_iff) auto
   229 
   230 lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
   231   unfolding abs_summable_on_def by (rule integrable_count_space)
   232 
   233 lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
   234   by simp
   235 
   236 lemma abs_summable_on_subset:
   237   assumes "f abs_summable_on B" and "A \<subseteq> B"
   238   shows   "f abs_summable_on A"
   239   unfolding abs_summable_on_altdef
   240   by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)
   241 
   242 lemma abs_summable_on_union [intro]:
   243   assumes "f abs_summable_on A" and "f abs_summable_on B"
   244   shows   "f abs_summable_on (A \<union> B)"
   245   using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto
   246 
   247 lemma abs_summable_on_insert_iff [simp]:
   248   "f abs_summable_on insert x A \<longleftrightarrow> f abs_summable_on A"
   249 proof safe
   250   assume "f abs_summable_on insert x A"
   251   thus "f abs_summable_on A"
   252     by (rule abs_summable_on_subset) auto
   253 next
   254   assume "f abs_summable_on A"
   255   from abs_summable_on_union[OF this, of "{x}"]
   256     show "f abs_summable_on insert x A" by simp
   257 qed
   258 
   259 lemma abs_summable_sum: 
   260   assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
   261   shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
   262   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
   263 
   264 lemma abs_summable_Re: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Re (f x)) abs_summable_on A"
   265   by (simp add: abs_summable_on_def)
   266 
   267 lemma abs_summable_Im: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Im (f x)) abs_summable_on A"
   268   by (simp add: abs_summable_on_def)
   269 
   270 lemma abs_summable_on_finite_diff:
   271   assumes "f abs_summable_on A" "A \<subseteq> B" "finite (B - A)"
   272   shows   "f abs_summable_on B"
   273 proof -
   274   have "f abs_summable_on (A \<union> (B - A))"
   275     by (intro abs_summable_on_union assms abs_summable_on_finite)
   276   also from assms have "A \<union> (B - A) = B" by blast
   277   finally show ?thesis .
   278 qed
   279 
   280 lemma abs_summable_on_reindex_bij_betw:
   281   assumes "bij_betw g A B"
   282   shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
   283 proof -
   284   have *: "count_space B = distr (count_space A) (count_space B) g"
   285     by (rule distr_bij_count_space [symmetric]) fact
   286   show ?thesis unfolding abs_summable_on_def
   287     by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) 
   288        (insert assms, auto simp: bij_betw_def)
   289 qed
   290 
   291 lemma abs_summable_on_reindex:
   292   assumes "(\<lambda>x. f (g x)) abs_summable_on A"
   293   shows   "f abs_summable_on (g ` A)"
   294 proof -
   295   define g' where "g' = inv_into A g"
   296   from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
   297     by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
   298   also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
   299     by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
   300   also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)"
   301     by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
   302   finally show ?thesis .
   303 qed
   304 
   305 lemma abs_summable_on_reindex_iff: 
   306   "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
   307   by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
   308 
   309 lemma abs_summable_on_Sigma_project2:
   310   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   311   assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
   312   shows   "(\<lambda>y. f (x, y)) abs_summable_on (B x)"
   313 proof -
   314   from assms(2) have "f abs_summable_on (Sigma {x} B)"
   315     by (intro abs_summable_on_subset [OF assms(1)]) auto
   316   also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)"
   317     by (rule abs_summable_on_cong) auto
   318   finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
   319     by (rule abs_summable_on_reindex)
   320   also have "snd ` Sigma {x} B = B x"
   321     using assms by (auto simp: image_iff)
   322   finally show ?thesis .
   323 qed
   324 
   325 lemma abs_summable_on_Times_swap:
   326   "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A"
   327 proof -
   328   have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
   329     by (auto simp: bij_betw_def inj_on_def)
   330   show ?thesis
   331     by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
   332        (simp_all add: case_prod_unfold)
   333 qed
   334 
   335 lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A"
   336   by (simp add: abs_summable_on_def)
   337 
   338 lemma abs_summable_on_uminus [intro]:
   339   "f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A"
   340   unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)
   341 
   342 lemma abs_summable_on_add [intro]:
   343   assumes "f abs_summable_on A" and "g abs_summable_on A"
   344   shows   "(\<lambda>x. f x + g x) abs_summable_on A"
   345   using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)
   346 
   347 lemma abs_summable_on_diff [intro]:
   348   assumes "f abs_summable_on A" and "g abs_summable_on A"
   349   shows   "(\<lambda>x. f x - g x) abs_summable_on A"
   350   using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)
   351 
   352 lemma abs_summable_on_scaleR_left [intro]:
   353   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   354   shows   "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A"
   355   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)
   356 
   357 lemma abs_summable_on_scaleR_right [intro]:
   358   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   359   shows   "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A"
   360   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)
   361 
   362 lemma abs_summable_on_cmult_right [intro]:
   363   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   364   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   365   shows   "(\<lambda>x. c * f x) abs_summable_on A"
   366   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)
   367 
   368 lemma abs_summable_on_cmult_left [intro]:
   369   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   370   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   371   shows   "(\<lambda>x. f x * c) abs_summable_on A"
   372   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
   373 
   374 lemma abs_summable_on_prod_PiE:
   375   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
   376   assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   377   assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
   378   shows   "(\<lambda>g. \<Prod>x\<in>A. f x (g x)) abs_summable_on PiE A B"
   379 proof -
   380   define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
   381   from assms have [simp]: "countable (B' x)" for x
   382     by (auto simp: B'_def)
   383   then interpret product_sigma_finite "count_space \<circ> B'"
   384     unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
   385   from assms have "integrable (PiM A (count_space \<circ> B')) (\<lambda>g. \<Prod>x\<in>A. f x (g x))"
   386     by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
   387   also have "PiM A (count_space \<circ> B') = count_space (PiE A B')"
   388     unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
   389   also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
   390   finally show ?thesis by (simp add: abs_summable_on_def)
   391 qed
   392 
   393 
   394 
   395 lemma not_summable_infsetsum_eq:
   396   "\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0"
   397   by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)
   398 
   399 lemma infsetsum_altdef:
   400   "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
   401   by (subst integral_restrict_space [symmetric])
   402      (auto simp: restrict_count_space_subset infsetsum_def)
   403 
   404 lemma infsetsum_altdef':
   405   "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
   406   by (subst integral_restrict_space [symmetric])
   407      (auto simp: restrict_count_space_subset infsetsum_def)
   408 
   409 lemma nn_integral_conv_infsetsum:
   410   assumes "f abs_summable_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
   411   shows   "nn_integral (count_space A) f = ennreal (infsetsum f A)"
   412   using assms unfolding infsetsum_def abs_summable_on_def
   413   by (subst nn_integral_eq_integral) auto
   414 
   415 lemma infsetsum_conv_nn_integral:
   416   assumes "nn_integral (count_space A) f \<noteq> \<infinity>" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
   417   shows   "infsetsum f A = enn2real (nn_integral (count_space A) f)"
   418   unfolding infsetsum_def using assms
   419   by (subst integral_eq_nn_integral) auto
   420 
   421 lemma infsetsum_cong [cong]:
   422   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
   423   unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
   424 
   425 lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0"
   426   by (simp add: infsetsum_def)
   427 
   428 lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
   429   by simp
   430 
   431 lemma infsetsum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (0::real)) \<Longrightarrow> infsetsum f A \<ge> 0"
   432   unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
   433 
   434 lemma sum_infsetsum:
   435   assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
   436   shows   "(\<Sum>x\<in>A. \<Sum>\<^sub>ay\<in>B. f x y) = (\<Sum>\<^sub>ay\<in>B. \<Sum>x\<in>A. f x y)"
   437   using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
   438 
   439 lemma Re_infsetsum: "f abs_summable_on A \<Longrightarrow> Re (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Re (f x))"
   440   by (simp add: infsetsum_def abs_summable_on_def)
   441 
   442 lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
   443   by (simp add: infsetsum_def abs_summable_on_def)
   444 
   445 lemma infsetsum_of_real: 
   446   shows "infsetsum (\<lambda>x. of_real (f x) 
   447            :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
   448              of_real (infsetsum f A)"
   449   unfolding infsetsum_def
   450   by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
   451 
   452 lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
   453   by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
   454 
   455 lemma infsetsum_nat: 
   456   assumes "f abs_summable_on A"
   457   shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
   458 proof -
   459   from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
   460     unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto
   461   also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
   462     by auto
   463   finally show ?thesis .
   464 qed
   465 
   466 lemma infsetsum_nat': 
   467   assumes "f abs_summable_on UNIV"
   468   shows   "infsetsum f UNIV = (\<Sum>n. f n)"
   469   using assms by (subst infsetsum_nat) auto
   470 
   471 lemma sums_infsetsum_nat:
   472   assumes "f abs_summable_on A"
   473   shows   "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A"
   474 proof -
   475   from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
   476     by (simp add: abs_summable_on_nat_iff)
   477   also have "(\<lambda>n. if n \<in> A then norm (f n) else 0) = (\<lambda>n. norm (if n \<in> A then f n else 0))"
   478     by auto
   479   finally have "summable (\<lambda>n. if n \<in> A then f n else 0)"
   480     by (rule summable_norm_cancel)
   481   with assms show ?thesis
   482     by (auto simp: sums_iff infsetsum_nat)
   483 qed
   484 
   485 lemma sums_infsetsum_nat':
   486   assumes "f abs_summable_on UNIV"
   487   shows   "f sums infsetsum f UNIV"
   488   using sums_infsetsum_nat [OF assms] by simp
   489 
   490 lemma infsetsum_Un_disjoint:
   491   assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}"
   492   shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B"
   493   using assms unfolding infsetsum_altdef abs_summable_on_altdef
   494   by (subst set_integral_Un) auto
   495 
   496 lemma infsetsum_Diff:
   497   assumes "f abs_summable_on B" "A \<subseteq> B"
   498   shows   "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
   499 proof -
   500   have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A"
   501     using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
   502   also from assms(2) have "(B - A) \<union> A = B"
   503     by auto
   504   ultimately show ?thesis
   505     by (simp add: algebra_simps)
   506 qed
   507 
   508 lemma infsetsum_Un_Int:
   509   assumes "f abs_summable_on (A \<union> B)"
   510   shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)"
   511 proof -
   512   have "A \<union> B = A \<union> (B - A \<inter> B)"
   513     by auto
   514   also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)"
   515     by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
   516   also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)"
   517     by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
   518   finally show ?thesis 
   519     by (simp add: algebra_simps)
   520 qed
   521 
   522 lemma infsetsum_reindex_bij_betw:
   523   assumes "bij_betw g A B"
   524   shows   "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B"
   525 proof -
   526   have *: "count_space B = distr (count_space A) (count_space B) g"
   527     by (rule distr_bij_count_space [symmetric]) fact
   528   show ?thesis unfolding infsetsum_def
   529     by (subst *, subst integral_distr[of _ _ "count_space B"]) 
   530        (insert assms, auto simp: bij_betw_def)    
   531 qed
   532 
   533 lemma infsetsum_reindex:
   534   assumes "inj_on g A"
   535   shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
   536   by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
   537 
   538 lemma infsetsum_cong_neutral:
   539   assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
   540   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   541   assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   542   shows   "infsetsum f A = infsetsum g B"
   543   unfolding infsetsum_altdef using assms
   544   by (intro Bochner_Integration.integral_cong refl)
   545      (auto simp: indicator_def split: if_splits)
   546 
   547 lemma infsetsum_mono_neutral:
   548   fixes f g :: "'a \<Rightarrow> real"
   549   assumes "f abs_summable_on A" and "g abs_summable_on B"
   550   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   551   assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
   552   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
   553   shows   "infsetsum f A \<le> infsetsum g B"
   554   using assms unfolding infsetsum_altdef abs_summable_on_altdef
   555   by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)
   556 
   557 lemma infsetsum_mono_neutral_left:
   558   fixes f g :: "'a \<Rightarrow> real"
   559   assumes "f abs_summable_on A" and "g abs_summable_on B"
   560   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   561   assumes "A \<subseteq> B"
   562   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
   563   shows   "infsetsum f A \<le> infsetsum g B"
   564   using \<open>A \<subseteq> B\<close> by (intro infsetsum_mono_neutral assms) auto
   565 
   566 lemma infsetsum_mono_neutral_right:
   567   fixes f g :: "'a \<Rightarrow> real"
   568   assumes "f abs_summable_on A" and "g abs_summable_on B"
   569   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   570   assumes "B \<subseteq> A"
   571   assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
   572   shows   "infsetsum f A \<le> infsetsum g B"
   573   using \<open>B \<subseteq> A\<close> by (intro infsetsum_mono_neutral assms) auto
   574 
   575 lemma infsetsum_mono:
   576   fixes f g :: "'a \<Rightarrow> real"
   577   assumes "f abs_summable_on A" and "g abs_summable_on A"
   578   assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   579   shows   "infsetsum f A \<le> infsetsum g A"
   580   by (intro infsetsum_mono_neutral assms) auto
   581 
   582 lemma norm_infsetsum_bound:
   583   "norm (infsetsum f A) \<le> infsetsum (\<lambda>x. norm (f x)) A"
   584   unfolding abs_summable_on_def infsetsum_def
   585   by (rule Bochner_Integration.integral_norm_bound)
   586 
   587 lemma infsetsum_Sigma:
   588   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   589   assumes [simp]: "countable A" and "\<And>i. countable (B i)"
   590   assumes summable: "f abs_summable_on (Sigma A B)"
   591   shows   "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
   592 proof -
   593   define B' where "B' = (\<Union>i\<in>A. B i)"
   594   have [simp]: "countable B'" 
   595     unfolding B'_def by (intro countable_UN assms)
   596   interpret pair_sigma_finite "count_space A" "count_space B'"
   597     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
   598 
   599   have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
   600     using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
   601   also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))"
   602     by (intro Bochner_Integration.integrable_cong)
   603        (auto simp: pair_measure_countable indicator_def split: if_splits)
   604   finally have integrable: \<dots> .
   605   
   606   have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
   607           (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
   608     unfolding infsetsum_def by simp
   609   also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
   610     by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl)
   611        (auto simp: B'_def)
   612   also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
   613     by (subst integral_fst [OF integrable]) auto
   614   also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
   615     by (intro Bochner_Integration.integral_cong)
   616        (auto simp: pair_measure_countable indicator_def split: if_splits)
   617   also have "\<dots> = infsetsum f (Sigma A B)"
   618     by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
   619   finally show ?thesis ..
   620 qed
   621 
   622 lemma infsetsum_Sigma':
   623   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   624   assumes [simp]: "countable A" and "\<And>i. countable (B i)"
   625   assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (Sigma A B)"
   626   shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) A = infsetsum (\<lambda>(x,y). f x y) (Sigma A B)"
   627   using assms by (subst infsetsum_Sigma) auto
   628 
   629 lemma infsetsum_Times:
   630   fixes A :: "'a set" and B :: "'b set"
   631   assumes [simp]: "countable A" and "countable B"
   632   assumes summable: "f abs_summable_on (A \<times> B)"
   633   shows   "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A"
   634   using assms by (subst infsetsum_Sigma) auto
   635 
   636 lemma infsetsum_Times':
   637   fixes A :: "'a set" and B :: "'b set"
   638   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
   639   assumes [simp]: "countable A" and [simp]: "countable B"
   640   assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)"
   641   shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
   642   using assms by (subst infsetsum_Times) auto
   643 
   644 lemma infsetsum_swap:
   645   fixes A :: "'a set" and B :: "'b set"
   646   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
   647   assumes [simp]: "countable A" and [simp]: "countable B"
   648   assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B"
   649   shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
   650 proof -
   651   from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A"
   652     by (subst abs_summable_on_Times_swap) auto
   653   have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)"
   654     by (auto simp: bij_betw_def inj_on_def)
   655   have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
   656     using summable by (subst infsetsum_Times) auto
   657   also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)"
   658     by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric])
   659        (simp_all add: case_prod_unfold)
   660   also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
   661     using summable' by (subst infsetsum_Times) auto
   662   finally show ?thesis .
   663 qed
   664 
   665 lemma abs_summable_on_Sigma_iff:
   666   assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   667   shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
   668              (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
   669              ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
   670 proof safe
   671   define B' where "B' = (\<Union>x\<in>A. B x)"
   672   have [simp]: "countable B'" 
   673     unfolding B'_def using assms by auto
   674   interpret pair_sigma_finite "count_space A" "count_space B'"
   675     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
   676 
   677   {
   678     assume *: "f abs_summable_on Sigma A B"
   679     thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
   680       using that by (rule abs_summable_on_Sigma_project2)
   681 
   682     have "set_integrable (count_space (A \<times> B')) (Sigma A B) (\<lambda>z. norm (f z))"
   683       using abs_summable_on_normI[OF *]
   684       by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
   685     also have "count_space (A \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
   686       by (simp add: pair_measure_countable)
   687     finally have "integrable (count_space A) 
   688                     (\<lambda>x. lebesgue_integral (count_space B') 
   689                       (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
   690       by (rule integrable_fst')
   691     also have "?this \<longleftrightarrow> integrable (count_space A)
   692                     (\<lambda>x. lebesgue_integral (count_space B') 
   693                       (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
   694       by (intro integrable_cong refl) (simp_all add: indicator_def)
   695     also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
   696       by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
   697     also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
   698       by (simp add: abs_summable_on_def)
   699     finally show \<dots> .
   700   }
   701 
   702   {
   703     assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
   704     assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
   705     also have "?this \<longleftrightarrow> (\<lambda>x. \<integral>y\<in>B x. norm (f (x, y)) \<partial>count_space B') abs_summable_on A"
   706       by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
   707     also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
   708                         abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
   709       by (intro abs_summable_on_cong) (auto simp: indicator_def)
   710     also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
   711       by (simp add: abs_summable_on_def)
   712     finally have **: \<dots> .
   713 
   714     have "integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
   715     proof (rule Fubini_integrable, goal_cases)
   716       case 3
   717       {
   718         fix x assume x: "x \<in> A"
   719         with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
   720           by blast
   721         also have "?this \<longleftrightarrow> integrable (count_space B') 
   722                       (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
   723           using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
   724         also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
   725                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
   726           using x by (auto simp: indicator_def)
   727         finally have "integrable (count_space B')
   728                         (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" .
   729       }
   730       thus ?case by (auto simp: AE_count_space)
   731     qed (insert **, auto simp: pair_measure_countable)
   732     also have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
   733       by (simp add: pair_measure_countable)
   734     also have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
   735                  f abs_summable_on Sigma A B"
   736       by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
   737     finally show \<dots> .
   738   }
   739 qed
   740 
   741 lemma abs_summable_on_Sigma_project1:
   742   assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
   743   assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   744   shows   "(\<lambda>x. infsetsum (\<lambda>y. norm (f x y)) (B x)) abs_summable_on A"
   745   using assms by (subst (asm) abs_summable_on_Sigma_iff) auto
   746 
   747 lemma abs_summable_on_Sigma_project1':
   748   assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
   749   assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   750   shows   "(\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) abs_summable_on A"
   751   by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
   752         norm_infsetsum_bound)
   753 
   754 lemma infsetsum_prod_PiE:
   755   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
   756   assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   757   assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
   758   shows   "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
   759 proof -
   760   define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
   761   from assms have [simp]: "countable (B' x)" for x
   762     by (auto simp: B'_def)
   763   then interpret product_sigma_finite "count_space \<circ> B'"
   764     unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
   765   have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) =
   766           (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))"
   767     by (simp add: infsetsum_def)
   768   also have "PiE A B = PiE A B'"
   769     by (intro PiE_cong) (simp_all add: B'_def)
   770   hence "count_space (PiE A B) = count_space (PiE A B')"
   771     by simp
   772   also have "\<dots> = PiM A (count_space \<circ> B')"
   773     unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
   774   also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))"
   775     by (subst product_integral_prod) 
   776        (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
   777   also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
   778     by (intro prod.cong refl) (simp_all add: B'_def)
   779   finally show ?thesis .
   780 qed
   781 
   782 lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A"
   783   unfolding infsetsum_def abs_summable_on_def 
   784   by (rule Bochner_Integration.integral_minus)
   785 
   786 lemma infsetsum_add:
   787   assumes "f abs_summable_on A" and "g abs_summable_on A"
   788   shows   "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A"
   789   using assms unfolding infsetsum_def abs_summable_on_def 
   790   by (rule Bochner_Integration.integral_add)
   791 
   792 lemma infsetsum_diff:
   793   assumes "f abs_summable_on A" and "g abs_summable_on A"
   794   shows   "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A"
   795   using assms unfolding infsetsum_def abs_summable_on_def 
   796   by (rule Bochner_Integration.integral_diff)
   797 
   798 lemma infsetsum_scaleR_left:
   799   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   800   shows   "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c"
   801   using assms unfolding infsetsum_def abs_summable_on_def 
   802   by (rule Bochner_Integration.integral_scaleR_left)
   803 
   804 lemma infsetsum_scaleR_right:
   805   "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A"
   806   unfolding infsetsum_def abs_summable_on_def 
   807   by (subst Bochner_Integration.integral_scaleR_right) auto
   808 
   809 lemma infsetsum_cmult_left:
   810   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   811   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   812   shows   "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c"
   813   using assms unfolding infsetsum_def abs_summable_on_def 
   814   by (rule Bochner_Integration.integral_mult_left)
   815 
   816 lemma infsetsum_cmult_right:
   817   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   818   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   819   shows   "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A"
   820   using assms unfolding infsetsum_def abs_summable_on_def 
   821   by (rule Bochner_Integration.integral_mult_right)
   822 
   823 lemma infsetsum_cdiv:
   824   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
   825   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   826   shows   "infsetsum (\<lambda>x. f x / c) A = infsetsum f A / c"
   827   using assms unfolding infsetsum_def abs_summable_on_def by auto
   828 
   829 
   830 (* TODO Generalise with bounded_linear *)
   831 
   832 lemma
   833   fixes f :: "'a \<Rightarrow> 'c :: {banach, real_normed_field, second_countable_topology}"
   834   assumes [simp]: "countable A" and [simp]: "countable B"
   835   assumes "f abs_summable_on A" and "g abs_summable_on B"
   836   shows   abs_summable_on_product: "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
   837     and   infsetsum_product: "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) =
   838                                 infsetsum f A * infsetsum g B"
   839 proof -
   840   from assms show "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
   841     by (subst abs_summable_on_Sigma_iff)
   842        (auto intro!: abs_summable_on_cmult_right simp: norm_mult infsetsum_cmult_right)
   843   with assms show "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) = infsetsum f A * infsetsum g B"
   844     by (subst infsetsum_Sigma)
   845        (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
   846 qed
   847 
   848 end