src/HOL/Probability/Product_Measure.thy
 author hoelzl Mon Dec 06 19:54:56 2010 +0100 (2010-12-06) changeset 41026 bea75746dc9d parent 41023 9118eb4eb8dc child 41095 c335d880ff82 permissions -rw-r--r--
folding on arbitrary Lebesgue integrable functions
 hoelzl@35833  1 theory Product_Measure  hoelzl@38656  2 imports Lebesgue_Integration  hoelzl@35833  3 begin  hoelzl@35833  4 hoelzl@40859  5 lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)"  hoelzl@40859  6  by auto  hoelzl@40859  7 hoelzl@40859  8 lemma Pair_vimage_times[simp]: "\A B x. Pair x - (A \ B) = (if x \ A then B else {})"  hoelzl@40859  9  by auto  hoelzl@40859  10 hoelzl@40859  11 lemma rev_Pair_vimage_times[simp]: "\A B y. (\x. (x, y)) - (A \ B) = (if y \ B then A else {})"  hoelzl@40859  12  by auto  hoelzl@40859  13 hoelzl@40859  14 lemma case_prod_distrib: "f (case x of (x, y) \ g x y) = (case x of (x, y) \ f (g x y))"  hoelzl@40859  15  by (cases x) simp  hoelzl@40859  16 hoelzl@41026  17 lemma split_beta': "($$x,y). f x y) = (\x. f (fst x) (snd x))"  hoelzl@41026  18  by (auto simp: fun_eq_iff)  hoelzl@41026  19 hoelzl@40859  20 abbreviation  hoelzl@40859  21  "Pi\<^isub>E A B \ Pi A B \ extensional A"  hellerar@39094  22 hoelzl@40859  23 abbreviation  hoelzl@40859  24  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"  hoelzl@40859  25  (infixr "->\<^isub>E" 60) where  hoelzl@40859  26  "A ->\<^isub>E B \ Pi\<^isub>E A (%_. B)"  hoelzl@40859  27 hoelzl@40859  28 notation (xsymbols)  hoelzl@40859  29  funcset_extensional (infixr "\\<^isub>E" 60)  hoelzl@40859  30 hoelzl@40859  31 lemma extensional_empty[simp]: "extensional {} = {\x. undefined}"  hoelzl@40859  32  by safe (auto simp add: extensional_def fun_eq_iff)  hoelzl@40859  33 hoelzl@40859  34 lemma extensional_insert[intro, simp]:  hoelzl@40859  35  assumes "a \ extensional (insert i I)"  hoelzl@40859  36  shows "a(i := b) \ extensional (insert i I)"  hoelzl@40859  37  using assms unfolding extensional_def by auto  hoelzl@40859  38 hoelzl@40859  39 lemma extensional_Int[simp]:  hoelzl@40859  40  "extensional I \ extensional I' = extensional (I \ I')"  hoelzl@40859  41  unfolding extensional_def by auto  hoelzl@38656  42 hoelzl@35833  43 definition  hoelzl@40859  44  "merge I x J y = (\i. if i \ I then x i else if i \ J then y i else undefined)"  hoelzl@40859  45 hoelzl@40859  46 lemma merge_apply[simp]:  hoelzl@40859  47  "I \ J = {} \ i \ I \ merge I x J y i = x i"  hoelzl@40859  48  "I \ J = {} \ i \ J \ merge I x J y i = y i"  hoelzl@40859  49  "J \ I = {} \ i \ I \ merge I x J y i = x i"  hoelzl@40859  50  "J \ I = {} \ i \ J \ merge I x J y i = y i"  hoelzl@40859  51  "i \ I \ i \ J \ merge I x J y i = undefined"  hoelzl@40859  52  unfolding merge_def by auto  hoelzl@40859  53 hoelzl@40859  54 lemma merge_commute:  hoelzl@40859  55  "I \ J = {} \ merge I x J y = merge J y I x"  hoelzl@40859  56  by (auto simp: merge_def intro!: ext)  hoelzl@40859  57 hoelzl@40859  58 lemma Pi_cancel_merge_range[simp]:  hoelzl@40859  59  "I \ J = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  hoelzl@40859  60  "I \ J = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  hoelzl@40859  61  "J \ I = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  hoelzl@40859  62  "J \ I = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  hoelzl@40859  63  by (auto simp: Pi_def)  hoelzl@40859  64 hoelzl@40859  65 lemma Pi_cancel_merge[simp]:  hoelzl@40859  66  "I \ J = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  hoelzl@40859  67  "J \ I = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  hoelzl@40859  68  "I \ J = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  hoelzl@40859  69  "J \ I = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  hoelzl@40859  70  by (auto simp: Pi_def)  hoelzl@40859  71 hoelzl@40859  72 lemma extensional_merge[simp]: "merge I x J y \ extensional (I \ J)"  hoelzl@40859  73  by (auto simp: extensional_def)  hoelzl@40859  74 hoelzl@40859  75 lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A"  hoelzl@40859  76  by (auto simp: restrict_def Pi_def)  hoelzl@40859  77 hoelzl@40859  78 lemma restrict_merge[simp]:  hoelzl@40859  79  "I \ J = {} \ restrict (merge I x J y) I = restrict x I"  hoelzl@40859  80  "I \ J = {} \ restrict (merge I x J y) J = restrict y J"  hoelzl@40859  81  "J \ I = {} \ restrict (merge I x J y) I = restrict x I"  hoelzl@40859  82  "J \ I = {} \ restrict (merge I x J y) J = restrict y J"  hoelzl@40859  83  by (auto simp: restrict_def intro!: ext)  hoelzl@40859  84 hoelzl@40859  85 lemma extensional_insert_undefined[intro, simp]:  hoelzl@40859  86  assumes "a \ extensional (insert i I)"  hoelzl@40859  87  shows "a(i := undefined) \ extensional I"  hoelzl@40859  88  using assms unfolding extensional_def by auto  hoelzl@40859  89 hoelzl@40859  90 lemma extensional_insert_cancel[intro, simp]:  hoelzl@40859  91  assumes "a \ extensional I"  hoelzl@40859  92  shows "a \ extensional (insert i I)"  hoelzl@40859  93  using assms unfolding extensional_def by auto  hoelzl@40859  94 hoelzl@40859  95 lemma PiE_Int: "(Pi\<^isub>E I A) \ (Pi\<^isub>E I B) = Pi\<^isub>E I (\x. A x \ B x)"  hoelzl@40859  96  by auto  hoelzl@40859  97 hoelzl@40859  98 lemma Pi_cancel_fupd_range[simp]: "i \ I \ x \ Pi I (B(i := b)) \ x \ Pi I B"  hoelzl@40859  99  by (auto simp: Pi_def)  hoelzl@40859  100 hoelzl@40859  101 lemma Pi_split_insert_domain[simp]: "x \ Pi (insert i I) X \ x \ Pi I X \ x i \ X i"  hoelzl@40859  102  by (auto simp: Pi_def)  hoelzl@39088  103 hoelzl@40859  104 lemma Pi_split_domain[simp]: "x \ Pi (I \ J) X \ x \ Pi I X \ x \ Pi J X"  hoelzl@40859  105  by (auto simp: Pi_def)  hoelzl@40859  106 hoelzl@40859  107 lemma Pi_cancel_fupd[simp]: "i \ I \ x(i := a) \ Pi I B \ x \ Pi I B"  hoelzl@40859  108  by (auto simp: Pi_def)  hoelzl@40859  109 hoelzl@40859  110 section "Binary products"  hoelzl@40859  111 hoelzl@40859  112 definition  hoelzl@40859  113  "pair_algebra A B = \ space = space A \ space B,  hoelzl@40859  114  sets = {a \ b | a b. a \ sets A \ b \ sets B} \"  hoelzl@40859  115 hoelzl@40859  116 locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2  hoelzl@40859  117  for M1 M2  hoelzl@40859  118 hoelzl@40859  119 abbreviation (in pair_sigma_algebra)  hoelzl@40859  120  "E \ pair_algebra M1 M2"  hoelzl@40859  121 hoelzl@40859  122 abbreviation (in pair_sigma_algebra)  hoelzl@40859  123  "P \ sigma E"  hoelzl@40859  124 hoelzl@40859  125 sublocale pair_sigma_algebra \ sigma_algebra P  hoelzl@40859  126  using M1.sets_into_space M2.sets_into_space  hoelzl@40859  127  by (force simp: pair_algebra_def intro!: sigma_algebra_sigma)  hoelzl@40859  128 hoelzl@40859  129 lemma pair_algebraI[intro, simp]:  hoelzl@40859  130  "x \ sets A \ y \ sets B \ x \ y \ sets (pair_algebra A B)"  hoelzl@40859  131  by (auto simp add: pair_algebra_def)  hoelzl@40859  132 hoelzl@40859  133 lemma space_pair_algebra:  hoelzl@40859  134  "space (pair_algebra A B) = space A \ space B"  hoelzl@40859  135  by (simp add: pair_algebra_def)  hoelzl@40859  136 hoelzl@40859  137 lemma pair_algebra_Int_snd:  hoelzl@40859  138  assumes "sets S1 \ Pow (space S1)"  hoelzl@40859  139  shows "pair_algebra S1 (algebra.restricted_space S2 A) =  hoelzl@40859  140  algebra.restricted_space (pair_algebra S1 S2) (space S1 \ A)"  hoelzl@40859  141  (is "?L = ?R")  hoelzl@40859  142 proof (intro algebra.equality set_eqI iffI)  hoelzl@40859  143  fix X assume "X \ sets ?L"  hoelzl@40859  144  then obtain A1 A2 where X: "X = A1 \ (A \ A2)" and "A1 \ sets S1" "A2 \ sets S2"  hoelzl@40859  145  by (auto simp: pair_algebra_def)  hoelzl@40859  146  then show "X \ sets ?R" unfolding pair_algebra_def  hoelzl@40859  147  using assms apply simp by (intro image_eqI[of _ _ "A1 \ A2"]) auto  hoelzl@40859  148 next  hoelzl@40859  149  fix X assume "X \ sets ?R"  hoelzl@40859  150  then obtain A1 A2 where "X = space S1 \ A \ A1 \ A2" "A1 \ sets S1" "A2 \ sets S2"  hoelzl@40859  151  by (auto simp: pair_algebra_def)  hoelzl@40859  152  moreover then have "X = A1 \ (A \ A2)"  hoelzl@40859  153  using assms by auto  hoelzl@40859  154  ultimately show "X \ sets ?L"  hoelzl@40859  155  unfolding pair_algebra_def by auto  hoelzl@40859  156 qed (auto simp add: pair_algebra_def)  hoelzl@40859  157 hoelzl@40859  158 lemma (in pair_sigma_algebra)  hoelzl@40859  159  shows measurable_fst[intro!, simp]:  hoelzl@40859  160  "fst \ measurable P M1" (is ?fst)  hoelzl@40859  161  and measurable_snd[intro!, simp]:  hoelzl@40859  162  "snd \ measurable P M2" (is ?snd)  hoelzl@39088  163 proof -  hoelzl@39088  164  { fix X assume "X \ sets M1"  hoelzl@39088  165  then have "\X1\sets M1. \X2\sets M2. fst - X \ space M1 \ space M2 = X1 \ X2"  hoelzl@39088  166  apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])  hoelzl@39088  167  using M1.sets_into_space by force+ }  hoelzl@39088  168  moreover  hoelzl@39088  169  { fix X assume "X \ sets M2"  hoelzl@39088  170  then have "\X1\sets M1. \X2\sets M2. snd - X \ space M1 \ space M2 = X1 \ X2"  hoelzl@39088  171  apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])  hoelzl@39088  172  using M2.sets_into_space by force+ }  hoelzl@40859  173  ultimately have "?fst \ ?snd"  hoelzl@40859  174  by (fastsimp simp: measurable_def sets_sigma space_pair_algebra  hoelzl@40859  175  intro!: sigma_sets.Basic)  hoelzl@40859  176  then show ?fst ?snd by auto  hoelzl@40859  177 qed  hoelzl@40859  178 hoelzl@40859  179 lemma (in pair_sigma_algebra) measurable_pair:  hoelzl@40859  180  assumes "sigma_algebra M"  hoelzl@40859  181  shows "f \ measurable M P \  hoelzl@40859  182  (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2"  hoelzl@40859  183 proof -  hoelzl@40859  184  interpret M: sigma_algebra M by fact  hoelzl@40859  185  from assms show ?thesis  hoelzl@40859  186  proof (safe intro!: measurable_comp[where b=P])  hoelzl@40859  187  assume f: "(fst \ f) \ measurable M M1" and s: "(snd \ f) \ measurable M M2"  hoelzl@40859  188  show "f \ measurable M P"  hoelzl@40859  189  proof (rule M.measurable_sigma)  hoelzl@40859  190  show "sets (pair_algebra M1 M2) \ Pow (space E)"  hoelzl@40859  191  unfolding pair_algebra_def using M1.sets_into_space M2.sets_into_space by auto  hoelzl@40859  192  show "f \ space M \ space E"  hoelzl@40859  193  using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma space_pair_algebra)  hoelzl@40859  194  fix A assume "A \ sets E"  hoelzl@40859  195  then obtain B C where "B \ sets M1" "C \ sets M2" "A = B \ C"  hoelzl@40859  196  unfolding pair_algebra_def by auto  hoelzl@40859  197  moreover have "(fst \ f) - B \ space M \ sets M"  hoelzl@40859  198  using f B \ sets M1 unfolding measurable_def by auto  hoelzl@40859  199  moreover have "(snd \ f) - C \ space M \ sets M"  hoelzl@40859  200  using s C \ sets M2 unfolding measurable_def by auto  hoelzl@40859  201  moreover have "f - A \ space M = ((fst \ f) - B \ space M) \ ((snd \ f) - C \ space M)"  hoelzl@40859  202  unfolding A = B \ C by (auto simp: vimage_Times)  hoelzl@40859  203  ultimately show "f - A \ space M \ sets M" by auto  hoelzl@40859  204  qed  hoelzl@40859  205  qed  hoelzl@40859  206 qed  hoelzl@40859  207 hoelzl@40859  208 lemma (in pair_sigma_algebra) measurable_prod_sigma:  hoelzl@40859  209  assumes "sigma_algebra M"  hoelzl@40859  210  assumes 1: "(fst \ f) \ measurable M M1" and 2: "(snd \ f) \ measurable M M2"  hoelzl@40859  211  shows "f \ measurable M P"  hoelzl@40859  212 proof -  hoelzl@40859  213  interpret M: sigma_algebra M by fact  hoelzl@40859  214  from 1 have fn1: "fst \ f \ space M \ space M1"  hoelzl@40859  215  and q1: "\y\sets M1. (fst \ f) - y \ space M \ sets M"  hoelzl@40859  216  by (auto simp add: measurable_def)  hoelzl@40859  217  from 2 have fn2: "snd \ f \ space M \ space M2"  hoelzl@40859  218  and q2: "\y\sets M2. (snd \ f) - y \ space M \ sets M"  hoelzl@40859  219  by (auto simp add: measurable_def)  hoelzl@40859  220  show ?thesis  hoelzl@40859  221  proof (rule M.measurable_sigma)  hoelzl@40859  222  show "sets E \ Pow (space E)"  hoelzl@40859  223  using M1.space_closed M2.space_closed  hoelzl@40859  224  by (auto simp add: sigma_algebra_iff pair_algebra_def)  hoelzl@40859  225  next  hoelzl@40859  226  show "f \ space M \ space E"  hoelzl@40859  227  by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])  hoelzl@40859  228  next  hoelzl@40859  229  fix z  hoelzl@40859  230  assume z: "z \ sets E"  hoelzl@40859  231  thus "f - z \ space M \ sets M"  hoelzl@40859  232  proof (auto simp add: pair_algebra_def vimage_Times)  hoelzl@40859  233  fix x y  hoelzl@40859  234  assume x: "x \ sets M1" and y: "y \ sets M2"  hoelzl@40859  235  have "(fst \ f) - x \ (snd \ f) - y \ space M =  hoelzl@40859  236  ((fst \ f) - x \ space M) \ ((snd \ f) - y \ space M)"  hoelzl@40859  237  by blast  hoelzl@40859  238  also have "... \ sets M" using x y q1 q2  hoelzl@40859  239  by blast  hoelzl@40859  240  finally show "(fst \ f) - x \ (snd \ f) - y \ space M \ sets M" .  hoelzl@40859  241  qed  hoelzl@40859  242  qed  hoelzl@40859  243 qed  hoelzl@40859  244 hoelzl@40859  245 lemma pair_algebraE:  hoelzl@40859  246  assumes "X \ sets (pair_algebra M1 M2)"  hoelzl@40859  247  obtains A B where "X = A \ B" "A \ sets M1" "B \ sets M2"  hoelzl@40859  248  using assms unfolding pair_algebra_def by auto  hoelzl@40859  249 hoelzl@40859  250 lemma (in pair_sigma_algebra) pair_algebra_swap:  hoelzl@40859  251  "(\X. (\(x,y). (y,x)) - X \ space M2 \ space M1)  sets E = sets (pair_algebra M2 M1)"  hoelzl@40859  252 proof (safe elim!: pair_algebraE)  hoelzl@40859  253  fix A B assume "A \ sets M1" "B \ sets M2"  hoelzl@40859  254  moreover then have "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 = B \ A"  hoelzl@40859  255  using M1.sets_into_space M2.sets_into_space by auto  hoelzl@40859  256  ultimately show "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 \ sets (pair_algebra M2 M1)"  hoelzl@40859  257  by (auto intro: pair_algebraI)  hoelzl@40859  258 next  hoelzl@40859  259  fix A B assume "A \ sets M1" "B \ sets M2"  hoelzl@40859  260  then show "B \ A \ (\X. (\(x, y). (y, x)) - X \ space M2 \ space M1)  sets E"  hoelzl@40859  261  using M1.sets_into_space M2.sets_into_space  hoelzl@40859  262  by (auto intro!: image_eqI[where x="A \ B"] pair_algebraI)  hoelzl@40859  263 qed  hoelzl@40859  264 hoelzl@40859  265 lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap:  hoelzl@40859  266  assumes Q: "Q \ sets P"  hoelzl@40859  267  shows "(\(x,y). (y, x))  Q \ sets (sigma (pair_algebra M2 M1))" (is "_ \ sets ?Q")  hoelzl@40859  268 proof -  hoelzl@40859  269  have *: "(\(x,y). (y, x)) \ space M2 \ space M1 \ (space M1 \ space M2)"  hoelzl@40859  270  "sets (pair_algebra M1 M2) \ Pow (space M1 \ space M2)"  hoelzl@40859  271  using M1.sets_into_space M2.sets_into_space by (auto elim!: pair_algebraE)  hoelzl@40859  272  from Q sets_into_space show ?thesis  hoelzl@40859  273  by (auto intro!: image_eqI[where x=Q]  hoelzl@40859  274  simp: pair_algebra_swap[symmetric] sets_sigma  hoelzl@40859  275  sigma_sets_vimage[OF *] space_pair_algebra)  hoelzl@40859  276 qed  hoelzl@40859  277 hoelzl@40859  278 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable:  hoelzl@40859  279  shows "(\(x,y). (y, x)) \ measurable P (sigma (pair_algebra M2 M1))"  hoelzl@40859  280  (is "?f \ measurable ?P ?Q")  hoelzl@40859  281  unfolding measurable_def  hoelzl@40859  282 proof (intro CollectI conjI Pi_I ballI)  hoelzl@40859  283  fix x assume "x \ space ?P" then show "(case x of (x, y) \ (y, x)) \ space ?Q"  hoelzl@40859  284  unfolding pair_algebra_def by auto  hoelzl@40859  285 next  hoelzl@40859  286  fix A assume "A \ sets ?Q"  hoelzl@40859  287  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  288  have "?f - A \ space ?P = (\(x,y). (y, x))  A"  hoelzl@40859  289  using Q.sets_into_space A \ sets ?Q by (auto simp: pair_algebra_def)  hoelzl@40859  290  with Q.sets_pair_sigma_algebra_swap[OF A \ sets ?Q]  hoelzl@40859  291  show "?f - A \ space ?P \ sets ?P" by simp  hoelzl@40859  292 qed  hoelzl@40859  293 hoelzl@40859  294 lemma (in pair_sigma_algebra) measurable_cut_fst:  hoelzl@40859  295  assumes "Q \ sets P" shows "Pair x - Q \ sets M2"  hoelzl@40859  296 proof -  hoelzl@40859  297  let ?Q' = "{Q. Q \ space P \ Pair x - Q \ sets M2}"  hoelzl@40859  298  let ?Q = "\ space = space P, sets = ?Q' \"  hoelzl@40859  299  interpret Q: sigma_algebra ?Q  hoelzl@40859  300  proof qed (auto simp: vimage_UN vimage_Diff space_pair_algebra)  hoelzl@40859  301  have "sets E \ sets ?Q"  hoelzl@40859  302  using M1.sets_into_space M2.sets_into_space  hoelzl@40859  303  by (auto simp: pair_algebra_def space_pair_algebra)  hoelzl@40859  304  then have "sets P \ sets ?Q"  hoelzl@40859  305  by (subst pair_algebra_def, intro Q.sets_sigma_subset)  hoelzl@40859  306  (simp_all add: pair_algebra_def)  hoelzl@40859  307  with assms show ?thesis by auto  hoelzl@40859  308 qed  hoelzl@40859  309 hoelzl@40859  310 lemma (in pair_sigma_algebra) measurable_cut_snd:  hoelzl@40859  311  assumes Q: "Q \ sets P" shows "(\x. (x, y)) - Q \ sets M1" (is "?cut Q \ sets M1")  hoelzl@40859  312 proof -  hoelzl@40859  313  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  314  have "Pair y - (\(x, y). (y, x))  Q = (\x. (x, y)) - Q" by auto  hoelzl@40859  315  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]  hoelzl@40859  316  show ?thesis by simp  hoelzl@40859  317 qed  hoelzl@40859  318 hoelzl@40859  319 lemma (in pair_sigma_algebra) measurable_pair_image_snd:  hoelzl@40859  320  assumes m: "f \ measurable P M" and "x \ space M1"  hoelzl@40859  321  shows "(\y. f (x, y)) \ measurable M2 M"  hoelzl@40859  322  unfolding measurable_def  hoelzl@40859  323 proof (intro CollectI conjI Pi_I ballI)  hoelzl@40859  324  fix y assume "y \ space M2" with f \ measurable P M x \ space M1  hoelzl@40859  325  show "f (x, y) \ space M" unfolding measurable_def pair_algebra_def by auto  hoelzl@40859  326 next  hoelzl@40859  327  fix A assume "A \ sets M"  hoelzl@40859  328  then have "Pair x - (f - A \ space P) \ sets M2" (is "?C \ _")  hoelzl@40859  329  using f \ measurable P M  hoelzl@40859  330  by (intro measurable_cut_fst) (auto simp: measurable_def)  hoelzl@40859  331  also have "?C = (\y. f (x, y)) - A \ space M2"  hoelzl@40859  332  using x \ space M1 by (auto simp: pair_algebra_def)  hoelzl@40859  333  finally show "(\y. f (x, y)) - A \ space M2 \ sets M2" .  hoelzl@40859  334 qed  hoelzl@40859  335 hoelzl@40859  336 lemma (in pair_sigma_algebra) measurable_pair_image_fst:  hoelzl@40859  337  assumes m: "f \ measurable P M" and "y \ space M2"  hoelzl@40859  338  shows "(\x. f (x, y)) \ measurable M1 M"  hoelzl@40859  339 proof -  hoelzl@40859  340  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  341  from Q.measurable_pair_image_snd[OF measurable_comp y \ space M2,  hoelzl@40859  342  OF Q.pair_sigma_algebra_swap_measurable m]  hoelzl@40859  343  show ?thesis by simp  hoelzl@40859  344 qed  hoelzl@40859  345 hoelzl@40859  346 lemma (in pair_sigma_algebra) Int_stable_pair_algebra: "Int_stable E"  hoelzl@40859  347  unfolding Int_stable_def  hoelzl@40859  348 proof (intro ballI)  hoelzl@40859  349  fix A B assume "A \ sets E" "B \ sets E"  hoelzl@40859  350  then obtain A1 A2 B1 B2 where "A = A1 \ A2" "B = B1 \ B2"  hoelzl@40859  351  "A1 \ sets M1" "A2 \ sets M2" "B1 \ sets M1" "B2 \ sets M2"  hoelzl@40859  352  unfolding pair_algebra_def by auto  hoelzl@40859  353  then show "A \ B \ sets E"  hoelzl@40859  354  by (auto simp add: times_Int_times pair_algebra_def)  hoelzl@40859  355 qed  hoelzl@40859  356 hoelzl@40859  357 lemma finite_measure_cut_measurable:  hoelzl@40859  358  fixes M1 :: "'a algebra" and M2 :: "'b algebra"  hoelzl@40859  359  assumes "sigma_finite_measure M1 \1" "finite_measure M2 \2"  hoelzl@40859  360  assumes "Q \ sets (sigma (pair_algebra M1 M2))"  hoelzl@40859  361  shows "(\x. \2 (Pair x - Q)) \ borel_measurable M1"  hoelzl@40859  362  (is "?s Q \ _")  hoelzl@40859  363 proof -  hoelzl@40859  364  interpret M1: sigma_finite_measure M1 \1 by fact  hoelzl@40859  365  interpret M2: finite_measure M2 \2 by fact  hoelzl@40859  366  interpret pair_sigma_algebra M1 M2 by default  hoelzl@40859  367  have [intro]: "sigma_algebra M1" by fact  hoelzl@40859  368  have [intro]: "sigma_algebra M2" by fact  hoelzl@40859  369  let ?D = "\ space = space P, sets = {A\sets P. ?s A \ borel_measurable M1} \"  hoelzl@40859  370  note space_pair_algebra[simp]  hoelzl@40859  371  interpret dynkin_system ?D  hoelzl@40859  372  proof (intro dynkin_systemI)  hoelzl@40859  373  fix A assume "A \ sets ?D" then show "A \ space ?D"  hoelzl@40859  374  using sets_into_space by simp  hoelzl@40859  375  next  hoelzl@40859  376  from top show "space ?D \ sets ?D"  hoelzl@40859  377  by (auto simp add: if_distrib intro!: M1.measurable_If)  hoelzl@40859  378  next  hoelzl@40859  379  fix A assume "A \ sets ?D"  hoelzl@40859  380  with sets_into_space have "\x. \2 (Pair x - (space M1 \ space M2 - A)) =  hoelzl@40859  381  (if x \ space M1 then \2 (space M2) - ?s A x else 0)"  hoelzl@40859  382  by (auto intro!: M2.finite_measure_compl measurable_cut_fst  hoelzl@40859  383  simp: vimage_Diff)  hoelzl@40859  384  with A \ sets ?D top show "space ?D - A \ sets ?D"  hoelzl@41023  385  by (auto intro!: Diff M1.measurable_If M1.borel_measurable_pextreal_diff)  hoelzl@40859  386  next  hoelzl@40859  387  fix F :: "nat \ ('a\'b) set" assume "disjoint_family F" "range F \ sets ?D"  hoelzl@40859  388  moreover then have "\x. \2 (\i. Pair x - F i) = (\\<^isub>\ i. ?s (F i) x)"  hoelzl@40859  389  by (intro M2.measure_countably_additive[symmetric])  hoelzl@40859  390  (auto intro!: measurable_cut_fst simp: disjoint_family_on_def)  hoelzl@40859  391  ultimately show "(\i. F i) \ sets ?D"  hoelzl@40859  392  by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf)  hoelzl@40859  393  qed  hoelzl@40859  394  have "P = ?D"  hoelzl@40859  395  proof (intro dynkin_lemma)  hoelzl@40859  396  show "Int_stable E" by (rule Int_stable_pair_algebra)  hoelzl@40859  397  from M1.sets_into_space have "\A. A \ sets M1 \ {x \ space M1. x \ A} = A"  hoelzl@40859  398  by auto  hoelzl@40859  399  then show "sets E \ sets ?D"  hoelzl@40859  400  by (auto simp: pair_algebra_def sets_sigma if_distrib  hoelzl@40859  401  intro: sigma_sets.Basic intro!: M1.measurable_If)  hoelzl@40859  402  qed auto  hoelzl@40859  403  with Q \ sets P have "Q \ sets ?D" by simp  hoelzl@40859  404  then show "?s Q \ borel_measurable M1" by simp  hoelzl@40859  405 qed  hoelzl@40859  406 hoelzl@40859  407 subsection {* Binary products of \sigma-finite measure spaces *}  hoelzl@40859  408 hoelzl@40859  409 locale pair_sigma_finite = M1: sigma_finite_measure M1 \1 + M2: sigma_finite_measure M2 \2  hoelzl@40859  410  for M1 \1 M2 \2  hoelzl@40859  411 hoelzl@40859  412 sublocale pair_sigma_finite \ pair_sigma_algebra M1 M2  hoelzl@40859  413  by default  hoelzl@40859  414 hoelzl@40859  415 lemma (in pair_sigma_finite) measure_cut_measurable_fst:  hoelzl@40859  416  assumes "Q \ sets P" shows "(\x. \2 (Pair x - Q)) \ borel_measurable M1" (is "?s Q \ _")  hoelzl@40859  417 proof -  hoelzl@40859  418  have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+  hoelzl@40859  419  have M1: "sigma_finite_measure M1 \1" by default  hoelzl@40859  420 hoelzl@40859  421  from M2.disjoint_sigma_finite guess F .. note F = this  hoelzl@40859  422  let "?C x i" = "F i \ Pair x - Q"  hoelzl@40859  423  { fix i  hoelzl@40859  424  let ?R = "M2.restricted_space (F i)"  hoelzl@40859  425  have [simp]: "space M1 \ F i \ space M1 \ space M2 = space M1 \ F i"  hoelzl@40859  426  using F M2.sets_into_space by auto  hoelzl@40859  427  have "(\x. \2 (Pair x - (space M1 \ F i \ Q))) \ borel_measurable M1"  hoelzl@40859  428  proof (intro finite_measure_cut_measurable[OF M1])  hoelzl@40859  429  show "finite_measure (M2.restricted_space (F i)) \2"  hoelzl@40859  430  using F by (intro M2.restricted_to_finite_measure) auto  hoelzl@40859  431  have "space M1 \ F i \ sets P"  hoelzl@40859  432  using M1.top F by blast  hoelzl@40859  433  from sigma_sets_Int[symmetric,  hoelzl@40859  434  OF this[unfolded pair_sigma_algebra_def sets_sigma]]  hoelzl@40859  435  show "(space M1 \ F i) \ Q \ sets (sigma (pair_algebra M1 ?R))"  hoelzl@40859  436  using Q \ sets P  hoelzl@40859  437  using pair_algebra_Int_snd[OF M1.space_closed, of "F i" M2]  hoelzl@40859  438  by (auto simp: pair_algebra_def sets_sigma)  hoelzl@40859  439  qed  hoelzl@40859  440  moreover have "\x. Pair x - (space M1 \ F i \ Q) = ?C x i"  hoelzl@40859  441  using Q \ sets P sets_into_space by (auto simp: space_pair_algebra)  hoelzl@40859  442  ultimately have "(\x. \2 (?C x i)) \ borel_measurable M1"  hoelzl@40859  443  by simp }  hoelzl@40859  444  moreover  hoelzl@40859  445  { fix x  hoelzl@40859  446  have "(\\<^isub>\i. \2 (?C x i)) = \2 (\i. ?C x i)"  hoelzl@40859  447  proof (intro M2.measure_countably_additive)  hoelzl@40859  448  show "range (?C x) \ sets M2"  hoelzl@40859  449  using F Q \ sets P by (auto intro!: M2.Int measurable_cut_fst)  hoelzl@40859  450  have "disjoint_family F" using F by auto  hoelzl@40859  451  show "disjoint_family (?C x)"  hoelzl@40859  452  by (rule disjoint_family_on_bisimulation[OF disjoint_family F]) auto  hoelzl@40859  453  qed  hoelzl@40859  454  also have "(\i. ?C x i) = Pair x - Q"  hoelzl@40859  455  using F sets_into_space Q \ sets P  hoelzl@40859  456  by (auto simp: space_pair_algebra)  hoelzl@40859  457  finally have "\2 (Pair x - Q) = (\\<^isub>\i. \2 (?C x i))"  hoelzl@40859  458  by simp }  hoelzl@40859  459  ultimately show ?thesis  hoelzl@40859  460  by (auto intro!: M1.borel_measurable_psuminf)  hoelzl@40859  461 qed  hoelzl@40859  462 hoelzl@40859  463 lemma (in pair_sigma_finite) measure_cut_measurable_snd:  hoelzl@40859  464  assumes "Q \ sets P" shows "(\y. \1 ((\x. (x, y)) - Q)) \ borel_measurable M2"  hoelzl@40859  465 proof -  hoelzl@40859  466  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@40859  467  have [simp]: "\y. (Pair y - (\(x, y). (y, x))  Q) = (\x. (x, y)) - Q"  hoelzl@40859  468  by auto  hoelzl@40859  469  note sets_pair_sigma_algebra_swap[OF assms]  hoelzl@40859  470  from Q.measure_cut_measurable_fst[OF this]  hoelzl@40859  471  show ?thesis by simp  hoelzl@40859  472 qed  hoelzl@40859  473 hoelzl@40859  474 lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable:  hoelzl@40859  475  assumes "f \ measurable P M"  hoelzl@40859  476  shows "(\(x,y). f (y, x)) \ measurable (sigma (pair_algebra M2 M1)) M"  hoelzl@40859  477 proof -  hoelzl@40859  478  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  479  have *: "(\(x,y). f (y, x)) = f \ (\(x,y). (y, x))" by (simp add: fun_eq_iff)  hoelzl@40859  480  show ?thesis  hoelzl@40859  481  using Q.pair_sigma_algebra_swap_measurable assms  hoelzl@40859  482  unfolding * by (rule measurable_comp)  hoelzl@39088  483 qed  hoelzl@39088  484 hoelzl@40859  485 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:  hoelzl@40859  486  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \ space M1) (\(x, y). (y, x)))"  hoelzl@40859  487  unfolding vimage_algebra_def  hoelzl@40859  488  apply (simp add: sets_sigma)  hoelzl@40859  489  apply (subst sigma_sets_vimage[symmetric])  hoelzl@40859  490  apply (fastsimp simp: pair_algebra_def)  hoelzl@40859  491  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)  hoelzl@40859  492 proof -  hoelzl@40859  493  have "(\X. (\(x, y). (y, x)) - X \ space M2 \ space M1)  sets E  hoelzl@40859  494  = sets (pair_algebra M2 M1)" (is "?S = _")  hoelzl@40859  495  by (rule pair_algebra_swap)  hoelzl@40859  496  then show "sigma (pair_algebra M2 M1) = \space = space M2 \ space M1,  hoelzl@40859  497  sets = sigma_sets (space M2 \ space M1) ?S\"  hoelzl@40859  498  by (simp add: pair_algebra_def sigma_def)  hoelzl@40859  499 qed  hoelzl@40859  500 hoelzl@40859  501 definition (in pair_sigma_finite)  hoelzl@40859  502  "pair_measure A = M1.positive_integral (\x.  hoelzl@40859  503  M2.positive_integral (\y. indicator A (x, y)))"  hoelzl@40859  504 hoelzl@40859  505 lemma (in pair_sigma_finite) pair_measure_alt:  hoelzl@40859  506  assumes "A \ sets P"  hoelzl@40859  507  shows "pair_measure A = M1.positive_integral (\x. \2 (Pair x - A))"  hoelzl@40859  508  unfolding pair_measure_def  hoelzl@40859  509 proof (rule M1.positive_integral_cong)  hoelzl@40859  510  fix x assume "x \ space M1"  hoelzl@41023  511  have *: "\y. indicator A (x, y) = (indicator (Pair x - A) y :: pextreal)"  hoelzl@40859  512  unfolding indicator_def by auto  hoelzl@40859  513  show "M2.positive_integral (\y. indicator A (x, y)) = \2 (Pair x - A)"  hoelzl@40859  514  unfolding *  hoelzl@40859  515  apply (subst M2.positive_integral_indicator)  hoelzl@40859  516  apply (rule measurable_cut_fst[OF assms])  hoelzl@40859  517  by simp  hoelzl@40859  518 qed  hoelzl@40859  519 hoelzl@40859  520 lemma (in pair_sigma_finite) pair_measure_times:  hoelzl@40859  521  assumes A: "A \ sets M1" and "B \ sets M2"  hoelzl@40859  522  shows "pair_measure (A \ B) = \1 A * \2 B"  hoelzl@40859  523 proof -  hoelzl@40859  524  from assms have "pair_measure (A \ B) =  hoelzl@40859  525  M1.positive_integral (\x. \2 B * indicator A x)"  hoelzl@40859  526  by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)  hoelzl@40859  527  with assms show ?thesis  hoelzl@40859  528  by (simp add: M1.positive_integral_cmult_indicator ac_simps)  hoelzl@40859  529 qed  hoelzl@40859  530 hoelzl@40859  531 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra:  hoelzl@40859  532  "\F::nat \ ('a \ 'b) set. range F \ sets E \ F \ space E \  hoelzl@40859  533  (\i. pair_measure (F i) \$$"  hoelzl@40859  534 proof -  hoelzl@40859  535  obtain F1 :: "nat \ 'a set" and F2 :: "nat \ 'b set" where  hoelzl@40859  536  F1: "range F1 \ sets M1" "F1 \ space M1" "\i. \1 (F1 i) \ \" and  hoelzl@40859  537  F2: "range F2 \ sets M2" "F2 \ space M2" "\i. \2 (F2 i) \ \"  hoelzl@40859  538  using M1.sigma_finite_up M2.sigma_finite_up by auto  hoelzl@40859  539  then have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)"  hoelzl@40859  540  unfolding isoton_def by auto  hoelzl@40859  541  let ?F = "\i. F1 i \ F2 i"  hoelzl@40859  542  show ?thesis unfolding isoton_def space_pair_algebra  hoelzl@40859  543  proof (intro exI[of _ ?F] conjI allI)  hoelzl@40859  544  show "range ?F \ sets E" using F1 F2  hoelzl@40859  545  by (fastsimp intro!: pair_algebraI)  hoelzl@40859  546  next  hoelzl@40859  547  have "space M1 \ space M2 \ (\i. ?F i)"  hoelzl@40859  548  proof (intro subsetI)  hoelzl@40859  549  fix x assume "x \ space M1 \ space M2"  hoelzl@40859  550  then obtain i j where "fst x \ F1 i" "snd x \ F2 j"  hoelzl@40859  551  by (auto simp: space)  hoelzl@40859  552  then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)"  hoelzl@40859  553  using F1 \ space M1 F2 \ space M2  hoelzl@40859  554  by (auto simp: max_def dest: isoton_mono_le)  hoelzl@40859  555  then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)"  hoelzl@40859  556  by (intro SigmaI) (auto simp add: min_max.sup_commute)  hoelzl@40859  557  then show "x \ (\i. ?F i)" by auto  hoelzl@40859  558  qed  hoelzl@40859  559  then show "(\i. ?F i) = space M1 \ space M2"  hoelzl@40859  560  using space by (auto simp: space)  hoelzl@40859  561  next  hoelzl@40859  562  fix i show "F1 i \ F2 i \ F1 (Suc i) \ F2 (Suc i)"  hoelzl@40859  563  using F1 \ space M1 F2 \ space M2 unfolding isoton_def  hoelzl@40859  564  by auto  hoelzl@40859  565  next  hoelzl@40859  566  fix i  hoelzl@40859  567  from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto  hoelzl@40859  568  with F1 F2 show "pair_measure (F1 i \ F2 i) \ \"  hoelzl@40859  569  by (simp add: pair_measure_times)  hoelzl@40859  570  qed  hoelzl@40859  571 qed  hoelzl@40859  572 hoelzl@40859  573 sublocale pair_sigma_finite \ sigma_finite_measure P pair_measure  hoelzl@40859  574 proof  hoelzl@40859  575  show "pair_measure {} = 0"  hoelzl@40859  576  unfolding pair_measure_def by auto  hoelzl@40859  577 hoelzl@40859  578  show "countably_additive P pair_measure"  hoelzl@40859  579  unfolding countably_additive_def  hoelzl@40859  580  proof (intro allI impI)  hoelzl@40859  581  fix F :: "nat \ ('a \ 'b) set"  hoelzl@40859  582  assume F: "range F \ sets P" "disjoint_family F"  hoelzl@40859  583  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  hoelzl@40859  584  moreover from F have "\i. (\x. \2 (Pair x - F i)) \ borel_measurable M1"  hoelzl@40859  585  by (intro measure_cut_measurable_fst) auto  hoelzl@40859  586  moreover have "\x. disjoint_family (\i. Pair x - F i)"  hoelzl@40859  587  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  hoelzl@40859  588  moreover have "\x. x \ space M1 \ range (\i. Pair x - F i) \ sets M2"  hoelzl@40859  589  using F by (auto intro!: measurable_cut_fst)  hoelzl@40859  590  ultimately show "(\\<^isub>\n. pair_measure (F n)) = pair_measure (\i. F i)"  hoelzl@40859  591  by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric]  hoelzl@40859  592  M2.measure_countably_additive  hoelzl@40859  593  cong: M1.positive_integral_cong)  hoelzl@40859  594  qed  hoelzl@40859  595 hoelzl@40859  596  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  hoelzl@40859  597  show "\F::nat \ ('a \ 'b) set. range F \ sets P \ (\i. F i) = space P \ (\i. pair_measure (F i) \ \)"  hoelzl@40859  598  proof (rule exI[of _ F], intro conjI)  hoelzl@40859  599  show "range F \ sets P" using F by auto  hoelzl@40859  600  show "(\i. F i) = space P"  hoelzl@40859  601  using F by (auto simp: space_pair_algebra isoton_def)  hoelzl@40859  602  show "\i. pair_measure (F i) \ \" using F by auto  hoelzl@40859  603  qed  hoelzl@40859  604 qed  hoelzl@39088  605 hoelzl@40859  606 lemma (in pair_sigma_finite) pair_measure_alt2:  hoelzl@40859  607  assumes "A \ sets P"  hoelzl@40859  608  shows "pair_measure A = M2.positive_integral (\y. \1 ((\x. (x, y)) - A))"  hoelzl@40859  609  (is "_ = ?\ A")  hoelzl@40859  610 proof -  hoelzl@40859  611  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  hoelzl@40859  612  show ?thesis  hoelzl@40859  613  proof (rule measure_unique_Int_stable[where \="?\", OF Int_stable_pair_algebra],  hoelzl@40859  614  simp_all add: pair_sigma_algebra_def[symmetric])  hoelzl@40859  615  show "range F \ sets E" "F \ space E" "\i. pair_measure (F i) \ \"  hoelzl@40859  616  using F by auto  hoelzl@40859  617  show "measure_space P pair_measure" by default  hoelzl@40859  618  next  hoelzl@40859  619  show "measure_space P ?\"  hoelzl@40859  620  proof  hoelzl@40859  621  show "?\ {} = 0" by auto  hoelzl@40859  622  show "countably_additive P ?\"  hoelzl@40859  623  unfolding countably_additive_def  hoelzl@40859  624  proof (intro allI impI)  hoelzl@40859  625  fix F :: "nat \ ('a \ 'b) set"  hoelzl@40859  626  assume F: "range F \ sets P" "disjoint_family F"  hoelzl@40859  627  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  hoelzl@40859  628  moreover from F have "\i. (\y. \1 ((\x. (x, y)) - F i)) \ borel_measurable M2"  hoelzl@40859  629  by (intro measure_cut_measurable_snd) auto  hoelzl@40859  630  moreover have "\y. disjoint_family (\i. (\x. (x, y)) - F i)"  hoelzl@40859  631  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  hoelzl@40859  632  moreover have "\y. y \ space M2 \ range (\i. (\x. (x, y)) - F i) \ sets M1"  hoelzl@40859  633  using F by (auto intro!: measurable_cut_snd)  hoelzl@40859  634  ultimately show "(\\<^isub>\n. ?\ (F n)) = ?\ (\i. F i)"  hoelzl@40859  635  by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]  hoelzl@40859  636  M1.measure_countably_additive  hoelzl@40859  637  cong: M2.positive_integral_cong)  hoelzl@40859  638  qed  hoelzl@40859  639  qed  hoelzl@40859  640  next  hoelzl@40859  641  fix X assume "X \ sets E"  hoelzl@40859  642  then obtain A B where X: "X = A \ B" and AB: "A \ sets M1" "B \ sets M2"  hoelzl@40859  643  unfolding pair_algebra_def by auto  hoelzl@40859  644  show "pair_measure X = ?\ X"  hoelzl@40859  645  proof -  hoelzl@40859  646  from AB have "?\ (A \ B) =  hoelzl@40859  647  M2.positive_integral (\y. \1 A * indicator B y)"  hoelzl@40859  648  by (auto intro!: M2.positive_integral_cong)  hoelzl@40859  649  with AB show ?thesis  hoelzl@40859  650  unfolding pair_measure_times[OF AB] X  hoelzl@40859  651  by (simp add: M2.positive_integral_cmult_indicator ac_simps)  hoelzl@40859  652  qed  hoelzl@40859  653  qed fact  hoelzl@40859  654 qed  hoelzl@40859  655 hoelzl@40859  656 section "Fubinis theorem"  hoelzl@40859  657 hoelzl@40859  658 lemma (in pair_sigma_finite) simple_function_cut:  hoelzl@40859  659  assumes f: "simple_function f"  hoelzl@40859  660  shows "(\x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  661  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  hoelzl@40859  662  = positive_integral f"  hoelzl@40859  663 proof -  hoelzl@40859  664  have f_borel: "f \ borel_measurable P"  hoelzl@40859  665  using f by (rule borel_measurable_simple_function)  hoelzl@40859  666  let "?F z" = "f - {z} \ space P"  hoelzl@40859  667  let "?F' x z" = "Pair x - ?F z"  hoelzl@40859  668  { fix x assume "x \ space M1"  hoelzl@40859  669  have [simp]: "\z y. indicator (?F z) (x, y) = indicator (?F' x z) y"  hoelzl@40859  670  by (auto simp: indicator_def)  hoelzl@40859  671  have "\y. y \ space M2 \ (x, y) \ space P" using x \ space M1  hoelzl@40859  672  by (simp add: space_pair_algebra)  hoelzl@40859  673  moreover have "\x z. ?F' x z \ sets M2" using f_borel  hoelzl@40859  674  by (intro borel_measurable_vimage measurable_cut_fst)  hoelzl@40859  675  ultimately have "M2.simple_function (\ y. f (x, y))"  hoelzl@40859  676  apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])  hoelzl@40859  677  apply (rule simple_function_indicator_representation[OF f])  hoelzl@40859  678  using x \ space M1 by (auto simp del: space_sigma) }  hoelzl@40859  679  note M2_sf = this  hoelzl@40859  680  { fix x assume x: "x \ space M1"  hoelzl@40859  681  then have "M2.positive_integral (\ y. f (x, y)) =  hoelzl@40859  682  (\z\f  space P. z * \2 (?F' x z))"  hoelzl@40859  683  unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]]  hoelzl@40859  684  unfolding M2.simple_integral_def  hoelzl@40859  685  proof (safe intro!: setsum_mono_zero_cong_left)  hoelzl@40859  686  from f show "finite (f  space P)" by (rule simple_functionD)  hoelzl@40859  687  next  hoelzl@40859  688  fix y assume "y \ space M2" then show "f (x, y) \ f  space P"  hoelzl@40859  689  using x \ space M1 by (auto simp: space_pair_algebra)  hoelzl@40859  690  next  hoelzl@40859  691  fix x' y assume "(x', y) \ space P"  hoelzl@40859  692  "f (x', y) \ (\y. f (x, y))  space M2"  hoelzl@40859  693  then have *: "?F' x (f (x', y)) = {}"  hoelzl@40859  694  by (force simp: space_pair_algebra)  hoelzl@40859  695  show "f (x', y) * \2 (?F' x (f (x', y))) = 0"  hoelzl@40859  696  unfolding * by simp  hoelzl@40859  697  qed (simp add: vimage_compose[symmetric] comp_def  hoelzl@40859  698  space_pair_algebra) }  hoelzl@40859  699  note eq = this  hoelzl@40859  700  moreover have "\z. ?F z \ sets P"  hoelzl@40859  701  by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)  hoelzl@40859  702  moreover then have "\z. (\x. \2 (?F' x z)) \ borel_measurable M1"  hoelzl@40859  703  by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)  hoelzl@40859  704  ultimately  hoelzl@40859  705  show "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  706  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  hoelzl@40859  707  = positive_integral f"  hoelzl@40859  708  by (auto simp del: vimage_Int cong: measurable_cong  hoelzl@41023  709  intro!: M1.borel_measurable_pextreal_setsum  hoelzl@40859  710  simp add: M1.positive_integral_setsum simple_integral_def  hoelzl@40859  711  M1.positive_integral_cmult  hoelzl@40859  712  M1.positive_integral_cong[OF eq]  hoelzl@40859  713  positive_integral_eq_simple_integral[OF f]  hoelzl@40859  714  pair_measure_alt[symmetric])  hoelzl@40859  715 qed  hoelzl@40859  716 hoelzl@40859  717 lemma (in pair_sigma_finite) positive_integral_fst_measurable:  hoelzl@40859  718  assumes f: "f \ borel_measurable P"  hoelzl@40859  719  shows "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  720  (is "?C f \ borel_measurable M1")  hoelzl@40859  721  and "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  hoelzl@40859  722  positive_integral f"  hoelzl@40859  723 proof -  hoelzl@40859  724  from borel_measurable_implies_simple_function_sequence[OF f]  hoelzl@40859  725  obtain F where F: "\i. simple_function (F i)" "F \ f" by auto  hoelzl@40859  726  then have F_borel: "\i. F i \ borel_measurable P"  hoelzl@40859  727  and F_mono: "\i x. F i x \ F (Suc i) x"  hoelzl@40859  728  and F_SUPR: "\x. (SUP i. F i x) = f x"  hoelzl@40859  729  unfolding isoton_def le_fun_def SUPR_fun_expand  hoelzl@40859  730  by (auto intro: borel_measurable_simple_function)  hoelzl@40859  731  note sf = simple_function_cut[OF F(1)]  hoelzl@40859  732  then have "(SUP i. ?C (F i)) \ borel_measurable M1"  hoelzl@40859  733  using F(1) by (auto intro!: M1.borel_measurable_SUP)  hoelzl@40859  734  moreover  hoelzl@40859  735  { fix x assume "x \ space M1"  hoelzl@40859  736  have isotone: "(\ i y. F i (x, y)) \ (\y. f (x, y))"  hoelzl@40859  737  using F \ f unfolding isoton_fun_expand  hoelzl@40859  738  by (auto simp: isoton_def)  hoelzl@40859  739  note measurable_pair_image_snd[OF F_borelx \ space M1]  hoelzl@40859  740  from M2.positive_integral_isoton[OF isotone this]  hoelzl@40859  741  have "(SUP i. ?C (F i) x) = ?C f x"  hoelzl@40859  742  by (simp add: isoton_def) }  hoelzl@40859  743  note SUPR_C = this  hoelzl@40859  744  ultimately show "?C f \ borel_measurable M1"  hoelzl@40859  745  unfolding SUPR_fun_expand by (simp cong: measurable_cong)  hoelzl@40859  746  have "positive_integral (\x. SUP i. F i x) = (SUP i. positive_integral (F i))"  hoelzl@40859  747  using F_borel F_mono  hoelzl@40859  748  by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])  hoelzl@40859  749  also have "(SUP i. positive_integral (F i)) =  hoelzl@40859  750  (SUP i. M1.positive_integral (\x. M2.positive_integral (\y. F i (x, y))))"  hoelzl@40859  751  unfolding sf(2) by simp  hoelzl@40859  752  also have "\ = M1.positive_integral (\x. SUP i. M2.positive_integral (\y. F i (x, y)))"  hoelzl@40859  753  by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)]  hoelzl@40859  754  M2.positive_integral_mono F_mono)  hoelzl@40859  755  also have "\ = M1.positive_integral (\x. M2.positive_integral (\y. SUP i. F i (x, y)))"  hoelzl@40859  756  using F_borel F_mono  hoelzl@40859  757  by (auto intro!: M2.positive_integral_monotone_convergence_SUP  hoelzl@40859  758  M1.positive_integral_cong measurable_pair_image_snd)  hoelzl@40859  759  finally show "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  hoelzl@40859  760  positive_integral f"  hoelzl@40859  761  unfolding F_SUPR by simp  hoelzl@40859  762 qed  hoelzl@40859  763 hoelzl@40859  764 lemma (in pair_sigma_finite) positive_integral_snd_measurable:  hoelzl@40859  765  assumes f: "f \ borel_measurable P"  hoelzl@40859  766  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  767  positive_integral f"  hoelzl@40859  768 proof -  hoelzl@40859  769  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@40859  770  have s: "\x y. (case (x, y) of (x, y) \ f (y, x)) = f (y, x)" by simp  hoelzl@40859  771  have t: "(\x. f (case x of (x, y) \ (y, x))) = ($$x, y). f (y, x))" by (auto simp: fun_eq_iff)  hoelzl@40859  772  have bij: "bij_betw (\(x, y). (y, x)) (space M2 \ space M1) (space P)"  hoelzl@40859  773  by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)  hoelzl@40859  774  note pair_sigma_algebra_measurable[OF f]  hoelzl@40859  775  from Q.positive_integral_fst_measurable[OF this]  hoelzl@40859  776  have "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  777  Q.positive_integral (\(x, y). f (y, x))"  hoelzl@40859  778  by simp  hoelzl@40859  779  also have "\ = positive_integral f"  hoelzl@40859  780  unfolding positive_integral_vimage[OF bij, of f] t  hoelzl@40859  781  unfolding pair_sigma_algebra_swap[symmetric]  hoelzl@40859  782  proof (rule Q.positive_integral_cong_measure[symmetric])  hoelzl@40859  783  fix A assume "A \ sets Q.P"  hoelzl@40859  784  from this Q.sets_pair_sigma_algebra_swap[OF this]  hoelzl@40859  785  show "pair_measure ((\(x, y). (y, x))  A) = Q.pair_measure A"  hoelzl@40859  786  by (auto intro!: M1.positive_integral_cong arg_cong[where f=\2]  hoelzl@40859  787  simp: pair_measure_alt Q.pair_measure_alt2)  hoelzl@40859  788  qed  hoelzl@40859  789  finally show ?thesis .  hoelzl@40859  790 qed  hoelzl@40859  791 hoelzl@40859  792 lemma (in pair_sigma_finite) Fubini:  hoelzl@40859  793  assumes f: "f \ borel_measurable P"  hoelzl@40859  794  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  795  M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))"  hoelzl@40859  796  unfolding positive_integral_snd_measurable[OF assms]  hoelzl@40859  797  unfolding positive_integral_fst_measurable[OF assms] ..  hoelzl@40859  798 hoelzl@40859  799 lemma (in pair_sigma_finite) AE_pair:  hoelzl@40859  800  assumes "almost_everywhere (\x. Q x)"  hoelzl@40859  801  shows "M1.almost_everywhere (\x. M2.almost_everywhere (\y. Q (x, y)))"  hoelzl@40859  802 proof -  hoelzl@40859  803  obtain N where N: "N \ sets P" "pair_measure N = 0" "{x\space P. \ Q x} \ N"  hoelzl@40859  804  using assms unfolding almost_everywhere_def by auto  hoelzl@40859  805  show ?thesis  hoelzl@40859  806  proof (rule M1.AE_I)  hoelzl@40859  807  from N measure_cut_measurable_fst[OF N \ sets P]  hoelzl@40859  808  show "\1 {x\space M1. \2 (Pair x - N) \ 0} = 0"  hoelzl@40859  809  by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def)  hoelzl@40859  810  show "{x \ space M1. \2 (Pair x - N) \ 0} \ sets M1"  hoelzl@41023  811  by (intro M1.borel_measurable_pextreal_neq_const measure_cut_measurable_fst N)  hoelzl@40859  812  { fix x assume "x \ space M1" "\2 (Pair x - N) = 0"  hoelzl@40859  813  have "M2.almost_everywhere (\y. Q (x, y))"  hoelzl@40859  814  proof (rule M2.AE_I)  hoelzl@40859  815  show "\2 (Pair x - N) = 0" by fact  hoelzl@40859  816  show "Pair x - N \ sets M2" by (intro measurable_cut_fst N)  hoelzl@40859  817  show "{y \ space M2. \ Q (x, y)} \ Pair x - N"  hoelzl@40859  818  using N x \ space M1 unfolding space_sigma space_pair_algebra by auto  hoelzl@40859  819  qed }  hoelzl@40859  820  then show "{x \ space M1. \ M2.almost_everywhere (\y. Q (x, y))} \ {x \ space M1. \2 (Pair x - N) \ 0}"  hoelzl@40859  821  by auto  hoelzl@39088  822  qed  hoelzl@39088  823 qed  hoelzl@35833  824 hoelzl@41026  825 lemma (in pair_sigma_finite) positive_integral_product_swap:  hoelzl@41026  826  "measure_space.positive_integral  hoelzl@41026  827  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) f =  hoelzl@41026  828  positive_integral (\(x,y). f (y,x))"  hoelzl@41026  829 proof -  hoelzl@41026  830  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41026  831  have t: "(\y. case case y of (y, x) \ (x, y) of (x, y) \ f (y, x)) = f"  hoelzl@41026  832  by (auto simp: fun_eq_iff)  hoelzl@41026  833  have bij: "bij_betw (\(x, y). (y, x)) (space M2 \ space M1) (space P)"  hoelzl@41026  834  by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)  hoelzl@41026  835  show ?thesis  hoelzl@41026  836  unfolding positive_integral_vimage[OF bij, of "\(y,x). f (x,y)"]  hoelzl@41026  837  unfolding pair_sigma_algebra_swap[symmetric] t  hoelzl@41026  838  proof (rule Q.positive_integral_cong_measure[symmetric])  hoelzl@41026  839  fix A assume "A \ sets Q.P"  hoelzl@41026  840  from this Q.sets_pair_sigma_algebra_swap[OF this]  hoelzl@41026  841  show "pair_measure ((\(x, y). (y, x))  A) = Q.pair_measure A"  hoelzl@41026  842  by (auto intro!: M1.positive_integral_cong arg_cong[where f=\2]  hoelzl@41026  843  simp: pair_measure_alt Q.pair_measure_alt2)  hoelzl@41026  844  qed  hoelzl@41026  845 qed  hoelzl@41026  846 hoelzl@41026  847 lemma (in pair_sigma_algebra) measurable_product_swap:  hoelzl@41026  848  "f \ measurable (sigma (pair_algebra M2 M1)) M \ (\(x,y). f (y,x)) \ measurable P M"  hoelzl@41026  849 proof -  hoelzl@41026  850  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@41026  851  show ?thesis  hoelzl@41026  852  using pair_sigma_algebra_measurable[of "\(x,y). f (y, x)"]  hoelzl@41026  853  by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI)  hoelzl@41026  854 qed  hoelzl@41026  855 hoelzl@41026  856 lemma (in pair_sigma_finite) integrable_product_swap:  hoelzl@41026  857  "measure_space.integrable  hoelzl@41026  858  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) f \  hoelzl@41026  859  integrable (\(x,y). f (y,x))"  hoelzl@41026  860 proof -  hoelzl@41026  861  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41026  862  show ?thesis  hoelzl@41026  863  unfolding Q.integrable_def integrable_def  hoelzl@41026  864  unfolding positive_integral_product_swap  hoelzl@41026  865  unfolding measurable_product_swap  hoelzl@41026  866  by (simp add: case_prod_distrib)  hoelzl@41026  867 qed  hoelzl@41026  868 hoelzl@41026  869 lemma (in pair_sigma_finite) integral_product_swap:  hoelzl@41026  870  "measure_space.integral  hoelzl@41026  871  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) f =  hoelzl@41026  872  integral (\(x,y). f (y,x))"  hoelzl@41026  873 proof -  hoelzl@41026  874  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41026  875  show ?thesis  hoelzl@41026  876  unfolding integral_def Q.integral_def positive_integral_product_swap  hoelzl@41026  877  by (simp add: case_prod_distrib)  hoelzl@41026  878 qed  hoelzl@41026  879 hoelzl@41026  880 lemma (in pair_sigma_finite) integrable_fst_measurable:  hoelzl@41026  881  assumes f: "integrable f"  hoelzl@41026  882  shows "M1.almost_everywhere (\x. M2.integrable (\ y. f (x, y)))" (is "?AE")  hoelzl@41026  883  and "M1.integral (\ x. M2.integral (\ y. f (x, y))) = integral f" (is "?INT")  hoelzl@41026  884 proof -  hoelzl@41026  885  let "?pf x" = "Real (f x)" and "?nf x" = "Real (- f x)"  hoelzl@41026  886  have  hoelzl@41026  887  borel: "?nf \ borel_measurable P""?pf \ borel_measurable P" and  hoelzl@41026  888  int: "positive_integral ?nf \ \" "positive_integral ?pf \ \"  hoelzl@41026  889  using assms by auto  hoelzl@41026  890  have "M1.positive_integral (\x. M2.positive_integral (\y. Real (f (x, y)))) \ \"  hoelzl@41026  891  "M1.positive_integral (\x. M2.positive_integral (\y. Real (- f (x, y)))) \ \"  hoelzl@41026  892  using borel[THEN positive_integral_fst_measurable(1)] int  hoelzl@41026  893  unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all  hoelzl@41026  894  with borel[THEN positive_integral_fst_measurable(1)]  hoelzl@41026  895  have AE: "M1.almost_everywhere (\x. M2.positive_integral (\y. Real (f (x, y))) \$$"  hoelzl@41026  896  "M1.almost_everywhere (\x. M2.positive_integral (\y. Real (- f (x, y))) \ \)"  hoelzl@41026  897  by (auto intro!: M1.positive_integral_omega_AE)  hoelzl@41026  898  then show ?AE  hoelzl@41026  899  apply (rule M1.AE_mp[OF _ M1.AE_mp])  hoelzl@41026  900  apply (rule M1.AE_cong)  hoelzl@41026  901  using assms unfolding M2.integrable_def  hoelzl@41026  902  by (auto intro!: measurable_pair_image_snd)  hoelzl@41026  903  have "M1.integrable  hoelzl@41026  904  (\x. real (M2.positive_integral (\xa. Real (f (x, xa)))))" (is "M1.integrable ?f")  hoelzl@41026  905  proof (unfold M1.integrable_def, intro conjI)  hoelzl@41026  906  show "?f \ borel_measurable M1"  hoelzl@41026  907  using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)  hoelzl@41026  908  have "M1.positive_integral (\x. Real (?f x)) =  hoelzl@41026  909  M1.positive_integral (\x. M2.positive_integral (\xa. Real (f (x, xa))))"  hoelzl@41026  910  apply (rule M1.positive_integral_cong_AE)  hoelzl@41026  911  apply (rule M1.AE_mp[OF AE(1)])  hoelzl@41026  912  apply (rule M1.AE_cong)  hoelzl@41026  913  by (auto simp: Real_real)  hoelzl@41026  914  then show "M1.positive_integral (\x. Real (?f x)) \ \"  hoelzl@41026  915  using positive_integral_fst_measurable[OF borel(2)] int by simp  hoelzl@41026  916  have "M1.positive_integral (\x. Real (- ?f x)) = M1.positive_integral (\x. 0)"  hoelzl@41026  917  by (intro M1.positive_integral_cong) simp  hoelzl@41026  918  then show "M1.positive_integral (\x. Real (- ?f x)) \ \" by simp  hoelzl@41026  919  qed  hoelzl@41026  920  moreover have "M1.integrable  hoelzl@41026  921  (\x. real (M2.positive_integral (\xa. Real (- f (x, xa)))))" (is "M1.integrable ?f")  hoelzl@41026  922  proof (unfold M1.integrable_def, intro conjI)  hoelzl@41026  923  show "?f \ borel_measurable M1"  hoelzl@41026  924  using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)  hoelzl@41026  925  have "M1.positive_integral (\x. Real (?f x)) =  hoelzl@41026  926  M1.positive_integral (\x. M2.positive_integral (\xa. Real (- f (x, xa))))"  hoelzl@41026  927  apply (rule M1.positive_integral_cong_AE)  hoelzl@41026  928  apply (rule M1.AE_mp[OF AE(2)])  hoelzl@41026  929  apply (rule M1.AE_cong)  hoelzl@41026  930  by (auto simp: Real_real)  hoelzl@41026  931  then show "M1.positive_integral (\x. Real (?f x)) \ \"  hoelzl@41026  932  using positive_integral_fst_measurable[OF borel(1)] int by simp  hoelzl@41026  933  have "M1.positive_integral (\x. Real (- ?f x)) = M1.positive_integral (\x. 0)"  hoelzl@41026  934  by (intro M1.positive_integral_cong) simp  hoelzl@41026  935  then show "M1.positive_integral (\x. Real (- ?f x)) \ \" by simp  hoelzl@41026  936  qed  hoelzl@41026  937  ultimately show ?INT  hoelzl@41026  938  unfolding M2.integral_def integral_def  hoelzl@41026  939  borel[THEN positive_integral_fst_measurable(2), symmetric]  hoelzl@41026  940  by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])  hoelzl@41026  941 qed  hoelzl@41026  942 hoelzl@41026  943 lemma (in pair_sigma_finite) integrable_snd_measurable:  hoelzl@41026  944  assumes f: "integrable f"  hoelzl@41026  945  shows "M2.almost_everywhere (\y. M1.integrable (\x. f (x, y)))" (is "?AE")  hoelzl@41026  946  and "M2.integral (\y. M1.integral (\x. f (x, y))) = integral f" (is "?INT")  hoelzl@41026  947 proof -  hoelzl@41026  948  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41026  949  have Q_int: "Q.integrable (\(x, y). f (y, x))"  hoelzl@41026  950  using f unfolding integrable_product_swap by simp  hoelzl@41026  951  show ?INT  hoelzl@41026  952  using Q.integrable_fst_measurable(2)[OF Q_int]  hoelzl@41026  953  unfolding integral_product_swap by simp  hoelzl@41026  954  show ?AE  hoelzl@41026  955  using Q.integrable_fst_measurable(1)[OF Q_int]  hoelzl@41026  956  by simp  hoelzl@41026  957 qed  hoelzl@41026  958 hoelzl@41026  959 lemma (in pair_sigma_finite) Fubini_integral:  hoelzl@41026  960  assumes f: "integrable f"  hoelzl@41026  961  shows "M2.integral (\y. M1.integral (\x. f (x, y))) =  hoelzl@41026  962  M1.integral (\x. M2.integral (\y. f (x, y)))"  hoelzl@41026  963  unfolding integrable_snd_measurable[OF assms]  hoelzl@41026  964  unfolding integrable_fst_measurable[OF assms] ..  hoelzl@41026  965 hoelzl@40859  966 section "Finite product spaces"  hoelzl@40859  967 hoelzl@40859  968 section "Products"  hoelzl@40859  969 hoelzl@40859  970 locale product_sigma_algebra =  hoelzl@40859  971  fixes M :: "'i \ 'a algebra"  hoelzl@40859  972  assumes sigma_algebras: "\i. sigma_algebra (M i)"  hoelzl@40859  973 hoelzl@40859  974 locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \ 'a algebra" +  hoelzl@40859  975  fixes I :: "'i set"  hoelzl@40859  976  assumes finite_index: "finite I"  hoelzl@40859  977 hoelzl@40859  978 syntax  hoelzl@40859  979  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)  hoelzl@40859  980 hoelzl@40859  981 syntax (xsymbols)  hoelzl@40859  982  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@40859  983 hoelzl@40859  984 syntax (HTML output)  hoelzl@40859  985  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@40859  986 hoelzl@40859  987 translations  hoelzl@40859  988  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"  hoelzl@40859  989 hoelzl@35833  990 definition  hoelzl@40859  991  "product_algebra M I = \ space = (\\<^isub>E i\I. space (M i)), sets = Pi\<^isub>E I  (\ i \ I. sets (M i)) \"  hoelzl@40859  992 hoelzl@40859  993 abbreviation (in finite_product_sigma_algebra) "G \ product_algebra M I"  hoelzl@40859  994 abbreviation (in finite_product_sigma_algebra) "P \ sigma G"  hoelzl@40859  995 hoelzl@40859  996 sublocale product_sigma_algebra \ M: sigma_algebra "M i" for i by (rule sigma_algebras)  hoelzl@40859  997 hoelzl@40859  998 lemma (in finite_product_sigma_algebra) product_algebra_into_space:  hoelzl@40859  999  "sets G \ Pow (space G)"  hoelzl@40859  1000  using M.sets_into_space unfolding product_algebra_def  hoelzl@40859  1001  by auto blast  hoelzl@40859  1002 hoelzl@40859  1003 sublocale finite_product_sigma_algebra \ sigma_algebra P  hoelzl@40859  1004  using product_algebra_into_space by (rule sigma_algebra_sigma)  hoelzl@40859  1005 hoelzl@40859  1006 lemma space_product_algebra[simp]:  hoelzl@40859  1007  "space (product_algebra M I) = Pi\<^isub>E I (\i. space (M i))"  hoelzl@40859  1008  unfolding product_algebra_def by simp  hoelzl@40859  1009 hoelzl@40859  1010 lemma (in finite_product_sigma_algebra) P_empty:  hoelzl@40859  1011  "I = {} \ P = \ space = {\k. undefined}, sets = { {}, {\k. undefined} }\"  hoelzl@40872  1012  unfolding product_algebra_def by (simp add: sigma_def image_constant)  hoelzl@40859  1013 hoelzl@40859  1014 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:  hoelzl@40859  1015  "\ \i. i \ I \ A i \ sets (M i) \ \ Pi\<^isub>E I A \ sets P"  hoelzl@40859  1016  by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)  hoelzl@40859  1017 hoelzl@40859  1018 lemma bij_betw_prod_fold:  hoelzl@40859  1019  assumes "i \ I"  hoelzl@40859  1020  shows "bij_betw (\x. (x(i:=undefined), x i)) (\\<^isub>E j\insert i I. space (M j)) ((\\<^isub>E j\I. space (M j)) \ space (M i))"  hoelzl@40859  1021  (is "bij_betw ?f ?P ?F")  hoelzl@40859  1022  using i \ I  hoelzl@40859  1023 proof (unfold bij_betw_def, intro conjI set_eqI iffI)  hoelzl@40859  1024  show "inj_on ?f ?P"  hoelzl@40859  1025  proof (safe intro!: inj_onI ext)  hoelzl@40859  1026  fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"  hoelzl@40859  1027  then show "a x = b x"  hoelzl@40859  1028  by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)  hoelzl@40859  1029  qed  hoelzl@40859  1030 next  hoelzl@40859  1031  fix X assume *: "X \ ?F" show "X \ ?f  ?P"  hoelzl@40859  1032  proof (cases X)  hoelzl@40859  1033  case (Pair a b) with * i \ I show ?thesis  hoelzl@40859  1034  by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)  hoelzl@40859  1035  qed  hoelzl@40859  1036 qed auto  hoelzl@40859  1037 hoelzl@41026  1038 lemma borel_measurable_product_component:  hoelzl@41026  1039  assumes "i \ I"  hoelzl@41026  1040  shows "(\x. x i) \ borel_measurable (sigma (product_algebra (\x. borel) I))"  hoelzl@41026  1041 proof -  hoelzl@41026  1042  have *: "\A. (\x. x i) - A \ extensional I = (\\<^isub>E j\I. if j = i then A else UNIV)"  hoelzl@41026  1043  using i \ I by (auto elim!: PiE)  hoelzl@41026  1044  show ?thesis  hoelzl@41026  1045  by (auto simp: * measurable_def product_algebra_def)  hoelzl@41026  1046 qed  hoelzl@41026  1047 hoelzl@40859  1048 section "Generating set generates also product algebra"  hoelzl@40859  1049 hoelzl@40859  1050 lemma pair_sigma_algebra_sigma:  hoelzl@40859  1051  assumes 1: "S1 \ (space E1)" "range S1 \ sets E1" and E1: "sets E1 \ Pow (space E1)"  hoelzl@40859  1052  assumes 2: "S2 \ (space E2)" "range S2 \ sets E2" and E2: "sets E2 \ Pow (space E2)"  hoelzl@40859  1053  shows "sigma (pair_algebra (sigma E1) (sigma E2)) = sigma (pair_algebra E1 E2)"  hoelzl@40859  1054  (is "?S = ?E")  hoelzl@40859  1055 proof -  hoelzl@40859  1056  interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)  hoelzl@40859  1057  interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)  hoelzl@40859  1058  have P: "sets (pair_algebra E1 E2) \ Pow (space E1 \ space E2)"  hoelzl@40859  1059  using E1 E2 by (auto simp add: pair_algebra_def)  hoelzl@40859  1060  interpret E: sigma_algebra ?E unfolding pair_algebra_def  hoelzl@40859  1061  using E1 E2 by (intro sigma_algebra_sigma) auto  hoelzl@40859  1062  { fix A assume "A \ sets E1"  hoelzl@40859  1063  then have "fst - A \ space ?E = A \ (\i. S2 i)"  hoelzl@40859  1064  using E1 2 unfolding isoton_def pair_algebra_def by auto  hoelzl@40859  1065  also have "\ = (\i. A \ S2 i)" by auto  hoelzl@40859  1066  also have "\ \ sets ?E" unfolding pair_algebra_def sets_sigma  hoelzl@40859  1067  using 2 A \ sets E1  hoelzl@40859  1068  by (intro sigma_sets.Union)  hoelzl@40859  1069  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@40859  1070  finally have "fst - A \ space ?E \ sets ?E" . }  hoelzl@40859  1071  moreover  hoelzl@40859  1072  { fix B assume "B \ sets E2"  hoelzl@40859  1073  then have "snd - B \ space ?E = (\i. S1 i) \ B"  hoelzl@40859  1074  using E2 1 unfolding isoton_def pair_algebra_def by auto  hoelzl@40859  1075  also have "\ = (\i. S1 i \ B)" by auto  hoelzl@40859  1076  also have "\ \ sets ?E"  hoelzl@40859  1077  using 1 B \ sets E2 unfolding pair_algebra_def sets_sigma  hoelzl@40859  1078  by (intro sigma_sets.Union)  hoelzl@40859  1079  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@40859  1080  finally have "snd - B \ space ?E \ sets ?E" . }  hoelzl@40859  1081  ultimately have proj:  hoelzl@40859  1082  "fst \ measurable ?E (sigma E1) \ snd \ measurable ?E (sigma E2)"  hoelzl@40859  1083  using E1 E2 by (subst (1 2) E.measurable_iff_sigma)  hoelzl@40859  1084  (auto simp: pair_algebra_def sets_sigma)  hoelzl@40859  1085  { fix A B assume A: "A \ sets (sigma E1)" and B: "B \ sets (sigma E2)"  hoelzl@40859  1086  with proj have "fst - A \ space ?E \ sets ?E" "snd - B \ space ?E \ sets ?E"  hoelzl@40859  1087  unfolding measurable_def by simp_all  hoelzl@40859  1088  moreover have "A \ B = (fst - A \ space ?E) \ (snd - B \ space ?E)"  hoelzl@40859  1089  using A B M1.sets_into_space M2.sets_into_space  hoelzl@40859  1090  by (auto simp: pair_algebra_def)  hoelzl@40859  1091  ultimately have "A \ B \ sets ?E" by auto }