src/HOL/Probability/Product_Measure.thy
 author hoelzl Mon Jan 24 22:29:50 2011 +0100 (2011-01-24) changeset 41661 baf1964bc468 parent 41659 a5d1b2df5e97 child 41689 3e39b0e730d6 permissions -rw-r--r--
use pre-image measure, instead of image
 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 definition (in pair_sigma_finite)  hoelzl@40859  527  "pair_measure A = M1.positive_integral (\x.  hoelzl@40859  528  M2.positive_integral (\y. indicator A (x, y)))"  hoelzl@40859  529 hoelzl@40859  530 lemma (in pair_sigma_finite) pair_measure_alt:  hoelzl@40859  531  assumes "A \ sets P"  hoelzl@40859  532  shows "pair_measure A = M1.positive_integral (\x. \2 (Pair x - A))"  hoelzl@40859  533  unfolding pair_measure_def  hoelzl@40859  534 proof (rule M1.positive_integral_cong)  hoelzl@40859  535  fix x assume "x \ space M1"  hoelzl@41023  536  have *: "\y. indicator A (x, y) = (indicator (Pair x - A) y :: pextreal)"  hoelzl@40859  537  unfolding indicator_def by auto  hoelzl@40859  538  show "M2.positive_integral (\y. indicator A (x, y)) = \2 (Pair x - A)"  hoelzl@40859  539  unfolding *  hoelzl@40859  540  apply (subst M2.positive_integral_indicator)  hoelzl@40859  541  apply (rule measurable_cut_fst[OF assms])  hoelzl@40859  542  by simp  hoelzl@40859  543 qed  hoelzl@40859  544 hoelzl@40859  545 lemma (in pair_sigma_finite) pair_measure_times:  hoelzl@40859  546  assumes A: "A \ sets M1" and "B \ sets M2"  hoelzl@40859  547  shows "pair_measure (A \ B) = \1 A * \2 B"  hoelzl@40859  548 proof -  hoelzl@40859  549  from assms have "pair_measure (A \ B) =  hoelzl@40859  550  M1.positive_integral (\x. \2 B * indicator A x)"  hoelzl@40859  551  by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)  hoelzl@40859  552  with assms show ?thesis  hoelzl@40859  553  by (simp add: M1.positive_integral_cmult_indicator ac_simps)  hoelzl@40859  554 qed  hoelzl@40859  555 hoelzl@40859  556 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra:  hoelzl@40859  557  "\F::nat \ ('a \ 'b) set. range F \ sets E \ F \ space E \  hoelzl@40859  558  (\i. pair_measure (F i) \$$"  hoelzl@40859  559 proof -  hoelzl@40859  560  obtain F1 :: "nat \ 'a set" and F2 :: "nat \ 'b set" where  hoelzl@40859  561  F1: "range F1 \ sets M1" "F1 \ space M1" "\i. \1 (F1 i) \ \" and  hoelzl@40859  562  F2: "range F2 \ sets M2" "F2 \ space M2" "\i. \2 (F2 i) \ \"  hoelzl@40859  563  using M1.sigma_finite_up M2.sigma_finite_up by auto  hoelzl@40859  564  then have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)"  hoelzl@40859  565  unfolding isoton_def by auto  hoelzl@40859  566  let ?F = "\i. F1 i \ F2 i"  hoelzl@40859  567  show ?thesis unfolding isoton_def space_pair_algebra  hoelzl@40859  568  proof (intro exI[of _ ?F] conjI allI)  hoelzl@40859  569  show "range ?F \ sets E" using F1 F2  hoelzl@40859  570  by (fastsimp intro!: pair_algebraI)  hoelzl@40859  571  next  hoelzl@40859  572  have "space M1 \ space M2 \ (\i. ?F i)"  hoelzl@40859  573  proof (intro subsetI)  hoelzl@40859  574  fix x assume "x \ space M1 \ space M2"  hoelzl@40859  575  then obtain i j where "fst x \ F1 i" "snd x \ F2 j"  hoelzl@40859  576  by (auto simp: space)  hoelzl@40859  577  then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)"  hoelzl@40859  578  using F1 \ space M1 F2 \ space M2  hoelzl@40859  579  by (auto simp: max_def dest: isoton_mono_le)  hoelzl@40859  580  then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)"  hoelzl@40859  581  by (intro SigmaI) (auto simp add: min_max.sup_commute)  hoelzl@40859  582  then show "x \ (\i. ?F i)" by auto  hoelzl@40859  583  qed  hoelzl@40859  584  then show "(\i. ?F i) = space M1 \ space M2"  hoelzl@40859  585  using space by (auto simp: space)  hoelzl@40859  586  next  hoelzl@40859  587  fix i show "F1 i \ F2 i \ F1 (Suc i) \ F2 (Suc i)"  hoelzl@40859  588  using F1 \ space M1 F2 \ space M2 unfolding isoton_def  hoelzl@40859  589  by auto  hoelzl@40859  590  next  hoelzl@40859  591  fix i  hoelzl@40859  592  from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto  hoelzl@40859  593  with F1 F2 show "pair_measure (F1 i \ F2 i) \ \"  hoelzl@40859  594  by (simp add: pair_measure_times)  hoelzl@40859  595  qed  hoelzl@40859  596 qed  hoelzl@40859  597 hoelzl@40859  598 sublocale pair_sigma_finite \ sigma_finite_measure P pair_measure  hoelzl@40859  599 proof  hoelzl@40859  600  show "pair_measure {} = 0"  hoelzl@40859  601  unfolding pair_measure_def by auto  hoelzl@40859  602 hoelzl@40859  603  show "countably_additive P pair_measure"  hoelzl@40859  604  unfolding countably_additive_def  hoelzl@40859  605  proof (intro allI impI)  hoelzl@40859  606  fix F :: "nat \ ('a \ 'b) set"  hoelzl@40859  607  assume F: "range F \ sets P" "disjoint_family F"  hoelzl@40859  608  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  hoelzl@40859  609  moreover from F have "\i. (\x. \2 (Pair x - F i)) \ borel_measurable M1"  hoelzl@40859  610  by (intro measure_cut_measurable_fst) auto  hoelzl@40859  611  moreover have "\x. disjoint_family (\i. Pair x - F i)"  hoelzl@40859  612  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  hoelzl@40859  613  moreover have "\x. x \ space M1 \ range (\i. Pair x - F i) \ sets M2"  hoelzl@40859  614  using F by (auto intro!: measurable_cut_fst)  hoelzl@40859  615  ultimately show "(\\<^isub>\n. pair_measure (F n)) = pair_measure (\i. F i)"  hoelzl@40859  616  by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric]  hoelzl@40859  617  M2.measure_countably_additive  hoelzl@40859  618  cong: M1.positive_integral_cong)  hoelzl@40859  619  qed  hoelzl@40859  620 hoelzl@40859  621  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  hoelzl@40859  622  show "\F::nat \ ('a \ 'b) set. range F \ sets P \ (\i. F i) = space P \ (\i. pair_measure (F i) \ \)"  hoelzl@40859  623  proof (rule exI[of _ F], intro conjI)  hoelzl@40859  624  show "range F \ sets P" using F by auto  hoelzl@40859  625  show "(\i. F i) = space P"  hoelzl@40859  626  using F by (auto simp: space_pair_algebra isoton_def)  hoelzl@40859  627  show "\i. pair_measure (F i) \ \" using F by auto  hoelzl@40859  628  qed  hoelzl@40859  629 qed  hoelzl@39088  630 hoelzl@41661  631 lemma (in pair_sigma_algebra) sets_swap:  hoelzl@41661  632  assumes "A \ sets P"  hoelzl@41661  633  shows "($$x, y). (y, x)) - A \ space (sigma (pair_algebra M2 M1)) \ sets (sigma (pair_algebra M2 M1))"  hoelzl@41661  634  (is "_ - A \ space ?Q \ sets ?Q")  hoelzl@41661  635 proof -  hoelzl@41661  636  have *: "(\(x, y). (y, x)) - A \ space ?Q = (\(x, y). (y, x))  A"  hoelzl@41661  637  using A \ sets P sets_into_space by (auto simp: space_pair_algebra)  hoelzl@41661  638  show ?thesis  hoelzl@41661  639  unfolding * using assms by (rule sets_pair_sigma_algebra_swap)  hoelzl@41661  640 qed  hoelzl@41661  641 hoelzl@40859  642 lemma (in pair_sigma_finite) pair_measure_alt2:  hoelzl@40859  643  assumes "A \ sets P"  hoelzl@40859  644  shows "pair_measure A = M2.positive_integral (\y. \1 ((\x. (x, y)) - A))"  hoelzl@40859  645  (is "_ = ?\ A")  hoelzl@40859  646 proof -  hoelzl@40859  647  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  hoelzl@40859  648  show ?thesis  hoelzl@40859  649  proof (rule measure_unique_Int_stable[where \="?\", OF Int_stable_pair_algebra],  hoelzl@40859  650  simp_all add: pair_sigma_algebra_def[symmetric])  hoelzl@40859  651  show "range F \ sets E" "F \ space E" "\i. pair_measure (F i) \ \"  hoelzl@40859  652  using F by auto  hoelzl@40859  653  show "measure_space P pair_measure" by default  hoelzl@41659  654  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41661  655  have P: "sigma_algebra P" by default  hoelzl@41661  656  show "measure_space P ?\"  hoelzl@41661  657  apply (rule Q.measure_space_vimage[OF P])  hoelzl@41661  658  apply (rule Q.pair_sigma_algebra_swap_measurable)  hoelzl@41661  659  proof -  hoelzl@41661  660  fix A assume "A \ sets P"  hoelzl@41661  661  from sets_swap[OF this]  hoelzl@41661  662  show "M2.positive_integral (\y. \1 ((\x. (x, y)) - A)) =  hoelzl@41661  663  Q.pair_measure ((\(x, y). (y, x)) - A \ space Q.P)"  hoelzl@41661  664  using sets_into_space[OF A \ sets P]  hoelzl@41661  665  by (auto simp add: Q.pair_measure_alt space_pair_algebra  hoelzl@41661  666  intro!: M2.positive_integral_cong arg_cong[where f=\1])  hoelzl@41661  667  qed  hoelzl@40859  668  fix X assume "X \ sets E"  hoelzl@40859  669  then obtain A B where X: "X = A \ B" and AB: "A \ sets M1" "B \ sets M2"  hoelzl@40859  670  unfolding pair_algebra_def by auto  hoelzl@40859  671  show "pair_measure X = ?\ X"  hoelzl@40859  672  proof -  hoelzl@40859  673  from AB have "?\ (A \ B) =  hoelzl@40859  674  M2.positive_integral (\y. \1 A * indicator B y)"  hoelzl@40859  675  by (auto intro!: M2.positive_integral_cong)  hoelzl@40859  676  with AB show ?thesis  hoelzl@40859  677  unfolding pair_measure_times[OF AB] X  hoelzl@40859  678  by (simp add: M2.positive_integral_cmult_indicator ac_simps)  hoelzl@40859  679  qed  hoelzl@40859  680  qed fact  hoelzl@40859  681 qed  hoelzl@40859  682 hoelzl@40859  683 section "Fubinis theorem"  hoelzl@40859  684 hoelzl@40859  685 lemma (in pair_sigma_finite) simple_function_cut:  hoelzl@40859  686  assumes f: "simple_function f"  hoelzl@40859  687  shows "(\x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  688  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  hoelzl@40859  689  = positive_integral f"  hoelzl@40859  690 proof -  hoelzl@40859  691  have f_borel: "f \ borel_measurable P"  hoelzl@40859  692  using f by (rule borel_measurable_simple_function)  hoelzl@40859  693  let "?F z" = "f - {z} \ space P"  hoelzl@40859  694  let "?F' x z" = "Pair x - ?F z"  hoelzl@40859  695  { fix x assume "x \ space M1"  hoelzl@40859  696  have [simp]: "\z y. indicator (?F z) (x, y) = indicator (?F' x z) y"  hoelzl@40859  697  by (auto simp: indicator_def)  hoelzl@40859  698  have "\y. y \ space M2 \ (x, y) \ space P" using x \ space M1  hoelzl@40859  699  by (simp add: space_pair_algebra)  hoelzl@40859  700  moreover have "\x z. ?F' x z \ sets M2" using f_borel  hoelzl@40859  701  by (intro borel_measurable_vimage measurable_cut_fst)  hoelzl@40859  702  ultimately have "M2.simple_function (\ y. f (x, y))"  hoelzl@40859  703  apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])  hoelzl@40859  704  apply (rule simple_function_indicator_representation[OF f])  hoelzl@40859  705  using x \ space M1 by (auto simp del: space_sigma) }  hoelzl@40859  706  note M2_sf = this  hoelzl@40859  707  { fix x assume x: "x \ space M1"  hoelzl@40859  708  then have "M2.positive_integral (\ y. f (x, y)) =  hoelzl@40859  709  (\z\f  space P. z * \2 (?F' x z))"  hoelzl@40859  710  unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]]  hoelzl@40859  711  unfolding M2.simple_integral_def  hoelzl@40859  712  proof (safe intro!: setsum_mono_zero_cong_left)  hoelzl@40859  713  from f show "finite (f  space P)" by (rule simple_functionD)  hoelzl@40859  714  next  hoelzl@40859  715  fix y assume "y \ space M2" then show "f (x, y) \ f  space P"  hoelzl@40859  716  using x \ space M1 by (auto simp: space_pair_algebra)  hoelzl@40859  717  next  hoelzl@40859  718  fix x' y assume "(x', y) \ space P"  hoelzl@40859  719  "f (x', y) \ (\y. f (x, y))  space M2"  hoelzl@40859  720  then have *: "?F' x (f (x', y)) = {}"  hoelzl@40859  721  by (force simp: space_pair_algebra)  hoelzl@40859  722  show "f (x', y) * \2 (?F' x (f (x', y))) = 0"  hoelzl@40859  723  unfolding * by simp  hoelzl@40859  724  qed (simp add: vimage_compose[symmetric] comp_def  hoelzl@40859  725  space_pair_algebra) }  hoelzl@40859  726  note eq = this  hoelzl@40859  727  moreover have "\z. ?F z \ sets P"  hoelzl@40859  728  by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)  hoelzl@40859  729  moreover then have "\z. (\x. \2 (?F' x z)) \ borel_measurable M1"  hoelzl@40859  730  by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)  hoelzl@40859  731  ultimately  hoelzl@40859  732  show "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  733  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  hoelzl@40859  734  = positive_integral f"  hoelzl@40859  735  by (auto simp del: vimage_Int cong: measurable_cong  hoelzl@41023  736  intro!: M1.borel_measurable_pextreal_setsum  hoelzl@40859  737  simp add: M1.positive_integral_setsum simple_integral_def  hoelzl@40859  738  M1.positive_integral_cmult  hoelzl@40859  739  M1.positive_integral_cong[OF eq]  hoelzl@40859  740  positive_integral_eq_simple_integral[OF f]  hoelzl@40859  741  pair_measure_alt[symmetric])  hoelzl@40859  742 qed  hoelzl@40859  743 hoelzl@40859  744 lemma (in pair_sigma_finite) positive_integral_fst_measurable:  hoelzl@40859  745  assumes f: "f \ borel_measurable P"  hoelzl@40859  746  shows "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  hoelzl@40859  747  (is "?C f \ borel_measurable M1")  hoelzl@40859  748  and "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  hoelzl@40859  749  positive_integral f"  hoelzl@40859  750 proof -  hoelzl@40859  751  from borel_measurable_implies_simple_function_sequence[OF f]  hoelzl@40859  752  obtain F where F: "\i. simple_function (F i)" "F \ f" by auto  hoelzl@40859  753  then have F_borel: "\i. F i \ borel_measurable P"  hoelzl@40859  754  and F_mono: "\i x. F i x \ F (Suc i) x"  hoelzl@40859  755  and F_SUPR: "\x. (SUP i. F i x) = f x"  hoelzl@41097  756  unfolding isoton_fun_expand unfolding isoton_def le_fun_def  hoelzl@40859  757  by (auto intro: borel_measurable_simple_function)  hoelzl@40859  758  note sf = simple_function_cut[OF F(1)]  hoelzl@41097  759  then have "(\x. SUP i. ?C (F i) x) \ borel_measurable M1"  hoelzl@41097  760  using F(1) by auto  hoelzl@40859  761  moreover  hoelzl@40859  762  { fix x assume "x \ space M1"  hoelzl@40859  763  have isotone: "(\ i y. F i (x, y)) \ (\y. f (x, y))"  hoelzl@40859  764  using F \ f unfolding isoton_fun_expand  hoelzl@40859  765  by (auto simp: isoton_def)  hoelzl@40859  766  note measurable_pair_image_snd[OF F_borelx \ space M1]  hoelzl@40859  767  from M2.positive_integral_isoton[OF isotone this]  hoelzl@40859  768  have "(SUP i. ?C (F i) x) = ?C f x"  hoelzl@40859  769  by (simp add: isoton_def) }  hoelzl@40859  770  note SUPR_C = this  hoelzl@40859  771  ultimately show "?C f \ borel_measurable M1"  hoelzl@41097  772  by (simp cong: measurable_cong)  hoelzl@41544  773  have "positive_integral (\x. (SUP i. F i x)) = (SUP i. positive_integral (F i))"  hoelzl@40859  774  using F_borel F_mono  hoelzl@40859  775  by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])  hoelzl@40859  776  also have "(SUP i. positive_integral (F i)) =  hoelzl@40859  777  (SUP i. M1.positive_integral (\x. M2.positive_integral (\y. F i (x, y))))"  hoelzl@40859  778  unfolding sf(2) by simp  hoelzl@40859  779  also have "\ = M1.positive_integral (\x. SUP i. M2.positive_integral (\y. F i (x, y)))"  hoelzl@40859  780  by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)]  hoelzl@40859  781  M2.positive_integral_mono F_mono)  hoelzl@40859  782  also have "\ = M1.positive_integral (\x. M2.positive_integral (\y. SUP i. F i (x, y)))"  hoelzl@40859  783  using F_borel F_mono  hoelzl@40859  784  by (auto intro!: M2.positive_integral_monotone_convergence_SUP  hoelzl@40859  785  M1.positive_integral_cong measurable_pair_image_snd)  hoelzl@40859  786  finally show "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  hoelzl@40859  787  positive_integral f"  hoelzl@40859  788  unfolding F_SUPR by simp  hoelzl@40859  789 qed  hoelzl@40859  790 hoelzl@41661  791 lemma (in pair_sigma_finite) positive_integral_product_swap:  hoelzl@41661  792  assumes f: "f \ borel_measurable P"  hoelzl@41661  793  shows "measure_space.positive_integral  hoelzl@41661  794  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) (\x. f (case x of (x,y)\(y,x))) =  hoelzl@41661  795  positive_integral f"  hoelzl@41661  796 proof -  hoelzl@41661  797  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41661  798  have P: "sigma_algebra P" by default  hoelzl@41661  799  show ?thesis  hoelzl@41661  800  unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]  hoelzl@41661  801  proof (rule positive_integral_cong_measure)  hoelzl@41661  802  fix A  hoelzl@41661  803  assume A: "A \ sets P"  hoelzl@41661  804  from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]  hoelzl@41661  805  show "Q.pair_measure ((\(x, y). (y, x)) - A \ space Q.P) = pair_measure A"  hoelzl@41661  806  by (auto intro!: M1.positive_integral_cong arg_cong[where f=\2]  hoelzl@41661  807  simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)  hoelzl@41661  808  qed  hoelzl@41661  809 qed  hoelzl@41661  810 hoelzl@40859  811 lemma (in pair_sigma_finite) positive_integral_snd_measurable:  hoelzl@40859  812  assumes f: "f \ borel_measurable P"  hoelzl@40859  813  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  814  positive_integral f"  hoelzl@40859  815 proof -  hoelzl@40859  816  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@40859  817  note pair_sigma_algebra_measurable[OF f]  hoelzl@40859  818  from Q.positive_integral_fst_measurable[OF this]  hoelzl@40859  819  have "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  820  Q.positive_integral (\(x, y). f (y, x))"  hoelzl@40859  821  by simp  hoelzl@41661  822  also have "Q.positive_integral (\(x, y). f (y, x)) = positive_integral f"  hoelzl@41661  823  unfolding positive_integral_product_swap[OF f, symmetric]  hoelzl@41661  824  by (auto intro!: Q.positive_integral_cong)  hoelzl@40859  825  finally show ?thesis .  hoelzl@40859  826 qed  hoelzl@40859  827 hoelzl@40859  828 lemma (in pair_sigma_finite) Fubini:  hoelzl@40859  829  assumes f: "f \ borel_measurable P"  hoelzl@40859  830  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  hoelzl@40859  831  M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))"  hoelzl@40859  832  unfolding positive_integral_snd_measurable[OF assms]  hoelzl@40859  833  unfolding positive_integral_fst_measurable[OF assms] ..  hoelzl@40859  834 hoelzl@40859  835 lemma (in pair_sigma_finite) AE_pair:  hoelzl@40859  836  assumes "almost_everywhere (\x. Q x)"  hoelzl@40859  837  shows "M1.almost_everywhere (\x. M2.almost_everywhere (\y. Q (x, y)))"  hoelzl@40859  838 proof -  hoelzl@40859  839  obtain N where N: "N \ sets P" "pair_measure N = 0" "{x\space P. \ Q x} \ N"  hoelzl@40859  840  using assms unfolding almost_everywhere_def by auto  hoelzl@40859  841  show ?thesis  hoelzl@40859  842  proof (rule M1.AE_I)  hoelzl@40859  843  from N measure_cut_measurable_fst[OF N \ sets P]  hoelzl@40859  844  show "\1 {x\space M1. \2 (Pair x - N) \ 0} = 0"  hoelzl@40859  845  by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def)  hoelzl@40859  846  show "{x \ space M1. \2 (Pair x - N) \ 0} \ sets M1"  hoelzl@41023  847  by (intro M1.borel_measurable_pextreal_neq_const measure_cut_measurable_fst N)  hoelzl@40859  848  { fix x assume "x \ space M1" "\2 (Pair x - N) = 0"  hoelzl@40859  849  have "M2.almost_everywhere (\y. Q (x, y))"  hoelzl@40859  850  proof (rule M2.AE_I)  hoelzl@40859  851  show "\2 (Pair x - N) = 0" by fact  hoelzl@40859  852  show "Pair x - N \ sets M2" by (intro measurable_cut_fst N)  hoelzl@40859  853  show "{y \ space M2. \ Q (x, y)} \ Pair x - N"  hoelzl@40859  854  using N x \ space M1 unfolding space_sigma space_pair_algebra by auto  hoelzl@40859  855  qed }  hoelzl@40859  856  then show "{x \ space M1. \ M2.almost_everywhere (\y. Q (x, y))} \ {x \ space M1. \2 (Pair x - N) \ 0}"  hoelzl@40859  857  by auto  hoelzl@39088  858  qed  hoelzl@39088  859 qed  hoelzl@35833  860 hoelzl@41026  861 lemma (in pair_sigma_algebra) measurable_product_swap:  hoelzl@41026  862  "f \ measurable (sigma (pair_algebra M2 M1)) M \ (\(x,y). f (y,x)) \ measurable P M"  hoelzl@41026  863 proof -  hoelzl@41026  864  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@41026  865  show ?thesis  hoelzl@41026  866  using pair_sigma_algebra_measurable[of "\(x,y). f (y, x)"]  hoelzl@41026  867  by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI)  hoelzl@41026  868 qed  hoelzl@41026  869 hoelzl@41026  870 lemma (in pair_sigma_finite) integrable_product_swap:  hoelzl@41661  871  assumes "integrable f"  hoelzl@41661  872  shows "measure_space.integrable  hoelzl@41661  873  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) (\(x,y). f (y,x))"  hoelzl@41026  874 proof -  hoelzl@41026  875  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41661  876  have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff)  hoelzl@41661  877  show ?thesis unfolding *  hoelzl@41661  878  using assms unfolding Q.integrable_def integrable_def  hoelzl@41661  879  apply (subst (1 2) positive_integral_product_swap)  hoelzl@41661  880  using integrable f unfolding integrable_def  hoelzl@41661  881  by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])  hoelzl@41661  882 qed  hoelzl@41661  883 hoelzl@41661  884 lemma (in pair_sigma_finite) integrable_product_swap_iff:  hoelzl@41661  885  "measure_space.integrable  hoelzl@41661  886  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) (\(x,y). f (y,x)) \  hoelzl@41661  887  integrable f"  hoelzl@41661  888 proof -  hoelzl@41661  889  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41661  890  from Q.integrable_product_swap[of "\(x,y). f (y,x)"] integrable_product_swap[of f]  hoelzl@41661  891  show ?thesis by auto  hoelzl@41026  892 qed  hoelzl@41026  893 hoelzl@41026  894 lemma (in pair_sigma_finite) integral_product_swap:  hoelzl@41661  895  assumes "integrable f"  hoelzl@41661  896  shows "measure_space.integral  hoelzl@41661  897  (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \2 M1 \1) (\(x,y). f (y,x)) =  hoelzl@41661  898  integral f"  hoelzl@41026  899 proof -  hoelzl@41026  900  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41661  901  have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff)  hoelzl@41026  902  show ?thesis  hoelzl@41661  903  unfolding integral_def Q.integral_def *  hoelzl@41661  904  apply (subst (1 2) positive_integral_product_swap)  hoelzl@41661  905  using integrable f unfolding integrable_def  hoelzl@41661  906  by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])  hoelzl@41026  907 qed  hoelzl@41026  908 hoelzl@41026  909 lemma (in pair_sigma_finite) integrable_fst_measurable:  hoelzl@41026  910  assumes f: "integrable f"  hoelzl@41026  911  shows "M1.almost_everywhere (\x. M2.integrable (\ y. f (x, y)))" (is "?AE")  hoelzl@41026  912  and "M1.integral (\ x. M2.integral (\ y. f (x, y))) = integral f" (is "?INT")  hoelzl@41026  913 proof -  hoelzl@41026  914  let "?pf x" = "Real (f x)" and "?nf x" = "Real (- f x)"  hoelzl@41026  915  have  hoelzl@41026  916  borel: "?nf \ borel_measurable P""?pf \ borel_measurable P" and  hoelzl@41026  917  int: "positive_integral ?nf \ \" "positive_integral ?pf \ \"  hoelzl@41026  918  using assms by auto  hoelzl@41026  919  have "M1.positive_integral (\x. M2.positive_integral (\y. Real (f (x, y)))) \ \"  hoelzl@41026  920  "M1.positive_integral (\x. M2.positive_integral (\y. Real (- f (x, y)))) \ \"  hoelzl@41026  921  using borel[THEN positive_integral_fst_measurable(1)] int  hoelzl@41026  922  unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all  hoelzl@41026  923  with borel[THEN positive_integral_fst_measurable(1)]  hoelzl@41026  924  have AE: "M1.almost_everywhere (\x. M2.positive_integral (\y. Real (f (x, y))) \$$"  hoelzl@41026  925  "M1.almost_everywhere (\x. M2.positive_integral (\y. Real (- f (x, y))) \ \)"  hoelzl@41026  926  by (auto intro!: M1.positive_integral_omega_AE)  hoelzl@41026  927  then show ?AE  hoelzl@41026  928  apply (rule M1.AE_mp[OF _ M1.AE_mp])  hoelzl@41026  929  apply (rule M1.AE_cong)  hoelzl@41026  930  using assms unfolding M2.integrable_def  hoelzl@41026  931  by (auto intro!: measurable_pair_image_snd)  hoelzl@41026  932  have "M1.integrable  hoelzl@41026  933  (\x. real (M2.positive_integral (\xa. Real (f (x, xa)))))" (is "M1.integrable ?f")  hoelzl@41026  934  proof (unfold M1.integrable_def, intro conjI)  hoelzl@41026  935  show "?f \ borel_measurable M1"  hoelzl@41026  936  using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)  hoelzl@41026  937  have "M1.positive_integral (\x. Real (?f x)) =  hoelzl@41026  938  M1.positive_integral (\x. M2.positive_integral (\xa. Real (f (x, xa))))"  hoelzl@41026  939  apply (rule M1.positive_integral_cong_AE)  hoelzl@41026  940  apply (rule M1.AE_mp[OF AE(1)])  hoelzl@41026  941  apply (rule M1.AE_cong)  hoelzl@41026  942  by (auto simp: Real_real)  hoelzl@41026  943  then show "M1.positive_integral (\x. Real (?f x)) \ \"  hoelzl@41026  944  using positive_integral_fst_measurable[OF borel(2)] int by simp  hoelzl@41026  945  have "M1.positive_integral (\x. Real (- ?f x)) = M1.positive_integral (\x. 0)"  hoelzl@41026  946  by (intro M1.positive_integral_cong) simp  hoelzl@41026  947  then show "M1.positive_integral (\x. Real (- ?f x)) \ \" by simp  hoelzl@41026  948  qed  hoelzl@41026  949  moreover have "M1.integrable  hoelzl@41026  950  (\x. real (M2.positive_integral (\xa. Real (- f (x, xa)))))" (is "M1.integrable ?f")  hoelzl@41026  951  proof (unfold M1.integrable_def, intro conjI)  hoelzl@41026  952  show "?f \ borel_measurable M1"  hoelzl@41026  953  using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)  hoelzl@41026  954  have "M1.positive_integral (\x. Real (?f x)) =  hoelzl@41026  955  M1.positive_integral (\x. M2.positive_integral (\xa. Real (- f (x, xa))))"  hoelzl@41026  956  apply (rule M1.positive_integral_cong_AE)  hoelzl@41026  957  apply (rule M1.AE_mp[OF AE(2)])  hoelzl@41026  958  apply (rule M1.AE_cong)  hoelzl@41026  959  by (auto simp: Real_real)  hoelzl@41026  960  then show "M1.positive_integral (\x. Real (?f x)) \ \"  hoelzl@41026  961  using positive_integral_fst_measurable[OF borel(1)] int by simp  hoelzl@41026  962  have "M1.positive_integral (\x. Real (- ?f x)) = M1.positive_integral (\x. 0)"  hoelzl@41026  963  by (intro M1.positive_integral_cong) simp  hoelzl@41026  964  then show "M1.positive_integral (\x. Real (- ?f x)) \ \" by simp  hoelzl@41026  965  qed  hoelzl@41026  966  ultimately show ?INT  hoelzl@41026  967  unfolding M2.integral_def integral_def  hoelzl@41026  968  borel[THEN positive_integral_fst_measurable(2), symmetric]  hoelzl@41026  969  by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])  hoelzl@41026  970 qed  hoelzl@41026  971 hoelzl@41026  972 lemma (in pair_sigma_finite) integrable_snd_measurable:  hoelzl@41026  973  assumes f: "integrable f"  hoelzl@41026  974  shows "M2.almost_everywhere (\y. M1.integrable (\x. f (x, y)))" (is "?AE")  hoelzl@41026  975  and "M2.integral (\y. M1.integral (\x. f (x, y))) = integral f" (is "?INT")  hoelzl@41026  976 proof -  hoelzl@41026  977  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  hoelzl@41026  978  have Q_int: "Q.integrable (\(x, y). f (y, x))"  hoelzl@41661  979  using f unfolding integrable_product_swap_iff .  hoelzl@41026  980  show ?INT  hoelzl@41026  981  using Q.integrable_fst_measurable(2)[OF Q_int]  hoelzl@41661  982  using integral_product_swap[OF f] by simp  hoelzl@41026  983  show ?AE  hoelzl@41026  984  using Q.integrable_fst_measurable(1)[OF Q_int]  hoelzl@41026  985  by simp  hoelzl@41026  986 qed  hoelzl@41026  987 hoelzl@41026  988 lemma (in pair_sigma_finite) Fubini_integral:  hoelzl@41026  989  assumes f: "integrable f"  hoelzl@41026  990  shows "M2.integral (\y. M1.integral (\x. f (x, y))) =  hoelzl@41026  991  M1.integral (\x. M2.integral (\y. f (x, y)))"  hoelzl@41026  992  unfolding integrable_snd_measurable[OF assms]  hoelzl@41026  993  unfolding integrable_fst_measurable[OF assms] ..  hoelzl@41026  994 hoelzl@40859  995 section "Finite product spaces"  hoelzl@40859  996 hoelzl@40859  997 section "Products"  hoelzl@40859  998 hoelzl@40859  999 locale product_sigma_algebra =  hoelzl@40859  1000  fixes M :: "'i \ 'a algebra"  hoelzl@40859  1001  assumes sigma_algebras: "\i. sigma_algebra (M i)"  hoelzl@40859  1002 hoelzl@40859  1003 locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \ 'a algebra" +  hoelzl@40859  1004  fixes I :: "'i set"  hoelzl@40859  1005  assumes finite_index: "finite I"  hoelzl@40859  1006 hoelzl@40859  1007 syntax  hoelzl@40859  1008  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)  hoelzl@40859  1009 hoelzl@40859  1010 syntax (xsymbols)  hoelzl@40859  1011  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@40859  1012 hoelzl@40859  1013 syntax (HTML output)  hoelzl@40859  1014  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@40859  1015 hoelzl@40859  1016 translations  hoelzl@40859  1017  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"  hoelzl@40859  1018 hoelzl@35833  1019 definition  hoelzl@40859  1020  "product_algebra M I = \ space = (\\<^isub>E i\I. space (M i)), sets = Pi\<^isub>E I  (\ i \ I. sets (M i)) \"  hoelzl@40859  1021 hoelzl@40859  1022 abbreviation (in finite_product_sigma_algebra) "G \ product_algebra M I"  hoelzl@40859  1023 abbreviation (in finite_product_sigma_algebra) "P \ sigma G"  hoelzl@40859  1024 hoelzl@40859  1025 sublocale product_sigma_algebra \ M: sigma_algebra "M i" for i by (rule sigma_algebras)  hoelzl@40859  1026 hoelzl@40859  1027 lemma (in finite_product_sigma_algebra) product_algebra_into_space:  hoelzl@40859  1028  "sets G \ Pow (space G)"  hoelzl@40859  1029  using M.sets_into_space unfolding product_algebra_def  hoelzl@40859  1030  by auto blast  hoelzl@40859  1031 hoelzl@40859  1032 sublocale finite_product_sigma_algebra \ sigma_algebra P  hoelzl@40859  1033  using product_algebra_into_space by (rule sigma_algebra_sigma)  hoelzl@40859  1034 hoelzl@41095  1035 lemma product_algebraE:  hoelzl@41095  1036  assumes "A \ sets (product_algebra M I)"  hoelzl@41095  1037  obtains E where "A = Pi\<^isub>E I E" "E \ (\ i\I. sets (M i))"  hoelzl@41095  1038  using assms unfolding product_algebra_def by auto  hoelzl@41095  1039 hoelzl@41095  1040 lemma product_algebraI[intro]:  hoelzl@41095  1041  assumes "E \ (\ i\I. sets (M i))"  hoelzl@41095  1042  shows "Pi\<^isub>E I E \ sets (product_algebra M I)"  hoelzl@41095  1043  using assms unfolding product_algebra_def by auto  hoelzl@41095  1044 hoelzl@40859  1045 lemma space_product_algebra[simp]:  hoelzl@40859  1046  "space (product_algebra M I) = Pi\<^isub>E I (\i. space (M i))"  hoelzl@40859  1047  unfolding product_algebra_def by simp  hoelzl@40859  1048 hoelzl@41095  1049 lemma product_algebra_sets_into_space:  hoelzl@41095  1050  assumes "\i. i\I \ sets (M i) \ Pow (space (M i))"  hoelzl@41095  1051  shows "sets (product_algebra M I) \ Pow (space (product_algebra M I))"  hoelzl@41095  1052  using assms by (auto simp: product_algebra_def) blast  hoelzl@41095  1053 hoelzl@40859  1054 lemma (in finite_product_sigma_algebra) P_empty:  hoelzl@40859  1055  "I = {} \ P = \ space = {\k. undefined}, sets = { {}, {\k. undefined} }\"  hoelzl@40872  1056  unfolding product_algebra_def by (simp add: sigma_def image_constant)  hoelzl@40859  1057 hoelzl@40859  1058 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:  hoelzl@40859  1059  "\ \i. i \ I \ A i \ sets (M i) \ \ Pi\<^isub>E I A \ sets P"  hoelzl@40859  1060  by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)  hoelzl@40859  1061 hoelzl@41095  1062 lemma (in product_sigma_algebra) bij_inv_restrict_merge:  hoelzl@41095  1063  assumes [simp]: "I \ J = {}"  hoelzl@41095  1064  shows "bij_inv  hoelzl@41095  1065  (space (sigma (product_algebra M (I \ J))))  hoelzl@41095  1066  (space (sigma (pair_algebra (product_algebra M I) (product_algebra M J))))  hoelzl@41095  1067  (\x. (restrict x I, restrict x J)) (\(x, y). merge I x J y)"  hoelzl@41095  1068  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)  hoelzl@41095  1069 hoelzl@41095  1070 lemma (in product_sigma_algebra) bij_inv_singleton:  hoelzl@41095  1071  "bij_inv (space (sigma (product_algebra M {i}))) (space (M i))  hoelzl@41095  1072  (\x. x i) (\x. (\j\{i}. x))"  hoelzl@41095  1073  by (rule bij_invI) (auto simp: restrict_def extensional_def fun_eq_iff)  hoelzl@41095  1074 hoelzl@41095  1075 lemma (in product_sigma_algebra) bij_inv_restrict_insert:  hoelzl@41095  1076  assumes [simp]: "i \ I"  hoelzl@41095  1077  shows "bij_inv  hoelzl@41095  1078  (space (sigma (product_algebra M (insert i I))))  hoelzl@41095  1079  (space (sigma (pair_algebra (product_algebra M I) (M i))))  hoelzl@41095  1080  (\x. (restrict x I, x i)) (\(x, y). x(i := y))"  hoelzl@41095  1081  by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)  hoelzl@41095  1082 hoelzl@41095  1083 lemma (in product_sigma_algebra) measurable_restrict_on_generating:  hoelzl@41095  1084  assumes [simp]: "I \ J = {}"  hoelzl@41095  1085  shows "(\x. (restrict x I, restrict x J)) \ measurable  hoelzl@41095  1086  (product_algebra M (I \ J))  hoelzl@41095  1087  (pair_algebra (product_algebra M I) (product_algebra M J))"  hoelzl@41095  1088  (is "?R \ measurable ?IJ ?P")  hoelzl@41095  1089 proof (unfold measurable_def, intro CollectI conjI ballI)  hoelzl@41095  1090  show "?R \ space ?IJ \ space ?P" by (auto simp: space_pair_algebra)  hoelzl@41095  1091  { fix F E assume "E \ (\ i\I. sets (M i))" "F \ (\ i\J. sets (M i))"  hoelzl@41095  1092  then have "Pi (I \ J) (merge I E J F) \ (\\<^isub>E i\I \ J. space (M i)) =  hoelzl@41095  1093  Pi\<^isub>E (I \ J) (merge I E J F)"  hoelzl@41095  1094  using M.sets_into_space by auto blast+ }  hoelzl@41095  1095  note this[simp]  hoelzl@41095  1096  show "\A. A \ sets ?P \ ?R - A \ space ?IJ \ sets ?IJ"  hoelzl@41095  1097  by (force elim!: pair_algebraE product_algebraE  hoelzl@41095  1098  simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)  hoelzl@41095  1099  qed  hoelzl@41095  1100 hoelzl@41095  1101 lemma (in product_sigma_algebra) measurable_merge_on_generating:  hoelzl@41095  1102  assumes [simp]: "I \ J = {}"  hoelzl@41095  1103  shows "(\(x, y). merge I x J y) \ measurable  hoelzl@41095  1104  (pair_algebra (product_algebra M I) (product_algebra M J))  hoelzl@41095  1105  (product_algebra M (I \ J))"  hoelzl@41095  1106  (is "?M \ measurable ?P ?IJ")  hoelzl@41095  1107 proof (unfold measurable_def, intro CollectI conjI ballI)  hoelzl@41095  1108  show "?M \ space ?P \ space ?IJ" by (auto simp: space_pair_algebra)  hoelzl@41095  1109  { fix E assume "E \ (\ i\I. sets (M i))" "E \ (\ i\J. sets (M i))"  hoelzl@41095  1110  then have "Pi I E \ Pi J E \ (\\<^isub>E i\I. space (M i)) \ (\\<^isub>E i\J. space (M i)) =  hoelzl@41095  1111  Pi\<^isub>E I E \ Pi\<^isub>E J E"  hoelzl@41095  1112  using M.sets_into_space by auto blast+ }  hoelzl@41095  1113  note this[simp]  hoelzl@41095  1114  show "\A. A \ sets ?IJ \ ?M - A \ space ?P \ sets ?P"  hoelzl@41095  1115  by (force elim!: pair_algebraE product_algebraE  hoelzl@41095  1116  simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)  hoelzl@40859  1117  qed  hoelzl@41095  1118 hoelzl@41095  1119 lemma (in product_sigma_algebra) measurable_singleton_on_generator:  hoelzl@41095  1120  "(\x. \j\{i}. x) \ measurable (M i) (product_algebra M {i})"  hoelzl@41095  1121  (is "?f \ measurable _ ?P")  hoelzl@41095  1122 proof (unfold measurable_def, intro CollectI conjI)  hoelzl@41095  1123  show "?f \ space (M i) \ space ?P" by auto  hoelzl@41095  1124  have "\E. E i \ sets (M i) \ ?f - Pi\<^isub>E {i} E \ space (M i) = E i"  hoelzl@41095  1125  using M.sets_into_space by auto  hoelzl@41095  1126  then show "\A \ sets ?P. ?f - A \ space (M i) \ sets (M i)"  hoelzl@41095  1127  by (auto elim!: product_algebraE)  hoelzl@41095  1128 qed  hoelzl@41095  1129 hoelzl@41095  1130 lemma (in product_sigma_algebra) measurable_component_on_generator:  hoelzl@41095  1131  assumes "i \ I" shows "(\x. x i) \ measurable (product_algebra M I) (M i)"  hoelzl@41095  1132  (is "?f \ measurable ?P _")  hoelzl@41095  1133 proof (unfold measurable_def, intro CollectI conjI ballI)  hoelzl@41095  1134  show "?f \ space ?P \ space (M i)" using i \ I by auto  hoelzl@41095  1135  fix A assume "A \ sets (M i)"  hoelzl@41095  1136  moreover then have "(\x. x i) - A \ (\\<^isub>E i\I. space (M i)) =  hoelzl@41095  1137  (\\<^isub>E j\I. if i = j then A else space (M j))"  hoelzl@41095  1138  using M.sets_into_space i \ I  hoelzl@41095  1139  by (fastsimp dest: Pi_mem split: split_if_asm)  hoelzl@41095  1140  ultimately show "?f - A \ space ?P \ sets ?P"  hoelzl@41095  1141  by (auto intro!: product_algebraI)  hoelzl@41095  1142 qed  hoelzl@40859  1143 hoelzl@41095  1144 lemma (in product_sigma_algebra) measurable_restrict_singleton_on_generating:  hoelzl@41095  1145  assumes [simp]: "i \ I"  hoelzl@41095  1146  shows "(\x. (restrict x I, x i)) \ measurable  hoelzl@41095  1147  (product_algebra M (insert i I))  hoelzl@41095  1148  (pair_algebra (product_algebra M I) (M i))"  hoelzl@41095  1149  (is "?R \ measurable ?I ?P")  hoelzl@41095  1150 proof (unfold measurable_def, intro CollectI conjI ballI)  hoelzl@41095  1151  show "?R \ space ?I \ space ?P" by (auto simp: space_pair_algebra)  hoelzl@41095  1152  { fix E F assume "E \ (\ i\I. sets (M i))" "F \ sets (M i)"  hoelzl@41095  1153  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  1154  Pi\<^isub>E (insert i I) (E(i := F))"  hoelzl@41095  1155  using M.sets_into_space using i\I by (auto simp: restrict_Pi_cancel) blast+ }  hoelzl@41095  1156  note this[simp]  hoelzl@41095  1157  show "\A. A \ sets ?P \ ?R - A \ space ?I \ sets ?I"  hoelzl@41095  1158  by (force elim!: pair_algebraE product_algebraE  hoelzl@41095  1159  simp del: vimage_Int simp: space_pair_algebra)  hoelzl@41095  1160 qed  hoelzl@41095  1161 hoelzl@41095  1162 lemma (in product_sigma_algebra) measurable_merge_singleton_on_generating:  hoelzl@41095  1163  assumes [simp]: "i \ I"  hoelzl@41095  1164  shows "(\(x, y). x(i := y)) \ measurable  hoelzl@41095  1165  (pair_algebra (product_algebra M I) (M i))  hoelzl@41095  1166  (product_algebra M (insert i I))"  hoelzl@41095  1167  (is "?M \ measurable ?P ?IJ")  hoelzl@41095  1168 proof (unfold measurable_def, intro CollectI conjI ballI)  hoelzl@41095  1169  show "?M \ space ?P \ space ?IJ" by (auto simp: space_pair_algebra)  hoelzl@41095  1170  { fix E assume "E \ (\ i\I. sets (M i))" "E i \ sets (M i)"  hoelzl@41095  1171  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  1172  Pi\<^isub>E I E \ E i"  hoelzl@41095  1173  using M.sets_into_space by auto blast+ }  hoelzl@41095  1174  note this[simp]  hoelzl@41095  1175  show "\A. A \ sets ?IJ \ ?M - A \ space ?P \ sets ?P"  hoelzl@41095  1176  by (force elim!: pair_algebraE product_algebraE  hoelzl@41095  1177  simp del: vimage_Int simp: space_pair_algebra)  hoelzl@41026  1178 qed  hoelzl@41026  1179 hoelzl@40859  1180 section "Generating set generates also product algebra"  hoelzl@40859  1181 hoelzl@40859  1182 lemma pair_sigma_algebra_sigma:  hoelzl@40859  1183  assumes 1: "S1 \ (space E1)" "range S1 \ sets E1" and E1: "sets E1 \ Pow (space E1)"  hoelzl@40859  1184  assumes 2: "S2 \ (space E2)" "range S2 \ sets E2" and E2: "sets E2 \ Pow (space E2)"  hoelzl@40859  1185  shows "sigma (pair_algebra (sigma E1) (sigma E2)) = sigma (pair_algebra E1 E2)"  hoelzl@40859  1186  (is "?S = ?E")  hoelzl@40859  1187 proof -  hoelzl@40859  1188  interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)  hoelzl@40859  1189  interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)  hoelzl@40859  1190  have P: "sets (pair_algebra E1 E2) \ Pow (space E1 \ space E2)"  hoelzl@40859  1191  using E1 E2 by (auto simp add: pair_algebra_def)  hoelzl@40859  1192  interpret E: sigma_algebra ?E unfolding pair_algebra_def  hoelzl@40859  1193  using E1 E2 by (intro sigma_algebra_sigma) auto  hoelzl@40859  1194  { fix A assume "A \ sets E1"  hoelzl@40859  1195  then have "fst - A \ space ?E = A \ (\i. S2 i)"  hoelzl@40859  1196  using E1 2 unfolding isoton_def pair_algebra_def by auto  hoelzl@40859  1197  also have "\ = (\i. A \ S2 i)" by auto  hoelzl@40859  1198  also have "\ \ sets ?E" unfolding pair_algebra_def sets_sigma  hoelzl@40859  1199  using 2 A \ sets E1  hoelzl@40859  1200  by (intro sigma_sets.Union)  hoelzl@40859  1201  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@40859  1202  finally have "fst - A \ space ?E \ sets ?E" . }  hoelzl@40859  1203  moreover  hoelzl@40859  1204  { fix B assume "B \ sets E2"  hoelzl@40859  1205  then have "snd - B \ space ?E = (\i. S1 i) \ B"  hoelzl@40859  1206  using E2 1 unfolding isoton_def pair_algebra_def by auto  hoelzl@40859  1207  also have "\ = (\i. S1 i \ B)" by auto  hoelzl@40859  1208  also have "\ \ sets ?E"  hoelzl@40859  1209  using 1 B \ sets E2 unfolding pair_algebra_def sets_sigma  hoelzl@40859  1210  by (intro sigma_sets.Union)  hoelzl@40859  1211  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@40859  1212  finally have "snd - B \ space ?E \ sets ?E" . }  hoelzl@40859  1213  ultimately have proj:  hoelzl@40859  1214  "fst \ measurable ?E (sigma E1) \ snd \ measurable ?E (sigma E2)"  hoelzl@40859  1215  using E1 E2 by (subst (1 2) E.measurable_iff_sigma)  hoelzl@40859  1216  (auto simp: pair_algebra_def sets_sigma)  hoelzl@40859  1217  { fix A B assume A: "A \ sets (sigma E1)" and B: "B \ sets (sigma E2)"  hoelzl@40859  1218  with proj have "fst - A \ space ?E \ sets ?E" "snd - B \ space ?E \ sets ?E"  hoelzl@40859  1219  unfolding measurable_def by simp_all  hoelzl@40859  1220  moreover have "A \ B = (fst - A \ space ?E) \ (snd - B \ space ?E)"  hoelzl@40859  1221  using A B M1.sets_into_space M2.sets_into_space  hoelzl@40859  1222  by (auto simp: pair_algebra_def)  hoelzl@40859  1223  ultimately have "A \ B \ sets ?E" by auto }  hoelzl@40859  1224  then have "sigma_sets (space ?E) (sets (pair_algebra (sigma E1) (sigma E2))) \ sets ?E"  hoelzl@40859  1225  by (intro E.sigma_sets_subset) (auto simp add: pair_algebra_def sets_sigma)  hoelzl@40859  1226  then have subset: "sets ?S \ sets ?E"  hoelzl@40859  1227  by (simp add: sets_sigma pair_algebra_def)  hoelzl@40859  1228  have "sets ?S = sets ?E"  hoelzl@40859  1229  proof (intro set_eqI iffI)  hoelzl@40859  1230  fix A assume "A \ sets ?E" then show "A \ sets ?S"  hoelzl@40859  1231  unfolding sets_sigma  hoelzl@40859  1232  proof induct  hoelzl@40859  1233  case (Basic A) then show ?case `