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