src/HOL/Probability/Finite_Product_Measure.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 43920 cedb5cb948fd child 44890 22f665a2e91c permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 (*  Title:      HOL/Probability/Finite_Product_Measure.thy
```
```     2     Author:     Johannes Hölzl, TU München
```
```     3 *)
```
```     4
```
```     5 header {*Finite product measures*}
```
```     6
```
```     7 theory Finite_Product_Measure
```
```     8 imports Binary_Product_Measure
```
```     9 begin
```
```    10
```
```    11 lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
```
```    12   unfolding Pi_def by auto
```
```    13
```
```    14 abbreviation
```
```    15   "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
```
```    16
```
```    17 syntax
```
```    18   "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
```
```    19
```
```    20 syntax (xsymbols)
```
```    21   "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
```
```    22
```
```    23 syntax (HTML output)
```
```    24   "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
```
```    25
```
```    26 translations
```
```    27   "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
```
```    28
```
```    29 abbreviation
```
```    30   funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
```
```    31     (infixr "->\<^isub>E" 60) where
```
```    32   "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
```
```    33
```
```    34 notation (xsymbols)
```
```    35   funcset_extensional  (infixr "\<rightarrow>\<^isub>E" 60)
```
```    36
```
```    37 lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
```
```    38   by safe (auto simp add: extensional_def fun_eq_iff)
```
```    39
```
```    40 lemma extensional_insert[intro, simp]:
```
```    41   assumes "a \<in> extensional (insert i I)"
```
```    42   shows "a(i := b) \<in> extensional (insert i I)"
```
```    43   using assms unfolding extensional_def by auto
```
```    44
```
```    45 lemma extensional_Int[simp]:
```
```    46   "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
```
```    47   unfolding extensional_def by auto
```
```    48
```
```    49 definition
```
```    50   "merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
```
```    51
```
```    52 lemma merge_apply[simp]:
```
```    53   "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
```
```    54   "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
```
```    55   "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
```
```    56   "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
```
```    57   "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined"
```
```    58   unfolding merge_def by auto
```
```    59
```
```    60 lemma merge_commute:
```
```    61   "I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x"
```
```    62   by (auto simp: merge_def intro!: ext)
```
```    63
```
```    64 lemma Pi_cancel_merge_range[simp]:
```
```    65   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
```
```    66   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
```
```    67   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
```
```    68   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
```
```    69   by (auto simp: Pi_def)
```
```    70
```
```    71 lemma Pi_cancel_merge[simp]:
```
```    72   "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
```
```    73   "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
```
```    74   "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
```
```    75   "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
```
```    76   by (auto simp: Pi_def)
```
```    77
```
```    78 lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)"
```
```    79   by (auto simp: extensional_def)
```
```    80
```
```    81 lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
```
```    82   by (auto simp: restrict_def Pi_def)
```
```    83
```
```    84 lemma restrict_merge[simp]:
```
```    85   "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
```
```    86   "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
```
```    87   "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
```
```    88   "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
```
```    89   by (auto simp: restrict_def intro!: ext)
```
```    90
```
```    91 lemma extensional_insert_undefined[intro, simp]:
```
```    92   assumes "a \<in> extensional (insert i I)"
```
```    93   shows "a(i := undefined) \<in> extensional I"
```
```    94   using assms unfolding extensional_def by auto
```
```    95
```
```    96 lemma extensional_insert_cancel[intro, simp]:
```
```    97   assumes "a \<in> extensional I"
```
```    98   shows "a \<in> extensional (insert i I)"
```
```    99   using assms unfolding extensional_def by auto
```
```   100
```
```   101 lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
```
```   102   unfolding merge_def by (auto simp: fun_eq_iff)
```
```   103
```
```   104 lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
```
```   105   by auto
```
```   106
```
```   107 lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
```
```   108   by auto
```
```   109
```
```   110 lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
```
```   111   by (auto simp: Pi_def)
```
```   112
```
```   113 lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
```
```   114   by (auto simp: Pi_def)
```
```   115
```
```   116 lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
```
```   117   by (auto simp: Pi_def)
```
```   118
```
```   119 lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
```
```   120   by (auto simp: Pi_def)
```
```   121
```
```   122 lemma restrict_vimage:
```
```   123   assumes "I \<inter> J = {}"
```
```   124   shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
```
```   125   using assms by (auto simp: restrict_Pi_cancel)
```
```   126
```
```   127 lemma merge_vimage:
```
```   128   assumes "I \<inter> J = {}"
```
```   129   shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
```
```   130   using assms by (auto simp: restrict_Pi_cancel)
```
```   131
```
```   132 lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
```
```   133   by (auto simp: restrict_def intro!: ext)
```
```   134
```
```   135 lemma merge_restrict[simp]:
```
```   136   "merge I (restrict x I) J y = merge I x J y"
```
```   137   "merge I x J (restrict y J) = merge I x J y"
```
```   138   unfolding merge_def by (auto intro!: ext)
```
```   139
```
```   140 lemma merge_x_x_eq_restrict[simp]:
```
```   141   "merge I x J x = restrict x (I \<union> J)"
```
```   142   unfolding merge_def by (auto intro!: ext)
```
```   143
```
```   144 lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
```
```   145   apply auto
```
```   146   apply (drule_tac x=x in Pi_mem)
```
```   147   apply (simp_all split: split_if_asm)
```
```   148   apply (drule_tac x=i in Pi_mem)
```
```   149   apply (auto dest!: Pi_mem)
```
```   150   done
```
```   151
```
```   152 lemma Pi_UN:
```
```   153   fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
```
```   154   assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
```
```   155   shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
```
```   156 proof (intro set_eqI iffI)
```
```   157   fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
```
```   158   then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
```
```   159   from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
```
```   160   obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
```
```   161     using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
```
```   162   have "f \<in> Pi I (A k)"
```
```   163   proof (intro Pi_I)
```
```   164     fix i assume "i \<in> I"
```
```   165     from mono[OF this, of "n i" k] k[OF this] n[OF this]
```
```   166     show "f i \<in> A k i" by auto
```
```   167   qed
```
```   168   then show "f \<in> (\<Union>n. Pi I (A n))" by auto
```
```   169 qed auto
```
```   170
```
```   171 lemma PiE_cong:
```
```   172   assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
```
```   173   shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
```
```   174   using assms by (auto intro!: Pi_cong)
```
```   175
```
```   176 lemma restrict_upd[simp]:
```
```   177   "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
```
```   178   by (auto simp: fun_eq_iff)
```
```   179
```
```   180 lemma Pi_eq_subset:
```
```   181   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
```
```   182   assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
```
```   183   shows "F i \<subseteq> F' i"
```
```   184 proof
```
```   185   fix x assume "x \<in> F i"
```
```   186   with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
```
```   187   from choice[OF this] guess f .. note f = this
```
```   188   then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
```
```   189   then have "f \<in> Pi\<^isub>E I F'" using assms by simp
```
```   190   then show "x \<in> F' i" using f `i \<in> I` by auto
```
```   191 qed
```
```   192
```
```   193 lemma Pi_eq_iff_not_empty:
```
```   194   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
```
```   195   shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
```
```   196 proof (intro iffI ballI)
```
```   197   fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
```
```   198   show "F i = F' i"
```
```   199     using Pi_eq_subset[of I F F', OF ne eq i]
```
```   200     using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
```
```   201     by auto
```
```   202 qed auto
```
```   203
```
```   204 lemma Pi_eq_empty_iff:
```
```   205   "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
```
```   206 proof
```
```   207   assume "Pi\<^isub>E I F = {}"
```
```   208   show "\<exists>i\<in>I. F i = {}"
```
```   209   proof (rule ccontr)
```
```   210     assume "\<not> ?thesis"
```
```   211     then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
```
```   212     from choice[OF this] guess f ..
```
```   213     then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
```
```   214     with `Pi\<^isub>E I F = {}` show False by auto
```
```   215   qed
```
```   216 qed auto
```
```   217
```
```   218 lemma Pi_eq_iff:
```
```   219   "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
```
```   220 proof (intro iffI disjCI)
```
```   221   assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
```
```   222   assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
```
```   223   then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
```
```   224     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
```
```   225   with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
```
```   226 next
```
```   227   assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
```
```   228   then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
```
```   229     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
```
```   230 qed
```
```   231
```
```   232 section "Finite product spaces"
```
```   233
```
```   234 section "Products"
```
```   235
```
```   236 locale product_sigma_algebra =
```
```   237   fixes M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme"
```
```   238   assumes sigma_algebras: "\<And>i. sigma_algebra (M i)"
```
```   239
```
```   240 locale finite_product_sigma_algebra = product_sigma_algebra M
```
```   241   for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
```
```   242   fixes I :: "'i set"
```
```   243   assumes finite_index: "finite I"
```
```   244
```
```   245 definition
```
```   246   "product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)),
```
```   247     sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)),
```
```   248     measure = \<lambda>A. (\<Prod>i\<in>I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \<rparr>"
```
```   249
```
```   250 definition product_algebra_def:
```
```   251   "Pi\<^isub>M I M = sigma (product_algebra_generator I M)
```
```   252     \<lparr> measure := (SOME \<mu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<mu> \<rparr>) \<and>
```
```   253       (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))))\<rparr>"
```
```   254
```
```   255 syntax
```
```   256   "_PiM"  :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
```
```   257               ('i => 'a, 'b) measure_space_scheme"  ("(3PIM _:_./ _)" 10)
```
```   258
```
```   259 syntax (xsymbols)
```
```   260   "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
```
```   261              ('i => 'a, 'b) measure_space_scheme"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"   10)
```
```   262
```
```   263 syntax (HTML output)
```
```   264   "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
```
```   265              ('i => 'a, 'b) measure_space_scheme"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"   10)
```
```   266
```
```   267 translations
```
```   268   "PIM x:I. M" == "CONST Pi\<^isub>M I (%x. M)"
```
```   269
```
```   270 abbreviation (in finite_product_sigma_algebra) "G \<equiv> product_algebra_generator I M"
```
```   271 abbreviation (in finite_product_sigma_algebra) "P \<equiv> Pi\<^isub>M I M"
```
```   272
```
```   273 sublocale product_sigma_algebra \<subseteq> M: sigma_algebra "M i" for i by (rule sigma_algebras)
```
```   274
```
```   275 lemma sigma_into_space:
```
```   276   assumes "sets M \<subseteq> Pow (space M)"
```
```   277   shows "sets (sigma M) \<subseteq> Pow (space M)"
```
```   278   using sigma_sets_into_sp[OF assms] unfolding sigma_def by auto
```
```   279
```
```   280 lemma (in product_sigma_algebra) product_algebra_generator_into_space:
```
```   281   "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
```
```   282   using M.sets_into_space unfolding product_algebra_generator_def
```
```   283   by auto blast
```
```   284
```
```   285 lemma (in product_sigma_algebra) product_algebra_into_space:
```
```   286   "sets (Pi\<^isub>M I M) \<subseteq> Pow (space (Pi\<^isub>M I M))"
```
```   287   using product_algebra_generator_into_space
```
```   288   by (auto intro!: sigma_into_space simp add: product_algebra_def)
```
```   289
```
```   290 lemma (in product_sigma_algebra) sigma_algebra_product_algebra: "sigma_algebra (Pi\<^isub>M I M)"
```
```   291   using product_algebra_generator_into_space unfolding product_algebra_def
```
```   292   by (rule sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) simp_all
```
```   293
```
```   294 sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
```
```   295   using sigma_algebra_product_algebra .
```
```   296
```
```   297 lemma product_algebraE:
```
```   298   assumes "A \<in> sets (product_algebra_generator I M)"
```
```   299   obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
```
```   300   using assms unfolding product_algebra_generator_def by auto
```
```   301
```
```   302 lemma product_algebra_generatorI[intro]:
```
```   303   assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
```
```   304   shows "Pi\<^isub>E I E \<in> sets (product_algebra_generator I M)"
```
```   305   using assms unfolding product_algebra_generator_def by auto
```
```   306
```
```   307 lemma space_product_algebra_generator[simp]:
```
```   308   "space (product_algebra_generator I M) = Pi\<^isub>E I (\<lambda>i. space (M i))"
```
```   309   unfolding product_algebra_generator_def by simp
```
```   310
```
```   311 lemma space_product_algebra[simp]:
```
```   312   "space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
```
```   313   unfolding product_algebra_def product_algebra_generator_def by simp
```
```   314
```
```   315 lemma sets_product_algebra:
```
```   316   "sets (Pi\<^isub>M I M) = sets (sigma (product_algebra_generator I M))"
```
```   317   unfolding product_algebra_def sigma_def by simp
```
```   318
```
```   319 lemma product_algebra_generator_sets_into_space:
```
```   320   assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
```
```   321   shows "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
```
```   322   using assms by (auto simp: product_algebra_generator_def) blast
```
```   323
```
```   324 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
```
```   325   "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
```
```   326   by (auto simp: sets_product_algebra)
```
```   327
```
```   328 lemma Int_stable_product_algebra_generator:
```
```   329   "(\<And>i. i \<in> I \<Longrightarrow> Int_stable (M i)) \<Longrightarrow> Int_stable (product_algebra_generator I M)"
```
```   330   by (auto simp add: product_algebra_generator_def Int_stable_def PiE_Int Pi_iff)
```
```   331
```
```   332 section "Generating set generates also product algebra"
```
```   333
```
```   334 lemma sigma_product_algebra_sigma_eq:
```
```   335   assumes "finite I"
```
```   336   assumes mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
```
```   337   assumes union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (E i)"
```
```   338   assumes sets_into: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> sets (E i)"
```
```   339   and E: "\<And>i. sets (E i) \<subseteq> Pow (space (E i))"
```
```   340   shows "sets (\<Pi>\<^isub>M i\<in>I. sigma (E i)) = sets (\<Pi>\<^isub>M i\<in>I. E i)"
```
```   341     (is "sets ?S = sets ?E")
```
```   342 proof cases
```
```   343   assume "I = {}" then show ?thesis
```
```   344     by (simp add: product_algebra_def product_algebra_generator_def)
```
```   345 next
```
```   346   assume "I \<noteq> {}"
```
```   347   interpret E: sigma_algebra "sigma (E i)" for i
```
```   348     using E by (rule sigma_algebra_sigma)
```
```   349   have into_space[intro]: "\<And>i x A. A \<in> sets (E i) \<Longrightarrow> x i \<in> A \<Longrightarrow> x i \<in> space (E i)"
```
```   350     using E by auto
```
```   351   interpret G: sigma_algebra ?E
```
```   352     unfolding product_algebra_def product_algebra_generator_def using E
```
```   353     by (intro sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) (auto dest: Pi_mem)
```
```   354   { fix A i assume "i \<in> I" and A: "A \<in> sets (E i)"
```
```   355     then have "(\<lambda>x. x i) -` A \<inter> space ?E = (\<Pi>\<^isub>E j\<in>I. if j = i then A else \<Union>n. S j n) \<inter> space ?E"
```
```   356       using mono union unfolding incseq_Suc_iff space_product_algebra
```
```   357       by (auto dest: Pi_mem)
```
```   358     also have "\<dots> = (\<Union>n. (\<Pi>\<^isub>E j\<in>I. if j = i then A else S j n))"
```
```   359       unfolding space_product_algebra
```
```   360       apply simp
```
```   361       apply (subst Pi_UN[OF `finite I`])
```
```   362       using mono[THEN incseqD] apply simp
```
```   363       apply (simp add: PiE_Int)
```
```   364       apply (intro PiE_cong)
```
```   365       using A sets_into by (auto intro!: into_space)
```
```   366     also have "\<dots> \<in> sets ?E"
```
```   367       using sets_into `A \<in> sets (E i)`
```
```   368       unfolding sets_product_algebra sets_sigma
```
```   369       by (intro sigma_sets.Union)
```
```   370          (auto simp: image_subset_iff intro!: sigma_sets.Basic)
```
```   371     finally have "(\<lambda>x. x i) -` A \<inter> space ?E \<in> sets ?E" . }
```
```   372   then have proj:
```
```   373     "\<And>i. i\<in>I \<Longrightarrow> (\<lambda>x. x i) \<in> measurable ?E (sigma (E i))"
```
```   374     using E by (subst G.measurable_iff_sigma)
```
```   375                (auto simp: sets_product_algebra sets_sigma)
```
```   376   { fix A assume A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (sigma (E i))"
```
```   377     with proj have basic: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) -` (A i) \<inter> space ?E \<in> sets ?E"
```
```   378       unfolding measurable_def by simp
```
```   379     have "Pi\<^isub>E I A = (\<Inter>i\<in>I. (\<lambda>x. x i) -` (A i) \<inter> space ?E)"
```
```   380       using A E.sets_into_space `I \<noteq> {}` unfolding product_algebra_def by auto blast
```
```   381     then have "Pi\<^isub>E I A \<in> sets ?E"
```
```   382       using G.finite_INT[OF `finite I` `I \<noteq> {}` basic, of "\<lambda>i. i"] by simp }
```
```   383   then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\<lambda>i. sigma (E i)))) \<subseteq> sets ?E"
```
```   384     by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def)
```
```   385   then have subset: "sets ?S \<subseteq> sets ?E"
```
```   386     by (simp add: sets_sigma sets_product_algebra)
```
```   387   show "sets ?S = sets ?E"
```
```   388   proof (intro set_eqI iffI)
```
```   389     fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
```
```   390       unfolding sets_sigma sets_product_algebra
```
```   391     proof induct
```
```   392       case (Basic A) then show ?case
```
```   393         by (auto simp: sets_sigma product_algebra_generator_def intro: sigma_sets.Basic)
```
```   394     qed (auto intro: sigma_sets.intros simp: product_algebra_generator_def)
```
```   395   next
```
```   396     fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
```
```   397   qed
```
```   398 qed
```
```   399
```
```   400 lemma product_algebraI[intro]:
```
```   401     "E \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> Pi\<^isub>E I E \<in> sets (Pi\<^isub>M I M)"
```
```   402   using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI)
```
```   403
```
```   404 lemma (in product_sigma_algebra) measurable_component_update:
```
```   405   assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
```
```   406   shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
```
```   407   unfolding product_algebra_def apply simp
```
```   408 proof (intro measurable_sigma)
```
```   409   let ?G = "product_algebra_generator (insert i I) M"
```
```   410   show "sets ?G \<subseteq> Pow (space ?G)" using product_algebra_generator_into_space .
```
```   411   show "?f \<in> space (M i) \<rightarrow> space ?G"
```
```   412     using M.sets_into_space assms by auto
```
```   413   fix A assume "A \<in> sets ?G"
```
```   414   from product_algebraE[OF this] guess E . note E = this
```
```   415   then have "?f -` A \<inter> space (M i) = E i \<or> ?f -` A \<inter> space (M i) = {}"
```
```   416     using M.sets_into_space assms by auto
```
```   417   then show "?f -` A \<inter> space (M i) \<in> sets (M i)"
```
```   418     using E by (auto intro!: product_algebraI)
```
```   419 qed
```
```   420
```
```   421 lemma (in product_sigma_algebra) measurable_add_dim:
```
```   422   assumes "i \<notin> I"
```
```   423   shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
```
```   424 proof -
```
```   425   let ?f = "(\<lambda>(f, y). f(i := y))" and ?G = "product_algebra_generator (insert i I) M"
```
```   426   interpret Ii: pair_sigma_algebra "Pi\<^isub>M I M" "M i"
```
```   427     unfolding pair_sigma_algebra_def
```
```   428     by (intro sigma_algebra_product_algebra sigma_algebras conjI)
```
```   429   have "?f \<in> measurable Ii.P (sigma ?G)"
```
```   430   proof (rule Ii.measurable_sigma)
```
```   431     show "sets ?G \<subseteq> Pow (space ?G)"
```
```   432       using product_algebra_generator_into_space .
```
```   433     show "?f \<in> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<rightarrow> space ?G"
```
```   434       by (auto simp: space_pair_measure)
```
```   435   next
```
```   436     fix A assume "A \<in> sets ?G"
```
```   437     then obtain F where "A = Pi\<^isub>E (insert i I) F"
```
```   438       and F: "\<And>j. j \<in> I \<Longrightarrow> F j \<in> sets (M j)" "F i \<in> sets (M i)"
```
```   439       by (auto elim!: product_algebraE)
```
```   440     then have "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = Pi\<^isub>E I F \<times> (F i)"
```
```   441       using sets_into_space `i \<notin> I`
```
```   442       by (auto simp add: space_pair_measure) blast+
```
```   443     then show "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M M i)"
```
```   444       using F by (auto intro!: pair_measureI)
```
```   445   qed
```
```   446   then show ?thesis
```
```   447     by (simp add: product_algebra_def)
```
```   448 qed
```
```   449
```
```   450 lemma (in product_sigma_algebra) measurable_merge:
```
```   451   assumes [simp]: "I \<inter> J = {}"
```
```   452   shows "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
```
```   453 proof -
```
```   454   let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M"
```
```   455   interpret P: sigma_algebra "?I \<Otimes>\<^isub>M ?J"
```
```   456     by (intro sigma_algebra_pair_measure product_algebra_into_space)
```
```   457   let ?f = "\<lambda>(x, y). merge I x J y"
```
```   458   let ?G = "product_algebra_generator (I \<union> J) M"
```
```   459   have "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (sigma ?G)"
```
```   460   proof (rule P.measurable_sigma)
```
```   461     fix A assume "A \<in> sets ?G"
```
```   462     from product_algebraE[OF this]
```
```   463     obtain E where E: "A = Pi\<^isub>E (I \<union> J) E" "E \<in> (\<Pi> i\<in>I \<union> J. sets (M i))" .
```
```   464     then have *: "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) = Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
```
```   465       using sets_into_space `I \<inter> J = {}`
```
```   466       by (auto simp add: space_pair_measure) fast+
```
```   467     then show "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) \<in> sets (?I \<Otimes>\<^isub>M ?J)"
```
```   468       using E unfolding * by (auto intro!: pair_measureI in_sigma product_algebra_generatorI
```
```   469         simp: product_algebra_def)
```
```   470   qed (insert product_algebra_generator_into_space, auto simp: space_pair_measure)
```
```   471   then show "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (Pi\<^isub>M (I \<union> J) M)"
```
```   472     unfolding product_algebra_def[of "I \<union> J"] by simp
```
```   473 qed
```
```   474
```
```   475 lemma (in product_sigma_algebra) measurable_component_singleton:
```
```   476   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
```
```   477 proof (unfold measurable_def, intro CollectI conjI ballI)
```
```   478   fix A assume "A \<in> sets (M i)"
```
```   479   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
```
```   480     using M.sets_into_space `i \<in> I` by (fastsimp dest: Pi_mem split: split_if_asm)
```
```   481   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
```
```   482     using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
```
```   483 qed (insert `i \<in> I`, auto)
```
```   484
```
```   485 lemma (in sigma_algebra) measurable_restrict:
```
```   486   assumes I: "finite I"
```
```   487   assumes "\<And>i. i \<in> I \<Longrightarrow> sets (N i) \<subseteq> Pow (space (N i))"
```
```   488   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (N i)"
```
```   489   shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
```
```   490   unfolding product_algebra_def
```
```   491 proof (simp, rule measurable_sigma)
```
```   492   show "sets (product_algebra_generator I N) \<subseteq> Pow (space (product_algebra_generator I N))"
```
```   493     by (rule product_algebra_generator_sets_into_space) fact
```
```   494   show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space M \<rightarrow> space (product_algebra_generator I N)"
```
```   495     using X by (auto simp: measurable_def)
```
```   496   fix E assume "E \<in> sets (product_algebra_generator I N)"
```
```   497   then obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (N i)"
```
```   498     by (auto simp: product_algebra_generator_def)
```
```   499   then have "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M = (\<Inter>i\<in>I. X i -` F i \<inter> space M) \<inter> space M"
```
```   500     by (auto simp: Pi_iff)
```
```   501   also have "\<dots> \<in> sets M"
```
```   502   proof cases
```
```   503     assume "I = {}" then show ?thesis by simp
```
```   504   next
```
```   505     assume "I \<noteq> {}" with X F I show ?thesis
```
```   506       by (intro finite_INT measurable_sets Int) auto
```
```   507   qed
```
```   508   finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M \<in> sets M" .
```
```   509 qed
```
```   510
```
```   511 locale product_sigma_finite =
```
```   512   fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
```
```   513   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
```
```   514
```
```   515 locale finite_product_sigma_finite = product_sigma_finite M
```
```   516   for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
```
```   517   fixes I :: "'i set" assumes finite_index'[intro]: "finite I"
```
```   518
```
```   519 sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
```
```   520   by (rule sigma_finite_measures)
```
```   521
```
```   522 sublocale product_sigma_finite \<subseteq> product_sigma_algebra
```
```   523   by default
```
```   524
```
```   525 sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
```
```   526   by default (fact finite_index')
```
```   527
```
```   528 lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
```
```   529   assumes "Pi\<^isub>E I F \<in> sets G"
```
```   530   shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
```
```   531 proof cases
```
```   532   assume ne: "\<forall>i\<in>I. F i \<noteq> {}"
```
```   533   have "\<forall>i\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') i = F i"
```
```   534     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
```
```   535        (insert ne, auto simp: Pi_eq_iff)
```
```   536   then show ?thesis
```
```   537     unfolding product_algebra_generator_def by simp
```
```   538 next
```
```   539   assume empty: "\<not> (\<forall>j\<in>I. F j \<noteq> {})"
```
```   540   then have "(\<Prod>j\<in>I. M.\<mu> j (F j)) = 0"
```
```   541     by (auto simp: setprod_ereal_0 intro!: bexI)
```
```   542   moreover
```
```   543   have "\<exists>j\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j = {}"
```
```   544     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
```
```   545        (insert empty, auto simp: Pi_eq_empty_iff[symmetric])
```
```   546   then have "(\<Prod>j\<in>I. M.\<mu> j ((SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j)) = 0"
```
```   547     by (auto simp: setprod_ereal_0 intro!: bexI)
```
```   548   ultimately show ?thesis
```
```   549     unfolding product_algebra_generator_def by simp
```
```   550 qed
```
```   551
```
```   552 lemma (in finite_product_sigma_finite) sigma_finite_pairs:
```
```   553   "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
```
```   554     (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
```
```   555     (\<forall>k. \<forall>i\<in>I. \<mu> i (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k) \<and>
```
```   556     (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space G"
```
```   557 proof -
```
```   558   have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. \<mu> i (F k) \<noteq> \<infinity>)"
```
```   559     using M.sigma_finite_up by simp
```
```   560   from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
```
```   561   then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. \<mu> i (F i k) \<noteq> \<infinity>"
```
```   562     by auto
```
```   563   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k"
```
```   564   note space_product_algebra[simp]
```
```   565   show ?thesis
```
```   566   proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
```
```   567     fix i show "range (F i) \<subseteq> sets (M i)" by fact
```
```   568   next
```
```   569     fix i k show "\<mu> i (F i k) \<noteq> \<infinity>" by fact
```
```   570   next
```
```   571     fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
```
```   572       using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
```
```   573       by (force simp: image_subset_iff)
```
```   574   next
```
```   575     fix f assume "f \<in> space G"
```
```   576     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
```
```   577     show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
```
```   578   next
```
```   579     fix i show "?F i \<subseteq> ?F (Suc i)"
```
```   580       using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
```
```   581   qed
```
```   582 qed
```
```   583
```
```   584 lemma sets_pair_cancel_measure[simp]:
```
```   585   "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
```
```   586   "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
```
```   587   unfolding pair_measure_def pair_measure_generator_def sets_sigma
```
```   588   by simp_all
```
```   589
```
```   590 lemma measurable_pair_cancel_measure[simp]:
```
```   591   "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
```
```   592   "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
```
```   593   "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
```
```   594   "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
```
```   595   unfolding measurable_def by (auto simp add: space_pair_measure)
```
```   596
```
```   597 lemma (in product_sigma_finite) product_measure_exists:
```
```   598   assumes "finite I"
```
```   599   shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
```
```   600     (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i)))"
```
```   601 using `finite I` proof induct
```
```   602   case empty
```
```   603   interpret finite_product_sigma_finite M "{}" by default simp
```
```   604   let ?\<nu> = "(\<lambda>A. if A = {} then 0 else 1) :: 'd set \<Rightarrow> ereal"
```
```   605   show ?case
```
```   606   proof (intro exI conjI ballI)
```
```   607     have "sigma_algebra (sigma G \<lparr>measure := ?\<nu>\<rparr>)"
```
```   608       by (rule sigma_algebra_cong) (simp_all add: product_algebra_def)
```
```   609     then have "measure_space (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
```
```   610       by (rule finite_additivity_sufficient)
```
```   611          (simp_all add: positive_def additive_def sets_sigma
```
```   612                         product_algebra_generator_def image_constant)
```
```   613     then show "sigma_finite_measure (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
```
```   614       by (auto intro!: exI[of _ "\<lambda>i. {\<lambda>_. undefined}"]
```
```   615                simp: sigma_finite_measure_def sigma_finite_measure_axioms_def
```
```   616                      product_algebra_generator_def)
```
```   617   qed auto
```
```   618 next
```
```   619   case (insert i I)
```
```   620   interpret finite_product_sigma_finite M I by default fact
```
```   621   have "finite (insert i I)" using `finite I` by auto
```
```   622   interpret I': finite_product_sigma_finite M "insert i I" by default fact
```
```   623   from insert obtain \<nu> where
```
```   624     prod: "\<And>A. A \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))" and
```
```   625     "sigma_finite_measure (sigma G\<lparr> measure := \<nu> \<rparr>)" by auto
```
```   626   then interpret I: sigma_finite_measure "P\<lparr> measure := \<nu>\<rparr>" unfolding product_algebra_def by simp
```
```   627   interpret P: pair_sigma_finite "P\<lparr> measure := \<nu>\<rparr>" "M i" ..
```
```   628   let ?h = "(\<lambda>(f, y). f(i := y))"
```
```   629   let ?\<nu> = "\<lambda>A. P.\<mu> (?h -` A \<inter> space P.P)"
```
```   630   have I': "sigma_algebra (I'.P\<lparr> measure := ?\<nu> \<rparr>)"
```
```   631     by (rule I'.sigma_algebra_cong) simp_all
```
```   632   interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
```
```   633     using measurable_add_dim[OF `i \<notin> I`]
```
```   634     by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
```
```   635   show ?case
```
```   636   proof (intro exI[of _ ?\<nu>] conjI ballI)
```
```   637     let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
```
```   638     { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
```
```   639       then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
```
```   640         using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
```
```   641       show "?m (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. M.\<mu> i (A i))"
```
```   642         unfolding * using A
```
```   643         apply (subst P.pair_measure_times)
```
```   644         using A apply fastsimp
```
```   645         using A apply fastsimp
```
```   646         using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
```
```   647     note product = this
```
```   648     have *: "sigma I'.G\<lparr> measure := ?\<nu> \<rparr> = I'.P\<lparr> measure := ?\<nu> \<rparr>"
```
```   649       by (simp add: product_algebra_def)
```
```   650     show "sigma_finite_measure (sigma I'.G\<lparr> measure := ?\<nu> \<rparr>)"
```
```   651     proof (unfold *, default, simp)
```
```   652       from I'.sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
```
```   653       then have F: "\<And>j. j \<in> insert i I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
```
```   654         "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k)"
```
```   655         "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
```
```   656         "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
```
```   657         by blast+
```
```   658       let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
```
```   659       show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
```
```   660           (\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
```
```   661       proof (intro exI[of _ ?F] conjI allI)
```
```   662         show "range ?F \<subseteq> sets I'.P" using F(1) by auto
```
```   663       next
```
```   664         from F(3) show "(\<Union>i. ?F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i))" by simp
```
```   665       next
```
```   666         fix j
```
```   667         have "\<And>k. k \<in> insert i I \<Longrightarrow> 0 \<le> measure (M k) (F k j)"
```
```   668           using F(1) by auto
```
```   669         with F `finite I` setprod_PInf[of "insert i I", OF this] show "?\<nu> (?F j) \<noteq> \<infinity>"
```
```   670           by (subst product) auto
```
```   671       qed
```
```   672     qed
```
```   673   qed
```
```   674 qed
```
```   675
```
```   676 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure P
```
```   677   unfolding product_algebra_def
```
```   678   using product_measure_exists[OF finite_index]
```
```   679   by (rule someI2_ex) auto
```
```   680
```
```   681 lemma (in finite_product_sigma_finite) measure_times:
```
```   682   assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
```
```   683   shows "\<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
```
```   684   unfolding product_algebra_def
```
```   685   using product_measure_exists[OF finite_index]
```
```   686   proof (rule someI2_ex, elim conjE)
```
```   687     fix \<nu> assume *: "\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
```
```   688     have "Pi\<^isub>E I A = Pi\<^isub>E I (\<lambda>i\<in>I. A i)" by (auto dest: Pi_mem)
```
```   689     then have "\<nu> (Pi\<^isub>E I A) = \<nu> (Pi\<^isub>E I (\<lambda>i\<in>I. A i))" by simp
```
```   690     also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i ((\<lambda>i\<in>I. A i) i))" using assms * by auto
```
```   691     finally show "measure (sigma G\<lparr>measure := \<nu>\<rparr>) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
```
```   692       by (simp add: sigma_def)
```
```   693   qed
```
```   694
```
```   695 lemma (in product_sigma_finite) product_measure_empty[simp]:
```
```   696   "measure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
```
```   697 proof -
```
```   698   interpret finite_product_sigma_finite M "{}" by default auto
```
```   699   from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
```
```   700 qed
```
```   701
```
```   702 lemma (in finite_product_sigma_algebra) P_empty:
```
```   703   assumes "I = {}"
```
```   704   shows "space P = {\<lambda>k. undefined}" "sets P = { {}, {\<lambda>k. undefined} }"
```
```   705   unfolding product_algebra_def product_algebra_generator_def `I = {}`
```
```   706   by (simp_all add: sigma_def image_constant)
```
```   707
```
```   708 lemma (in product_sigma_finite) positive_integral_empty:
```
```   709   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
```
```   710   shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
```
```   711 proof -
```
```   712   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
```
```   713   have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
```
```   714     using assms by (subst measure_times) auto
```
```   715   then show ?thesis
```
```   716     unfolding positive_integral_def simple_function_def simple_integral_def_raw
```
```   717   proof (simp add: P_empty, intro antisym)
```
```   718     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
```
```   719       by (intro le_SUPI) (auto simp: le_fun_def split: split_max)
```
```   720     show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
```
```   721       by (intro SUP_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm)
```
```   722   qed
```
```   723 qed
```
```   724
```
```   725 lemma (in product_sigma_finite) measure_fold:
```
```   726   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
```
```   727   assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
```
```   728   shows "measure (Pi\<^isub>M (I \<union> J) M) A =
```
```   729     measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M))"
```
```   730 proof -
```
```   731   interpret I: finite_product_sigma_finite M I by default fact
```
```   732   interpret J: finite_product_sigma_finite M J by default fact
```
```   733   have "finite (I \<union> J)" using fin by auto
```
```   734   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
```
```   735   interpret P: pair_sigma_finite I.P J.P by default
```
```   736   let ?g = "\<lambda>(x,y). merge I x J y"
```
```   737   let "?X S" = "?g -` S \<inter> space P.P"
```
```   738   from IJ.sigma_finite_pairs obtain F where
```
```   739     F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
```
```   740        "incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
```
```   741        "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space IJ.G"
```
```   742        "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<infinity>"
```
```   743     by auto
```
```   744   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
```
```   745   show "IJ.\<mu> A = P.\<mu> (?X A)"
```
```   746   proof (rule measure_unique_Int_stable_vimage)
```
```   747     show "measure_space IJ.P" "measure_space P.P" by default
```
```   748     show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
```
```   749       using A unfolding product_algebra_def by auto
```
```   750   next
```
```   751     show "Int_stable IJ.G"
```
```   752       by (rule Int_stable_product_algebra_generator)
```
```   753          (auto simp: Int_stable_def)
```
```   754     show "range ?F \<subseteq> sets IJ.G" using F
```
```   755       by (simp add: image_subset_iff product_algebra_def
```
```   756                     product_algebra_generator_def)
```
```   757     show "incseq ?F" "(\<Union>i. ?F i) = space IJ.G " by fact+
```
```   758   next
```
```   759     fix k
```
```   760     have "\<And>j. j \<in> I \<union> J \<Longrightarrow> 0 \<le> measure (M j) (F j k)"
```
```   761       using F(1) by auto
```
```   762     with F `finite I` setprod_PInf[of "I \<union> J", OF this]
```
```   763     show "IJ.\<mu> (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
```
```   764   next
```
```   765     fix A assume "A \<in> sets IJ.G"
```
```   766     then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
```
```   767       and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
```
```   768       by (auto simp: product_algebra_generator_def)
```
```   769     then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
```
```   770       using sets_into_space by (auto simp: space_pair_measure) blast+
```
```   771     then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
```
```   772       using `finite J` `finite I` F
```
```   773       by (simp add: P.pair_measure_times I.measure_times J.measure_times)
```
```   774     also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
```
```   775       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
```
```   776     also have "\<dots> = IJ.\<mu> A"
```
```   777       using `finite J` `finite I` F unfolding A
```
```   778       by (intro IJ.measure_times[symmetric]) auto
```
```   779     finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
```
```   780   qed (rule measurable_merge[OF IJ])
```
```   781 qed
```
```   782
```
```   783 lemma (in product_sigma_finite) measure_preserving_merge:
```
```   784   assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
```
```   785   shows "(\<lambda>(x,y). merge I x J y) \<in> measure_preserving (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
```
```   786   by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
```
```   787
```
```   788 lemma (in product_sigma_finite) product_positive_integral_fold:
```
```   789   assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
```
```   790   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
```
```   791   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
```
```   792     (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
```
```   793 proof -
```
```   794   interpret I: finite_product_sigma_finite M I by default fact
```
```   795   interpret J: finite_product_sigma_finite M J by default fact
```
```   796   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
```
```   797   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
```
```   798   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
```
```   799     using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
```
```   800   show ?thesis
```
```   801     unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
```
```   802   proof (rule P.positive_integral_vimage)
```
```   803     show "sigma_algebra IJ.P" by default
```
```   804     show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
```
```   805       using IJ by (rule measure_preserving_merge)
```
```   806     show "f \<in> borel_measurable IJ.P" using f by simp
```
```   807   qed
```
```   808 qed
```
```   809
```
```   810 lemma (in product_sigma_finite) measure_preserving_component_singelton:
```
```   811   "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
```
```   812 proof (intro measure_preservingI measurable_component_singleton)
```
```   813   interpret I: finite_product_sigma_finite M "{i}" by default simp
```
```   814   fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
```
```   815   assume A: "A \<in> sets (M i)"
```
```   816   then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
```
```   817   show "I.\<mu> ?P = M.\<mu> i A" unfolding *
```
```   818     using A I.measure_times[of "\<lambda>_. A"] by auto
```
```   819 qed auto
```
```   820
```
```   821 lemma (in product_sigma_finite) product_positive_integral_singleton:
```
```   822   assumes f: "f \<in> borel_measurable (M i)"
```
```   823   shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
```
```   824 proof -
```
```   825   interpret I: finite_product_sigma_finite M "{i}" by default simp
```
```   826   show ?thesis
```
```   827   proof (rule I.positive_integral_vimage[symmetric])
```
```   828     show "sigma_algebra (M i)" by (rule sigma_algebras)
```
```   829     show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
```
```   830       by (rule measure_preserving_component_singelton)
```
```   831     show "f \<in> borel_measurable (M i)" by fact
```
```   832   qed
```
```   833 qed
```
```   834
```
```   835 lemma (in product_sigma_finite) product_positive_integral_insert:
```
```   836   assumes [simp]: "finite I" "i \<notin> I"
```
```   837     and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
```
```   838   shows "integral\<^isup>P (Pi\<^isub>M (insert i I) M) f = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^isub>M I M))"
```
```   839 proof -
```
```   840   interpret I: finite_product_sigma_finite M I by default auto
```
```   841   interpret i: finite_product_sigma_finite M "{i}" by default auto
```
```   842   interpret P: pair_sigma_algebra I.P i.P ..
```
```   843   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
```
```   844     using f by auto
```
```   845   show ?thesis
```
```   846     unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
```
```   847   proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
```
```   848     fix x assume x: "x \<in> space I.P"
```
```   849     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
```
```   850     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
```
```   851       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
```
```   852     show "?f \<in> borel_measurable (M i)" unfolding f'_eq
```
```   853       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
```
```   854       by (simp add: comp_def)
```
```   855     show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
```
```   856       unfolding f'_eq by simp
```
```   857   qed
```
```   858 qed
```
```   859
```
```   860 lemma (in product_sigma_finite) product_positive_integral_setprod:
```
```   861   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
```
```   862   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
```
```   863   and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
```
```   864   shows "(\<integral>\<^isup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^isub>M I M) = (\<Prod>i\<in>I. integral\<^isup>P (M i) (f i))"
```
```   865 using assms proof induct
```
```   866   case empty
```
```   867   interpret finite_product_sigma_finite M "{}" by default auto
```
```   868   then show ?case by simp
```
```   869 next
```
```   870   case (insert i I)
```
```   871   note `finite I`[intro, simp]
```
```   872   interpret I: finite_product_sigma_finite M I by default auto
```
```   873   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
```
```   874     using insert by (auto intro!: setprod_cong)
```
```   875   have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^isub>M J M)"
```
```   876     using sets_into_space insert
```
```   877     by (intro sigma_algebra.borel_measurable_ereal_setprod sigma_algebra_product_algebra
```
```   878               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
```
```   879        auto
```
```   880   then show ?case
```
```   881     apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
```
```   882     apply (simp add: insert * pos borel setprod_ereal_pos M.positive_integral_multc)
```
```   883     apply (subst I.positive_integral_cmult)
```
```   884     apply (auto simp add: pos borel insert setprod_ereal_pos positive_integral_positive)
```
```   885     done
```
```   886 qed
```
```   887
```
```   888 lemma (in product_sigma_finite) product_integral_singleton:
```
```   889   assumes f: "f \<in> borel_measurable (M i)"
```
```   890   shows "(\<integral>x. f (x i) \<partial>Pi\<^isub>M {i} M) = integral\<^isup>L (M i) f"
```
```   891 proof -
```
```   892   interpret I: finite_product_sigma_finite M "{i}" by default simp
```
```   893   have *: "(\<lambda>x. ereal (f x)) \<in> borel_measurable (M i)"
```
```   894     "(\<lambda>x. ereal (- f x)) \<in> borel_measurable (M i)"
```
```   895     using assms by auto
```
```   896   show ?thesis
```
```   897     unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
```
```   898 qed
```
```   899
```
```   900 lemma (in product_sigma_finite) product_integral_fold:
```
```   901   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
```
```   902   and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
```
```   903   shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I x J y) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
```
```   904 proof -
```
```   905   interpret I: finite_product_sigma_finite M I by default fact
```
```   906   interpret J: finite_product_sigma_finite M J by default fact
```
```   907   have "finite (I \<union> J)" using fin by auto
```
```   908   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
```
```   909   interpret P: pair_sigma_finite I.P J.P by default
```
```   910   let ?M = "\<lambda>(x, y). merge I x J y"
```
```   911   let ?f = "\<lambda>x. f (?M x)"
```
```   912   show ?thesis
```
```   913   proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
```
```   914     have 1: "sigma_algebra IJ.P" by default
```
```   915     have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
```
```   916     have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
```
```   917     then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
```
```   918       by (simp add: integrable_def)
```
```   919     show "integrable P.P ?f"
```
```   920       by (rule P.integrable_vimage[where f=f, OF 1 2 3])
```
```   921     show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
```
```   922       by (rule P.integral_vimage[where f=f, OF 1 2 4])
```
```   923   qed
```
```   924 qed
```
```   925
```
```   926 lemma (in product_sigma_finite) product_integral_insert:
```
```   927   assumes [simp]: "finite I" "i \<notin> I"
```
```   928     and f: "integrable (Pi\<^isub>M (insert i I) M) f"
```
```   929   shows "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = (\<integral>x. (\<integral>y. f (x(i:=y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
```
```   930 proof -
```
```   931   interpret I: finite_product_sigma_finite M I by default auto
```
```   932   interpret I': finite_product_sigma_finite M "insert i I" by default auto
```
```   933   interpret i: finite_product_sigma_finite M "{i}" by default auto
```
```   934   interpret P: pair_sigma_finite I.P i.P ..
```
```   935   have IJ: "I \<inter> {i} = {}" by auto
```
```   936   show ?thesis
```
```   937     unfolding product_integral_fold[OF IJ, simplified, OF f]
```
```   938   proof (rule I.integral_cong, subst product_integral_singleton)
```
```   939     fix x assume x: "x \<in> space I.P"
```
```   940     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
```
```   941     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
```
```   942       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
```
```   943     have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
```
```   944     show "?f \<in> borel_measurable (M i)"
```
```   945       unfolding measurable_cong[OF f'_eq]
```
```   946       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
```
```   947       by (simp add: comp_def)
```
```   948     show "integral\<^isup>L (M i) ?f = integral\<^isup>L (M i) (\<lambda>y. f (x(i := y)))"
```
```   949       unfolding f'_eq by simp
```
```   950   qed
```
```   951 qed
```
```   952
```
```   953 lemma (in product_sigma_finite) product_integrable_setprod:
```
```   954   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
```
```   955   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
```
```   956   shows "integrable (Pi\<^isub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
```
```   957 proof -
```
```   958   interpret finite_product_sigma_finite M I by default fact
```
```   959   have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
```
```   960     using integrable unfolding integrable_def by auto
```
```   961   then have borel: "?f \<in> borel_measurable P"
```
```   962     using measurable_comp[OF measurable_component_singleton f]
```
```   963     by (auto intro!: borel_measurable_setprod simp: comp_def)
```
```   964   moreover have "integrable (Pi\<^isub>M I M) (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
```
```   965   proof (unfold integrable_def, intro conjI)
```
```   966     show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
```
```   967       using borel by auto
```
```   968     have "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. ereal (abs (f i (x i)))) \<partial>P)"
```
```   969       by (simp add: setprod_ereal abs_setprod)
```
```   970     also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^isup>+x. ereal (abs (f i x)) \<partial>M i))"
```
```   971       using f by (subst product_positive_integral_setprod) auto
```
```   972     also have "\<dots> < \<infinity>"
```
```   973       using integrable[THEN M.integrable_abs]
```
```   974       by (simp add: setprod_PInf integrable_def M.positive_integral_positive)
```
```   975     finally show "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>P) \<noteq> \<infinity>" by auto
```
```   976     have "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. 0 \<partial>P)"
```
```   977       by (intro positive_integral_cong_pos) auto
```
```   978     then show "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>P) \<noteq> \<infinity>" by simp
```
```   979   qed
```
```   980   ultimately show ?thesis
```
```   981     by (rule integrable_abs_iff[THEN iffD1])
```
```   982 qed
```
```   983
```
```   984 lemma (in product_sigma_finite) product_integral_setprod:
```
```   985   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
```
```   986   assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
```
```   987   shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^isub>M I M) = (\<Prod>i\<in>I. integral\<^isup>L (M i) (f i))"
```
```   988 using assms proof (induct rule: finite_ne_induct)
```
```   989   case (singleton i)
```
```   990   then show ?case by (simp add: product_integral_singleton integrable_def)
```
```   991 next
```
```   992   case (insert i I)
```
```   993   then have iI: "finite (insert i I)" by auto
```
```   994   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
```
```   995     integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
```
```   996     by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
```
```   997   interpret I: finite_product_sigma_finite M I by default fact
```
```   998   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
```
```   999     using `i \<notin> I` by (auto intro!: setprod_cong)
```
```  1000   show ?case
```
```  1001     unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
```
```  1002     by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
```
```  1003 qed
```
```  1004
```
`  1005 end`