src/HOL/Probability/Finite_Product_Measure.thy
author hoelzl
Tue Mar 29 14:27:39 2011 +0200 (2011-03-29)
changeset 42146 5b52c6a9c627
parent 42067 src/HOL/Probability/Product_Measure.thy@66c8281349ec
child 42950 6e5c2a3c69da
permissions -rw-r--r--
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
     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 section "Generating set generates also product algebra"
   329 
   330 lemma sigma_product_algebra_sigma_eq:
   331   assumes "finite I"
   332   assumes mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
   333   assumes union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (E i)"
   334   assumes sets_into: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> sets (E i)"
   335   and E: "\<And>i. sets (E i) \<subseteq> Pow (space (E i))"
   336   shows "sets (\<Pi>\<^isub>M i\<in>I. sigma (E i)) = sets (\<Pi>\<^isub>M i\<in>I. E i)"
   337     (is "sets ?S = sets ?E")
   338 proof cases
   339   assume "I = {}" then show ?thesis
   340     by (simp add: product_algebra_def product_algebra_generator_def)
   341 next
   342   assume "I \<noteq> {}"
   343   interpret E: sigma_algebra "sigma (E i)" for i
   344     using E by (rule sigma_algebra_sigma)
   345   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)"
   346     using E by auto
   347   interpret G: sigma_algebra ?E
   348     unfolding product_algebra_def product_algebra_generator_def using E
   349     by (intro sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) (auto dest: Pi_mem)
   350   { fix A i assume "i \<in> I" and A: "A \<in> sets (E i)"
   351     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"
   352       using mono union unfolding incseq_Suc_iff space_product_algebra
   353       by (auto dest: Pi_mem)
   354     also have "\<dots> = (\<Union>n. (\<Pi>\<^isub>E j\<in>I. if j = i then A else S j n))"
   355       unfolding space_product_algebra
   356       apply simp
   357       apply (subst Pi_UN[OF `finite I`])
   358       using mono[THEN incseqD] apply simp
   359       apply (simp add: PiE_Int)
   360       apply (intro PiE_cong)
   361       using A sets_into by (auto intro!: into_space)
   362     also have "\<dots> \<in> sets ?E"
   363       using sets_into `A \<in> sets (E i)`
   364       unfolding sets_product_algebra sets_sigma
   365       by (intro sigma_sets.Union)
   366          (auto simp: image_subset_iff intro!: sigma_sets.Basic)
   367     finally have "(\<lambda>x. x i) -` A \<inter> space ?E \<in> sets ?E" . }
   368   then have proj:
   369     "\<And>i. i\<in>I \<Longrightarrow> (\<lambda>x. x i) \<in> measurable ?E (sigma (E i))"
   370     using E by (subst G.measurable_iff_sigma)
   371                (auto simp: sets_product_algebra sets_sigma)
   372   { fix A assume A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (sigma (E i))"
   373     with proj have basic: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) -` (A i) \<inter> space ?E \<in> sets ?E"
   374       unfolding measurable_def by simp
   375     have "Pi\<^isub>E I A = (\<Inter>i\<in>I. (\<lambda>x. x i) -` (A i) \<inter> space ?E)"
   376       using A E.sets_into_space `I \<noteq> {}` unfolding product_algebra_def by auto blast
   377     then have "Pi\<^isub>E I A \<in> sets ?E"
   378       using G.finite_INT[OF `finite I` `I \<noteq> {}` basic, of "\<lambda>i. i"] by simp }
   379   then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\<lambda>i. sigma (E i)))) \<subseteq> sets ?E"
   380     by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def)
   381   then have subset: "sets ?S \<subseteq> sets ?E"
   382     by (simp add: sets_sigma sets_product_algebra)
   383   show "sets ?S = sets ?E"
   384   proof (intro set_eqI iffI)
   385     fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
   386       unfolding sets_sigma sets_product_algebra
   387     proof induct
   388       case (Basic A) then show ?case
   389         by (auto simp: sets_sigma product_algebra_generator_def intro: sigma_sets.Basic)
   390     qed (auto intro: sigma_sets.intros simp: product_algebra_generator_def)
   391   next
   392     fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
   393   qed
   394 qed
   395 
   396 lemma product_algebraI[intro]:
   397     "E \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> Pi\<^isub>E I E \<in> sets (Pi\<^isub>M I M)"
   398   using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI)
   399 
   400 lemma (in product_sigma_algebra) measurable_component_update:
   401   assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
   402   shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
   403   unfolding product_algebra_def apply simp
   404 proof (intro measurable_sigma)
   405   let ?G = "product_algebra_generator (insert i I) M"
   406   show "sets ?G \<subseteq> Pow (space ?G)" using product_algebra_generator_into_space .
   407   show "?f \<in> space (M i) \<rightarrow> space ?G"
   408     using M.sets_into_space assms by auto
   409   fix A assume "A \<in> sets ?G"
   410   from product_algebraE[OF this] guess E . note E = this
   411   then have "?f -` A \<inter> space (M i) = E i \<or> ?f -` A \<inter> space (M i) = {}"
   412     using M.sets_into_space assms by auto
   413   then show "?f -` A \<inter> space (M i) \<in> sets (M i)"
   414     using E by (auto intro!: product_algebraI)
   415 qed
   416 
   417 lemma (in product_sigma_algebra) measurable_add_dim:
   418   assumes "i \<notin> I"
   419   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)"
   420 proof -
   421   let ?f = "(\<lambda>(f, y). f(i := y))" and ?G = "product_algebra_generator (insert i I) M"
   422   interpret Ii: pair_sigma_algebra "Pi\<^isub>M I M" "M i"
   423     unfolding pair_sigma_algebra_def
   424     by (intro sigma_algebra_product_algebra sigma_algebras conjI)
   425   have "?f \<in> measurable Ii.P (sigma ?G)"
   426   proof (rule Ii.measurable_sigma)
   427     show "sets ?G \<subseteq> Pow (space ?G)"
   428       using product_algebra_generator_into_space .
   429     show "?f \<in> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<rightarrow> space ?G"
   430       by (auto simp: space_pair_measure)
   431   next
   432     fix A assume "A \<in> sets ?G"
   433     then obtain F where "A = Pi\<^isub>E (insert i I) F"
   434       and F: "\<And>j. j \<in> I \<Longrightarrow> F j \<in> sets (M j)" "F i \<in> sets (M i)"
   435       by (auto elim!: product_algebraE)
   436     then have "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = Pi\<^isub>E I F \<times> (F i)"
   437       using sets_into_space `i \<notin> I`
   438       by (auto simp add: space_pair_measure) blast+
   439     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)"
   440       using F by (auto intro!: pair_measureI)
   441   qed
   442   then show ?thesis
   443     by (simp add: product_algebra_def)
   444 qed
   445 
   446 lemma (in product_sigma_algebra) measurable_merge:
   447   assumes [simp]: "I \<inter> J = {}"
   448   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)"
   449 proof -
   450   let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M"
   451   interpret P: sigma_algebra "?I \<Otimes>\<^isub>M ?J"
   452     by (intro sigma_algebra_pair_measure product_algebra_into_space)
   453   let ?f = "\<lambda>(x, y). merge I x J y"
   454   let ?G = "product_algebra_generator (I \<union> J) M"
   455   have "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (sigma ?G)"
   456   proof (rule P.measurable_sigma)
   457     fix A assume "A \<in> sets ?G"
   458     from product_algebraE[OF this]
   459     obtain E where E: "A = Pi\<^isub>E (I \<union> J) E" "E \<in> (\<Pi> i\<in>I \<union> J. sets (M i))" .
   460     then have *: "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) = Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
   461       using sets_into_space `I \<inter> J = {}`
   462       by (auto simp add: space_pair_measure) fast+
   463     then show "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) \<in> sets (?I \<Otimes>\<^isub>M ?J)"
   464       using E unfolding * by (auto intro!: pair_measureI in_sigma product_algebra_generatorI
   465         simp: product_algebra_def)
   466   qed (insert product_algebra_generator_into_space, auto simp: space_pair_measure)
   467   then show "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (Pi\<^isub>M (I \<union> J) M)"
   468     unfolding product_algebra_def[of "I \<union> J"] by simp
   469 qed
   470 
   471 lemma (in product_sigma_algebra) measurable_component_singleton:
   472   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
   473 proof (unfold measurable_def, intro CollectI conjI ballI)
   474   fix A assume "A \<in> sets (M i)"
   475   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))"
   476     using M.sets_into_space `i \<in> I` by (fastsimp dest: Pi_mem split: split_if_asm)
   477   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
   478     using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
   479 qed (insert `i \<in> I`, auto)
   480 
   481 locale product_sigma_finite =
   482   fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
   483   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
   484 
   485 locale finite_product_sigma_finite = product_sigma_finite M
   486   for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
   487   fixes I :: "'i set" assumes finite_index'[intro]: "finite I"
   488 
   489 sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
   490   by (rule sigma_finite_measures)
   491 
   492 sublocale product_sigma_finite \<subseteq> product_sigma_algebra
   493   by default
   494 
   495 sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
   496   by default (fact finite_index')
   497 
   498 lemma setprod_extreal_0:
   499   fixes f :: "'a \<Rightarrow> extreal"
   500   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
   501 proof cases
   502   assume "finite A"
   503   then show ?thesis by (induct A) auto
   504 qed auto
   505 
   506 lemma setprod_extreal_pos:
   507   fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
   508 proof cases
   509   assume "finite I" from this pos show ?thesis by induct auto
   510 qed simp
   511 
   512 lemma setprod_PInf:
   513   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   514   shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
   515 proof cases
   516   assume "finite I" from this assms show ?thesis
   517   proof (induct I)
   518     case (insert i I)
   519     then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
   520     from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
   521     also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
   522       using setprod_extreal_pos[of I f] pos
   523       by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
   524     also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
   525       using insert by (auto simp: setprod_extreal_0)
   526     finally show ?case .
   527   qed simp
   528 qed simp
   529 
   530 lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
   531 proof cases
   532   assume "finite A" then show ?thesis
   533     by induct (auto simp: one_extreal_def)
   534 qed (simp add: one_extreal_def)
   535 
   536 lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
   537   assumes "Pi\<^isub>E I F \<in> sets G"
   538   shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
   539 proof cases
   540   assume ne: "\<forall>i\<in>I. F i \<noteq> {}"
   541   have "\<forall>i\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') i = F i"
   542     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
   543        (insert ne, auto simp: Pi_eq_iff)
   544   then show ?thesis
   545     unfolding product_algebra_generator_def by simp
   546 next
   547   assume empty: "\<not> (\<forall>j\<in>I. F j \<noteq> {})"
   548   then have "(\<Prod>j\<in>I. M.\<mu> j (F j)) = 0"
   549     by (auto simp: setprod_extreal_0 intro!: bexI)
   550   moreover
   551   have "\<exists>j\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j = {}"
   552     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
   553        (insert empty, auto simp: Pi_eq_empty_iff[symmetric])
   554   then have "(\<Prod>j\<in>I. M.\<mu> j ((SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j)) = 0"
   555     by (auto simp: setprod_extreal_0 intro!: bexI)
   556   ultimately show ?thesis
   557     unfolding product_algebra_generator_def by simp
   558 qed
   559 
   560 lemma (in finite_product_sigma_finite) sigma_finite_pairs:
   561   "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
   562     (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
   563     (\<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>
   564     (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space G"
   565 proof -
   566   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>)"
   567     using M.sigma_finite_up by simp
   568   from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   569   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>"
   570     by auto
   571   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k"
   572   note space_product_algebra[simp]
   573   show ?thesis
   574   proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
   575     fix i show "range (F i) \<subseteq> sets (M i)" by fact
   576   next
   577     fix i k show "\<mu> i (F i k) \<noteq> \<infinity>" by fact
   578   next
   579     fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
   580       using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
   581       by (force simp: image_subset_iff)
   582   next
   583     fix f assume "f \<in> space G"
   584     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
   585     show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
   586   next
   587     fix i show "?F i \<subseteq> ?F (Suc i)"
   588       using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
   589   qed
   590 qed
   591 
   592 lemma sets_pair_cancel_measure[simp]:
   593   "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
   594   "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
   595   unfolding pair_measure_def pair_measure_generator_def sets_sigma
   596   by simp_all
   597 
   598 lemma measurable_pair_cancel_measure[simp]:
   599   "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
   600   "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
   601   "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
   602   "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
   603   unfolding measurable_def by (auto simp add: space_pair_measure)
   604 
   605 lemma (in product_sigma_finite) product_measure_exists:
   606   assumes "finite I"
   607   shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
   608     (\<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)))"
   609 using `finite I` proof induct
   610   case empty
   611   interpret finite_product_sigma_finite M "{}" by default simp
   612   let ?\<nu> = "(\<lambda>A. if A = {} then 0 else 1) :: 'd set \<Rightarrow> extreal"
   613   show ?case
   614   proof (intro exI conjI ballI)
   615     have "sigma_algebra (sigma G \<lparr>measure := ?\<nu>\<rparr>)"
   616       by (rule sigma_algebra_cong) (simp_all add: product_algebra_def)
   617     then have "measure_space (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
   618       by (rule finite_additivity_sufficient)
   619          (simp_all add: positive_def additive_def sets_sigma
   620                         product_algebra_generator_def image_constant)
   621     then show "sigma_finite_measure (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
   622       by (auto intro!: exI[of _ "\<lambda>i. {\<lambda>_. undefined}"]
   623                simp: sigma_finite_measure_def sigma_finite_measure_axioms_def
   624                      product_algebra_generator_def)
   625   qed auto
   626 next
   627   case (insert i I)
   628   interpret finite_product_sigma_finite M I by default fact
   629   have "finite (insert i I)" using `finite I` by auto
   630   interpret I': finite_product_sigma_finite M "insert i I" by default fact
   631   from insert obtain \<nu> where
   632     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
   633     "sigma_finite_measure (sigma G\<lparr> measure := \<nu> \<rparr>)" by auto
   634   then interpret I: sigma_finite_measure "P\<lparr> measure := \<nu>\<rparr>" unfolding product_algebra_def by simp
   635   interpret P: pair_sigma_finite "P\<lparr> measure := \<nu>\<rparr>" "M i" ..
   636   let ?h = "(\<lambda>(f, y). f(i := y))"
   637   let ?\<nu> = "\<lambda>A. P.\<mu> (?h -` A \<inter> space P.P)"
   638   have I': "sigma_algebra (I'.P\<lparr> measure := ?\<nu> \<rparr>)"
   639     by (rule I'.sigma_algebra_cong) simp_all
   640   interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
   641     using measurable_add_dim[OF `i \<notin> I`]
   642     by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
   643   show ?case
   644   proof (intro exI[of _ ?\<nu>] conjI ballI)
   645     let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
   646     { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
   647       then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
   648         using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
   649       show "?m (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. M.\<mu> i (A i))"
   650         unfolding * using A
   651         apply (subst P.pair_measure_times)
   652         using A apply fastsimp
   653         using A apply fastsimp
   654         using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
   655     note product = this
   656     have *: "sigma I'.G\<lparr> measure := ?\<nu> \<rparr> = I'.P\<lparr> measure := ?\<nu> \<rparr>"
   657       by (simp add: product_algebra_def)
   658     show "sigma_finite_measure (sigma I'.G\<lparr> measure := ?\<nu> \<rparr>)"
   659     proof (unfold *, default, simp)
   660       from I'.sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   661       then have F: "\<And>j. j \<in> insert i I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
   662         "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k)"
   663         "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
   664         "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
   665         by blast+
   666       let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
   667       show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
   668           (\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
   669       proof (intro exI[of _ ?F] conjI allI)
   670         show "range ?F \<subseteq> sets I'.P" using F(1) by auto
   671       next
   672         from F(3) show "(\<Union>i. ?F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i))" by simp
   673       next
   674         fix j
   675         have "\<And>k. k \<in> insert i I \<Longrightarrow> 0 \<le> measure (M k) (F k j)"
   676           using F(1) by auto
   677         with F `finite I` setprod_PInf[of "insert i I", OF this] show "?\<nu> (?F j) \<noteq> \<infinity>"
   678           by (subst product) auto
   679       qed
   680     qed
   681   qed
   682 qed
   683 
   684 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure P
   685   unfolding product_algebra_def
   686   using product_measure_exists[OF finite_index]
   687   by (rule someI2_ex) auto
   688 
   689 lemma (in finite_product_sigma_finite) measure_times:
   690   assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
   691   shows "\<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
   692   unfolding product_algebra_def
   693   using product_measure_exists[OF finite_index]
   694   proof (rule someI2_ex, elim conjE)
   695     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))"
   696     have "Pi\<^isub>E I A = Pi\<^isub>E I (\<lambda>i\<in>I. A i)" by (auto dest: Pi_mem)
   697     then have "\<nu> (Pi\<^isub>E I A) = \<nu> (Pi\<^isub>E I (\<lambda>i\<in>I. A i))" by simp
   698     also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i ((\<lambda>i\<in>I. A i) i))" using assms * by auto
   699     finally show "measure (sigma G\<lparr>measure := \<nu>\<rparr>) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
   700       by (simp add: sigma_def)
   701   qed
   702 
   703 lemma (in product_sigma_finite) product_measure_empty[simp]:
   704   "measure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
   705 proof -
   706   interpret finite_product_sigma_finite M "{}" by default auto
   707   from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
   708 qed
   709 
   710 lemma (in finite_product_sigma_algebra) P_empty:
   711   assumes "I = {}"
   712   shows "space P = {\<lambda>k. undefined}" "sets P = { {}, {\<lambda>k. undefined} }"
   713   unfolding product_algebra_def product_algebra_generator_def `I = {}`
   714   by (simp_all add: sigma_def image_constant)
   715 
   716 lemma (in product_sigma_finite) positive_integral_empty:
   717   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   718   shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
   719 proof -
   720   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
   721   have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
   722     using assms by (subst measure_times) auto
   723   then show ?thesis
   724     unfolding positive_integral_def simple_function_def simple_integral_def_raw
   725   proof (simp add: P_empty, intro antisym)
   726     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
   727       by (intro le_SUPI) (auto simp: le_fun_def split: split_max)
   728     show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
   729       by (intro SUP_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm)
   730   qed
   731 qed
   732 
   733 lemma (in product_sigma_finite) measure_fold:
   734   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   735   assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   736   shows "measure (Pi\<^isub>M (I \<union> J) M) A =
   737     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))"
   738 proof -
   739   interpret I: finite_product_sigma_finite M I by default fact
   740   interpret J: finite_product_sigma_finite M J by default fact
   741   have "finite (I \<union> J)" using fin by auto
   742   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   743   interpret P: pair_sigma_finite I.P J.P by default
   744   let ?g = "\<lambda>(x,y). merge I x J y"
   745   let "?X S" = "?g -` S \<inter> space P.P"
   746   from IJ.sigma_finite_pairs obtain F where
   747     F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   748        "incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
   749        "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space IJ.G"
   750        "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<infinity>"
   751     by auto
   752   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
   753   show "IJ.\<mu> A = P.\<mu> (?X A)"
   754   proof (rule measure_unique_Int_stable_vimage)
   755     show "measure_space IJ.P" "measure_space P.P" by default
   756     show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
   757       using A unfolding product_algebra_def by auto
   758   next
   759     show "Int_stable IJ.G"
   760       by (simp add: PiE_Int Int_stable_def product_algebra_def
   761                     product_algebra_generator_def)
   762           auto
   763     show "range ?F \<subseteq> sets IJ.G" using F
   764       by (simp add: image_subset_iff product_algebra_def
   765                     product_algebra_generator_def)
   766     show "incseq ?F" "(\<Union>i. ?F i) = space IJ.G " by fact+
   767   next
   768     fix k
   769     have "\<And>j. j \<in> I \<union> J \<Longrightarrow> 0 \<le> measure (M j) (F j k)"
   770       using F(1) by auto
   771     with F `finite I` setprod_PInf[of "I \<union> J", OF this]
   772     show "IJ.\<mu> (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
   773   next
   774     fix A assume "A \<in> sets IJ.G"
   775     then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
   776       and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
   777       by (auto simp: product_algebra_generator_def)
   778     then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   779       using sets_into_space by (auto simp: space_pair_measure) blast+
   780     then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
   781       using `finite J` `finite I` F
   782       by (simp add: P.pair_measure_times I.measure_times J.measure_times)
   783     also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
   784       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   785     also have "\<dots> = IJ.\<mu> A"
   786       using `finite J` `finite I` F unfolding A
   787       by (intro IJ.measure_times[symmetric]) auto
   788     finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
   789   qed (rule measurable_merge[OF IJ])
   790 qed
   791 
   792 lemma (in product_sigma_finite) measure_preserving_merge:
   793   assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
   794   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)"
   795   by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
   796 
   797 lemma (in product_sigma_finite) product_positive_integral_fold:
   798   assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
   799   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   800   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
   801     (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
   802 proof -
   803   interpret I: finite_product_sigma_finite M I by default fact
   804   interpret J: finite_product_sigma_finite M J by default fact
   805   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   806   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
   807   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
   808     using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
   809   show ?thesis
   810     unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
   811   proof (rule P.positive_integral_vimage)
   812     show "sigma_algebra IJ.P" by default
   813     show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
   814       using IJ by (rule measure_preserving_merge)
   815     show "f \<in> borel_measurable IJ.P" using f by simp
   816   qed
   817 qed
   818 
   819 lemma (in product_sigma_finite) measure_preserving_component_singelton:
   820   "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
   821 proof (intro measure_preservingI measurable_component_singleton)
   822   interpret I: finite_product_sigma_finite M "{i}" by default simp
   823   fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
   824   assume A: "A \<in> sets (M i)"
   825   then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
   826   show "I.\<mu> ?P = M.\<mu> i A" unfolding *
   827     using A I.measure_times[of "\<lambda>_. A"] by auto
   828 qed auto
   829 
   830 lemma (in product_sigma_finite) product_positive_integral_singleton:
   831   assumes f: "f \<in> borel_measurable (M i)"
   832   shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
   833 proof -
   834   interpret I: finite_product_sigma_finite M "{i}" by default simp
   835   show ?thesis
   836   proof (rule I.positive_integral_vimage[symmetric])
   837     show "sigma_algebra (M i)" by (rule sigma_algebras)
   838     show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
   839       by (rule measure_preserving_component_singelton)
   840     show "f \<in> borel_measurable (M i)" by fact
   841   qed
   842 qed
   843 
   844 lemma (in product_sigma_finite) product_positive_integral_insert:
   845   assumes [simp]: "finite I" "i \<notin> I"
   846     and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
   847   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))"
   848 proof -
   849   interpret I: finite_product_sigma_finite M I by default auto
   850   interpret i: finite_product_sigma_finite M "{i}" by default auto
   851   interpret P: pair_sigma_algebra I.P i.P ..
   852   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
   853     using f by auto
   854   show ?thesis
   855     unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
   856   proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
   857     fix x assume x: "x \<in> space I.P"
   858     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
   859     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
   860       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
   861     show "?f \<in> borel_measurable (M i)" unfolding f'_eq
   862       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
   863       by (simp add: comp_def)
   864     show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
   865       unfolding f'_eq by simp
   866   qed
   867 qed
   868 
   869 lemma (in product_sigma_finite) product_positive_integral_setprod:
   870   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> extreal"
   871   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   872   and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
   873   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))"
   874 using assms proof induct
   875   case empty
   876   interpret finite_product_sigma_finite M "{}" by default auto
   877   then show ?case by simp
   878 next
   879   case (insert i I)
   880   note `finite I`[intro, simp]
   881   interpret I: finite_product_sigma_finite M I by default auto
   882   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))"
   883     using insert by (auto intro!: setprod_cong)
   884   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)"
   885     using sets_into_space insert
   886     by (intro sigma_algebra.borel_measurable_extreal_setprod sigma_algebra_product_algebra
   887               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
   888        auto
   889   then show ?case
   890     apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
   891     apply (simp add: insert * pos borel setprod_extreal_pos M.positive_integral_multc)
   892     apply (subst I.positive_integral_cmult)
   893     apply (auto simp add: pos borel insert setprod_extreal_pos positive_integral_positive)
   894     done
   895 qed
   896 
   897 lemma (in product_sigma_finite) product_integral_singleton:
   898   assumes f: "f \<in> borel_measurable (M i)"
   899   shows "(\<integral>x. f (x i) \<partial>Pi\<^isub>M {i} M) = integral\<^isup>L (M i) f"
   900 proof -
   901   interpret I: finite_product_sigma_finite M "{i}" by default simp
   902   have *: "(\<lambda>x. extreal (f x)) \<in> borel_measurable (M i)"
   903     "(\<lambda>x. extreal (- f x)) \<in> borel_measurable (M i)"
   904     using assms by auto
   905   show ?thesis
   906     unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
   907 qed
   908 
   909 lemma (in product_sigma_finite) product_integral_fold:
   910   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   911   and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
   912   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)"
   913 proof -
   914   interpret I: finite_product_sigma_finite M I by default fact
   915   interpret J: finite_product_sigma_finite M J by default fact
   916   have "finite (I \<union> J)" using fin by auto
   917   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   918   interpret P: pair_sigma_finite I.P J.P by default
   919   let ?M = "\<lambda>(x, y). merge I x J y"
   920   let ?f = "\<lambda>x. f (?M x)"
   921   show ?thesis
   922   proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
   923     have 1: "sigma_algebra IJ.P" by default
   924     have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
   925     have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
   926     then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   927       by (simp add: integrable_def)
   928     show "integrable P.P ?f"
   929       by (rule P.integrable_vimage[where f=f, OF 1 2 3])
   930     show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
   931       by (rule P.integral_vimage[where f=f, OF 1 2 4])
   932   qed
   933 qed
   934 
   935 lemma (in product_sigma_finite) product_integral_insert:
   936   assumes [simp]: "finite I" "i \<notin> I"
   937     and f: "integrable (Pi\<^isub>M (insert i I) M) f"
   938   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)"
   939 proof -
   940   interpret I: finite_product_sigma_finite M I by default auto
   941   interpret I': finite_product_sigma_finite M "insert i I" by default auto
   942   interpret i: finite_product_sigma_finite M "{i}" by default auto
   943   interpret P: pair_sigma_finite I.P i.P ..
   944   have IJ: "I \<inter> {i} = {}" by auto
   945   show ?thesis
   946     unfolding product_integral_fold[OF IJ, simplified, OF f]
   947   proof (rule I.integral_cong, subst product_integral_singleton)
   948     fix x assume x: "x \<in> space I.P"
   949     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
   950     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
   951       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
   952     have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
   953     show "?f \<in> borel_measurable (M i)"
   954       unfolding measurable_cong[OF f'_eq]
   955       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
   956       by (simp add: comp_def)
   957     show "integral\<^isup>L (M i) ?f = integral\<^isup>L (M i) (\<lambda>y. f (x(i := y)))"
   958       unfolding f'_eq by simp
   959   qed
   960 qed
   961 
   962 lemma (in product_sigma_finite) product_integrable_setprod:
   963   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   964   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   965   shows "integrable (Pi\<^isub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
   966 proof -
   967   interpret finite_product_sigma_finite M I by default fact
   968   have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   969     using integrable unfolding integrable_def by auto
   970   then have borel: "?f \<in> borel_measurable P"
   971     using measurable_comp[OF measurable_component_singleton f]
   972     by (auto intro!: borel_measurable_setprod simp: comp_def)
   973   moreover have "integrable (Pi\<^isub>M I M) (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
   974   proof (unfold integrable_def, intro conjI)
   975     show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
   976       using borel by auto
   977     have "(\<integral>\<^isup>+x. extreal (abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. extreal (abs (f i (x i)))) \<partial>P)"
   978       by (simp add: setprod_extreal abs_setprod)
   979     also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^isup>+x. extreal (abs (f i x)) \<partial>M i))"
   980       using f by (subst product_positive_integral_setprod) auto
   981     also have "\<dots> < \<infinity>"
   982       using integrable[THEN M.integrable_abs]
   983       by (simp add: setprod_PInf integrable_def M.positive_integral_positive)
   984     finally show "(\<integral>\<^isup>+x. extreal (abs (?f x)) \<partial>P) \<noteq> \<infinity>" by auto
   985     have "(\<integral>\<^isup>+x. extreal (- abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. 0 \<partial>P)"
   986       by (intro positive_integral_cong_pos) auto
   987     then show "(\<integral>\<^isup>+x. extreal (- abs (?f x)) \<partial>P) \<noteq> \<infinity>" by simp
   988   qed
   989   ultimately show ?thesis
   990     by (rule integrable_abs_iff[THEN iffD1])
   991 qed
   992 
   993 lemma (in product_sigma_finite) product_integral_setprod:
   994   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   995   assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   996   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))"
   997 using assms proof (induct rule: finite_ne_induct)
   998   case (singleton i)
   999   then show ?case by (simp add: product_integral_singleton integrable_def)
  1000 next
  1001   case (insert i I)
  1002   then have iI: "finite (insert i I)" by auto
  1003   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  1004     integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  1005     by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
  1006   interpret I: finite_product_sigma_finite M I by default fact
  1007   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))"
  1008     using `i \<notin> I` by (auto intro!: setprod_cong)
  1009   show ?case
  1010     unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
  1011     by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
  1012 qed
  1013 
  1014 end