src/HOL/Probability/Finite_Product_Measure.thy
author immler@in.tum.de
Tue Nov 06 11:03:28 2012 +0100 (2012-11-06)
changeset 50038 8e32c9254535
parent 50021 d96a3f468203
child 50041 afe886a04198
permissions -rw-r--r--
moved lemmas further up
     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 split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    12   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_insert[intro, simp]:
    38   assumes "a \<in> extensional (insert i I)"
    39   shows "a(i := b) \<in> extensional (insert i I)"
    40   using assms unfolding extensional_def by auto
    41 
    42 lemma extensional_Int[simp]:
    43   "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
    44   unfolding extensional_def by auto
    45 
    46 lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
    47   by (auto simp: extensional_def)
    48 
    49 lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
    50   unfolding restrict_def extensional_def by auto
    51 
    52 lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
    53   unfolding restrict_def by (simp add: fun_eq_iff)
    54 
    55 definition
    56   "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    57 
    58 lemma merge_apply[simp]:
    59   "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    60   "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    61   "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    62   "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    63   "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined"
    64   unfolding merge_def by auto
    65 
    66 lemma merge_commute:
    67   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
    68   by (force simp: merge_def)
    69 
    70 lemma Pi_cancel_merge_range[simp]:
    71   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    72   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    73   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    74   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    75   by (auto simp: Pi_def)
    76 
    77 lemma Pi_cancel_merge[simp]:
    78   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    79   "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    80   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    81   "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    82   by (auto simp: Pi_def)
    83 
    84 lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
    85   by (auto simp: extensional_def)
    86 
    87 lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
    88   by (auto simp: restrict_def Pi_def)
    89 
    90 lemma restrict_merge[simp]:
    91   "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    92   "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    93   "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    94   "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    95   by (auto simp: restrict_def)
    96 
    97 lemma extensional_insert_undefined[intro, simp]:
    98   assumes "a \<in> extensional (insert i I)"
    99   shows "a(i := undefined) \<in> extensional I"
   100   using assms unfolding extensional_def by auto
   101 
   102 lemma extensional_insert_cancel[intro, simp]:
   103   assumes "a \<in> extensional I"
   104   shows "a \<in> extensional (insert i I)"
   105   using assms unfolding extensional_def by auto
   106 
   107 lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
   108   unfolding merge_def by (auto simp: fun_eq_iff)
   109 
   110 lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
   111   by auto
   112 
   113 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)"
   114   by auto
   115 
   116 lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
   117   by (auto simp: Pi_def)
   118 
   119 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"
   120   by (auto simp: Pi_def)
   121 
   122 lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
   123   by (auto simp: Pi_def)
   124 
   125 lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   126   by (auto simp: Pi_def)
   127 
   128 lemma restrict_vimage:
   129   assumes "I \<inter> J = {}"
   130   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 J (E, F))"
   131   using assms by (auto simp: restrict_Pi_cancel)
   132 
   133 lemma merge_vimage:
   134   assumes "I \<inter> J = {}"
   135   shows "merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   136   using assms by (auto simp: restrict_Pi_cancel)
   137 
   138 lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   139   by (auto simp: restrict_def)
   140 
   141 lemma merge_restrict[simp]:
   142   "merge I J (restrict x I, y) = merge I J (x, y)"
   143   "merge I J (x, restrict y J) = merge I J (x, y)"
   144   unfolding merge_def by auto
   145 
   146 lemma merge_x_x_eq_restrict[simp]:
   147   "merge I J (x, x) = restrict x (I \<union> J)"
   148   unfolding merge_def by auto
   149 
   150 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"
   151   apply auto
   152   apply (drule_tac x=x in Pi_mem)
   153   apply (simp_all split: split_if_asm)
   154   apply (drule_tac x=i in Pi_mem)
   155   apply (auto dest!: Pi_mem)
   156   done
   157 
   158 lemma Pi_UN:
   159   fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
   160   assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
   161   shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
   162 proof (intro set_eqI iffI)
   163   fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
   164   then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
   165   from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
   166   obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
   167     using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
   168   have "f \<in> Pi I (A k)"
   169   proof (intro Pi_I)
   170     fix i assume "i \<in> I"
   171     from mono[OF this, of "n i" k] k[OF this] n[OF this]
   172     show "f i \<in> A k i" by auto
   173   qed
   174   then show "f \<in> (\<Union>n. Pi I (A n))" by auto
   175 qed auto
   176 
   177 lemma PiE_cong:
   178   assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
   179   shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
   180   using assms by (auto intro!: Pi_cong)
   181 
   182 lemma restrict_upd[simp]:
   183   "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
   184   by (auto simp: fun_eq_iff)
   185 
   186 lemma Pi_eq_subset:
   187   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   188   assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
   189   shows "F i \<subseteq> F' i"
   190 proof
   191   fix x assume "x \<in> F i"
   192   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
   193   from choice[OF this] guess f .. note f = this
   194   then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   195   then have "f \<in> Pi\<^isub>E I F'" using assms by simp
   196   then show "x \<in> F' i" using f `i \<in> I` by auto
   197 qed
   198 
   199 lemma Pi_eq_iff_not_empty:
   200   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   201   shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   202 proof (intro iffI ballI)
   203   fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
   204   show "F i = F' i"
   205     using Pi_eq_subset[of I F F', OF ne eq i]
   206     using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   207     by auto
   208 qed auto
   209 
   210 lemma Pi_eq_empty_iff:
   211   "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   212 proof
   213   assume "Pi\<^isub>E I F = {}"
   214   show "\<exists>i\<in>I. F i = {}"
   215   proof (rule ccontr)
   216     assume "\<not> ?thesis"
   217     then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
   218     from choice[OF this] guess f ..
   219     then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   220     with `Pi\<^isub>E I F = {}` show False by auto
   221   qed
   222 qed auto
   223 
   224 lemma Pi_eq_iff:
   225   "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 = {}))"
   226 proof (intro iffI disjCI)
   227   assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   228   assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   229   then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   230     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   231   with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
   232 next
   233   assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   234   then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   235     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   236 qed
   237 
   238 section "Finite product spaces"
   239 
   240 section "Products"
   241 
   242 definition prod_emb where
   243   "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
   244 
   245 lemma prod_emb_iff: 
   246   "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
   247   unfolding prod_emb_def by auto
   248 
   249 lemma
   250   shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
   251     and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B"
   252     and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B"
   253     and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))"
   254     and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))"
   255     and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
   256   by (auto simp: prod_emb_def)
   257 
   258 lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
   259     prod_emb I M J (\<Pi>\<^isub>E i\<in>J. E i) = (\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i))"
   260   by (force simp: prod_emb_def Pi_iff split_if_mem2)
   261 
   262 lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
   263   by (auto simp: prod_emb_def Pi_iff)
   264 
   265 lemma prod_emb_trans[simp]:
   266   "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
   267   by (auto simp add: Int_absorb1 prod_emb_def)
   268 
   269 lemma prod_emb_Pi:
   270   assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
   271   shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
   272   using assms space_closed
   273   by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
   274 
   275 lemma prod_emb_id:
   276   "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
   277   by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
   278 
   279 definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   280   "PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
   281     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
   282     (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j))
   283     (\<lambda>(J, X). \<Prod>j\<in>J \<union> {i\<in>I. emeasure (M i) (space (M i)) \<noteq> 1}. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
   284 
   285 definition prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
   286   "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j)) `
   287     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   288 
   289 abbreviation
   290   "Pi\<^isub>M I M \<equiv> PiM I M"
   291 
   292 syntax
   293   "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIM _:_./ _)" 10)
   294 
   295 syntax (xsymbols)
   296   "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"  10)
   297 
   298 syntax (HTML output)
   299   "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"  10)
   300 
   301 translations
   302   "PIM x:I. M" == "CONST PiM I (%x. M)"
   303 
   304 lemma prod_algebra_sets_into_space:
   305   "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
   306   using assms by (auto simp: prod_emb_def prod_algebra_def)
   307 
   308 lemma prod_algebra_eq_finite:
   309   assumes I: "finite I"
   310   shows "prod_algebra I M = {(\<Pi>\<^isub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R")
   311 proof (intro iffI set_eqI)
   312   fix A assume "A \<in> ?L"
   313   then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   314     and A: "A = prod_emb I M J (PIE j:J. E j)"
   315     by (auto simp: prod_algebra_def)
   316   let ?A = "\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i)"
   317   have A: "A = ?A"
   318     unfolding A using J by (intro prod_emb_PiE sets_into_space) auto
   319   show "A \<in> ?R" unfolding A using J top
   320     by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
   321 next
   322   fix A assume "A \<in> ?R"
   323   then obtain X where "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
   324   then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
   325     using sets_into_space by (force simp: prod_emb_def Pi_iff)
   326   from X I show "A \<in> ?L" unfolding A
   327     by (auto simp: prod_algebra_def)
   328 qed
   329 
   330 lemma prod_algebraI:
   331   "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
   332     \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
   333   by (auto simp: prod_algebra_def Pi_iff)
   334 
   335 lemma prod_algebraI_finite:
   336   "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
   337   using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
   338 
   339 lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
   340 proof (safe intro!: Int_stableI)
   341   fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   342   then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
   343     by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
   344 qed
   345 
   346 lemma prod_algebraE:
   347   assumes A: "A \<in> prod_algebra I M"
   348   obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
   349     "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)" 
   350   using A by (auto simp: prod_algebra_def)
   351 
   352 lemma prod_algebraE_all:
   353   assumes A: "A \<in> prod_algebra I M"
   354   obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
   355 proof -
   356   from A obtain E J where A: "A = prod_emb I M J (Pi\<^isub>E J E)"
   357     and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
   358     by (auto simp: prod_algebra_def)
   359   from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
   360     using sets_into_space by auto
   361   then have "A = (\<Pi>\<^isub>E i\<in>I. if i\<in>J then E i else space (M i))"
   362     using A J by (auto simp: prod_emb_PiE)
   363   moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
   364     using top E by auto
   365   ultimately show ?thesis using that by auto
   366 qed
   367 
   368 lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
   369 proof (unfold Int_stable_def, safe)
   370   fix A assume "A \<in> prod_algebra I M"
   371   from prod_algebraE[OF this] guess J E . note A = this
   372   fix B assume "B \<in> prod_algebra I M"
   373   from prod_algebraE[OF this] guess K F . note B = this
   374   have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^isub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter> 
   375       (if i \<in> K then F i else space (M i)))"
   376     unfolding A B using A(2,3,4) A(5)[THEN sets_into_space] B(2,3,4) B(5)[THEN sets_into_space]
   377     apply (subst (1 2 3) prod_emb_PiE)
   378     apply (simp_all add: subset_eq PiE_Int)
   379     apply blast
   380     apply (intro PiE_cong)
   381     apply auto
   382     done
   383   also have "\<dots> \<in> prod_algebra I M"
   384     using A B by (auto intro!: prod_algebraI)
   385   finally show "A \<inter> B \<in> prod_algebra I M" .
   386 qed
   387 
   388 lemma prod_algebra_mono:
   389   assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
   390   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
   391   shows "prod_algebra I E \<subseteq> prod_algebra I F"
   392 proof
   393   fix A assume "A \<in> prod_algebra I E"
   394   then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
   395     and A: "A = prod_emb I E J (\<Pi>\<^isub>E i\<in>J. G i)"
   396     and G: "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (E i)"
   397     by (auto simp: prod_algebra_def)
   398   moreover
   399   from space have "(\<Pi>\<^isub>E i\<in>I. space (E i)) = (\<Pi>\<^isub>E i\<in>I. space (F i))"
   400     by (rule PiE_cong)
   401   with A have "A = prod_emb I F J (\<Pi>\<^isub>E i\<in>J. G i)"
   402     by (simp add: prod_emb_def)
   403   moreover
   404   from sets G J have "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (F i)"
   405     by auto
   406   ultimately show "A \<in> prod_algebra I F"
   407     apply (simp add: prod_algebra_def image_iff)
   408     apply (intro exI[of _ J] exI[of _ G] conjI)
   409     apply auto
   410     done
   411 qed
   412 
   413 lemma space_PiM: "space (\<Pi>\<^isub>M i\<in>I. M i) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
   414   using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
   415 
   416 lemma sets_PiM: "sets (\<Pi>\<^isub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) (prod_algebra I M)"
   417   using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
   418 
   419 lemma sets_PiM_single: "sets (PiM I M) =
   420     sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}"
   421     (is "_ = sigma_sets ?\<Omega> ?R")
   422   unfolding sets_PiM
   423 proof (rule sigma_sets_eqI)
   424   interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
   425   fix A assume "A \<in> prod_algebra I M"
   426   from prod_algebraE[OF this] guess J X . note X = this
   427   show "A \<in> sigma_sets ?\<Omega> ?R"
   428   proof cases
   429     assume "I = {}"
   430     with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
   431     with `I = {}` show ?thesis by (auto intro!: sigma_sets_top)
   432   next
   433     assume "I \<noteq> {}"
   434     with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^isub>E i\<in>I. space (M i)). f j \<in> X j})"
   435       using sets_into_space[OF X(5)]
   436       by (auto simp: prod_emb_PiE[OF _ sets_into_space] Pi_iff split: split_if_asm) blast
   437     also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
   438       using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
   439     finally show "A \<in> sigma_sets ?\<Omega> ?R" .
   440   qed
   441 next
   442   fix A assume "A \<in> ?R"
   443   then obtain i B where A: "A = {f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)" 
   444     by auto
   445   then have "A = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. B)"
   446     using sets_into_space[OF A(3)]
   447     apply (subst prod_emb_PiE)
   448     apply (auto simp: Pi_iff split: split_if_asm)
   449     apply blast
   450     done
   451   also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
   452     using A by (intro sigma_sets.Basic prod_algebraI) auto
   453   finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
   454 qed
   455 
   456 lemma sets_PiM_I:
   457   assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   458   shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
   459 proof cases
   460   assume "J = {}"
   461   then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
   462     by (auto simp: prod_emb_def)
   463   then show ?thesis
   464     by (auto simp add: sets_PiM intro!: sigma_sets_top)
   465 next
   466   assume "J \<noteq> {}" with assms show ?thesis
   467     by (force simp add: sets_PiM prod_algebra_def)
   468 qed
   469 
   470 lemma measurable_PiM:
   471   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
   472   assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
   473     f -` prod_emb I M J (Pi\<^isub>E J X) \<inter> space N \<in> sets N" 
   474   shows "f \<in> measurable N (PiM I M)"
   475   using sets_PiM prod_algebra_sets_into_space space
   476 proof (rule measurable_sigma_sets)
   477   fix A assume "A \<in> prod_algebra I M"
   478   from prod_algebraE[OF this] guess J X .
   479   with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
   480 qed
   481 
   482 lemma measurable_PiM_Collect:
   483   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
   484   assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
   485     {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N" 
   486   shows "f \<in> measurable N (PiM I M)"
   487   using sets_PiM prod_algebra_sets_into_space space
   488 proof (rule measurable_sigma_sets)
   489   fix A assume "A \<in> prod_algebra I M"
   490   from prod_algebraE[OF this] guess J X . note X = this
   491   have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
   492     using sets_into_space[OF X(5)] X(2-) space unfolding X(1)
   493     by (subst prod_emb_PiE) (auto simp: Pi_iff split: split_if_asm)
   494   also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
   495   finally show "f -` A \<inter> space N \<in> sets N" .
   496 qed
   497 
   498 lemma measurable_PiM_single:
   499   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
   500   assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N" 
   501   shows "f \<in> measurable N (PiM I M)"
   502   using sets_PiM_single
   503 proof (rule measurable_sigma_sets)
   504   fix A assume "A \<in> {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   505   then obtain B i where "A = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" and B: "i \<in> I" "B \<in> sets (M i)"
   506     by auto
   507   with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto
   508   also have "\<dots> \<in> sets N" using B by (rule sets)
   509   finally show "f -` A \<inter> space N \<in> sets N" .
   510 qed (auto simp: space)
   511 
   512 lemma sets_PiM_I_finite[measurable]:
   513   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   514   shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
   515   using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
   516 
   517 lemma measurable_component_singleton:
   518   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
   519 proof (unfold measurable_def, intro CollectI conjI ballI)
   520   fix A assume "A \<in> sets (M i)"
   521   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)"
   522     using sets_into_space `i \<in> I`
   523     by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
   524   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
   525     using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
   526 qed (insert `i \<in> I`, auto simp: space_PiM)
   527 
   528 lemma measurable_component_singleton'[measurable_app]:
   529   assumes f: "f \<in> measurable N (Pi\<^isub>M I M)"
   530   assumes i: "i \<in> I"
   531   shows "(\<lambda>x. (f x) i) \<in> measurable N (M i)"
   532   using measurable_compose[OF f measurable_component_singleton, OF i] .
   533 
   534 lemma measurable_nat_case[measurable (raw)]:
   535   assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
   536     "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
   537   shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
   538   by (cases i) simp_all
   539 
   540 lemma measurable_add_dim[measurable]:
   541   "(\<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)"
   542     (is "?f \<in> measurable ?P ?I")
   543 proof (rule measurable_PiM_single)
   544   fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
   545   have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
   546     (if j = i then space (Pi\<^isub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
   547     using sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
   548   also have "\<dots> \<in> sets ?P"
   549     using A j
   550     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   551   finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
   552 qed (auto simp: space_pair_measure space_PiM)
   553 
   554 lemma measurable_component_update:
   555   "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
   556   by simp
   557 
   558 lemma measurable_merge[measurable]:
   559   "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
   560     (is "?f \<in> measurable ?P ?U")
   561 proof (rule measurable_PiM_single)
   562   fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
   563   then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
   564     (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
   565     by (auto simp: merge_def)
   566   also have "\<dots> \<in> sets ?P"
   567     using A
   568     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   569   finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
   570 qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
   571 
   572 lemma measurable_restrict[measurable (raw)]:
   573   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
   574   shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
   575 proof (rule measurable_PiM_single)
   576   fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
   577   then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N"
   578     by auto
   579   then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
   580     using A X by (auto intro!: measurable_sets)
   581 qed (insert X, auto dest: measurable_space)
   582 
   583 lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
   584   by (intro measurable_restrict measurable_component_singleton) auto
   585 
   586 lemma measurable_prod_emb[intro, simp]:
   587   "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
   588   unfolding prod_emb_def space_PiM[symmetric]
   589   by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
   590 
   591 lemma sets_in_Pi_aux:
   592   "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   593   {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
   594   by (simp add: subset_eq Pi_iff)
   595 
   596 lemma sets_in_Pi[measurable (raw)]:
   597   "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   598   (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   599   Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
   600   unfolding pred_def
   601   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
   602 
   603 lemma sets_in_extensional_aux:
   604   "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
   605 proof -
   606   have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
   607     by (auto simp add: extensional_def space_PiM)
   608   then show ?thesis by simp
   609 qed
   610 
   611 lemma sets_in_extensional[measurable (raw)]:
   612   "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
   613   unfolding pred_def
   614   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
   615 
   616 locale product_sigma_finite =
   617   fixes M :: "'i \<Rightarrow> 'a measure"
   618   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
   619 
   620 sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
   621   by (rule sigma_finite_measures)
   622 
   623 locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
   624   fixes I :: "'i set"
   625   assumes finite_index: "finite I"
   626 
   627 lemma (in finite_product_sigma_finite) sigma_finite_pairs:
   628   "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
   629     (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
   630     (\<forall>k. \<forall>i\<in>I. emeasure (M i) (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k) \<and>
   631     (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space (PiM I M)"
   632 proof -
   633   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. emeasure (M i) (F k) \<noteq> \<infinity>)"
   634     using M.sigma_finite_incseq by metis
   635   from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   636   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. emeasure (M i) (F i k) \<noteq> \<infinity>"
   637     by auto
   638   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k"
   639   note space_PiM[simp]
   640   show ?thesis
   641   proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
   642     fix i show "range (F i) \<subseteq> sets (M i)" by fact
   643   next
   644     fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
   645   next
   646     fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space (PiM I M)"
   647       using `\<And>i. range (F i) \<subseteq> sets (M i)` sets_into_space
   648       by auto blast
   649   next
   650     fix f assume "f \<in> space (PiM I M)"
   651     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
   652     show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
   653   next
   654     fix i show "?F i \<subseteq> ?F (Suc i)"
   655       using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
   656   qed
   657 qed
   658 
   659 lemma
   660   shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
   661     and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
   662   by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   663 
   664 lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   665 proof -
   666   let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
   667   have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
   668   proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   669     show "positive (PiM {} M) ?\<mu>"
   670       by (auto simp: positive_def)
   671     show "countably_additive (PiM {} M) ?\<mu>"
   672       by (rule countably_additiveI_finite)
   673          (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
   674   qed (auto simp: prod_emb_def)
   675   also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
   676     by (auto simp: prod_emb_def)
   677   finally show ?thesis
   678     by simp
   679 qed
   680 
   681 lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
   682   by (rule measure_eqI) (auto simp add: sets_PiM_empty one_ereal_def)
   683 
   684 lemma (in product_sigma_finite) emeasure_PiM:
   685   "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   686 proof (induct I arbitrary: A rule: finite_induct)
   687   case (insert i I)
   688   interpret finite_product_sigma_finite M I by default fact
   689   have "finite (insert i I)" using `finite I` by auto
   690   interpret I': finite_product_sigma_finite M "insert i I" by default fact
   691   let ?h = "(\<lambda>(f, y). f(i := y))"
   692 
   693   let ?P = "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M) ?h"
   694   let ?\<mu> = "emeasure ?P"
   695   let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
   696   let ?f = "\<lambda>J E j. if j \<in> J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
   697 
   698   have "emeasure (Pi\<^isub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^isub>E (insert i I) A)) =
   699     (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
   700   proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   701     fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
   702     then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
   703     let ?p = "prod_emb (insert i I) M J (Pi\<^isub>E J E)"
   704     let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^isub>E j\<in>J-{i}. E j)"
   705     have "?\<mu> ?p =
   706       emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
   707       by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
   708     also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
   709       using J E[rule_format, THEN sets_into_space]
   710       by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
   711     also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
   712       emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
   713       using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
   714     also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
   715       using J E[rule_format, THEN sets_into_space]
   716       by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
   717     also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
   718       (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
   719       using E by (subst insert) (auto intro!: setprod_cong)
   720     also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
   721        emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
   722       using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong)
   723     also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
   724       using insert(1,2) J E by (intro setprod_mono_one_right) auto
   725     finally show "?\<mu> ?p = \<dots>" .
   726 
   727     show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
   728       using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
   729   next
   730     show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
   731       using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
   732   next
   733     show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
   734       insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
   735       using insert by auto
   736   qed (auto intro!: setprod_cong)
   737   with insert show ?case
   738     by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
   739 qed simp
   740 
   741 lemma (in product_sigma_finite) sigma_finite: 
   742   assumes "finite I"
   743   shows "sigma_finite_measure (PiM I M)"
   744 proof -
   745   interpret finite_product_sigma_finite M I by default fact
   746 
   747   from sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   748   then have F: "\<And>j. j \<in> I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
   749     "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k)"
   750     "(\<Union>k. \<Pi>\<^isub>E j \<in> I. F j k) = space (Pi\<^isub>M I M)"
   751     "\<And>k. \<And>j. j \<in> I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
   752     by blast+
   753   let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> I. F j k"
   754 
   755   show ?thesis
   756   proof (unfold_locales, intro exI[of _ ?F] conjI allI)
   757     show "range ?F \<subseteq> sets (Pi\<^isub>M I M)" using F(1) `finite I` by auto
   758   next
   759     from F(3) show "(\<Union>i. ?F i) = space (Pi\<^isub>M I M)" by simp
   760   next
   761     fix j
   762     from F `finite I` setprod_PInf[of I, OF emeasure_nonneg, of M]
   763     show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (?F j) \<noteq> \<infinity>"
   764       by (subst emeasure_PiM) auto
   765   qed
   766 qed
   767 
   768 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^isub>M I M"
   769   using sigma_finite[OF finite_index] .
   770 
   771 lemma (in finite_product_sigma_finite) measure_times:
   772   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^isub>M I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   773   using emeasure_PiM[OF finite_index] by auto
   774 
   775 lemma (in product_sigma_finite) positive_integral_empty:
   776   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   777   shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
   778 proof -
   779   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
   780   have "\<And>A. emeasure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
   781     using assms by (subst measure_times) auto
   782   then show ?thesis
   783     unfolding positive_integral_def simple_function_def simple_integral_def[abs_def]
   784   proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
   785     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
   786       by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
   787     show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
   788       by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)
   789   qed
   790 qed
   791 
   792 lemma (in product_sigma_finite) distr_merge:
   793   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   794   shows "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M) (merge I J) = Pi\<^isub>M (I \<union> J) M"
   795    (is "?D = ?P")
   796 proof -
   797   interpret I: finite_product_sigma_finite M I by default fact
   798   interpret J: finite_product_sigma_finite M J by default fact
   799   have "finite (I \<union> J)" using fin by auto
   800   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   801   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   802   let ?g = "merge I J"
   803 
   804   from IJ.sigma_finite_pairs obtain F where
   805     F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   806        "incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
   807        "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space ?P"
   808        "\<And>k. \<forall>i\<in>I\<union>J. emeasure (M i) (F i k) \<noteq> \<infinity>"
   809     by auto
   810   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
   811   
   812   show ?thesis
   813   proof (rule measure_eqI_generator_eq[symmetric])
   814     show "Int_stable (prod_algebra (I \<union> J) M)"
   815       by (rule Int_stable_prod_algebra)
   816     show "prod_algebra (I \<union> J) M \<subseteq> Pow (\<Pi>\<^isub>E i \<in> I \<union> J. space (M i))"
   817       by (rule prod_algebra_sets_into_space)
   818     show "sets ?P = sigma_sets (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
   819       by (rule sets_PiM)
   820     then show "sets ?D = sigma_sets (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
   821       by simp
   822 
   823     show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
   824       using fin by (auto simp: prod_algebra_eq_finite)
   825     show "(\<Union>i. \<Pi>\<^isub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i))"
   826       using F(3) by (simp add: space_PiM)
   827   next
   828     fix k
   829     from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M]
   830     show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
   831   next
   832     fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
   833     with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   834       by (auto simp add: prod_algebra_eq_finite)
   835     let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
   836     let ?X = "?g -` A \<inter> space ?B"
   837     have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
   838       using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
   839     then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   840       unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
   841     have "emeasure ?D A = emeasure ?B ?X"
   842       using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
   843     also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
   844       using `finite J` `finite I` F unfolding X
   845       by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
   846     also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
   847       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   848     also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
   849       using `finite J` `finite I` F unfolding A
   850       by (intro IJ.measure_times[symmetric]) auto
   851     finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp
   852   qed
   853 qed
   854 
   855 lemma (in product_sigma_finite) product_positive_integral_fold:
   856   assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   857   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   858   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
   859     (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
   860 proof -
   861   interpret I: finite_product_sigma_finite M I by default fact
   862   interpret J: finite_product_sigma_finite M J by default fact
   863   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   864   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   865     using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   866   show ?thesis
   867     apply (subst distr_merge[OF IJ, symmetric])
   868     apply (subst positive_integral_distr[OF measurable_merge f])
   869     apply (subst J.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
   870     apply simp
   871     done
   872 qed
   873 
   874 lemma (in product_sigma_finite) distr_singleton:
   875   "distr (Pi\<^isub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
   876 proof (intro measure_eqI[symmetric])
   877   interpret I: finite_product_sigma_finite M "{i}" by default simp
   878   fix A assume A: "A \<in> sets (M i)"
   879   moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M {i} M) = (\<Pi>\<^isub>E i\<in>{i}. A)"
   880     using sets_into_space by (auto simp: space_PiM)
   881   ultimately show "emeasure (M i) A = emeasure ?D A"
   882     using A I.measure_times[of "\<lambda>_. A"]
   883     by (simp add: emeasure_distr measurable_component_singleton)
   884 qed simp
   885 
   886 lemma (in product_sigma_finite) product_positive_integral_singleton:
   887   assumes f: "f \<in> borel_measurable (M i)"
   888   shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
   889 proof -
   890   interpret I: finite_product_sigma_finite M "{i}" by default simp
   891   from f show ?thesis
   892     apply (subst distr_singleton[symmetric])
   893     apply (subst positive_integral_distr[OF measurable_component_singleton])
   894     apply simp_all
   895     done
   896 qed
   897 
   898 lemma (in product_sigma_finite) product_positive_integral_insert:
   899   assumes I[simp]: "finite I" "i \<notin> I"
   900     and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
   901   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))"
   902 proof -
   903   interpret I: finite_product_sigma_finite M I by default auto
   904   interpret i: finite_product_sigma_finite M "{i}" by default auto
   905   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
   906     using f by auto
   907   show ?thesis
   908     unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
   909   proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
   910     fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
   911     let ?f = "\<lambda>y. f (x(i := y))"
   912     show "?f \<in> borel_measurable (M i)"
   913       using measurable_comp[OF measurable_component_update f, OF x `i \<notin> I`]
   914       unfolding comp_def .
   915     show "(\<integral>\<^isup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^isub>M {i} M) = (\<integral>\<^isup>+ y. f (x(i := y i)) \<partial>Pi\<^isub>M {i} M)"
   916       using x
   917       by (auto intro!: positive_integral_cong arg_cong[where f=f]
   918                simp add: space_PiM extensional_def)
   919   qed
   920 qed
   921 
   922 lemma (in product_sigma_finite) product_positive_integral_setprod:
   923   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
   924   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   925   and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
   926   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))"
   927 using assms proof induct
   928   case (insert i I)
   929   note `finite I`[intro, simp]
   930   interpret I: finite_product_sigma_finite M I by default auto
   931   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))"
   932     using insert by (auto intro!: setprod_cong)
   933   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)"
   934     using sets_into_space insert
   935     by (intro borel_measurable_ereal_setprod
   936               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
   937        auto
   938   then show ?case
   939     apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
   940     apply (simp add: insert(2-) * pos borel setprod_ereal_pos positive_integral_multc)
   941     apply (subst positive_integral_cmult)
   942     apply (auto simp add: pos borel insert(2-) setprod_ereal_pos positive_integral_positive)
   943     done
   944 qed (simp add: space_PiM)
   945 
   946 lemma (in product_sigma_finite) product_integral_singleton:
   947   assumes f: "f \<in> borel_measurable (M i)"
   948   shows "(\<integral>x. f (x i) \<partial>Pi\<^isub>M {i} M) = integral\<^isup>L (M i) f"
   949 proof -
   950   interpret I: finite_product_sigma_finite M "{i}" by default simp
   951   have *: "(\<lambda>x. ereal (f x)) \<in> borel_measurable (M i)"
   952     "(\<lambda>x. ereal (- f x)) \<in> borel_measurable (M i)"
   953     using assms by auto
   954   show ?thesis
   955     unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
   956 qed
   957 
   958 lemma (in product_sigma_finite) product_integral_fold:
   959   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   960   and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
   961   shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
   962 proof -
   963   interpret I: finite_product_sigma_finite M I by default fact
   964   interpret J: finite_product_sigma_finite M J by default fact
   965   have "finite (I \<union> J)" using fin by auto
   966   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   967   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   968   let ?M = "merge I J"
   969   let ?f = "\<lambda>x. f (?M x)"
   970   from f have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   971     by auto
   972   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   973     using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
   974   have f_int: "integrable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ?f"
   975     by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
   976   show ?thesis
   977     apply (subst distr_merge[symmetric, OF IJ fin])
   978     apply (subst integral_distr[OF measurable_merge f_borel])
   979     apply (subst P.integrable_fst_measurable(2)[symmetric, OF f_int])
   980     apply simp
   981     done
   982 qed
   983 
   984 lemma (in product_sigma_finite)
   985   assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   986   shows emeasure_fold_integral:
   987     "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
   988     and emeasure_fold_measurable:
   989     "(\<lambda>x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
   990 proof -
   991   interpret I: finite_product_sigma_finite M I by default fact
   992   interpret J: finite_product_sigma_finite M J by default fact
   993   interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
   994   have merge: "merge I J -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   995     by (intro measurable_sets[OF _ A] measurable_merge assms)
   996 
   997   show ?I
   998     apply (subst distr_merge[symmetric, OF IJ])
   999     apply (subst emeasure_distr[OF measurable_merge A])
  1000     apply (subst J.emeasure_pair_measure_alt[OF merge])
  1001     apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
  1002     done
  1003 
  1004   show ?B
  1005     using IJ.measurable_emeasure_Pair1[OF merge]
  1006     by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
  1007 qed
  1008 
  1009 lemma (in product_sigma_finite) product_integral_insert:
  1010   assumes I: "finite I" "i \<notin> I"
  1011     and f: "integrable (Pi\<^isub>M (insert i I) M) f"
  1012   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)"
  1013 proof -
  1014   have "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = integral\<^isup>L (Pi\<^isub>M (I \<union> {i}) M) f"
  1015     by simp
  1016   also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
  1017     using f I by (intro product_integral_fold) auto
  1018   also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
  1019   proof (rule integral_cong, subst product_integral_singleton[symmetric])
  1020     fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
  1021     have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
  1022       using f by auto
  1023     show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
  1024       using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
  1025       unfolding comp_def .
  1026     from x I show "(\<integral> y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
  1027       by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
  1028   qed
  1029   finally show ?thesis .
  1030 qed
  1031 
  1032 lemma (in product_sigma_finite) product_integrable_setprod:
  1033   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
  1034   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1035   shows "integrable (Pi\<^isub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  1036 proof -
  1037   interpret finite_product_sigma_finite M I by default fact
  1038   have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
  1039     using integrable unfolding integrable_def by auto
  1040   have borel: "?f \<in> borel_measurable (Pi\<^isub>M I M)"
  1041     using measurable_comp[OF measurable_component_singleton[of _ I M] f] by (auto simp: comp_def)
  1042   moreover have "integrable (Pi\<^isub>M I M) (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
  1043   proof (unfold integrable_def, intro conjI)
  1044     show "(\<lambda>x. abs (?f x)) \<in> borel_measurable (Pi\<^isub>M I M)"
  1045       using borel by auto
  1046     have "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>Pi\<^isub>M I M) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. ereal (abs (f i (x i)))) \<partial>Pi\<^isub>M I M)"
  1047       by (simp add: setprod_ereal abs_setprod)
  1048     also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^isup>+x. ereal (abs (f i x)) \<partial>M i))"
  1049       using f by (subst product_positive_integral_setprod) auto
  1050     also have "\<dots> < \<infinity>"
  1051       using integrable[THEN integrable_abs]
  1052       by (simp add: setprod_PInf integrable_def positive_integral_positive)
  1053     finally show "(\<integral>\<^isup>+x. ereal (abs (?f x)) \<partial>(Pi\<^isub>M I M)) \<noteq> \<infinity>" by auto
  1054     have "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>(Pi\<^isub>M I M)) = (\<integral>\<^isup>+x. 0 \<partial>(Pi\<^isub>M I M))"
  1055       by (intro positive_integral_cong_pos) auto
  1056     then show "(\<integral>\<^isup>+x. ereal (- abs (?f x)) \<partial>(Pi\<^isub>M I M)) \<noteq> \<infinity>" by simp
  1057   qed
  1058   ultimately show ?thesis
  1059     by (rule integrable_abs_iff[THEN iffD1])
  1060 qed
  1061 
  1062 lemma (in product_sigma_finite) product_integral_setprod:
  1063   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
  1064   assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1065   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))"
  1066 using assms proof induct
  1067   case empty
  1068   interpret finite_measure "Pi\<^isub>M {} M"
  1069     by rule (simp add: space_PiM)
  1070   show ?case by (simp add: space_PiM measure_def)
  1071 next
  1072   case (insert i I)
  1073   then have iI: "finite (insert i I)" by auto
  1074   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  1075     integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  1076     by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
  1077   interpret I: finite_product_sigma_finite M I by default fact
  1078   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))"
  1079     using `i \<notin> I` by (auto intro!: setprod_cong)
  1080   show ?case
  1081     unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
  1082     by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
  1083 qed
  1084 
  1085 lemma sets_Collect_single:
  1086   "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
  1087   by simp
  1088 
  1089 lemma sigma_prod_algebra_sigma_eq_infinite:
  1090   fixes E :: "'i \<Rightarrow> 'a set set"
  1091   assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
  1092     and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
  1093   assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
  1094     and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
  1095   defines "P == {{f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> E i}"
  1096   shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
  1097 proof
  1098   let ?P = "sigma (space (Pi\<^isub>M I M)) P"
  1099   have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
  1100     using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
  1101   then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
  1102     by (simp add: space_PiM)
  1103   have "sets (PiM I M) =
  1104       sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
  1105     using sets_PiM_single[of I M] by (simp add: space_P)
  1106   also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
  1107   proof (safe intro!: sigma_sets_subset)
  1108     fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
  1109     then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
  1110       apply (subst measurable_iff_measure_of)
  1111       apply (simp_all add: P_closed)
  1112       using E_closed
  1113       apply (force simp: subset_eq space_PiM)
  1114       apply (force simp: subset_eq space_PiM)
  1115       apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
  1116       apply (rule_tac x=Aa in exI)
  1117       apply (auto simp: space_PiM)
  1118       done
  1119     from measurable_sets[OF this, of A] A `i \<in> I` E_closed
  1120     have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
  1121       by (simp add: E_generates)
  1122     also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A}"
  1123       using P_closed by (auto simp: space_PiM)
  1124     finally show "\<dots> \<in> sets ?P" .
  1125   qed
  1126   finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
  1127     by (simp add: P_closed)
  1128   show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
  1129     unfolding P_def space_PiM[symmetric]
  1130     by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
  1131 qed
  1132 
  1133 lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
  1134   by metis
  1135 
  1136 lemma sigma_prod_algebra_sigma_eq:
  1137   fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
  1138   assumes "finite I"
  1139   assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
  1140     and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
  1141   assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
  1142     and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
  1143   defines "P == { Pi\<^isub>E I F | F. \<forall>i\<in>I. F i \<in> E i }"
  1144   shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
  1145 proof
  1146   let ?P = "sigma (space (Pi\<^isub>M I M)) P"
  1147   from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
  1148   then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
  1149     by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
  1150   have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
  1151     using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
  1152   then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
  1153     by (simp add: space_PiM)
  1154   have "sets (PiM I M) =
  1155       sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
  1156     using sets_PiM_single[of I M] by (simp add: space_P)
  1157   also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
  1158   proof (safe intro!: sigma_sets_subset)
  1159     fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
  1160     have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
  1161     proof (subst measurable_iff_measure_of)
  1162       show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
  1163       from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)"
  1164         by (auto simp: Pi_iff)
  1165       show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
  1166       proof
  1167         fix A assume A: "A \<in> E i"
  1168         then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
  1169           using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
  1170         also have "\<dots> = (\<Pi>\<^isub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
  1171           by (intro PiE_cong) (simp add: S_union)
  1172         also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j))"
  1173           using T
  1174           apply (auto simp: Pi_iff bchoice_iff)
  1175           apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
  1176           apply (auto simp: bij_betw_def)
  1177           done
  1178         also have "\<dots> \<in> sets ?P"
  1179         proof (safe intro!: countable_UN)
  1180           fix xs show "(\<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
  1181             using A S_in_E
  1182             by (simp add: P_closed)
  1183                (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
  1184         qed
  1185         finally show "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
  1186           using P_closed by simp
  1187       qed
  1188     qed
  1189     from measurable_sets[OF this, of A] A `i \<in> I` E_closed
  1190     have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
  1191       by (simp add: E_generates)
  1192     also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A}"
  1193       using P_closed by (auto simp: space_PiM)
  1194     finally show "\<dots> \<in> sets ?P" .
  1195   qed
  1196   finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
  1197     by (simp add: P_closed)
  1198   show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
  1199     using `finite I`
  1200     by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
  1201 qed
  1202 
  1203 end