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