src/HOL/Analysis/Finite_Product_Measure.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69918 eddcc7c726f3
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/Finite_Product_Measure.thy
     2     Author:     Johannes Hölzl, TU München
     3 *)
     4 
     5 section \<open>Finite Product Measure\<close>
     6 
     7 theory Finite_Product_Measure
     8 imports Binary_Product_Measure Function_Topology
     9 begin
    10 
    11 lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
    12   by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
    13      (force intro: exI[of _ "restrict f I" for f])
    14 
    15 lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    16   by auto
    17 
    18 subsection%unimportant \<open>More about Function restricted by \<^const>\<open>extensional\<close>\<close>
    19 
    20 definition
    21   "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    22 
    23 lemma merge_apply[simp]:
    24   "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    25   "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    26   "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    27   "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    28   "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined"
    29   unfolding merge_def by auto
    30 
    31 lemma merge_commute:
    32   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
    33   by (force simp: merge_def)
    34 
    35 lemma Pi_cancel_merge_range[simp]:
    36   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    37   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    38   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    39   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    40   by (auto simp: Pi_def)
    41 
    42 lemma Pi_cancel_merge[simp]:
    43   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    44   "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    45   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    46   "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    47   by (auto simp: Pi_def)
    48 
    49 lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
    50   by (auto simp: extensional_def)
    51 
    52 lemma restrict_merge[simp]:
    53   "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    54   "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    55   "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    56   "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    57   by (auto simp: restrict_def)
    58 
    59 lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
    60   unfolding merge_def by auto
    61 
    62 lemma PiE_cancel_merge[simp]:
    63   "I \<inter> J = {} \<Longrightarrow>
    64     merge I J (x, y) \<in> Pi\<^sub>E (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
    65   by (auto simp: PiE_def restrict_Pi_cancel)
    66 
    67 lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
    68   unfolding merge_def by (auto simp: fun_eq_iff)
    69 
    70 lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
    71   unfolding merge_def extensional_def by auto
    72 
    73 lemma merge_restrict[simp]:
    74   "merge I J (restrict x I, y) = merge I J (x, y)"
    75   "merge I J (x, restrict y J) = merge I J (x, y)"
    76   unfolding merge_def by auto
    77 
    78 lemma merge_x_x_eq_restrict[simp]:
    79   "merge I J (x, x) = restrict x (I \<union> J)"
    80   unfolding merge_def by auto
    81 
    82 lemma injective_vimage_restrict:
    83   assumes J: "J \<subseteq> I"
    84   and sets: "A \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" and ne: "(\<Pi>\<^sub>E i\<in>I. S i) \<noteq> {}"
    85   and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
    86   shows "A = B"
    87 proof  (intro set_eqI)
    88   fix x
    89   from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
    90   have "J \<inter> (I - J) = {}" by auto
    91   show "x \<in> A \<longleftrightarrow> x \<in> B"
    92   proof cases
    93     assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)"
    94     have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
    95       using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S]
    96       by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    97     then show "x \<in> A \<longleftrightarrow> x \<in> B"
    98       using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S]
    99       by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
   100   qed (insert sets, auto)
   101 qed
   102 
   103 lemma restrict_vimage:
   104   "I \<inter> J = {} \<Longrightarrow>
   105     (\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^sub>E I E \<times> Pi\<^sub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
   106   by (auto simp: restrict_Pi_cancel PiE_def)
   107 
   108 lemma merge_vimage:
   109   "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   110   by (auto simp: restrict_Pi_cancel PiE_def)
   111 
   112 subsection \<open>Finite product spaces\<close>
   113 
   114 definition%important prod_emb where
   115   "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   116 
   117 lemma prod_emb_iff:
   118   "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))"
   119   unfolding%unimportant prod_emb_def PiE_def by auto
   120 
   121 lemma
   122   shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
   123     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"
   124     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"
   125     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))"
   126     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))"
   127     and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
   128   by (auto simp: prod_emb_def)
   129 
   130 lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
   131     prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))"
   132   by (force simp: prod_emb_def PiE_iff if_split_mem2)
   133 
   134 lemma prod_emb_PiE_same_index[simp]:
   135     "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E"
   136   by (auto simp: prod_emb_def PiE_iff)
   137 
   138 lemma prod_emb_trans[simp]:
   139   "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"
   140   by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
   141 
   142 lemma prod_emb_Pi:
   143   assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
   144   shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))"
   145   using assms sets.space_closed
   146   by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+
   147 
   148 lemma prod_emb_id:
   149   "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
   150   by (auto simp: prod_emb_def subset_eq extensional_restrict)
   151 
   152 lemma prod_emb_mono:
   153   "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
   154   by (auto simp: prod_emb_def)
   155 
   156 definition%important PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   157   "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
   158     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
   159     (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
   160     (\<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)))"
   161 
   162 definition%important prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
   163   "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j)) `
   164     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   165 
   166 abbreviation
   167   "Pi\<^sub>M I M \<equiv> PiM I M"
   168 
   169 syntax
   170   "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
   171 translations
   172   "\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
   173 
   174 lemma extend_measure_cong:
   175   assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
   176   shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
   177   unfolding extend_measure_def by (auto simp add: assms)
   178 
   179 lemma Pi_cong_sets:
   180     "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
   181   unfolding Pi_def by auto
   182 
   183 lemma PiM_cong:
   184   assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
   185   shows "PiM I M = PiM J N"
   186   unfolding PiM_def
   187 proof (rule extend_measure_cong, goal_cases)
   188   case 1
   189   show ?case using assms
   190     by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
   191 next
   192   case 2
   193   have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
   194     using assms by (intro Pi_cong_sets) auto
   195   thus ?case by (auto simp: assms)
   196 next
   197   case 3
   198   show ?case using assms
   199     by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
   200 next
   201   case (4 x)
   202   thus ?case using assms
   203     by (auto intro!: prod.cong split: if_split_asm)
   204 qed
   205 
   206 
   207 lemma prod_algebra_sets_into_space:
   208   "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
   209   by (auto simp: prod_emb_def prod_algebra_def)
   210 
   211 lemma prod_algebra_eq_finite:
   212   assumes I: "finite I"
   213   shows "prod_algebra I M = {(\<Pi>\<^sub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R")
   214 proof (intro iffI set_eqI)
   215   fix A assume "A \<in> ?L"
   216   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)"
   217     and A: "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   218     by (auto simp: prod_algebra_def)
   219   let ?A = "\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i)"
   220   have A: "A = ?A"
   221     unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
   222   show "A \<in> ?R" unfolding A using J sets.top
   223     by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
   224 next
   225   fix A assume "A \<in> ?R"
   226   then obtain X where A: "A = (\<Pi>\<^sub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
   227   then have A: "A = prod_emb I M I (\<Pi>\<^sub>E i\<in>I. X i)"
   228     by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
   229   from X I show "A \<in> ?L" unfolding A
   230     by (auto simp: prod_algebra_def)
   231 qed
   232 
   233 lemma prod_algebraI:
   234   "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
   235     \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M"
   236   by (auto simp: prod_algebra_def)
   237 
   238 lemma prod_algebraI_finite:
   239   "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>E I E) \<in> prod_algebra I M"
   240   using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
   241 
   242 lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
   243 proof (safe intro!: Int_stableI)
   244   fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   245   then show "\<exists>G. Pi\<^sub>E J E \<inter> Pi\<^sub>E J F = Pi\<^sub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
   246     by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
   247 qed
   248 
   249 lemma prod_algebraE:
   250   assumes A: "A \<in> prod_algebra I M"
   251   obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   252     "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
   253   using A by (auto simp: prod_algebra_def)
   254 
   255 lemma prod_algebraE_all:
   256   assumes A: "A \<in> prod_algebra I M"
   257   obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
   258 proof -
   259   from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)"
   260     and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
   261     by (auto simp: prod_algebra_def)
   262   from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
   263     using sets.sets_into_space by auto
   264   then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
   265     using A J by (auto simp: prod_emb_PiE)
   266   moreover have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
   267     using sets.top E by auto
   268   ultimately show ?thesis using that by auto
   269 qed
   270 
   271 lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
   272 proof (unfold Int_stable_def, safe)
   273   fix A assume "A \<in> prod_algebra I M"
   274   from prod_algebraE[OF this] guess J E . note A = this
   275   fix B assume "B \<in> prod_algebra I M"
   276   from prod_algebraE[OF this] guess K F . note B = this
   277   have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^sub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter>
   278       (if i \<in> K then F i else space (M i)))"
   279     unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
   280       B(5)[THEN sets.sets_into_space]
   281     apply (subst (1 2 3) prod_emb_PiE)
   282     apply (simp_all add: subset_eq PiE_Int)
   283     apply blast
   284     apply (intro PiE_cong)
   285     apply auto
   286     done
   287   also have "\<dots> \<in> prod_algebra I M"
   288     using A B by (auto intro!: prod_algebraI)
   289   finally show "A \<inter> B \<in> prod_algebra I M" .
   290 qed
   291 
   292 proposition prod_algebra_mono:
   293   assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
   294   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
   295   shows "prod_algebra I E \<subseteq> prod_algebra I F"
   296 proof
   297   fix A assume "A \<in> prod_algebra I E"
   298   then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
   299     and A: "A = prod_emb I E J (\<Pi>\<^sub>E i\<in>J. G i)"
   300     and G: "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (E i)"
   301     by (auto simp: prod_algebra_def)
   302   moreover
   303   from space have "(\<Pi>\<^sub>E i\<in>I. space (E i)) = (\<Pi>\<^sub>E i\<in>I. space (F i))"
   304     by (rule PiE_cong)
   305   with A have "A = prod_emb I F J (\<Pi>\<^sub>E i\<in>J. G i)"
   306     by (simp add: prod_emb_def)
   307   moreover
   308   from sets G J have "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (F i)"
   309     by auto
   310   ultimately show "A \<in> prod_algebra I F"
   311     apply (simp add: prod_algebra_def image_iff)
   312     apply (intro exI[of _ J] exI[of _ G] conjI)
   313     apply auto
   314     done
   315 qed
   316 proposition prod_algebra_cong:
   317   assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
   318   shows "prod_algebra I M = prod_algebra J N"
   319 proof -
   320   have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
   321     using sets_eq_imp_space_eq[OF sets] by auto
   322   with sets show ?thesis unfolding \<open>I = J\<close>
   323     by (intro antisym prod_algebra_mono) auto
   324 qed
   325 
   326 lemma space_in_prod_algebra:
   327   "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
   328 proof cases
   329   assume "I = {}" then show ?thesis
   330     by (auto simp add: prod_algebra_def image_iff prod_emb_def)
   331 next
   332   assume "I \<noteq> {}"
   333   then obtain i where "i \<in> I" by auto
   334   then have "(\<Pi>\<^sub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
   335     by (auto simp: prod_emb_def)
   336   also have "\<dots> \<in> prod_algebra I M"
   337     using \<open>i \<in> I\<close> by (intro prod_algebraI) auto
   338   finally show ?thesis .
   339 qed
   340 
   341 lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   342   using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
   343 
   344 lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)"
   345   by (auto simp: prod_emb_def space_PiM)
   346 
   347 lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow>  (\<exists>i\<in>I. space (M i) = {})"
   348   by (auto simp: space_PiM PiE_eq_empty_iff)
   349 
   350 lemma undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)"
   351   by (auto simp: space_PiM)
   352 
   353 lemma sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
   354   using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
   355 
   356 proposition sets_PiM_single: "sets (PiM I M) =
   357     sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}"
   358     (is "_ = sigma_sets ?\<Omega> ?R")
   359   unfolding sets_PiM
   360 proof (rule sigma_sets_eqI)
   361   interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
   362   fix A assume "A \<in> prod_algebra I M"
   363   from prod_algebraE[OF this] guess J X . note X = this
   364   show "A \<in> sigma_sets ?\<Omega> ?R"
   365   proof cases
   366     assume "I = {}"
   367     with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
   368     with \<open>I = {}\<close> show ?thesis by (auto intro!: sigma_sets_top)
   369   next
   370     assume "I \<noteq> {}"
   371     with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^sub>E i\<in>I. space (M i)). f j \<in> X j})"
   372       by (auto simp: prod_emb_def)
   373     also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
   374       using X \<open>I \<noteq> {}\<close> by (intro R.finite_INT sigma_sets.Basic) auto
   375     finally show "A \<in> sigma_sets ?\<Omega> ?R" .
   376   qed
   377 next
   378   fix A assume "A \<in> ?R"
   379   then obtain i B where A: "A = {f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
   380     by auto
   381   then have "A = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. B)"
   382      by (auto simp: prod_emb_def)
   383   also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
   384     using A by (intro sigma_sets.Basic prod_algebraI) auto
   385   finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
   386 qed
   387 
   388 lemma sets_PiM_eq_proj:
   389   "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
   390   apply (simp add: sets_PiM_single)
   391   apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
   392   apply auto []
   393   apply auto []
   394   apply simp
   395   apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
   396   apply (rule sets_vimage_algebra2)
   397   apply (auto intro!: arg_cong2[where f=sigma_sets])
   398   done
   399 
   400 lemma
   401   shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
   402     and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
   403   by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   404 
   405 proposition sets_PiM_sigma:
   406   assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
   407   assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
   408   assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
   409   defines "P \<equiv> {{f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i} | A j. j \<in> J \<and> A \<in> Pi j E}"
   410   shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
   411 proof cases
   412   assume "I = {}"
   413   with \<open>\<Union>J = I\<close> have "P = {{\<lambda>_. undefined}} \<or> P = {}"
   414     by (auto simp: P_def)
   415   with \<open>I = {}\<close> show ?thesis
   416     by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
   417 next
   418   let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
   419   assume "I \<noteq> {}"
   420   then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
   421       sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
   422     by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
   423   also have "\<dots> = sets (SUP i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
   424     using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
   425   also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
   426     using \<open>I \<noteq> {}\<close> by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
   427   also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
   428   proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
   429     show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
   430       by (auto simp: P_def)
   431   next
   432     interpret P: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
   433       by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
   434 
   435     fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
   436     then obtain i A where i: "i \<in> I" "A \<in> E i" and Z_def: "Z = (\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega>"
   437       by auto
   438     from \<open>i \<in> I\<close> J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
   439       by auto
   440     obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)"
   441       "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
   442       by (metis subset_eq \<Omega>_cover \<open>j \<subseteq> I\<close>)
   443     define A' where "A' n = n(i := A)" for n
   444     then have A'_i: "\<And>n. A' n i = A"
   445       by simp
   446     { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
   447       then have "A' n \<in> Pi j E"
   448         unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def \<open>A \<in> E i\<close> )
   449       with \<open>j \<in> J\<close> have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
   450         by (auto simp: P_def) }
   451     note A'_in_P = this
   452 
   453     { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
   454       with S(3) \<open>j \<subseteq> I\<close> have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
   455         by (auto simp: PiE_def Pi_def)
   456       then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
   457         by metis
   458       with \<open>x i \<in> A\<close> have "\<exists>n\<in>Pi\<^sub>E (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
   459         by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
   460     then have "Z = (\<Union>n\<in>Pi\<^sub>E (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
   461       unfolding Z_def
   462       by (auto simp add: set_eq_iff ball_conj_distrib \<open>i\<in>j\<close> A'_i dest: bspec[OF _ \<open>i\<in>j\<close>]
   463                cong: conj_cong)
   464     also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
   465       using \<open>finite j\<close> S(2)
   466       by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
   467     finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
   468   next
   469     interpret F: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<Union>i\<in>I. ?F i)"
   470       by (auto intro!: sigma_algebra_sigma_sets)
   471 
   472     fix b assume "b \<in> P"
   473     then obtain A j where b: "b = {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i}" "j \<in> J" "A \<in> Pi j E"
   474       by (auto simp: P_def)
   475     show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
   476     proof cases
   477       assume "j = {}"
   478       with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
   479         by auto
   480       then show ?thesis
   481         by blast
   482     next
   483       assume "j \<noteq> {}"
   484       with J b(2,3) have eq: "b = (\<Inter>i\<in>j. ((\<lambda>x. x i) -` A i \<inter> Pi\<^sub>E I \<Omega>))"
   485         unfolding b(1)
   486         by (auto simp: PiE_def Pi_def)
   487       show ?thesis
   488         unfolding eq using \<open>A \<in> Pi j E\<close> \<open>j \<in> J\<close> J(2)
   489         by (intro F.finite_INT J \<open>j \<in> J\<close> \<open>j \<noteq> {}\<close> sigma_sets.Basic) blast
   490     qed
   491   qed
   492   finally show "?thesis" .
   493 qed
   494 
   495 lemma sets_PiM_in_sets:
   496   assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   497   assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
   498   shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
   499   unfolding sets_PiM_single space[symmetric]
   500   by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
   501 
   502 lemma sets_PiM_cong[measurable_cong]:
   503   assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
   504   using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
   505 
   506 lemma sets_PiM_I:
   507   assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   508   shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
   509 proof cases
   510   assume "J = {}"
   511   then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))"
   512     by (auto simp: prod_emb_def)
   513   then show ?thesis
   514     by (auto simp add: sets_PiM intro!: sigma_sets_top)
   515 next
   516   assume "J \<noteq> {}" with assms show ?thesis
   517     by (force simp add: sets_PiM prod_algebra_def)
   518 qed
   519 
   520 proposition measurable_PiM:
   521   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   522   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>
   523     f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N"
   524   shows "f \<in> measurable N (PiM I M)"
   525   using sets_PiM prod_algebra_sets_into_space space
   526 proof (rule measurable_sigma_sets)
   527   fix A assume "A \<in> prod_algebra I M"
   528   from prod_algebraE[OF this] guess J X .
   529   with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
   530 qed
   531 
   532 lemma measurable_PiM_Collect:
   533   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   534   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>
   535     {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N"
   536   shows "f \<in> measurable N (PiM I M)"
   537   using sets_PiM prod_algebra_sets_into_space space
   538 proof (rule measurable_sigma_sets)
   539   fix A assume "A \<in> prod_algebra I M"
   540   from prod_algebraE[OF this] guess J X . note X = this
   541   then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
   542     using space by (auto simp: prod_emb_def del: PiE_I)
   543   also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
   544   finally show "f -` A \<inter> space N \<in> sets N" .
   545 qed
   546 
   547 lemma measurable_PiM_single:
   548   assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   549   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"
   550   shows "f \<in> measurable N (PiM I M)"
   551   using sets_PiM_single
   552 proof (rule measurable_sigma_sets)
   553   fix A assume "A \<in> {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   554   then obtain B i where "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> B}" and B: "i \<in> I" "B \<in> sets (M i)"
   555     by auto
   556   with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto
   557   also have "\<dots> \<in> sets N" using B by (rule sets)
   558   finally show "f -` A \<inter> space N \<in> sets N" .
   559 qed (auto simp: space)
   560 
   561 lemma measurable_PiM_single':
   562   assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
   563     and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   564   shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)"
   565 proof (rule measurable_PiM_single)
   566   fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
   567   then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
   568     by auto
   569   then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N"
   570     using A f by (auto intro!: measurable_sets)
   571 qed fact
   572 
   573 lemma sets_PiM_I_finite[measurable]:
   574   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   575   shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
   576   using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
   577 
   578 lemma measurable_component_singleton[measurable (raw)]:
   579   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
   580 proof (unfold measurable_def, intro CollectI conjI ballI)
   581   fix A assume "A \<in> sets (M i)"
   582   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) = prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. A)"
   583     using sets.sets_into_space \<open>i \<in> I\<close>
   584     by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
   585   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
   586     using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
   587 qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
   588 
   589 lemma measurable_component_singleton'[measurable_dest]:
   590   assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
   591   assumes g: "g \<in> measurable L N"
   592   assumes i: "i \<in> I"
   593   shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)"
   594   using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] .
   595 
   596 lemma measurable_PiM_component_rev:
   597   "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
   598   by simp
   599 
   600 lemma measurable_case_nat[measurable (raw)]:
   601   assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
   602     "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
   603   shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
   604   by (cases i) simp_all
   605 
   606 lemma measurable_case_nat'[measurable (raw)]:
   607   assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   608   shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   609   using fg[THEN measurable_space]
   610   by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
   611 
   612 lemma measurable_add_dim[measurable]:
   613   "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M)"
   614     (is "?f \<in> measurable ?P ?I")
   615 proof (rule measurable_PiM_single)
   616   fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
   617   have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
   618     (if j = i then space (Pi\<^sub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
   619     using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
   620   also have "\<dots> \<in> sets ?P"
   621     using A j
   622     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   623   finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
   624 qed (auto simp: space_pair_measure space_PiM PiE_def)
   625 
   626 proposition measurable_fun_upd:
   627   assumes I: "I = J \<union> {i}"
   628   assumes f[measurable]: "f \<in> measurable N (PiM J M)"
   629   assumes h[measurable]: "h \<in> measurable N (M i)"
   630   shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)"
   631 proof (intro measurable_PiM_single')
   632   fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)"
   633     unfolding I by (cases "j = i") auto
   634 next
   635   show "(\<lambda>x. (f x)(i := h x)) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   636     using I f[THEN measurable_space] h[THEN measurable_space]
   637     by (auto simp: space_PiM PiE_iff extensional_def)
   638 qed
   639 
   640 lemma measurable_component_update:
   641   "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)"
   642   by simp
   643 
   644 lemma measurable_merge[measurable]:
   645   "merge I J \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M)"
   646     (is "?f \<in> measurable ?P ?U")
   647 proof (rule measurable_PiM_single)
   648   fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
   649   then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
   650     (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)"
   651     by (auto simp: merge_def)
   652   also have "\<dots> \<in> sets ?P"
   653     using A
   654     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   655   finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
   656 qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
   657 
   658 lemma measurable_restrict[measurable (raw)]:
   659   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
   660   shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)"
   661 proof (rule measurable_PiM_single)
   662   fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
   663   then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N"
   664     by auto
   665   then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
   666     using A X by (auto intro!: measurable_sets)
   667 qed (insert X, auto simp add: PiE_def dest: measurable_space)
   668 
   669 lemma measurable_abs_UNIV:
   670   "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
   671   by (intro measurable_PiM_single) (auto dest: measurable_space)
   672 
   673 lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
   674   by (intro measurable_restrict measurable_component_singleton) auto
   675 
   676 lemma measurable_restrict_subset':
   677   assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
   678   shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
   679 proof-
   680   from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
   681     by (rule measurable_restrict_subset)
   682   also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
   683     by (intro sets_PiM_cong measurable_cong_sets) simp_all
   684   finally show ?thesis .
   685 qed
   686 
   687 lemma measurable_prod_emb[intro, simp]:
   688   "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
   689   unfolding prod_emb_def space_PiM[symmetric]
   690   by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
   691 
   692 lemma merge_in_prod_emb:
   693   assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I"
   694   shows "merge J I (x, y) \<in> prod_emb I M J X"
   695   using assms sets.sets_into_space[OF X]
   696   by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff
   697            cong: if_cong restrict_cong)
   698      (simp add: extensional_def)
   699 
   700 lemma prod_emb_eq_emptyD:
   701   assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)"
   702     and *: "prod_emb I M J X = {}"
   703   shows "X = {}"
   704 proof safe
   705   fix x assume "x \<in> X"
   706   obtain \<omega> where "\<omega> \<in> space (PiM I M)"
   707     using ne by blast
   708   from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto
   709 qed
   710 
   711 lemma sets_in_Pi_aux:
   712   "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   713   {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
   714   by (simp add: subset_eq Pi_iff)
   715 
   716 lemma sets_in_Pi[measurable (raw)]:
   717   "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   718   (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   719   Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
   720   unfolding pred_def
   721   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
   722 
   723 lemma sets_in_extensional_aux:
   724   "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
   725 proof -
   726   have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
   727     by (auto simp add: extensional_def space_PiM)
   728   then show ?thesis by simp
   729 qed
   730 
   731 lemma sets_in_extensional[measurable (raw)]:
   732   "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
   733   unfolding pred_def
   734   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
   735 
   736 lemma sets_PiM_I_countable:
   737   assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)"
   738 proof cases
   739   assume "I \<noteq> {}"
   740   then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
   741     using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
   742   also have "\<dots> \<in> sets (PiM I M)"
   743     using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
   744   finally show ?thesis .
   745 qed (simp add: sets_PiM_empty)
   746 
   747 lemma sets_PiM_D_countable:
   748   assumes A: "A \<in> PiM I M"
   749   shows "\<exists>J\<subseteq>I. \<exists>X\<in>PiM J M. countable J \<and> A = prod_emb I M J X"
   750   using A[unfolded sets_PiM_single]
   751 proof induction
   752   case (Basic A)
   753   then obtain i X where *: "i \<in> I" "X \<in> sets (M i)" and "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> X}"
   754     by auto
   755   then have A: "A = prod_emb I M {i} (\<Pi>\<^sub>E _\<in>{i}. X)"
   756     by (auto simp: prod_emb_def)
   757   then show ?case
   758     by (intro exI[of _ "{i}"] conjI bexI[of _ "\<Pi>\<^sub>E _\<in>{i}. X"])
   759        (auto intro: countable_finite * sets_PiM_I_finite)
   760 next
   761   case Empty then show ?case
   762     by (intro exI[of _ "{}"] conjI bexI[of _ "{}"]) auto
   763 next
   764   case (Compl A)
   765   then obtain J X where "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)" "countable J" "A = prod_emb I M J X"
   766     by auto
   767   then show ?case
   768     by (intro exI[of _ J] bexI[of _ "space (PiM J M) - X"] conjI)
   769        (auto simp add: space_PiM prod_emb_PiE intro!: sets_PiM_I_countable)
   770 next
   771   case (Union K)
   772   obtain J X where J: "\<And>i. J i \<subseteq> I" "\<And>i. countable (J i)" and X: "\<And>i. X i \<in> sets (Pi\<^sub>M (J i) M)"
   773     and K: "\<And>i. K i = prod_emb I M (J i) (X i)"
   774     by (metis Union.IH)
   775   show ?case
   776   proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
   777     show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
   778     with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
   779       by (simp add: K[abs_def] SUP_upper)
   780   qed(auto intro: X)
   781 qed
   782 
   783 proposition measure_eqI_PiM_finite:
   784   assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M"
   785   assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)"
   786   assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>"
   787   shows "P = Q"
   788 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   789   show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
   790     unfolding space_PiM[symmetric] by fact+
   791   fix X assume "X \<in> prod_algebra I M"
   792   then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   793     and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
   794     by (force elim!: prod_algebraE)
   795   then show "emeasure P X = emeasure Q X"
   796     unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq)
   797 qed (simp_all add: sets_PiM)
   798 
   799 proposition measure_eqI_PiM_infinite:
   800   assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M"
   801   assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow>
   802     P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))"
   803   assumes A: "finite_measure P"
   804   shows "P = Q"
   805 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   806   interpret finite_measure P by fact
   807   define i where "i = (SOME i. i \<in> I)"
   808   have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
   809     unfolding i_def by (rule someI_ex) auto
   810   define A where "A n =
   811     (if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)))"
   812     for n :: nat
   813   then show "range A \<subseteq> prod_algebra I M"
   814     using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i)
   815   have "\<And>i. A i = space (PiM I M)"
   816     by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
   817   then show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. emeasure P (A i) \<noteq> \<infinity>"
   818     by (auto simp: space_PiM)
   819 next
   820   fix X assume X: "X \<in> prod_algebra I M"
   821   then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   822     and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
   823     by (force elim!: prod_algebraE)
   824   then show "emeasure P X = emeasure Q X"
   825     by (auto intro!: eq)
   826 qed (auto simp: sets_PiM)
   827 
   828 locale%unimportant product_sigma_finite =
   829   fixes M :: "'i \<Rightarrow> 'a measure"
   830   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
   831 
   832 sublocale%unimportant product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
   833   by (rule sigma_finite_measures)
   834 
   835 locale%unimportant finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
   836   fixes I :: "'i set"
   837   assumes finite_index: "finite I"
   838 
   839 proposition (in finite_product_sigma_finite) sigma_finite_pairs:
   840   "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
   841     (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
   842     (\<forall>k. \<forall>i\<in>I. emeasure (M i) (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k) \<and>
   843     (\<Union>k. \<Pi>\<^sub>E i\<in>I. F i k) = space (PiM I M)"
   844 proof -
   845   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>)"
   846     using M.sigma_finite_incseq by metis
   847   from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   848   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>"
   849     by auto
   850   let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k"
   851   note space_PiM[simp]
   852   show ?thesis
   853   proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
   854     fix i show "range (F i) \<subseteq> sets (M i)" by fact
   855   next
   856     fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
   857   next
   858     fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
   859       by (auto simp: PiE_def dest!: sets.sets_into_space)
   860   next
   861     fix f assume "f \<in> space (PiM I M)"
   862     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
   863     show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
   864   next
   865     fix i show "?F i \<subseteq> ?F (Suc i)"
   866       using \<open>\<And>i. incseq (F i)\<close>[THEN incseq_SucD] by auto
   867   qed
   868 qed
   869 
   870 lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   871 proof -
   872   let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ennreal)"
   873   have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = 1"
   874   proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   875     show "positive (PiM {} M) ?\<mu>"
   876       by (auto simp: positive_def)
   877     show "countably_additive (PiM {} M) ?\<mu>"
   878       by (rule sets.countably_additiveI_finite)
   879          (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
   880   qed (auto simp: prod_emb_def)
   881   also have "(prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
   882     by (auto simp: prod_emb_def)
   883   finally show ?thesis
   884     by simp
   885 qed
   886 
   887 lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
   888   by (rule measure_eqI) (auto simp add: sets_PiM_empty)
   889 
   890 lemma (in product_sigma_finite) emeasure_PiM:
   891   "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   892 proof (induct I arbitrary: A rule: finite_induct)
   893   case (insert i I)
   894   interpret finite_product_sigma_finite M I by standard fact
   895   have "finite (insert i I)" using \<open>finite I\<close> by auto
   896   interpret I': finite_product_sigma_finite M "insert i I" by standard fact
   897   let ?h = "(\<lambda>(f, y). f(i := y))"
   898 
   899   let ?P = "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h"
   900   let ?\<mu> = "emeasure ?P"
   901   let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
   902   let ?f = "\<lambda>J E j. if j \<in> J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
   903 
   904   have "emeasure (Pi\<^sub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^sub>E (insert i I) A)) =
   905     (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
   906   proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   907     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))"
   908     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
   909     let ?p = "prod_emb (insert i I) M J (Pi\<^sub>E J E)"
   910     let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^sub>E j\<in>J-{i}. E j)"
   911     have "?\<mu> ?p =
   912       emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M (M i)) (?h -` ?p \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M M i))"
   913       by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
   914     also have "?h -` ?p \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
   915       using J E[rule_format, THEN sets.sets_into_space]
   916       by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
   917     also have "emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
   918       emeasure (Pi\<^sub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
   919       using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
   920     also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
   921       using J E[rule_format, THEN sets.sets_into_space]
   922       by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
   923     also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
   924       (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
   925       using E by (subst insert) (auto intro!: prod.cong)
   926     also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
   927        emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
   928       using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
   929     also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
   930       using insert(1,2) J E by (intro prod.mono_neutral_right) auto
   931     finally show "?\<mu> ?p = \<dots>" .
   932 
   933     show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))"
   934       using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   935   next
   936     show "positive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>"
   937       using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
   938   next
   939     show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
   940       insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
   941       using insert by auto
   942   qed (auto intro!: prod.cong)
   943   with insert show ?case
   944     by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
   945 qed simp
   946 
   947 lemma (in product_sigma_finite) PiM_eqI:
   948   assumes I[simp]: "finite I" and P: "sets P = PiM I M"
   949   assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   950   shows "P = PiM I M"
   951 proof -
   952   interpret finite_product_sigma_finite M I
   953     proof qed fact
   954   from sigma_finite_pairs guess C .. note C = this
   955   show ?thesis
   956   proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
   957     show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A
   958       by (simp add: eq emeasure_PiM)
   959     define A where "A n = (\<Pi>\<^sub>E i\<in>I. C i n)" for n
   960     with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)"
   961       by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top)
   962   qed
   963 qed
   964 
   965 lemma (in product_sigma_finite) sigma_finite:
   966   assumes "finite I"
   967   shows "sigma_finite_measure (PiM I M)"
   968 proof
   969   interpret finite_product_sigma_finite M I by standard fact
   970 
   971   obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
   972     "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
   973     in_space: "\<And>j. space (M j) = \<Union>(F j)"
   974     using sigma_finite_countable by (metis subset_eq)
   975   moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
   976     using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
   977   ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
   978     by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
   979        (auto intro!: countable_PiE sets_PiM_I_finite
   980              simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
   981 qed
   982 
   983 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
   984   using sigma_finite[OF finite_index] .
   985 
   986 lemma (in finite_product_sigma_finite) measure_times:
   987   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   988   using emeasure_PiM[OF finite_index] by auto
   989 
   990 lemma (in product_sigma_finite) nn_integral_empty:
   991   "0 \<le> f (\<lambda>k. undefined) \<Longrightarrow> integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
   992   by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)
   993 
   994 lemma%important (in product_sigma_finite) distr_merge:
   995   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   996   shows "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J) = Pi\<^sub>M (I \<union> J) M"
   997    (is "?D = ?P")
   998 proof (rule PiM_eqI)
   999   interpret I: finite_product_sigma_finite M I by standard fact
  1000   interpret J: finite_product_sigma_finite M J by standard fact
  1001   fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
  1002   have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = Pi\<^sub>E I A \<times> Pi\<^sub>E J A"
  1003     using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
  1004   from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
  1005       (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
  1006     by (subst emeasure_distr)
  1007        (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
  1008 qed (insert fin, simp_all)
  1009 
  1010 proposition (in product_sigma_finite) product_nn_integral_fold:
  1011   assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
  1012   and f[measurable]: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
  1013   shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
  1014     (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
  1015 proof -
  1016   interpret I: finite_product_sigma_finite M I by standard fact
  1017   interpret J: finite_product_sigma_finite M J by standard fact
  1018   interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
  1019   have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
  1020     using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
  1021   show ?thesis
  1022     apply (subst distr_merge[OF IJ, symmetric])
  1023     apply (subst nn_integral_distr[OF measurable_merge])
  1024     apply measurable []
  1025     apply (subst J.nn_integral_fst[symmetric, OF P_borel])
  1026     apply simp
  1027     done
  1028 qed
  1029 
  1030 lemma (in product_sigma_finite) distr_singleton:
  1031   "distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
  1032 proof (intro measure_eqI[symmetric])
  1033   interpret I: finite_product_sigma_finite M "{i}" by standard simp
  1034   fix A assume A: "A \<in> sets (M i)"
  1035   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
  1036     using sets.sets_into_space by (auto simp: space_PiM)
  1037   then show "emeasure (M i) A = emeasure ?D A"
  1038     using A I.measure_times[of "\<lambda>_. A"]
  1039     by (simp add: emeasure_distr measurable_component_singleton)
  1040 qed simp
  1041 
  1042 lemma (in product_sigma_finite) product_nn_integral_singleton:
  1043   assumes f: "f \<in> borel_measurable (M i)"
  1044   shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
  1045 proof -
  1046   interpret I: finite_product_sigma_finite M "{i}" by standard simp
  1047   from f show ?thesis
  1048     apply (subst distr_singleton[symmetric])
  1049     apply (subst nn_integral_distr[OF measurable_component_singleton])
  1050     apply simp_all
  1051     done
  1052 qed
  1053 
  1054 proposition (in product_sigma_finite) product_nn_integral_insert:
  1055   assumes I[simp]: "finite I" "i \<notin> I"
  1056     and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
  1057   shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
  1058 proof -
  1059   interpret I: finite_product_sigma_finite M I by standard auto
  1060   interpret i: finite_product_sigma_finite M "{i}" by standard auto
  1061   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
  1062     using f by auto
  1063   show ?thesis
  1064     unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
  1065   proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
  1066     fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
  1067     let ?f = "\<lambda>y. f (x(i := y))"
  1068     show "?f \<in> borel_measurable (M i)"
  1069       using measurable_comp[OF measurable_component_update f, OF x \<open>i \<notin> I\<close>]
  1070       unfolding comp_def .
  1071     show "(\<integral>\<^sup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^sub>M {i} M) = (\<integral>\<^sup>+ y. f (x(i := y i)) \<partial>Pi\<^sub>M {i} M)"
  1072       using x
  1073       by (auto intro!: nn_integral_cong arg_cong[where f=f]
  1074                simp add: space_PiM extensional_def PiE_def)
  1075   qed
  1076 qed
  1077 
  1078 lemma (in product_sigma_finite) product_nn_integral_insert_rev:
  1079   assumes I[simp]: "finite I" "i \<notin> I"
  1080     and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
  1081   shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
  1082   apply (subst product_nn_integral_insert[OF assms])
  1083   apply (rule pair_sigma_finite.Fubini')
  1084   apply intro_locales []
  1085   apply (rule sigma_finite[OF I(1)])
  1086   apply measurable
  1087   done
  1088 
  1089 lemma (in product_sigma_finite) product_nn_integral_prod:
  1090   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
  1091   shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
  1092 using assms proof (induction I)
  1093   case (insert i I)
  1094   note insert.prems[measurable]
  1095   note \<open>finite I\<close>[intro, simp]
  1096   interpret I: finite_product_sigma_finite M I by standard auto
  1097   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))"
  1098     using insert by (auto intro!: prod.cong)
  1099   have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)"
  1100     using sets.sets_into_space insert
  1101     by (intro borel_measurable_prod_ennreal
  1102               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
  1103        auto
  1104   then show ?case
  1105     apply (simp add: product_nn_integral_insert[OF insert(1,2)])
  1106     apply (simp add: insert(2-) * nn_integral_multc)
  1107     apply (subst nn_integral_cmult)
  1108     apply (auto simp add: insert(2-))
  1109     done
  1110 qed (simp add: space_PiM)
  1111 
  1112 proposition (in product_sigma_finite) product_nn_integral_pair:
  1113   assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
  1114   assumes xy: "x \<noteq> y"
  1115   shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
  1116 proof -
  1117   interpret psm: pair_sigma_finite "M x" "M y"
  1118     unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
  1119   have "{x, y} = {y, x}" by auto
  1120   also have "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {y, x} M) = (\<integral>\<^sup>+y. \<integral>\<^sup>+\<sigma>. f (\<sigma> x) y \<partial>PiM {x} M \<partial>M y)"
  1121     using xy by (subst product_nn_integral_insert_rev) simp_all
  1122   also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
  1123     by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
  1124   also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
  1125     by (subst psm.nn_integral_snd[symmetric]) simp_all
  1126   finally show ?thesis .
  1127 qed
  1128 
  1129 lemma (in product_sigma_finite) distr_component:
  1130   "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
  1131 proof (intro PiM_eqI)
  1132   fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
  1133   then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
  1134     by (fastforce dest: sets.sets_into_space)
  1135   with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
  1136     by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
  1137 qed simp_all
  1138 
  1139 lemma (in product_sigma_finite)
  1140   assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
  1141   shows emeasure_fold_integral:
  1142     "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" (is ?I)
  1143     and emeasure_fold_measurable:
  1144     "(\<lambda>x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M))) \<in> borel_measurable (Pi\<^sub>M I M)" (is ?B)
  1145 proof -
  1146   interpret I: finite_product_sigma_finite M I by standard fact
  1147   interpret J: finite_product_sigma_finite M J by standard fact
  1148   interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
  1149   have merge: "merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) \<in> sets (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
  1150     by (intro measurable_sets[OF _ A] measurable_merge assms)
  1151 
  1152   show ?I
  1153     apply (subst distr_merge[symmetric, OF IJ])
  1154     apply (subst emeasure_distr[OF measurable_merge A])
  1155     apply (subst J.emeasure_pair_measure_alt[OF merge])
  1156     apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
  1157     done
  1158 
  1159   show ?B
  1160     using IJ.measurable_emeasure_Pair1[OF merge]
  1161     by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
  1162 qed
  1163 
  1164 lemma sets_Collect_single:
  1165   "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
  1166   by simp
  1167 
  1168 lemma pair_measure_eq_distr_PiM:
  1169   fixes M1 :: "'a measure" and M2 :: "'a measure"
  1170   assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
  1171   shows "(M1 \<Otimes>\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. (x True, x False))"
  1172     (is "?P = ?D")
  1173 proof (rule pair_measure_eqI[OF assms])
  1174   interpret B: product_sigma_finite "case_bool M1 M2"
  1175     unfolding product_sigma_finite_def using assms by (auto split: bool.split)
  1176   let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)"
  1177 
  1178   have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
  1179     by auto
  1180   fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
  1181   have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
  1182     by (simp add: UNIV_bool ac_simps)
  1183   also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))"
  1184     using A B by (subst B.emeasure_PiM) (auto split: bool.split)
  1185   also have "Pi\<^sub>E UNIV (case_bool A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
  1186     using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
  1187     by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
  1188   finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
  1189     using A B
  1190       measurable_component_singleton[of True UNIV "case_bool M1 M2"]
  1191       measurable_component_singleton[of False UNIV "case_bool M1 M2"]
  1192     by (subst emeasure_distr) (auto simp: measurable_pair_iff)
  1193 qed simp
  1194 
  1195 lemma infprod_in_sets[intro]:
  1196   fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
  1197   shows "Pi UNIV E \<in> sets (\<Pi>\<^sub>M i\<in>UNIV::nat set. M i)"
  1198 proof -
  1199   have "Pi UNIV E = (\<Inter>i. prod_emb UNIV M {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))"
  1200     using E E[THEN sets.sets_into_space]
  1201     by (auto simp: prod_emb_def Pi_iff extensional_def)
  1202   with E show ?thesis by auto
  1203 qed
  1204 
  1205 
  1206 
  1207 subsection \<open>Measurability\<close>
  1208 
  1209 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
  1210 generated by open sets in the product, and the product sigma algebra, countably generated by
  1211 products of measurable sets along finitely many coordinates. The second one is defined and studied
  1212 in \<^file>\<open>Finite_Product_Measure.thy\<close>.
  1213 
  1214 These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
  1215 but there is a fundamental difference: open sets are generated by arbitrary unions, not only
  1216 countable ones, so typically many open sets will not be measurable with respect to the product sigma
  1217 algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
  1218 only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
  1219 the factor is countably generated).
  1220 
  1221 In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
  1222 compare it with the product sigma algebra as explained above.
  1223 \<close>
  1224 
  1225 lemma measurable_product_coordinates [measurable (raw)]:
  1226   "(\<lambda>x. x i) \<in> measurable borel borel"
  1227 by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
  1228 
  1229 lemma measurable_product_then_coordinatewise:
  1230   fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
  1231   assumes [measurable]: "f \<in> borel_measurable M"
  1232   shows "(\<lambda>x. f x i) \<in> borel_measurable M"
  1233 proof -
  1234   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
  1235     unfolding comp_def by auto
  1236   then show ?thesis by simp
  1237 qed
  1238 
  1239 text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
  1240 of the product sigma algebra that is more similar to the one we used above for the product
  1241 topology.\<close>
  1242 
  1243 lemma sets_PiM_finite:
  1244   "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
  1245         {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
  1246 proof
  1247   have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
  1248   proof (auto)
  1249     fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
  1250     then have *: "X i \<in> sets (M i)" for i by simp
  1251     define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
  1252     have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
  1253     define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
  1254     have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
  1255       unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
  1256     moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
  1257       unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
  1258       by (auto simp add: PiE_iff, blast)
  1259     ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
  1260   qed
  1261   then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
  1262               \<subseteq> sets (Pi\<^sub>M I M)"
  1263     by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
  1264 
  1265   have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
  1266                 (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
  1267     if "i \<in> I" "A \<in> sets (M i)" for i A
  1268   proof -
  1269     define X where "X = (\<lambda>j. if j = i then A else space (M j))"
  1270     have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
  1271       unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
  1272       by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
  1273     moreover have "X j \<in> sets (M j)" for j
  1274       unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
  1275     moreover have "finite {j. X j \<noteq> space (M j)}"
  1276       unfolding X_def by simp
  1277     ultimately show ?thesis by auto
  1278   qed
  1279   show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
  1280     unfolding sets_PiM_single
  1281     apply (rule sigma_sets_mono')
  1282     apply (auto simp add: PiE_iff *)
  1283     done
  1284 qed
  1285 
  1286 lemma sets_PiM_subset_borel:
  1287   "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
  1288 proof -
  1289   have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
  1290   proof -
  1291     define I where "I = {i. X i \<noteq> UNIV}"
  1292     have "finite I" unfolding I_def using that by simp
  1293     have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
  1294       unfolding I_def by auto
  1295     also have "... \<in> sets borel"
  1296       using that \<open>finite I\<close> by measurable
  1297     finally show ?thesis by simp
  1298   qed
  1299   then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
  1300     by auto
  1301   then show ?thesis unfolding sets_PiM_finite space_borel
  1302     by (simp add: * sets.sigma_sets_subset')
  1303 qed
  1304 
  1305 proposition sets_PiM_equal_borel:
  1306   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
  1307 proof
  1308   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
  1309             "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
  1310     using product_topology_countable_basis by fast
  1311   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
  1312   proof -
  1313     obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
  1314       using K(3)[OF \<open>k \<in> K\<close>] by blast
  1315     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
  1316   qed
  1317   have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
  1318   proof -
  1319     obtain B where "B \<subseteq> K" "U = (\<Union>B)"
  1320       using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
  1321     have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
  1322     moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
  1323       using \<open>B \<subseteq> K\<close> * that by auto
  1324     ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
  1325   qed
  1326   have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
  1327     apply (rule sets.sigma_sets_subset') using ** by auto
  1328   then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
  1329     unfolding borel_def by auto
  1330 qed (simp add: sets_PiM_subset_borel)
  1331 
  1332 lemma measurable_coordinatewise_then_product:
  1333   fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
  1334   assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
  1335   shows "f \<in> borel_measurable M"
  1336 proof -
  1337   have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
  1338     by (rule measurable_PiM_single', auto simp add: assms)
  1339   then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
  1340 qed
  1341 
  1342 
  1343 end