src/HOL/Probability/Product_Measure.thy
author hoelzl
Tue Mar 22 18:53:05 2011 +0100 (2011-03-22)
changeset 42066 6db76c88907a
parent 41981 cdf7693bbe08
child 42067 66c8281349ec
permissions -rw-r--r--
generalized Caratheodory from algebra to ring_of_sets
     1 theory Product_Measure
     2 imports Lebesgue_Integration
     3 begin
     4 
     5 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
     6 proof
     7   fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
     8     by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
     9 qed
    10 
    11 lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
    12   by auto
    13 
    14 lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
    15   by auto
    16 
    17 lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
    18   by auto
    19 
    20 lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
    21   by (cases x) simp
    22 
    23 lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
    24   by (auto simp: fun_eq_iff)
    25 
    26 abbreviation
    27   "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
    28 
    29 syntax
    30   "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
    31 
    32 syntax (xsymbols)
    33   "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
    34 
    35 syntax (HTML output)
    36   "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
    37 
    38 translations
    39   "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
    40 
    41 abbreviation
    42   funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
    43     (infixr "->\<^isub>E" 60) where
    44   "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
    45 
    46 notation (xsymbols)
    47   funcset_extensional  (infixr "\<rightarrow>\<^isub>E" 60)
    48 
    49 lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
    50   by safe (auto simp add: extensional_def fun_eq_iff)
    51 
    52 lemma extensional_insert[intro, simp]:
    53   assumes "a \<in> extensional (insert i I)"
    54   shows "a(i := b) \<in> extensional (insert i I)"
    55   using assms unfolding extensional_def by auto
    56 
    57 lemma extensional_Int[simp]:
    58   "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
    59   unfolding extensional_def by auto
    60 
    61 definition
    62   "merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    63 
    64 lemma merge_apply[simp]:
    65   "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
    66   "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
    67   "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
    68   "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
    69   "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined"
    70   unfolding merge_def by auto
    71 
    72 lemma merge_commute:
    73   "I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x"
    74   by (auto simp: merge_def intro!: ext)
    75 
    76 lemma Pi_cancel_merge_range[simp]:
    77   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
    78   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
    79   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
    80   "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
    81   by (auto simp: Pi_def)
    82 
    83 lemma Pi_cancel_merge[simp]:
    84   "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    85   "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    86   "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    87   "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    88   by (auto simp: Pi_def)
    89 
    90 lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)"
    91   by (auto simp: extensional_def)
    92 
    93 lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
    94   by (auto simp: restrict_def Pi_def)
    95 
    96 lemma restrict_merge[simp]:
    97   "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
    98   "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
    99   "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
   100   "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
   101   by (auto simp: restrict_def intro!: ext)
   102 
   103 lemma extensional_insert_undefined[intro, simp]:
   104   assumes "a \<in> extensional (insert i I)"
   105   shows "a(i := undefined) \<in> extensional I"
   106   using assms unfolding extensional_def by auto
   107 
   108 lemma extensional_insert_cancel[intro, simp]:
   109   assumes "a \<in> extensional I"
   110   shows "a \<in> extensional (insert i I)"
   111   using assms unfolding extensional_def by auto
   112 
   113 lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
   114   unfolding merge_def by (auto simp: fun_eq_iff)
   115 
   116 lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
   117   by auto
   118 
   119 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)"
   120   by auto
   121 
   122 lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
   123   by (auto simp: Pi_def)
   124 
   125 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"
   126   by (auto simp: Pi_def)
   127 
   128 lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
   129   by (auto simp: Pi_def)
   130 
   131 lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   132   by (auto simp: Pi_def)
   133 
   134 lemma restrict_vimage:
   135   assumes "I \<inter> J = {}"
   136   shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
   137   using assms by (auto simp: restrict_Pi_cancel)
   138 
   139 lemma merge_vimage:
   140   assumes "I \<inter> J = {}"
   141   shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   142   using assms by (auto simp: restrict_Pi_cancel)
   143 
   144 lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   145   by (auto simp: restrict_def intro!: ext)
   146 
   147 lemma merge_restrict[simp]:
   148   "merge I (restrict x I) J y = merge I x J y"
   149   "merge I x J (restrict y J) = merge I x J y"
   150   unfolding merge_def by (auto intro!: ext)
   151 
   152 lemma merge_x_x_eq_restrict[simp]:
   153   "merge I x J x = restrict x (I \<union> J)"
   154   unfolding merge_def by (auto intro!: ext)
   155 
   156 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"
   157   apply auto
   158   apply (drule_tac x=x in Pi_mem)
   159   apply (simp_all split: split_if_asm)
   160   apply (drule_tac x=i in Pi_mem)
   161   apply (auto dest!: Pi_mem)
   162   done
   163 
   164 lemma Pi_UN:
   165   fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
   166   assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
   167   shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
   168 proof (intro set_eqI iffI)
   169   fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
   170   then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
   171   from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
   172   obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
   173     using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
   174   have "f \<in> Pi I (A k)"
   175   proof (intro Pi_I)
   176     fix i assume "i \<in> I"
   177     from mono[OF this, of "n i" k] k[OF this] n[OF this]
   178     show "f i \<in> A k i" by auto
   179   qed
   180   then show "f \<in> (\<Union>n. Pi I (A n))" by auto
   181 qed auto
   182 
   183 lemma PiE_cong:
   184   assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
   185   shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
   186   using assms by (auto intro!: Pi_cong)
   187 
   188 lemma restrict_upd[simp]:
   189   "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
   190   by (auto simp: fun_eq_iff)
   191 
   192 lemma Pi_eq_subset:
   193   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   194   assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
   195   shows "F i \<subseteq> F' i"
   196 proof
   197   fix x assume "x \<in> F i"
   198   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
   199   from choice[OF this] guess f .. note f = this
   200   then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   201   then have "f \<in> Pi\<^isub>E I F'" using assms by simp
   202   then show "x \<in> F' i" using f `i \<in> I` by auto
   203 qed
   204 
   205 lemma Pi_eq_iff_not_empty:
   206   assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   207   shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   208 proof (intro iffI ballI)
   209   fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
   210   show "F i = F' i"
   211     using Pi_eq_subset[of I F F', OF ne eq i]
   212     using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   213     by auto
   214 qed auto
   215 
   216 lemma Pi_eq_empty_iff:
   217   "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   218 proof
   219   assume "Pi\<^isub>E I F = {}"
   220   show "\<exists>i\<in>I. F i = {}"
   221   proof (rule ccontr)
   222     assume "\<not> ?thesis"
   223     then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
   224     from choice[OF this] guess f ..
   225     then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   226     with `Pi\<^isub>E I F = {}` show False by auto
   227   qed
   228 qed auto
   229 
   230 lemma Pi_eq_iff:
   231   "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 = {}))"
   232 proof (intro iffI disjCI)
   233   assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   234   assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   235   then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   236     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   237   with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
   238 next
   239   assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   240   then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   241     using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   242 qed
   243 
   244 section "Binary products"
   245 
   246 definition
   247   "pair_measure_generator A B =
   248     \<lparr> space = space A \<times> space B,
   249       sets = {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B},
   250       measure = \<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A \<rparr>"
   251 
   252 definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where
   253   "A \<Otimes>\<^isub>M B = sigma (pair_measure_generator A B)"
   254 
   255 locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2
   256   for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
   257 
   258 abbreviation (in pair_sigma_algebra)
   259   "E \<equiv> pair_measure_generator M1 M2"
   260 
   261 abbreviation (in pair_sigma_algebra)
   262   "P \<equiv> M1 \<Otimes>\<^isub>M M2"
   263 
   264 lemma sigma_algebra_pair_measure:
   265   "sets M1 \<subseteq> Pow (space M1) \<Longrightarrow> sets M2 \<subseteq> Pow (space M2) \<Longrightarrow> sigma_algebra (pair_measure M1 M2)"
   266   by (force simp: pair_measure_def pair_measure_generator_def intro!: sigma_algebra_sigma)
   267 
   268 sublocale pair_sigma_algebra \<subseteq> sigma_algebra P
   269   using M1.space_closed M2.space_closed
   270   by (rule sigma_algebra_pair_measure)
   271 
   272 lemma pair_measure_generatorI[intro, simp]:
   273   "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (pair_measure_generator A B)"
   274   by (auto simp add: pair_measure_generator_def)
   275 
   276 lemma pair_measureI[intro, simp]:
   277   "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
   278   by (auto simp add: pair_measure_def)
   279 
   280 lemma space_pair_measure:
   281   "space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
   282   by (simp add: pair_measure_def pair_measure_generator_def)
   283 
   284 lemma sets_pair_measure_generator:
   285   "sets (pair_measure_generator N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
   286   unfolding pair_measure_generator_def by auto
   287 
   288 lemma pair_measure_generator_sets_into_space:
   289   assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)"
   290   shows "sets (pair_measure_generator M N) \<subseteq> Pow (space (pair_measure_generator M N))"
   291   using assms by (auto simp: pair_measure_generator_def)
   292 
   293 lemma pair_measure_generator_Int_snd:
   294   assumes "sets S1 \<subseteq> Pow (space S1)"
   295   shows "sets (pair_measure_generator S1 (algebra.restricted_space S2 A)) =
   296          sets (algebra.restricted_space (pair_measure_generator S1 S2) (space S1 \<times> A))"
   297   (is "?L = ?R")
   298   apply (auto simp: pair_measure_generator_def image_iff)
   299   using assms
   300   apply (rule_tac x="a \<times> xa" in exI)
   301   apply force
   302   using assms
   303   apply (rule_tac x="a" in exI)
   304   apply (rule_tac x="b \<inter> A" in exI)
   305   apply auto
   306   done
   307 
   308 lemma (in pair_sigma_algebra)
   309   shows measurable_fst[intro!, simp]:
   310     "fst \<in> measurable P M1" (is ?fst)
   311   and measurable_snd[intro!, simp]:
   312     "snd \<in> measurable P M2" (is ?snd)
   313 proof -
   314   { fix X assume "X \<in> sets M1"
   315     then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
   316       apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])
   317       using M1.sets_into_space by force+ }
   318   moreover
   319   { fix X assume "X \<in> sets M2"
   320     then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
   321       apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
   322       using M2.sets_into_space by force+ }
   323   ultimately have "?fst \<and> ?snd"
   324     by (fastsimp simp: measurable_def sets_sigma space_pair_measure
   325                  intro!: sigma_sets.Basic)
   326   then show ?fst ?snd by auto
   327 qed
   328 
   329 lemma (in pair_sigma_algebra) measurable_pair_iff:
   330   assumes "sigma_algebra M"
   331   shows "f \<in> measurable M P \<longleftrightarrow>
   332     (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
   333 proof -
   334   interpret M: sigma_algebra M by fact
   335   from assms show ?thesis
   336   proof (safe intro!: measurable_comp[where b=P])
   337     assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
   338     show "f \<in> measurable M P" unfolding pair_measure_def
   339     proof (rule M.measurable_sigma)
   340       show "sets (pair_measure_generator M1 M2) \<subseteq> Pow (space E)"
   341         unfolding pair_measure_generator_def using M1.sets_into_space M2.sets_into_space by auto
   342       show "f \<in> space M \<rightarrow> space E"
   343         using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma pair_measure_generator_def)
   344       fix A assume "A \<in> sets E"
   345       then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C"
   346         unfolding pair_measure_generator_def by auto
   347       moreover have "(fst \<circ> f) -` B \<inter> space M \<in> sets M"
   348         using f `B \<in> sets M1` unfolding measurable_def by auto
   349       moreover have "(snd \<circ> f) -` C \<inter> space M \<in> sets M"
   350         using s `C \<in> sets M2` unfolding measurable_def by auto
   351       moreover have "f -` A \<inter> space M = ((fst \<circ> f) -` B \<inter> space M) \<inter> ((snd \<circ> f) -` C \<inter> space M)"
   352         unfolding `A = B \<times> C` by (auto simp: vimage_Times)
   353       ultimately show "f -` A \<inter> space M \<in> sets M" by auto
   354     qed
   355   qed
   356 qed
   357 
   358 lemma (in pair_sigma_algebra) measurable_pair:
   359   assumes "sigma_algebra M"
   360   assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
   361   shows "f \<in> measurable M P"
   362   unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp
   363 
   364 lemma pair_measure_generatorE:
   365   assumes "X \<in> sets (pair_measure_generator M1 M2)"
   366   obtains A B where "X = A \<times> B" "A \<in> sets M1" "B \<in> sets M2"
   367   using assms unfolding pair_measure_generator_def by auto
   368 
   369 lemma (in pair_sigma_algebra) pair_measure_generator_swap:
   370   "(\<lambda>X. (\<lambda>(x,y). (y,x)) -` X \<inter> space M2 \<times> space M1) ` sets E = sets (pair_measure_generator M2 M1)"
   371 proof (safe elim!: pair_measure_generatorE)
   372   fix A B assume "A \<in> sets M1" "B \<in> sets M2"
   373   moreover then have "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space M2 \<times> space M1 = B \<times> A"
   374     using M1.sets_into_space M2.sets_into_space by auto
   375   ultimately show "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space M2 \<times> space M1 \<in> sets (pair_measure_generator M2 M1)"
   376     by (auto intro: pair_measure_generatorI)
   377 next
   378   fix A B assume "A \<in> sets M1" "B \<in> sets M2"
   379   then show "B \<times> A \<in> (\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E"
   380     using M1.sets_into_space M2.sets_into_space
   381     by (auto intro!: image_eqI[where x="A \<times> B"] pair_measure_generatorI)
   382 qed
   383 
   384 lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap:
   385   assumes Q: "Q \<in> sets P"
   386   shows "(\<lambda>(x,y). (y, x)) -` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q")
   387 proof -
   388   let "?f Q" = "(\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
   389   have *: "(\<lambda>(x,y). (y, x)) -` Q = ?f Q"
   390     using sets_into_space[OF Q] by (auto simp: space_pair_measure)
   391   have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))"
   392     unfolding pair_measure_def ..
   393   also have "\<dots> = sigma_sets (space M2 \<times> space M1) (?f ` sets E)"
   394     unfolding sigma_def pair_measure_generator_swap[symmetric]
   395     by (simp add: pair_measure_generator_def)
   396   also have "\<dots> = ?f ` sigma_sets (space M1 \<times> space M2) (sets E)"
   397     using M1.sets_into_space M2.sets_into_space
   398     by (intro sigma_sets_vimage) (auto simp: pair_measure_generator_def)
   399   also have "\<dots> = ?f ` sets P"
   400     unfolding pair_measure_def pair_measure_generator_def sigma_def by simp
   401   finally show ?thesis
   402     using Q by (subst *) auto
   403 qed
   404 
   405 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable:
   406   shows "(\<lambda>(x,y). (y, x)) \<in> measurable P (M2 \<Otimes>\<^isub>M M1)"
   407     (is "?f \<in> measurable ?P ?Q")
   408   unfolding measurable_def
   409 proof (intro CollectI conjI Pi_I ballI)
   410   fix x assume "x \<in> space ?P" then show "(case x of (x, y) \<Rightarrow> (y, x)) \<in> space ?Q"
   411     unfolding pair_measure_generator_def pair_measure_def by auto
   412 next
   413   fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)"
   414   interpret Q: pair_sigma_algebra M2 M1 by default
   415   with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
   416   show "?f -` A \<inter> space ?P \<in> sets ?P" by simp
   417 qed
   418 
   419 lemma (in pair_sigma_algebra) measurable_cut_fst[simp,intro]:
   420   assumes "Q \<in> sets P" shows "Pair x -` Q \<in> sets M2"
   421 proof -
   422   let ?Q' = "{Q. Q \<subseteq> space P \<and> Pair x -` Q \<in> sets M2}"
   423   let ?Q = "\<lparr> space = space P, sets = ?Q' \<rparr>"
   424   interpret Q: sigma_algebra ?Q
   425     proof qed (auto simp: vimage_UN vimage_Diff space_pair_measure)
   426   have "sets E \<subseteq> sets ?Q"
   427     using M1.sets_into_space M2.sets_into_space
   428     by (auto simp: pair_measure_generator_def space_pair_measure)
   429   then have "sets P \<subseteq> sets ?Q"
   430     apply (subst pair_measure_def, intro Q.sets_sigma_subset)
   431     by (simp add: pair_measure_def)
   432   with assms show ?thesis by auto
   433 qed
   434 
   435 lemma (in pair_sigma_algebra) measurable_cut_snd:
   436   assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) -` Q \<in> sets M1" (is "?cut Q \<in> sets M1")
   437 proof -
   438   interpret Q: pair_sigma_algebra M2 M1 by default
   439   with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
   440   show ?thesis by (simp add: vimage_compose[symmetric] comp_def)
   441 qed
   442 
   443 lemma (in pair_sigma_algebra) measurable_pair_image_snd:
   444   assumes m: "f \<in> measurable P M" and "x \<in> space M1"
   445   shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M"
   446   unfolding measurable_def
   447 proof (intro CollectI conjI Pi_I ballI)
   448   fix y assume "y \<in> space M2" with `f \<in> measurable P M` `x \<in> space M1`
   449   show "f (x, y) \<in> space M"
   450     unfolding measurable_def pair_measure_generator_def pair_measure_def by auto
   451 next
   452   fix A assume "A \<in> sets M"
   453   then have "Pair x -` (f -` A \<inter> space P) \<in> sets M2" (is "?C \<in> _")
   454     using `f \<in> measurable P M`
   455     by (intro measurable_cut_fst) (auto simp: measurable_def)
   456   also have "?C = (\<lambda>y. f (x, y)) -` A \<inter> space M2"
   457     using `x \<in> space M1` by (auto simp: pair_measure_generator_def pair_measure_def)
   458   finally show "(\<lambda>y. f (x, y)) -` A \<inter> space M2 \<in> sets M2" .
   459 qed
   460 
   461 lemma (in pair_sigma_algebra) measurable_pair_image_fst:
   462   assumes m: "f \<in> measurable P M" and "y \<in> space M2"
   463   shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M"
   464 proof -
   465   interpret Q: pair_sigma_algebra M2 M1 by default
   466   from Q.measurable_pair_image_snd[OF measurable_comp `y \<in> space M2`,
   467                                       OF Q.pair_sigma_algebra_swap_measurable m]
   468   show ?thesis by simp
   469 qed
   470 
   471 lemma (in pair_sigma_algebra) Int_stable_pair_measure_generator: "Int_stable E"
   472   unfolding Int_stable_def
   473 proof (intro ballI)
   474   fix A B assume "A \<in> sets E" "B \<in> sets E"
   475   then obtain A1 A2 B1 B2 where "A = A1 \<times> A2" "B = B1 \<times> B2"
   476     "A1 \<in> sets M1" "A2 \<in> sets M2" "B1 \<in> sets M1" "B2 \<in> sets M2"
   477     unfolding pair_measure_generator_def by auto
   478   then show "A \<inter> B \<in> sets E"
   479     by (auto simp add: times_Int_times pair_measure_generator_def)
   480 qed
   481 
   482 lemma finite_measure_cut_measurable:
   483   fixes M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
   484   assumes "sigma_finite_measure M1" "finite_measure M2"
   485   assumes "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)"
   486   shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1"
   487     (is "?s Q \<in> _")
   488 proof -
   489   interpret M1: sigma_finite_measure M1 by fact
   490   interpret M2: finite_measure M2 by fact
   491   interpret pair_sigma_algebra M1 M2 by default
   492   have [intro]: "sigma_algebra M1" by fact
   493   have [intro]: "sigma_algebra M2" by fact
   494   let ?D = "\<lparr> space = space P, sets = {A\<in>sets P. ?s A \<in> borel_measurable M1}  \<rparr>"
   495   note space_pair_measure[simp]
   496   interpret dynkin_system ?D
   497   proof (intro dynkin_systemI)
   498     fix A assume "A \<in> sets ?D" then show "A \<subseteq> space ?D"
   499       using sets_into_space by simp
   500   next
   501     from top show "space ?D \<in> sets ?D"
   502       by (auto simp add: if_distrib intro!: M1.measurable_If)
   503   next
   504     fix A assume "A \<in> sets ?D"
   505     with sets_into_space have "\<And>x. measure M2 (Pair x -` (space M1 \<times> space M2 - A)) =
   506         (if x \<in> space M1 then measure M2 (space M2) - ?s A x else 0)"
   507       by (auto intro!: M2.measure_compl simp: vimage_Diff)
   508     with `A \<in> sets ?D` top show "space ?D - A \<in> sets ?D"
   509       by (auto intro!: Diff M1.measurable_If M1.borel_measurable_extreal_diff)
   510   next
   511     fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> sets ?D"
   512     moreover then have "\<And>x. measure M2 (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
   513       by (intro M2.measure_countably_additive[symmetric])
   514          (auto simp: disjoint_family_on_def)
   515     ultimately show "(\<Union>i. F i) \<in> sets ?D"
   516       by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf)
   517   qed
   518   have "sets P = sets ?D" apply (subst pair_measure_def)
   519   proof (intro dynkin_lemma)
   520     show "Int_stable E" by (rule Int_stable_pair_measure_generator)
   521     from M1.sets_into_space have "\<And>A. A \<in> sets M1 \<Longrightarrow> {x \<in> space M1. x \<in> A} = A"
   522       by auto
   523     then show "sets E \<subseteq> sets ?D"
   524       by (auto simp: pair_measure_generator_def sets_sigma if_distrib
   525                intro: sigma_sets.Basic intro!: M1.measurable_If)
   526   qed (auto simp: pair_measure_def)
   527   with `Q \<in> sets P` have "Q \<in> sets ?D" by simp
   528   then show "?s Q \<in> borel_measurable M1" by simp
   529 qed
   530 
   531 subsection {* Binary products of $\sigma$-finite measure spaces *}
   532 
   533 locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
   534   for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
   535 
   536 sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
   537   by default
   538 
   539 lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
   540   by auto
   541 
   542 lemma (in pair_sigma_finite) measure_cut_measurable_fst:
   543   assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
   544 proof -
   545   have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+
   546   have M1: "sigma_finite_measure M1" by default
   547   from M2.disjoint_sigma_finite guess F .. note F = this
   548   then have F_sets: "\<And>i. F i \<in> sets M2" by auto
   549   let "?C x i" = "F i \<inter> Pair x -` Q"
   550   { fix i
   551     let ?R = "M2.restricted_space (F i)"
   552     have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
   553       using F M2.sets_into_space by auto
   554     let ?R2 = "M2.restricted_space (F i)"
   555     have "(\<lambda>x. measure ?R2 (Pair x -` (space M1 \<times> space ?R2 \<inter> Q))) \<in> borel_measurable M1"
   556     proof (intro finite_measure_cut_measurable[OF M1])
   557       show "finite_measure ?R2"
   558         using F by (intro M2.restricted_to_finite_measure) auto
   559       have "(space M1 \<times> space ?R2) \<inter> Q \<in> (op \<inter> (space M1 \<times> F i)) ` sets P"
   560         using `Q \<in> sets P` by (auto simp: image_iff)
   561       also have "\<dots> = sigma_sets (space M1 \<times> F i) ((op \<inter> (space M1 \<times> F i)) ` sets E)"
   562         unfolding pair_measure_def pair_measure_generator_def sigma_def
   563         using `F i \<in> sets M2` M2.sets_into_space
   564         by (auto intro!: sigma_sets_Int sigma_sets.Basic)
   565       also have "\<dots> \<subseteq> sets (M1 \<Otimes>\<^isub>M ?R2)"
   566         using M1.sets_into_space
   567         apply (auto simp: times_Int_times pair_measure_def pair_measure_generator_def sigma_def
   568                     intro!: sigma_sets_subseteq)
   569         apply (rule_tac x="a" in exI)
   570         apply (rule_tac x="b \<inter> F i" in exI)
   571         by auto
   572       finally show "(space M1 \<times> space ?R2) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R2)" .
   573     qed
   574     moreover have "\<And>x. Pair x -` (space M1 \<times> F i \<inter> Q) = ?C x i"
   575       using `Q \<in> sets P` sets_into_space by (auto simp: space_pair_measure)
   576     ultimately have "(\<lambda>x. measure M2 (?C x i)) \<in> borel_measurable M1"
   577       by simp }
   578   moreover
   579   { fix x
   580     have "(\<Sum>i. measure M2 (?C x i)) = measure M2 (\<Union>i. ?C x i)"
   581     proof (intro M2.measure_countably_additive)
   582       show "range (?C x) \<subseteq> sets M2"
   583         using F `Q \<in> sets P` by (auto intro!: M2.Int)
   584       have "disjoint_family F" using F by auto
   585       show "disjoint_family (?C x)"
   586         by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
   587     qed
   588     also have "(\<Union>i. ?C x i) = Pair x -` Q"
   589       using F sets_into_space `Q \<in> sets P`
   590       by (auto simp: space_pair_measure)
   591     finally have "measure M2 (Pair x -` Q) = (\<Sum>i. measure M2 (?C x i))"
   592       by simp }
   593   ultimately show ?thesis using `Q \<in> sets P` F_sets
   594     by (auto intro!: M1.borel_measurable_psuminf M2.Int)
   595 qed
   596 
   597 lemma (in pair_sigma_finite) measure_cut_measurable_snd:
   598   assumes "Q \<in> sets P" shows "(\<lambda>y. M1.\<mu> ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2"
   599 proof -
   600   interpret Q: pair_sigma_finite M2 M1 by default
   601   note sets_pair_sigma_algebra_swap[OF assms]
   602   from Q.measure_cut_measurable_fst[OF this]
   603   show ?thesis by (simp add: vimage_compose[symmetric] comp_def)
   604 qed
   605 
   606 lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable:
   607   assumes "f \<in> measurable P M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M"
   608 proof -
   609   interpret Q: pair_sigma_algebra M2 M1 by default
   610   have *: "(\<lambda>(x,y). f (y, x)) = f \<circ> (\<lambda>(x,y). (y, x))" by (simp add: fun_eq_iff)
   611   show ?thesis
   612     using Q.pair_sigma_algebra_swap_measurable assms
   613     unfolding * by (rule measurable_comp)
   614 qed
   615 
   616 lemma (in pair_sigma_finite) pair_measure_alt:
   617   assumes "A \<in> sets P"
   618   shows "measure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+ x. measure M2 (Pair x -` A) \<partial>M1)"
   619   apply (simp add: pair_measure_def pair_measure_generator_def)
   620 proof (rule M1.positive_integral_cong)
   621   fix x assume "x \<in> space M1"
   622   have *: "\<And>y. indicator A (x, y) = (indicator (Pair x -` A) y :: extreal)"
   623     unfolding indicator_def by auto
   624   show "(\<integral>\<^isup>+ y. indicator A (x, y) \<partial>M2) = measure M2 (Pair x -` A)"
   625     unfolding *
   626     apply (subst M2.positive_integral_indicator)
   627     apply (rule measurable_cut_fst[OF assms])
   628     by simp
   629 qed
   630 
   631 lemma (in pair_sigma_finite) pair_measure_times:
   632   assumes A: "A \<in> sets M1" and "B \<in> sets M2"
   633   shows "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = M1.\<mu> A * measure M2 B"
   634 proof -
   635   have "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = (\<integral>\<^isup>+ x. measure M2 B * indicator A x \<partial>M1)"
   636     using assms by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)
   637   with assms show ?thesis
   638     by (simp add: M1.positive_integral_cmult_indicator ac_simps)
   639 qed
   640 
   641 lemma (in measure_space) measure_not_negative[simp,intro]:
   642   assumes A: "A \<in> sets M" shows "\<mu> A \<noteq> - \<infinity>"
   643   using positive_measure[OF A] by auto
   644 
   645 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator:
   646   "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> incseq F \<and> (\<Union>i. F i) = space E \<and>
   647     (\<forall>i. measure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>)"
   648 proof -
   649   obtain F1 :: "nat \<Rightarrow> 'a set" and F2 :: "nat \<Rightarrow> 'b set" where
   650     F1: "range F1 \<subseteq> sets M1" "incseq F1" "(\<Union>i. F1 i) = space M1" "\<And>i. M1.\<mu> (F1 i) \<noteq> \<infinity>" and
   651     F2: "range F2 \<subseteq> sets M2" "incseq F2" "(\<Union>i. F2 i) = space M2" "\<And>i. M2.\<mu> (F2 i) \<noteq> \<infinity>"
   652     using M1.sigma_finite_up M2.sigma_finite_up by auto
   653   then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto
   654   let ?F = "\<lambda>i. F1 i \<times> F2 i"
   655   show ?thesis unfolding space_pair_measure
   656   proof (intro exI[of _ ?F] conjI allI)
   657     show "range ?F \<subseteq> sets E" using F1 F2
   658       by (fastsimp intro!: pair_measure_generatorI)
   659   next
   660     have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)"
   661     proof (intro subsetI)
   662       fix x assume "x \<in> space M1 \<times> space M2"
   663       then obtain i j where "fst x \<in> F1 i" "snd x \<in> F2 j"
   664         by (auto simp: space)
   665       then have "fst x \<in> F1 (max i j)" "snd x \<in> F2 (max j i)"
   666         using `incseq F1` `incseq F2` unfolding incseq_def
   667         by (force split: split_max)+
   668       then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)"
   669         by (intro SigmaI) (auto simp add: min_max.sup_commute)
   670       then show "x \<in> (\<Union>i. ?F i)" by auto
   671     qed
   672     then show "(\<Union>i. ?F i) = space E"
   673       using space by (auto simp: space pair_measure_generator_def)
   674   next
   675     fix i show "incseq (\<lambda>i. F1 i \<times> F2 i)"
   676       using `incseq F1` `incseq F2` unfolding incseq_Suc_iff by auto
   677   next
   678     fix i
   679     from F1 F2 have "F1 i \<in> sets M1" "F2 i \<in> sets M2" by auto
   680     with F1 F2 M1.positive_measure[OF this(1)] M2.positive_measure[OF this(2)]
   681     show "measure P (F1 i \<times> F2 i) \<noteq> \<infinity>"
   682       by (simp add: pair_measure_times)
   683   qed
   684 qed
   685 
   686 sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P
   687 proof
   688   show "positive P (measure P)"
   689     unfolding pair_measure_def pair_measure_generator_def sigma_def positive_def
   690     by (auto intro: M1.positive_integral_positive M2.positive_integral_positive)
   691 
   692   show "countably_additive P (measure P)"
   693     unfolding countably_additive_def
   694   proof (intro allI impI)
   695     fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
   696     assume F: "range F \<subseteq> sets P" "disjoint_family F"
   697     from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
   698     moreover from F have "\<And>i. (\<lambda>x. measure M2 (Pair x -` F i)) \<in> borel_measurable M1"
   699       by (intro measure_cut_measurable_fst) auto
   700     moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
   701       by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
   702     moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> range (\<lambda>i. Pair x -` F i) \<subseteq> sets M2"
   703       using F by auto
   704     ultimately show "(\<Sum>n. measure P (F n)) = measure P (\<Union>i. F i)"
   705       by (simp add: pair_measure_alt vimage_UN M1.positive_integral_suminf[symmetric]
   706                     M2.measure_countably_additive
   707                cong: M1.positive_integral_cong)
   708   qed
   709 
   710   from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   711   show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets P \<and> (\<Union>i. F i) = space P \<and> (\<forall>i. measure P (F i) \<noteq> \<infinity>)"
   712   proof (rule exI[of _ F], intro conjI)
   713     show "range F \<subseteq> sets P" using F by (auto simp: pair_measure_def)
   714     show "(\<Union>i. F i) = space P"
   715       using F by (auto simp: pair_measure_def pair_measure_generator_def)
   716     show "\<forall>i. measure P (F i) \<noteq> \<infinity>" using F by auto
   717   qed
   718 qed
   719 
   720 lemma (in pair_sigma_algebra) sets_swap:
   721   assumes "A \<in> sets P"
   722   shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)"
   723     (is "_ -` A \<inter> space ?Q \<in> sets ?Q")
   724 proof -
   725   have *: "(\<lambda>(x, y). (y, x)) -` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) -` A"
   726     using `A \<in> sets P` sets_into_space by (auto simp: space_pair_measure)
   727   show ?thesis
   728     unfolding * using assms by (rule sets_pair_sigma_algebra_swap)
   729 qed
   730 
   731 lemma (in pair_sigma_finite) pair_measure_alt2:
   732   assumes A: "A \<in> sets P"
   733   shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) -` A) \<partial>M2)"
   734     (is "_ = ?\<nu> A")
   735 proof -
   736   interpret Q: pair_sigma_finite M2 M1 by default
   737   from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   738   have [simp]: "\<And>m. \<lparr> space = space E, sets = sets (sigma E), measure = m \<rparr> = P\<lparr> measure := m \<rparr>"
   739     unfolding pair_measure_def by simp
   740 
   741   have "\<mu> A = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` A \<inter> space Q.P)"
   742   proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator])
   743     show "measure_space P" "measure_space Q.P" by default
   744     show "(\<lambda>(y, x). (x, y)) \<in> measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable)
   745     show "sets (sigma E) = sets P" "space E = space P" "A \<in> sets (sigma E)"
   746       using assms unfolding pair_measure_def by auto
   747     show "range F \<subseteq> sets E" "incseq F" "(\<Union>i. F i) = space E" "\<And>i. \<mu> (F i) \<noteq> \<infinity>"
   748       using F `A \<in> sets P` by (auto simp: pair_measure_def)
   749     fix X assume "X \<in> sets E"
   750     then obtain A B where X[simp]: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
   751       unfolding pair_measure_def pair_measure_generator_def by auto
   752     then have "(\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P = B \<times> A"
   753       using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure)
   754     then show "\<mu> X = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P)"
   755       using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps)
   756   qed
   757   then show ?thesis
   758     using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]]
   759     by (auto simp add: Q.pair_measure_alt space_pair_measure
   760              intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"])
   761 qed
   762 
   763 lemma pair_sigma_algebra_sigma:
   764   assumes 1: "incseq S1" "(\<Union>i. S1 i) = space E1" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)"
   765   assumes 2: "decseq S2" "(\<Union>i. S2 i) = space E2" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)"
   766   shows "sets (sigma (pair_measure_generator (sigma E1) (sigma E2))) = sets (sigma (pair_measure_generator E1 E2))"
   767     (is "sets ?S = sets ?E")
   768 proof -
   769   interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)
   770   interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)
   771   have P: "sets (pair_measure_generator E1 E2) \<subseteq> Pow (space E1 \<times> space E2)"
   772     using E1 E2 by (auto simp add: pair_measure_generator_def)
   773   interpret E: sigma_algebra ?E unfolding pair_measure_generator_def
   774     using E1 E2 by (intro sigma_algebra_sigma) auto
   775   { fix A assume "A \<in> sets E1"
   776     then have "fst -` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)"
   777       using E1 2 unfolding pair_measure_generator_def by auto
   778     also have "\<dots> = (\<Union>i. A \<times> S2 i)" by auto
   779     also have "\<dots> \<in> sets ?E" unfolding pair_measure_generator_def sets_sigma
   780       using 2 `A \<in> sets E1`
   781       by (intro sigma_sets.Union)
   782          (force simp: image_subset_iff intro!: sigma_sets.Basic)
   783     finally have "fst -` A \<inter> space ?E \<in> sets ?E" . }
   784   moreover
   785   { fix B assume "B \<in> sets E2"
   786     then have "snd -` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B"
   787       using E2 1 unfolding pair_measure_generator_def by auto
   788     also have "\<dots> = (\<Union>i. S1 i \<times> B)" by auto
   789     also have "\<dots> \<in> sets ?E"
   790       using 1 `B \<in> sets E2` unfolding pair_measure_generator_def sets_sigma
   791       by (intro sigma_sets.Union)
   792          (force simp: image_subset_iff intro!: sigma_sets.Basic)
   793     finally have "snd -` B \<inter> space ?E \<in> sets ?E" . }
   794   ultimately have proj:
   795     "fst \<in> measurable ?E (sigma E1) \<and> snd \<in> measurable ?E (sigma E2)"
   796     using E1 E2 by (subst (1 2) E.measurable_iff_sigma)
   797                    (auto simp: pair_measure_generator_def sets_sigma)
   798   { fix A B assume A: "A \<in> sets (sigma E1)" and B: "B \<in> sets (sigma E2)"
   799     with proj have "fst -` A \<inter> space ?E \<in> sets ?E" "snd -` B \<inter> space ?E \<in> sets ?E"
   800       unfolding measurable_def by simp_all
   801     moreover have "A \<times> B = (fst -` A \<inter> space ?E) \<inter> (snd -` B \<inter> space ?E)"
   802       using A B M1.sets_into_space M2.sets_into_space
   803       by (auto simp: pair_measure_generator_def)
   804     ultimately have "A \<times> B \<in> sets ?E" by auto }
   805   then have "sigma_sets (space ?E) (sets (pair_measure_generator (sigma E1) (sigma E2))) \<subseteq> sets ?E"
   806     by (intro E.sigma_sets_subset) (auto simp add: pair_measure_generator_def sets_sigma)
   807   then have subset: "sets ?S \<subseteq> sets ?E"
   808     by (simp add: sets_sigma pair_measure_generator_def)
   809   show "sets ?S = sets ?E"
   810   proof (intro set_eqI iffI)
   811     fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
   812       unfolding sets_sigma
   813     proof induct
   814       case (Basic A) then show ?case
   815         by (auto simp: pair_measure_generator_def sets_sigma intro: sigma_sets.Basic)
   816     qed (auto intro: sigma_sets.intros simp: pair_measure_generator_def)
   817   next
   818     fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
   819   qed
   820 qed
   821 
   822 section "Fubinis theorem"
   823 
   824 lemma (in pair_sigma_finite) simple_function_cut:
   825   assumes f: "simple_function P f" "\<And>x. 0 \<le> f x"
   826   shows "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
   827     and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f"
   828 proof -
   829   have f_borel: "f \<in> borel_measurable P"
   830     using f(1) by (rule borel_measurable_simple_function)
   831   let "?F z" = "f -` {z} \<inter> space P"
   832   let "?F' x z" = "Pair x -` ?F z"
   833   { fix x assume "x \<in> space M1"
   834     have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
   835       by (auto simp: indicator_def)
   836     have "\<And>y. y \<in> space M2 \<Longrightarrow> (x, y) \<in> space P" using `x \<in> space M1`
   837       by (simp add: space_pair_measure)
   838     moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel
   839       by (intro borel_measurable_vimage measurable_cut_fst)
   840     ultimately have "simple_function M2 (\<lambda> y. f (x, y))"
   841       apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])
   842       apply (rule simple_function_indicator_representation[OF f(1)])
   843       using `x \<in> space M1` by (auto simp del: space_sigma) }
   844   note M2_sf = this
   845   { fix x assume x: "x \<in> space M1"
   846     then have "(\<integral>\<^isup>+y. f (x, y) \<partial>M2) = (\<Sum>z\<in>f ` space P. z * M2.\<mu> (?F' x z))"
   847       unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)]
   848       unfolding simple_integral_def
   849     proof (safe intro!: setsum_mono_zero_cong_left)
   850       from f(1) show "finite (f ` space P)" by (rule simple_functionD)
   851     next
   852       fix y assume "y \<in> space M2" then show "f (x, y) \<in> f ` space P"
   853         using `x \<in> space M1` by (auto simp: space_pair_measure)
   854     next
   855       fix x' y assume "(x', y) \<in> space P"
   856         "f (x', y) \<notin> (\<lambda>y. f (x, y)) ` space M2"
   857       then have *: "?F' x (f (x', y)) = {}"
   858         by (force simp: space_pair_measure)
   859       show  "f (x', y) * M2.\<mu> (?F' x (f (x', y))) = 0"
   860         unfolding * by simp
   861     qed (simp add: vimage_compose[symmetric] comp_def
   862                    space_pair_measure) }
   863   note eq = this
   864   moreover have "\<And>z. ?F z \<in> sets P"
   865     by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)
   866   moreover then have "\<And>z. (\<lambda>x. M2.\<mu> (?F' x z)) \<in> borel_measurable M1"
   867     by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)
   868   moreover have *: "\<And>i x. 0 \<le> M2.\<mu> (Pair x -` (f -` {i} \<inter> space P))"
   869     using f(1)[THEN simple_functionD(2)] f(2) by (intro M2.positive_measure measurable_cut_fst)
   870   moreover { fix i assume "i \<in> f`space P"
   871     with * have "\<And>x. 0 \<le> i * M2.\<mu> (Pair x -` (f -` {i} \<inter> space P))"
   872       using f(2) by auto }
   873   ultimately
   874   show "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
   875     and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" using f(2)
   876     by (auto simp del: vimage_Int cong: measurable_cong
   877              intro!: M1.borel_measurable_extreal_setsum setsum_cong
   878              simp add: M1.positive_integral_setsum simple_integral_def
   879                        M1.positive_integral_cmult
   880                        M1.positive_integral_cong[OF eq]
   881                        positive_integral_eq_simple_integral[OF f]
   882                        pair_measure_alt[symmetric])
   883 qed
   884 
   885 lemma (in pair_sigma_finite) positive_integral_fst_measurable:
   886   assumes f: "f \<in> borel_measurable P"
   887   shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
   888       (is "?C f \<in> borel_measurable M1")
   889     and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f"
   890 proof -
   891   from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this
   892   then have F_borel: "\<And>i. F i \<in> borel_measurable P"
   893     by (auto intro: borel_measurable_simple_function)
   894   note sf = simple_function_cut[OF F(1,5)]
   895   then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
   896     using F(1) by auto
   897   moreover
   898   { fix x assume "x \<in> space M1"
   899     from F measurable_pair_image_snd[OF F_borel`x \<in> space M1`]
   900     have "(\<integral>\<^isup>+y. (SUP i. F i (x, y)) \<partial>M2) = (SUP i. ?C (F i) x)"
   901       by (intro M2.positive_integral_monotone_convergence_SUP)
   902          (auto simp: incseq_Suc_iff le_fun_def)
   903     then have "(SUP i. ?C (F i) x) = ?C f x"
   904       unfolding F(4) positive_integral_max_0 by simp }
   905   note SUPR_C = this
   906   ultimately show "?C f \<in> borel_measurable M1"
   907     by (simp cong: measurable_cong)
   908   have "(\<integral>\<^isup>+x. (SUP i. F i x) \<partial>P) = (SUP i. integral\<^isup>P P (F i))"
   909     using F_borel F
   910     by (intro positive_integral_monotone_convergence_SUP) auto
   911   also have "(SUP i. integral\<^isup>P P (F i)) = (SUP i. \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1)"
   912     unfolding sf(2) by simp
   913   also have "\<dots> = \<integral>\<^isup>+ x. (SUP i. \<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1" using F sf(1)
   914     by (intro M1.positive_integral_monotone_convergence_SUP[symmetric])
   915        (auto intro!: M2.positive_integral_mono M2.positive_integral_positive
   916                 simp: incseq_Suc_iff le_fun_def)
   917   also have "\<dots> = \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. (SUP i. F i (x, y)) \<partial>M2) \<partial>M1"
   918     using F_borel F(2,5)
   919     by (auto intro!: M1.positive_integral_cong M2.positive_integral_monotone_convergence_SUP[symmetric]
   920              simp: incseq_Suc_iff le_fun_def measurable_pair_image_snd)
   921   finally show "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f"
   922     using F by (simp add: positive_integral_max_0)
   923 qed
   924 
   925 lemma (in pair_sigma_finite) measure_preserving_swap:
   926   "(\<lambda>(x,y). (y, x)) \<in> measure_preserving (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
   927 proof
   928   interpret Q: pair_sigma_finite M2 M1 by default
   929   show *: "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)"
   930     using pair_sigma_algebra_swap_measurable .
   931   fix X assume "X \<in> sets (M2 \<Otimes>\<^isub>M M1)"
   932   from measurable_sets[OF * this] this Q.sets_into_space[OF this]
   933   show "measure (M1 \<Otimes>\<^isub>M M2) ((\<lambda>(x, y). (y, x)) -` X \<inter> space P) = measure (M2 \<Otimes>\<^isub>M M1) X"
   934     by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"]
   935       simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)
   936 qed
   937 
   938 lemma (in pair_sigma_finite) positive_integral_product_swap:
   939   assumes f: "f \<in> borel_measurable P"
   940   shows "(\<integral>\<^isup>+x. f (case x of (x,y)\<Rightarrow>(y,x)) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P P f"
   941 proof -
   942   interpret Q: pair_sigma_finite M2 M1 by default
   943   have "sigma_algebra P" by default
   944   with f show ?thesis
   945     by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto
   946 qed
   947 
   948 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   949   assumes f: "f \<in> borel_measurable P"
   950   shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P P f"
   951 proof -
   952   interpret Q: pair_sigma_finite M2 M1 by default
   953   note pair_sigma_algebra_measurable[OF f]
   954   from Q.positive_integral_fst_measurable[OF this]
   955   have "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P)"
   956     by simp
   957   also have "(\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P) = integral\<^isup>P P f"
   958     unfolding positive_integral_product_swap[OF f, symmetric]
   959     by (auto intro!: Q.positive_integral_cong)
   960   finally show ?thesis .
   961 qed
   962 
   963 lemma (in pair_sigma_finite) Fubini:
   964   assumes f: "f \<in> borel_measurable P"
   965   shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
   966   unfolding positive_integral_snd_measurable[OF assms]
   967   unfolding positive_integral_fst_measurable[OF assms] ..
   968 
   969 lemma (in pair_sigma_finite) AE_pair:
   970   assumes "AE x in P. Q x"
   971   shows "AE x in M1. (AE y in M2. Q (x, y))"
   972 proof -
   973   obtain N where N: "N \<in> sets P" "\<mu> N = 0" "{x\<in>space P. \<not> Q x} \<subseteq> N"
   974     using assms unfolding almost_everywhere_def by auto
   975   show ?thesis
   976   proof (rule M1.AE_I)
   977     from N measure_cut_measurable_fst[OF `N \<in> sets P`]
   978     show "M1.\<mu> {x\<in>space M1. M2.\<mu> (Pair x -` N) \<noteq> 0} = 0"
   979       by (auto simp: pair_measure_alt M1.positive_integral_0_iff)
   980     show "{x \<in> space M1. M2.\<mu> (Pair x -` N) \<noteq> 0} \<in> sets M1"
   981       by (intro M1.borel_measurable_extreal_neq_const measure_cut_measurable_fst N)
   982     { fix x assume "x \<in> space M1" "M2.\<mu> (Pair x -` N) = 0"
   983       have "M2.almost_everywhere (\<lambda>y. Q (x, y))"
   984       proof (rule M2.AE_I)
   985         show "M2.\<mu> (Pair x -` N) = 0" by fact
   986         show "Pair x -` N \<in> sets M2" by (intro measurable_cut_fst N)
   987         show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
   988           using N `x \<in> space M1` unfolding space_sigma space_pair_measure by auto
   989       qed }
   990     then show "{x \<in> space M1. \<not> M2.almost_everywhere (\<lambda>y. Q (x, y))} \<subseteq> {x \<in> space M1. M2.\<mu> (Pair x -` N) \<noteq> 0}"
   991       by auto
   992   qed
   993 qed
   994 
   995 lemma (in pair_sigma_algebra) measurable_product_swap:
   996   "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
   997 proof -
   998   interpret Q: pair_sigma_algebra M2 M1 by default
   999   show ?thesis
  1000     using pair_sigma_algebra_measurable[of "\<lambda>(x,y). f (y, x)"]
  1001     by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI)
  1002 qed
  1003 
  1004 lemma (in pair_sigma_finite) integrable_product_swap:
  1005   assumes "integrable P f"
  1006   shows "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x))"
  1007 proof -
  1008   interpret Q: pair_sigma_finite M2 M1 by default
  1009   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  1010   show ?thesis unfolding *
  1011     using assms unfolding integrable_def
  1012     apply (subst (1 2) positive_integral_product_swap)
  1013     using `integrable P f` unfolding integrable_def
  1014     by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
  1015 qed
  1016 
  1017 lemma (in pair_sigma_finite) integrable_product_swap_iff:
  1018   "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable P f"
  1019 proof -
  1020   interpret Q: pair_sigma_finite M2 M1 by default
  1021   from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
  1022   show ?thesis by auto
  1023 qed
  1024 
  1025 lemma (in pair_sigma_finite) integral_product_swap:
  1026   assumes "integrable P f"
  1027   shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>L P f"
  1028 proof -
  1029   interpret Q: pair_sigma_finite M2 M1 by default
  1030   have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
  1031   show ?thesis
  1032     unfolding lebesgue_integral_def *
  1033     apply (subst (1 2) positive_integral_product_swap)
  1034     using `integrable P f` unfolding integrable_def
  1035     by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
  1036 qed
  1037 
  1038 lemma (in pair_sigma_finite) integrable_fst_measurable:
  1039   assumes f: "integrable P f"
  1040   shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE")
  1041     and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT")
  1042 proof -
  1043   let "?pf x" = "extreal (f x)" and "?nf x" = "extreal (- f x)"
  1044   have
  1045     borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and
  1046     int: "integral\<^isup>P P ?nf \<noteq> \<infinity>" "integral\<^isup>P P ?pf \<noteq> \<infinity>"
  1047     using assms by auto
  1048   have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>"
  1049      "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. extreal (- f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>"
  1050     using borel[THEN positive_integral_fst_measurable(1)] int
  1051     unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all
  1052   with borel[THEN positive_integral_fst_measurable(1)]
  1053   have AE_pos: "AE x in M1. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
  1054     "AE x in M1. (\<integral>\<^isup>+y. extreal (- f (x, y)) \<partial>M2) \<noteq> \<infinity>"
  1055     by (auto intro!: M1.positive_integral_PInf_AE )
  1056   then have AE: "AE x in M1. \<bar>\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>"
  1057     "AE x in M1. \<bar>\<integral>\<^isup>+y. extreal (- f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>"
  1058     by (auto simp: M2.positive_integral_positive)
  1059   from AE_pos show ?AE using assms
  1060     by (simp add: measurable_pair_image_snd integrable_def)
  1061   { fix f have "(\<integral>\<^isup>+ x. - \<integral>\<^isup>+ y. extreal (f x y) \<partial>M2 \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
  1062       using M2.positive_integral_positive
  1063       by (intro M1.positive_integral_cong_pos) (auto simp: extreal_uminus_le_reorder)
  1064     then have "(\<integral>\<^isup>+ x. - \<integral>\<^isup>+ y. extreal (f x y) \<partial>M2 \<partial>M1) = 0" by simp }
  1065   note this[simp]
  1066   { fix f assume borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable P"
  1067       and int: "integral\<^isup>P P (\<lambda>x. extreal (f x)) \<noteq> \<infinity>"
  1068       and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<noteq> \<infinity>)"
  1069     have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
  1070     proof (intro integrable_def[THEN iffD2] conjI)
  1071       show "?f \<in> borel_measurable M1"
  1072         using borel by (auto intro!: M1.borel_measurable_real_of_extreal positive_integral_fst_measurable)
  1073       have "(\<integral>\<^isup>+x. extreal (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. extreal (f (x, y))  \<partial>M2) \<partial>M1)"
  1074         using AE M2.positive_integral_positive
  1075         by (auto intro!: M1.positive_integral_cong_AE simp: extreal_real)
  1076       then show "(\<integral>\<^isup>+x. extreal (?f x) \<partial>M1) \<noteq> \<infinity>"
  1077         using positive_integral_fst_measurable[OF borel] int by simp
  1078       have "(\<integral>\<^isup>+x. extreal (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
  1079         by (intro M1.positive_integral_cong_pos)
  1080            (simp add: M2.positive_integral_positive real_of_extreal_pos)
  1081       then show "(\<integral>\<^isup>+x. extreal (- ?f x) \<partial>M1) \<noteq> \<infinity>" by simp
  1082     qed }
  1083   with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)]
  1084   show ?INT
  1085     unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2]
  1086       borel[THEN positive_integral_fst_measurable(2), symmetric]
  1087     using AE[THEN M1.integral_real]
  1088     by simp
  1089 qed
  1090 
  1091 lemma (in pair_sigma_finite) integrable_snd_measurable:
  1092   assumes f: "integrable P f"
  1093   shows "M2.almost_everywhere (\<lambda>y. integrable M1 (\<lambda>x. f (x, y)))" (is "?AE")
  1094     and "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>L P f" (is "?INT")
  1095 proof -
  1096   interpret Q: pair_sigma_finite M2 M1 by default
  1097   have Q_int: "integrable Q.P (\<lambda>(x, y). f (y, x))"
  1098     using f unfolding integrable_product_swap_iff .
  1099   show ?INT
  1100     using Q.integrable_fst_measurable(2)[OF Q_int]
  1101     using integral_product_swap[OF f] by simp
  1102   show ?AE
  1103     using Q.integrable_fst_measurable(1)[OF Q_int]
  1104     by simp
  1105 qed
  1106 
  1107 lemma (in pair_sigma_finite) Fubini_integral:
  1108   assumes f: "integrable P f"
  1109   shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)"
  1110   unfolding integrable_snd_measurable[OF assms]
  1111   unfolding integrable_fst_measurable[OF assms] ..
  1112 
  1113 section "Finite product spaces"
  1114 
  1115 section "Products"
  1116 
  1117 locale product_sigma_algebra =
  1118   fixes M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme"
  1119   assumes sigma_algebras: "\<And>i. sigma_algebra (M i)"
  1120 
  1121 locale finite_product_sigma_algebra = product_sigma_algebra M
  1122   for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
  1123   fixes I :: "'i set"
  1124   assumes finite_index: "finite I"
  1125 
  1126 definition
  1127   "product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)),
  1128     sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)),
  1129     measure = \<lambda>A. (\<Prod>i\<in>I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \<rparr>"
  1130 
  1131 definition product_algebra_def:
  1132   "Pi\<^isub>M I M = sigma (product_algebra_generator I M)
  1133     \<lparr> measure := (SOME \<mu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<mu> \<rparr>) \<and>
  1134       (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))))\<rparr>"
  1135 
  1136 syntax
  1137   "_PiM"  :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
  1138               ('i => 'a, 'b) measure_space_scheme"  ("(3PIM _:_./ _)" 10)
  1139 
  1140 syntax (xsymbols)
  1141   "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
  1142              ('i => 'a, 'b) measure_space_scheme"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"   10)
  1143 
  1144 syntax (HTML output)
  1145   "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>
  1146              ('i => 'a, 'b) measure_space_scheme"  ("(3\<Pi>\<^isub>M _\<in>_./ _)"   10)
  1147 
  1148 translations
  1149   "PIM x:I. M" == "CONST Pi\<^isub>M I (%x. M)"
  1150 
  1151 abbreviation (in finite_product_sigma_algebra) "G \<equiv> product_algebra_generator I M"
  1152 abbreviation (in finite_product_sigma_algebra) "P \<equiv> Pi\<^isub>M I M"
  1153 
  1154 sublocale product_sigma_algebra \<subseteq> M: sigma_algebra "M i" for i by (rule sigma_algebras)
  1155 
  1156 lemma sigma_into_space:
  1157   assumes "sets M \<subseteq> Pow (space M)"
  1158   shows "sets (sigma M) \<subseteq> Pow (space M)"
  1159   using sigma_sets_into_sp[OF assms] unfolding sigma_def by auto
  1160 
  1161 lemma (in product_sigma_algebra) product_algebra_generator_into_space:
  1162   "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
  1163   using M.sets_into_space unfolding product_algebra_generator_def
  1164   by auto blast
  1165 
  1166 lemma (in product_sigma_algebra) product_algebra_into_space:
  1167   "sets (Pi\<^isub>M I M) \<subseteq> Pow (space (Pi\<^isub>M I M))"
  1168   using product_algebra_generator_into_space
  1169   by (auto intro!: sigma_into_space simp add: product_algebra_def)
  1170 
  1171 lemma (in product_sigma_algebra) sigma_algebra_product_algebra: "sigma_algebra (Pi\<^isub>M I M)"
  1172   using product_algebra_generator_into_space unfolding product_algebra_def
  1173   by (rule sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) simp_all
  1174 
  1175 sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
  1176   using sigma_algebra_product_algebra .
  1177 
  1178 lemma product_algebraE:
  1179   assumes "A \<in> sets (product_algebra_generator I M)"
  1180   obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
  1181   using assms unfolding product_algebra_generator_def by auto
  1182 
  1183 lemma product_algebra_generatorI[intro]:
  1184   assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
  1185   shows "Pi\<^isub>E I E \<in> sets (product_algebra_generator I M)"
  1186   using assms unfolding product_algebra_generator_def by auto
  1187 
  1188 lemma space_product_algebra_generator[simp]:
  1189   "space (product_algebra_generator I M) = Pi\<^isub>E I (\<lambda>i. space (M i))"
  1190   unfolding product_algebra_generator_def by simp
  1191 
  1192 lemma space_product_algebra[simp]:
  1193   "space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
  1194   unfolding product_algebra_def product_algebra_generator_def by simp
  1195 
  1196 lemma sets_product_algebra:
  1197   "sets (Pi\<^isub>M I M) = sets (sigma (product_algebra_generator I M))"
  1198   unfolding product_algebra_def sigma_def by simp
  1199 
  1200 lemma product_algebra_generator_sets_into_space:
  1201   assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
  1202   shows "sets (product_algebra_generator I M) \<subseteq> Pow (space (product_algebra_generator I M))"
  1203   using assms by (auto simp: product_algebra_generator_def) blast
  1204 
  1205 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
  1206   "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
  1207   by (auto simp: sets_product_algebra)
  1208 
  1209 section "Generating set generates also product algebra"
  1210 
  1211 lemma sigma_product_algebra_sigma_eq:
  1212   assumes "finite I"
  1213   assumes mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
  1214   assumes union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (E i)"
  1215   assumes sets_into: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> sets (E i)"
  1216   and E: "\<And>i. sets (E i) \<subseteq> Pow (space (E i))"
  1217   shows "sets (\<Pi>\<^isub>M i\<in>I. sigma (E i)) = sets (\<Pi>\<^isub>M i\<in>I. E i)"
  1218     (is "sets ?S = sets ?E")
  1219 proof cases
  1220   assume "I = {}" then show ?thesis
  1221     by (simp add: product_algebra_def product_algebra_generator_def)
  1222 next
  1223   assume "I \<noteq> {}"
  1224   interpret E: sigma_algebra "sigma (E i)" for i
  1225     using E by (rule sigma_algebra_sigma)
  1226   have into_space[intro]: "\<And>i x A. A \<in> sets (E i) \<Longrightarrow> x i \<in> A \<Longrightarrow> x i \<in> space (E i)"
  1227     using E by auto
  1228   interpret G: sigma_algebra ?E
  1229     unfolding product_algebra_def product_algebra_generator_def using E
  1230     by (intro sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) (auto dest: Pi_mem)
  1231   { fix A i assume "i \<in> I" and A: "A \<in> sets (E i)"
  1232     then have "(\<lambda>x. x i) -` A \<inter> space ?E = (\<Pi>\<^isub>E j\<in>I. if j = i then A else \<Union>n. S j n) \<inter> space ?E"
  1233       using mono union unfolding incseq_Suc_iff space_product_algebra
  1234       by (auto dest: Pi_mem)
  1235     also have "\<dots> = (\<Union>n. (\<Pi>\<^isub>E j\<in>I. if j = i then A else S j n))"
  1236       unfolding space_product_algebra
  1237       apply simp
  1238       apply (subst Pi_UN[OF `finite I`])
  1239       using mono[THEN incseqD] apply simp
  1240       apply (simp add: PiE_Int)
  1241       apply (intro PiE_cong)
  1242       using A sets_into by (auto intro!: into_space)
  1243     also have "\<dots> \<in> sets ?E"
  1244       using sets_into `A \<in> sets (E i)`
  1245       unfolding sets_product_algebra sets_sigma
  1246       by (intro sigma_sets.Union)
  1247          (auto simp: image_subset_iff intro!: sigma_sets.Basic)
  1248     finally have "(\<lambda>x. x i) -` A \<inter> space ?E \<in> sets ?E" . }
  1249   then have proj:
  1250     "\<And>i. i\<in>I \<Longrightarrow> (\<lambda>x. x i) \<in> measurable ?E (sigma (E i))"
  1251     using E by (subst G.measurable_iff_sigma)
  1252                (auto simp: sets_product_algebra sets_sigma)
  1253   { fix A assume A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (sigma (E i))"
  1254     with proj have basic: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) -` (A i) \<inter> space ?E \<in> sets ?E"
  1255       unfolding measurable_def by simp
  1256     have "Pi\<^isub>E I A = (\<Inter>i\<in>I. (\<lambda>x. x i) -` (A i) \<inter> space ?E)"
  1257       using A E.sets_into_space `I \<noteq> {}` unfolding product_algebra_def by auto blast
  1258     then have "Pi\<^isub>E I A \<in> sets ?E"
  1259       using G.finite_INT[OF `finite I` `I \<noteq> {}` basic, of "\<lambda>i. i"] by simp }
  1260   then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\<lambda>i. sigma (E i)))) \<subseteq> sets ?E"
  1261     by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def)
  1262   then have subset: "sets ?S \<subseteq> sets ?E"
  1263     by (simp add: sets_sigma sets_product_algebra)
  1264   show "sets ?S = sets ?E"
  1265   proof (intro set_eqI iffI)
  1266     fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
  1267       unfolding sets_sigma sets_product_algebra
  1268     proof induct
  1269       case (Basic A) then show ?case
  1270         by (auto simp: sets_sigma product_algebra_generator_def intro: sigma_sets.Basic)
  1271     qed (auto intro: sigma_sets.intros simp: product_algebra_generator_def)
  1272   next
  1273     fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
  1274   qed
  1275 qed
  1276 
  1277 lemma product_algebraI[intro]:
  1278     "E \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> Pi\<^isub>E I E \<in> sets (Pi\<^isub>M I M)"
  1279   using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI)
  1280 
  1281 lemma (in product_sigma_algebra) measurable_component_update:
  1282   assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
  1283   shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
  1284   unfolding product_algebra_def apply simp
  1285 proof (intro measurable_sigma)
  1286   let ?G = "product_algebra_generator (insert i I) M"
  1287   show "sets ?G \<subseteq> Pow (space ?G)" using product_algebra_generator_into_space .
  1288   show "?f \<in> space (M i) \<rightarrow> space ?G"
  1289     using M.sets_into_space assms by auto
  1290   fix A assume "A \<in> sets ?G"
  1291   from product_algebraE[OF this] guess E . note E = this
  1292   then have "?f -` A \<inter> space (M i) = E i \<or> ?f -` A \<inter> space (M i) = {}"
  1293     using M.sets_into_space assms by auto
  1294   then show "?f -` A \<inter> space (M i) \<in> sets (M i)"
  1295     using E by (auto intro!: product_algebraI)
  1296 qed
  1297 
  1298 lemma (in product_sigma_algebra) measurable_add_dim:
  1299   assumes "i \<notin> I"
  1300   shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
  1301 proof -
  1302   let ?f = "(\<lambda>(f, y). f(i := y))" and ?G = "product_algebra_generator (insert i I) M"
  1303   interpret Ii: pair_sigma_algebra "Pi\<^isub>M I M" "M i"
  1304     unfolding pair_sigma_algebra_def
  1305     by (intro sigma_algebra_product_algebra sigma_algebras conjI)
  1306   have "?f \<in> measurable Ii.P (sigma ?G)"
  1307   proof (rule Ii.measurable_sigma)
  1308     show "sets ?G \<subseteq> Pow (space ?G)"
  1309       using product_algebra_generator_into_space .
  1310     show "?f \<in> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<rightarrow> space ?G"
  1311       by (auto simp: space_pair_measure)
  1312   next
  1313     fix A assume "A \<in> sets ?G"
  1314     then obtain F where "A = Pi\<^isub>E (insert i I) F"
  1315       and F: "\<And>j. j \<in> I \<Longrightarrow> F j \<in> sets (M j)" "F i \<in> sets (M i)"
  1316       by (auto elim!: product_algebraE)
  1317     then have "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = Pi\<^isub>E I F \<times> (F i)"
  1318       using sets_into_space `i \<notin> I`
  1319       by (auto simp add: space_pair_measure) blast+
  1320     then show "?f -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M M i)"
  1321       using F by (auto intro!: pair_measureI)
  1322   qed
  1323   then show ?thesis
  1324     by (simp add: product_algebra_def)
  1325 qed
  1326 
  1327 lemma (in product_sigma_algebra) measurable_merge:
  1328   assumes [simp]: "I \<inter> J = {}"
  1329   shows "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
  1330 proof -
  1331   let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M"
  1332   interpret P: sigma_algebra "?I \<Otimes>\<^isub>M ?J"
  1333     by (intro sigma_algebra_pair_measure product_algebra_into_space)
  1334   let ?f = "\<lambda>(x, y). merge I x J y"
  1335   let ?G = "product_algebra_generator (I \<union> J) M"
  1336   have "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (sigma ?G)"
  1337   proof (rule P.measurable_sigma)
  1338     fix A assume "A \<in> sets ?G"
  1339     from product_algebraE[OF this]
  1340     obtain E where E: "A = Pi\<^isub>E (I \<union> J) E" "E \<in> (\<Pi> i\<in>I \<union> J. sets (M i))" .
  1341     then have *: "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) = Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
  1342       using sets_into_space `I \<inter> J = {}`
  1343       by (auto simp add: space_pair_measure) fast+
  1344     then show "?f -` A \<inter> space (?I \<Otimes>\<^isub>M ?J) \<in> sets (?I \<Otimes>\<^isub>M ?J)"
  1345       using E unfolding * by (auto intro!: pair_measureI in_sigma product_algebra_generatorI
  1346         simp: product_algebra_def)
  1347   qed (insert product_algebra_generator_into_space, auto simp: space_pair_measure)
  1348   then show "?f \<in> measurable (?I \<Otimes>\<^isub>M ?J) (Pi\<^isub>M (I \<union> J) M)"
  1349     unfolding product_algebra_def[of "I \<union> J"] by simp
  1350 qed
  1351 
  1352 lemma (in product_sigma_algebra) measurable_component_singleton:
  1353   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
  1354 proof (unfold measurable_def, intro CollectI conjI ballI)
  1355   fix A assume "A \<in> sets (M i)"
  1356   then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
  1357     using M.sets_into_space `i \<in> I` by (fastsimp dest: Pi_mem split: split_if_asm)
  1358   then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
  1359     using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
  1360 qed (insert `i \<in> I`, auto)
  1361 
  1362 locale product_sigma_finite =
  1363   fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
  1364   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
  1365 
  1366 locale finite_product_sigma_finite = product_sigma_finite M
  1367   for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
  1368   fixes I :: "'i set" assumes finite_index'[intro]: "finite I"
  1369 
  1370 sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
  1371   by (rule sigma_finite_measures)
  1372 
  1373 sublocale product_sigma_finite \<subseteq> product_sigma_algebra
  1374   by default
  1375 
  1376 sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
  1377   by default (fact finite_index')
  1378 
  1379 lemma setprod_extreal_0:
  1380   fixes f :: "'a \<Rightarrow> extreal"
  1381   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
  1382 proof cases
  1383   assume "finite A"
  1384   then show ?thesis by (induct A) auto
  1385 qed auto
  1386 
  1387 lemma setprod_extreal_pos:
  1388   fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
  1389 proof cases
  1390   assume "finite I" from this pos show ?thesis by induct auto
  1391 qed simp
  1392 
  1393 lemma setprod_PInf:
  1394   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
  1395   shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
  1396 proof cases
  1397   assume "finite I" from this assms show ?thesis
  1398   proof (induct I)
  1399     case (insert i I)
  1400     then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
  1401     from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
  1402     also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
  1403       using setprod_extreal_pos[of I f] pos
  1404       by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
  1405     also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
  1406       using insert by (auto simp: setprod_extreal_0)
  1407     finally show ?case .
  1408   qed simp
  1409 qed simp
  1410 
  1411 lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
  1412 proof cases
  1413   assume "finite A" then show ?thesis
  1414     by induct (auto simp: one_extreal_def)
  1415 qed (simp add: one_extreal_def)
  1416 
  1417 lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
  1418   assumes "Pi\<^isub>E I F \<in> sets G"
  1419   shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
  1420 proof cases
  1421   assume ne: "\<forall>i\<in>I. F i \<noteq> {}"
  1422   have "\<forall>i\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') i = F i"
  1423     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
  1424        (insert ne, auto simp: Pi_eq_iff)
  1425   then show ?thesis
  1426     unfolding product_algebra_generator_def by simp
  1427 next
  1428   assume empty: "\<not> (\<forall>j\<in>I. F j \<noteq> {})"
  1429   then have "(\<Prod>j\<in>I. M.\<mu> j (F j)) = 0"
  1430     by (auto simp: setprod_extreal_0 intro!: bexI)
  1431   moreover
  1432   have "\<exists>j\<in>I. (SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j = {}"
  1433     by (rule someI2[where P="\<lambda>F'. Pi\<^isub>E I F = Pi\<^isub>E I F'"])
  1434        (insert empty, auto simp: Pi_eq_empty_iff[symmetric])
  1435   then have "(\<Prod>j\<in>I. M.\<mu> j ((SOME F'. Pi\<^isub>E I F = Pi\<^isub>E I F') j)) = 0"
  1436     by (auto simp: setprod_extreal_0 intro!: bexI)
  1437   ultimately show ?thesis
  1438     unfolding product_algebra_generator_def by simp
  1439 qed
  1440 
  1441 lemma (in finite_product_sigma_finite) sigma_finite_pairs:
  1442   "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
  1443     (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
  1444     (\<forall>k. \<forall>i\<in>I. \<mu> i (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k) \<and>
  1445     (\<Union>k. \<Pi>\<^isub>E i\<in>I. F i k) = space G"
  1446 proof -
  1447   have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. \<mu> i (F k) \<noteq> \<infinity>)"
  1448     using M.sigma_finite_up by simp
  1449   from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
  1450   then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. \<mu> i (F i k) \<noteq> \<infinity>"
  1451     by auto
  1452   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I. F i k"
  1453   note space_product_algebra[simp]
  1454   show ?thesis
  1455   proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
  1456     fix i show "range (F i) \<subseteq> sets (M i)" by fact
  1457   next
  1458     fix i k show "\<mu> i (F i k) \<noteq> \<infinity>" by fact
  1459   next
  1460     fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space G"
  1461       using `\<And>i. range (F i) \<subseteq> sets (M i)` M.sets_into_space
  1462       by (force simp: image_subset_iff)
  1463   next
  1464     fix f assume "f \<in> space G"
  1465     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
  1466     show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
  1467   next
  1468     fix i show "?F i \<subseteq> ?F (Suc i)"
  1469       using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
  1470   qed
  1471 qed
  1472 
  1473 lemma sets_pair_cancel_measure[simp]:
  1474   "sets (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) = sets (M1 \<Otimes>\<^isub>M M2)"
  1475   "sets (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) = sets (M1 \<Otimes>\<^isub>M M2)"
  1476   unfolding pair_measure_def pair_measure_generator_def sets_sigma
  1477   by simp_all
  1478 
  1479 lemma measurable_pair_cancel_measure[simp]:
  1480   "measurable (M1\<lparr>measure := m1\<rparr> \<Otimes>\<^isub>M M2) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
  1481   "measurable (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m2\<rparr>) M = measurable (M1 \<Otimes>\<^isub>M M2) M"
  1482   "measurable M (M1\<lparr>measure := m3\<rparr> \<Otimes>\<^isub>M M2) = measurable M (M1 \<Otimes>\<^isub>M M2)"
  1483   "measurable M (M1 \<Otimes>\<^isub>M M2\<lparr>measure := m4\<rparr>) = measurable M (M1 \<Otimes>\<^isub>M M2)"
  1484   unfolding measurable_def by (auto simp add: space_pair_measure)
  1485 
  1486 lemma (in product_sigma_finite) product_measure_exists:
  1487   assumes "finite I"
  1488   shows "\<exists>\<nu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<nu> \<rparr>) \<and>
  1489     (\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i)))"
  1490 using `finite I` proof induct
  1491   case empty
  1492   interpret finite_product_sigma_finite M "{}" by default simp
  1493   let ?\<nu> = "(\<lambda>A. if A = {} then 0 else 1) :: 'd set \<Rightarrow> extreal"
  1494   show ?case
  1495   proof (intro exI conjI ballI)
  1496     have "sigma_algebra (sigma G \<lparr>measure := ?\<nu>\<rparr>)"
  1497       by (rule sigma_algebra_cong) (simp_all add: product_algebra_def)
  1498     then have "measure_space (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
  1499       by (rule finite_additivity_sufficient)
  1500          (simp_all add: positive_def additive_def sets_sigma
  1501                         product_algebra_generator_def image_constant)
  1502     then show "sigma_finite_measure (sigma G\<lparr>measure := ?\<nu>\<rparr>)"
  1503       by (auto intro!: exI[of _ "\<lambda>i. {\<lambda>_. undefined}"]
  1504                simp: sigma_finite_measure_def sigma_finite_measure_axioms_def
  1505                      product_algebra_generator_def)
  1506   qed auto
  1507 next
  1508   case (insert i I)
  1509   interpret finite_product_sigma_finite M I by default fact
  1510   have "finite (insert i I)" using `finite I` by auto
  1511   interpret I': finite_product_sigma_finite M "insert i I" by default fact
  1512   from insert obtain \<nu> where
  1513     prod: "\<And>A. A \<in> (\<Pi> i\<in>I. sets (M i)) \<Longrightarrow> \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))" and
  1514     "sigma_finite_measure (sigma G\<lparr> measure := \<nu> \<rparr>)" by auto
  1515   then interpret I: sigma_finite_measure "P\<lparr> measure := \<nu>\<rparr>" unfolding product_algebra_def by simp
  1516   interpret P: pair_sigma_finite "P\<lparr> measure := \<nu>\<rparr>" "M i" ..
  1517   let ?h = "(\<lambda>(f, y). f(i := y))"
  1518   let ?\<nu> = "\<lambda>A. P.\<mu> (?h -` A \<inter> space P.P)"
  1519   have I': "sigma_algebra (I'.P\<lparr> measure := ?\<nu> \<rparr>)"
  1520     by (rule I'.sigma_algebra_cong) simp_all
  1521   interpret I'': measure_space "I'.P\<lparr> measure := ?\<nu> \<rparr>"
  1522     using measurable_add_dim[OF `i \<notin> I`]
  1523     by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
  1524   show ?case
  1525   proof (intro exI[of _ ?\<nu>] conjI ballI)
  1526     let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
  1527     { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
  1528       then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
  1529         using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
  1530       show "?m (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. M.\<mu> i (A i))"
  1531         unfolding * using A
  1532         apply (subst P.pair_measure_times)
  1533         using A apply fastsimp
  1534         using A apply fastsimp
  1535         using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
  1536     note product = this
  1537     have *: "sigma I'.G\<lparr> measure := ?\<nu> \<rparr> = I'.P\<lparr> measure := ?\<nu> \<rparr>"
  1538       by (simp add: product_algebra_def)
  1539     show "sigma_finite_measure (sigma I'.G\<lparr> measure := ?\<nu> \<rparr>)"
  1540     proof (unfold *, default, simp)
  1541       from I'.sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
  1542       then have F: "\<And>j. j \<in> insert i I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
  1543         "incseq (\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k)"
  1544         "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
  1545         "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
  1546         by blast+
  1547       let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
  1548       show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
  1549           (\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
  1550       proof (intro exI[of _ ?F] conjI allI)
  1551         show "range ?F \<subseteq> sets I'.P" using F(1) by auto
  1552       next
  1553         from F(3) show "(\<Union>i. ?F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i))" by simp
  1554       next
  1555         fix j
  1556         have "\<And>k. k \<in> insert i I \<Longrightarrow> 0 \<le> measure (M k) (F k j)"
  1557           using F(1) by auto
  1558         with F `finite I` setprod_PInf[of "insert i I", OF this] show "?\<nu> (?F j) \<noteq> \<infinity>"
  1559           by (subst product) auto
  1560       qed
  1561     qed
  1562   qed
  1563 qed
  1564 
  1565 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure P
  1566   unfolding product_algebra_def
  1567   using product_measure_exists[OF finite_index]
  1568   by (rule someI2_ex) auto
  1569 
  1570 lemma (in finite_product_sigma_finite) measure_times:
  1571   assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
  1572   shows "\<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
  1573   unfolding product_algebra_def
  1574   using product_measure_exists[OF finite_index]
  1575   proof (rule someI2_ex, elim conjE)
  1576     fix \<nu> assume *: "\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<nu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
  1577     have "Pi\<^isub>E I A = Pi\<^isub>E I (\<lambda>i\<in>I. A i)" by (auto dest: Pi_mem)
  1578     then have "\<nu> (Pi\<^isub>E I A) = \<nu> (Pi\<^isub>E I (\<lambda>i\<in>I. A i))" by simp
  1579     also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i ((\<lambda>i\<in>I. A i) i))" using assms * by auto
  1580     finally show "measure (sigma G\<lparr>measure := \<nu>\<rparr>) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu> i (A i))"
  1581       by (simp add: sigma_def)
  1582   qed
  1583 
  1584 lemma (in product_sigma_finite) product_measure_empty[simp]:
  1585   "measure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
  1586 proof -
  1587   interpret finite_product_sigma_finite M "{}" by default auto
  1588   from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
  1589 qed
  1590 
  1591 lemma (in finite_product_sigma_algebra) P_empty:
  1592   assumes "I = {}"
  1593   shows "space P = {\<lambda>k. undefined}" "sets P = { {}, {\<lambda>k. undefined} }"
  1594   unfolding product_algebra_def product_algebra_generator_def `I = {}`
  1595   by (simp_all add: sigma_def image_constant)
  1596 
  1597 lemma (in product_sigma_finite) positive_integral_empty:
  1598   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
  1599   shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
  1600 proof -
  1601   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
  1602   have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
  1603     using assms by (subst measure_times) auto
  1604   then show ?thesis
  1605     unfolding positive_integral_def simple_function_def simple_integral_def_raw
  1606   proof (simp add: P_empty, intro antisym)
  1607     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
  1608       by (intro le_SUPI) (auto simp: le_fun_def split: split_max)
  1609     show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
  1610       by (intro SUP_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm)
  1611   qed
  1612 qed
  1613 
  1614 lemma (in product_sigma_finite) measure_fold:
  1615   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  1616   assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
  1617   shows "measure (Pi\<^isub>M (I \<union> J) M) A =
  1618     measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M))"
  1619 proof -
  1620   interpret I: finite_product_sigma_finite M I by default fact
  1621   interpret J: finite_product_sigma_finite M J by default fact
  1622   have "finite (I \<union> J)" using fin by auto
  1623   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
  1624   interpret P: pair_sigma_finite I.P J.P by default
  1625   let ?g = "\<lambda>(x,y). merge I x J y"
  1626   let "?X S" = "?g -` S \<inter> space P.P"
  1627   from IJ.sigma_finite_pairs obtain F where
  1628     F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
  1629        "incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
  1630        "(\<Union>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) = space IJ.G"
  1631        "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<infinity>"
  1632     by auto
  1633   let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
  1634   show "IJ.\<mu> A = P.\<mu> (?X A)"
  1635   proof (rule measure_unique_Int_stable_vimage)
  1636     show "measure_space IJ.P" "measure_space P.P" by default
  1637     show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
  1638       using A unfolding product_algebra_def by auto
  1639   next
  1640     show "Int_stable IJ.G"
  1641       by (simp add: PiE_Int Int_stable_def product_algebra_def
  1642                     product_algebra_generator_def)
  1643           auto
  1644     show "range ?F \<subseteq> sets IJ.G" using F
  1645       by (simp add: image_subset_iff product_algebra_def
  1646                     product_algebra_generator_def)
  1647     show "incseq ?F" "(\<Union>i. ?F i) = space IJ.G " by fact+
  1648   next
  1649     fix k
  1650     have "\<And>j. j \<in> I \<union> J \<Longrightarrow> 0 \<le> measure (M j) (F j k)"
  1651       using F(1) by auto
  1652     with F `finite I` setprod_PInf[of "I \<union> J", OF this]
  1653     show "IJ.\<mu> (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
  1654   next
  1655     fix A assume "A \<in> sets IJ.G"
  1656     then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
  1657       and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
  1658       by (auto simp: product_algebra_generator_def)
  1659     then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
  1660       using sets_into_space by (auto simp: space_pair_measure) blast+
  1661     then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
  1662       using `finite J` `finite I` F
  1663       by (simp add: P.pair_measure_times I.measure_times J.measure_times)
  1664     also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
  1665       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
  1666     also have "\<dots> = IJ.\<mu> A"
  1667       using `finite J` `finite I` F unfolding A
  1668       by (intro IJ.measure_times[symmetric]) auto
  1669     finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
  1670   qed (rule measurable_merge[OF IJ])
  1671 qed
  1672 
  1673 lemma (in product_sigma_finite) measure_preserving_merge:
  1674   assumes IJ: "I \<inter> J = {}" and "finite I" "finite J"
  1675   shows "(\<lambda>(x,y). merge I x J y) \<in> measure_preserving (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
  1676   by (intro measure_preservingI measurable_merge[OF IJ] measure_fold[symmetric] assms)
  1677 
  1678 lemma (in product_sigma_finite) product_positive_integral_fold:
  1679   assumes IJ[simp]: "I \<inter> J = {}" "finite I" "finite J"
  1680   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
  1681   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
  1682     (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
  1683 proof -
  1684   interpret I: finite_product_sigma_finite M I by default fact
  1685   interpret J: finite_product_sigma_finite M J by default fact
  1686   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
  1687   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default simp
  1688   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
  1689     using measurable_comp[OF measurable_merge[OF IJ(1)] f] by (simp add: comp_def)
  1690   show ?thesis
  1691     unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
  1692   proof (rule P.positive_integral_vimage)
  1693     show "sigma_algebra IJ.P" by default
  1694     show "(\<lambda>(x, y). merge I x J y) \<in> measure_preserving P.P IJ.P"
  1695       using IJ by (rule measure_preserving_merge)
  1696     show "f \<in> borel_measurable IJ.P" using f by simp
  1697   qed
  1698 qed
  1699 
  1700 lemma (in product_sigma_finite) measure_preserving_component_singelton:
  1701   "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
  1702 proof (intro measure_preservingI measurable_component_singleton)
  1703   interpret I: finite_product_sigma_finite M "{i}" by default simp
  1704   fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space I.P"
  1705   assume A: "A \<in> sets (M i)"
  1706   then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
  1707   show "I.\<mu> ?P = M.\<mu> i A" unfolding *
  1708     using A I.measure_times[of "\<lambda>_. A"] by auto
  1709 qed auto
  1710 
  1711 lemma (in product_sigma_finite) product_positive_integral_singleton:
  1712   assumes f: "f \<in> borel_measurable (M i)"
  1713   shows "integral\<^isup>P (Pi\<^isub>M {i} M) (\<lambda>x. f (x i)) = integral\<^isup>P (M i) f"
  1714 proof -
  1715   interpret I: finite_product_sigma_finite M "{i}" by default simp
  1716   show ?thesis
  1717   proof (rule I.positive_integral_vimage[symmetric])
  1718     show "sigma_algebra (M i)" by (rule sigma_algebras)
  1719     show "(\<lambda>x. x i) \<in> measure_preserving (Pi\<^isub>M {i} M) (M i)"
  1720       by (rule measure_preserving_component_singelton)
  1721     show "f \<in> borel_measurable (M i)" by fact
  1722   qed
  1723 qed
  1724 
  1725 lemma (in product_sigma_finite) product_positive_integral_insert:
  1726   assumes [simp]: "finite I" "i \<notin> I"
  1727     and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
  1728   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))"
  1729 proof -
  1730   interpret I: finite_product_sigma_finite M I by default auto
  1731   interpret i: finite_product_sigma_finite M "{i}" by default auto
  1732   interpret P: pair_sigma_algebra I.P i.P ..
  1733   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
  1734     using f by auto
  1735   show ?thesis
  1736     unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
  1737   proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
  1738     fix x assume x: "x \<in> space I.P"
  1739     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
  1740     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
  1741       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
  1742     show "?f \<in> borel_measurable (M i)" unfolding f'_eq
  1743       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
  1744       by (simp add: comp_def)
  1745     show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
  1746       unfolding f'_eq by simp
  1747   qed
  1748 qed
  1749 
  1750 lemma (in product_sigma_finite) product_positive_integral_setprod:
  1751   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> extreal"
  1752   assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
  1753   and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
  1754   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))"
  1755 using assms proof induct
  1756   case empty
  1757   interpret finite_product_sigma_finite M "{}" by default auto
  1758   then show ?case by simp
  1759 next
  1760   case (insert i I)
  1761   note `finite I`[intro, simp]
  1762   interpret I: finite_product_sigma_finite M I by default auto
  1763   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))"
  1764     using insert by (auto intro!: setprod_cong)
  1765   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)"
  1766     using sets_into_space insert
  1767     by (intro sigma_algebra.borel_measurable_extreal_setprod sigma_algebra_product_algebra
  1768               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
  1769        auto
  1770   then show ?case
  1771     apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
  1772     apply (simp add: insert * pos borel setprod_extreal_pos M.positive_integral_multc)
  1773     apply (subst I.positive_integral_cmult)
  1774     apply (auto simp add: pos borel insert setprod_extreal_pos positive_integral_positive)
  1775     done
  1776 qed
  1777 
  1778 lemma (in product_sigma_finite) product_integral_singleton:
  1779   assumes f: "f \<in> borel_measurable (M i)"
  1780   shows "(\<integral>x. f (x i) \<partial>Pi\<^isub>M {i} M) = integral\<^isup>L (M i) f"
  1781 proof -
  1782   interpret I: finite_product_sigma_finite M "{i}" by default simp
  1783   have *: "(\<lambda>x. extreal (f x)) \<in> borel_measurable (M i)"
  1784     "(\<lambda>x. extreal (- f x)) \<in> borel_measurable (M i)"
  1785     using assms by auto
  1786   show ?thesis
  1787     unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
  1788 qed
  1789 
  1790 lemma (in product_sigma_finite) product_integral_fold:
  1791   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  1792   and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
  1793   shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I x J y) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
  1794 proof -
  1795   interpret I: finite_product_sigma_finite M I by default fact
  1796   interpret J: finite_product_sigma_finite M J by default fact
  1797   have "finite (I \<union> J)" using fin by auto
  1798   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
  1799   interpret P: pair_sigma_finite I.P J.P by default
  1800   let ?M = "\<lambda>(x, y). merge I x J y"
  1801   let ?f = "\<lambda>x. f (?M x)"
  1802   show ?thesis
  1803   proof (subst P.integrable_fst_measurable(2)[of ?f, simplified])
  1804     have 1: "sigma_algebra IJ.P" by default
  1805     have 2: "?M \<in> measure_preserving P.P IJ.P" using measure_preserving_merge[OF assms(1,2,3)] .
  1806     have 3: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
  1807     then have 4: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
  1808       by (simp add: integrable_def)
  1809     show "integrable P.P ?f"
  1810       by (rule P.integrable_vimage[where f=f, OF 1 2 3])
  1811     show "integral\<^isup>L IJ.P f = integral\<^isup>L P.P ?f"
  1812       by (rule P.integral_vimage[where f=f, OF 1 2 4])
  1813   qed
  1814 qed
  1815 
  1816 lemma (in product_sigma_finite) product_integral_insert:
  1817   assumes [simp]: "finite I" "i \<notin> I"
  1818     and f: "integrable (Pi\<^isub>M (insert i I) M) f"
  1819   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)"
  1820 proof -
  1821   interpret I: finite_product_sigma_finite M I by default auto
  1822   interpret I': finite_product_sigma_finite M "insert i I" by default auto
  1823   interpret i: finite_product_sigma_finite M "{i}" by default auto
  1824   interpret P: pair_sigma_finite I.P i.P ..
  1825   have IJ: "I \<inter> {i} = {}" by auto
  1826   show ?thesis
  1827     unfolding product_integral_fold[OF IJ, simplified, OF f]
  1828   proof (rule I.integral_cong, subst product_integral_singleton)
  1829     fix x assume x: "x \<in> space I.P"
  1830     let "?f y" = "f (restrict (x(i := y)) (insert i I))"
  1831     have f'_eq: "\<And>y. ?f y = f (x(i := y))"
  1832       using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
  1833     have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
  1834     show "?f \<in> borel_measurable (M i)"
  1835       unfolding measurable_cong[OF f'_eq]
  1836       using measurable_comp[OF measurable_component_update f] x `i \<notin> I`
  1837       by (simp add: comp_def)
  1838     show "integral\<^isup>L (M i) ?f = integral\<^isup>L (M i) (\<lambda>y. f (x(i := y)))"
  1839       unfolding f'_eq by simp
  1840   qed
  1841 qed
  1842 
  1843 lemma (in product_sigma_finite) product_integrable_setprod:
  1844   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
  1845   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1846   shows "integrable (Pi\<^isub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  1847 proof -
  1848   interpret finite_product_sigma_finite M I by default fact
  1849   have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
  1850     using integrable unfolding integrable_def by auto
  1851   then have borel: "?f \<in> borel_measurable P"
  1852     using measurable_comp[OF measurable_component_singleton f]
  1853     by (auto intro!: borel_measurable_setprod simp: comp_def)
  1854   moreover have "integrable (Pi\<^isub>M I M) (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
  1855   proof (unfold integrable_def, intro conjI)
  1856     show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
  1857       using borel by auto
  1858     have "(\<integral>\<^isup>+x. extreal (abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. (\<Prod>i\<in>I. extreal (abs (f i (x i)))) \<partial>P)"
  1859       by (simp add: setprod_extreal abs_setprod)
  1860     also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^isup>+x. extreal (abs (f i x)) \<partial>M i))"
  1861       using f by (subst product_positive_integral_setprod) auto
  1862     also have "\<dots> < \<infinity>"
  1863       using integrable[THEN M.integrable_abs]
  1864       by (simp add: setprod_PInf integrable_def M.positive_integral_positive)
  1865     finally show "(\<integral>\<^isup>+x. extreal (abs (?f x)) \<partial>P) \<noteq> \<infinity>" by auto
  1866     have "(\<integral>\<^isup>+x. extreal (- abs (?f x)) \<partial>P) = (\<integral>\<^isup>+x. 0 \<partial>P)"
  1867       by (intro positive_integral_cong_pos) auto
  1868     then show "(\<integral>\<^isup>+x. extreal (- abs (?f x)) \<partial>P) \<noteq> \<infinity>" by simp
  1869   qed
  1870   ultimately show ?thesis
  1871     by (rule integrable_abs_iff[THEN iffD1])
  1872 qed
  1873 
  1874 lemma (in product_sigma_finite) product_integral_setprod:
  1875   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
  1876   assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1877   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))"
  1878 using assms proof (induct rule: finite_ne_induct)
  1879   case (singleton i)
  1880   then show ?case by (simp add: product_integral_singleton integrable_def)
  1881 next
  1882   case (insert i I)
  1883   then have iI: "finite (insert i I)" by auto
  1884   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
  1885     integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
  1886     by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
  1887   interpret I: finite_product_sigma_finite M I by default fact
  1888   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))"
  1889     using `i \<notin> I` by (auto intro!: setprod_cong)
  1890   show ?case
  1891     unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
  1892     by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
  1893 qed
  1894 
  1895 section "Products on finite spaces"
  1896 
  1897 lemma sigma_sets_pair_measure_generator_finite:
  1898   assumes "finite A" and "finite B"
  1899   shows "sigma_sets (A \<times> B) { a \<times> b | a b. a \<in> Pow A \<and> b \<in> Pow B} = Pow (A \<times> B)"
  1900   (is "sigma_sets ?prod ?sets = _")
  1901 proof safe
  1902   have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
  1903   fix x assume subset: "x \<subseteq> A \<times> B"
  1904   hence "finite x" using fin by (rule finite_subset)
  1905   from this subset show "x \<in> sigma_sets ?prod ?sets"
  1906   proof (induct x)
  1907     case empty show ?case by (rule sigma_sets.Empty)
  1908   next
  1909     case (insert a x)
  1910     hence "{a} \<in> sigma_sets ?prod ?sets"
  1911       by (auto simp: pair_measure_generator_def intro!: sigma_sets.Basic)
  1912     moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
  1913     ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
  1914   qed
  1915 next
  1916   fix x a b
  1917   assume "x \<in> sigma_sets ?prod ?sets" and "(a, b) \<in> x"
  1918   from sigma_sets_into_sp[OF _ this(1)] this(2)
  1919   show "a \<in> A" and "b \<in> B" by auto
  1920 qed
  1921 
  1922 locale pair_finite_sigma_algebra = M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2
  1923   for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
  1924 
  1925 sublocale pair_finite_sigma_algebra \<subseteq> pair_sigma_algebra by default
  1926 
  1927 lemma (in pair_finite_sigma_algebra) finite_pair_sigma_algebra:
  1928   shows "P = \<lparr> space = space M1 \<times> space M2, sets = Pow (space M1 \<times> space M2), \<dots> = algebra.more P \<rparr>"
  1929 proof -
  1930   show ?thesis
  1931     using sigma_sets_pair_measure_generator_finite[OF M1.finite_space M2.finite_space]
  1932     by (intro algebra.equality) (simp_all add: pair_measure_def pair_measure_generator_def sigma_def)
  1933 qed
  1934 
  1935 sublocale pair_finite_sigma_algebra \<subseteq> finite_sigma_algebra P
  1936   apply default
  1937   using M1.finite_space M2.finite_space
  1938   apply (subst finite_pair_sigma_algebra) apply simp
  1939   apply (subst (1 2) finite_pair_sigma_algebra) apply simp
  1940   done
  1941 
  1942 locale pair_finite_space = M1: finite_measure_space M1 + M2: finite_measure_space M2
  1943   for M1 M2
  1944 
  1945 sublocale pair_finite_space \<subseteq> pair_finite_sigma_algebra
  1946   by default
  1947 
  1948 sublocale pair_finite_space \<subseteq> pair_sigma_finite
  1949   by default
  1950 
  1951 lemma (in pair_finite_space) pair_measure_Pair[simp]:
  1952   assumes "a \<in> space M1" "b \<in> space M2"
  1953   shows "\<mu> {(a, b)} = M1.\<mu> {a} * M2.\<mu> {b}"
  1954 proof -
  1955   have "\<mu> ({a}\<times>{b}) = M1.\<mu> {a} * M2.\<mu> {b}"
  1956     using M1.sets_eq_Pow M2.sets_eq_Pow assms
  1957     by (subst pair_measure_times) auto
  1958   then show ?thesis by simp
  1959 qed
  1960 
  1961 lemma (in pair_finite_space) pair_measure_singleton[simp]:
  1962   assumes "x \<in> space M1 \<times> space M2"
  1963   shows "\<mu> {x} = M1.\<mu> {fst x} * M2.\<mu> {snd x}"
  1964   using pair_measure_Pair assms by (cases x) auto
  1965 
  1966 sublocale pair_finite_space \<subseteq> finite_measure_space P
  1967   by default (auto simp: space_pair_measure)
  1968 
  1969 end