src/HOL/Analysis/Infinite_Set_Sum.thy
 author Manuel Eberl 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
```