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