src/HOL/Probability/Product_Measure.thy
 author hoelzl Mon Mar 14 14:37:49 2011 +0100 (2011-03-14) changeset 41981 cdf7693bbe08 parent 41831 91a2b435dd7a child 42067 66c8281349ec permissions -rw-r--r--
reworked Probability theory: measures are not type restricted to positive extended reals
 hoelzl@35833  1 theory Product_Measure  hoelzl@38656  2 imports Lebesgue_Integration  hoelzl@35833  3 begin  hoelzl@35833  4 hoelzl@41689  5 lemma sigma_sets_subseteq: assumes "A \ B" shows "sigma_sets X A \ sigma_sets X B"  hoelzl@41689  6 proof  hoelzl@41689  7  fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B"  hoelzl@41689  8  by induct (insert A \ B, auto intro: sigma_sets.intros)  hoelzl@41689  9 qed  hoelzl@41689  10 hoelzl@40859  11 lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)"  hoelzl@40859  12  by auto  hoelzl@40859  13 hoelzl@40859  14 lemma Pair_vimage_times[simp]: "\A B x. Pair x - (A \ B) = (if x \ A then B else {})"  hoelzl@40859  15  by auto  hoelzl@40859  16 hoelzl@40859  17 lemma rev_Pair_vimage_times[simp]: "\A B y. (\x. (x, y)) - (A \ B) = (if y \ B then A else {})"  hoelzl@40859  18  by auto  hoelzl@40859  19 hoelzl@40859  20 lemma case_prod_distrib: "f (case x of (x, y) \ g x y) = (case x of (x, y) \ f (g x y))"  hoelzl@40859  21  by (cases x) simp  hoelzl@40859  22 hoelzl@41026  23 lemma split_beta': "($$x,y). f x y) = (\x. f (fst x) (snd x))"  hoelzl@41026  24  by (auto simp: fun_eq_iff)  hoelzl@41026  25 hoelzl@40859  26 abbreviation  hoelzl@40859  27  "Pi\<^isub>E A B \ Pi A B \ extensional A"  hellerar@39094  28 hoelzl@41689  29 syntax  hoelzl@41689  30  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)  hoelzl@41689  31 hoelzl@41689  32 syntax (xsymbols)  hoelzl@41689  33  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@41689  34 hoelzl@41689  35 syntax (HTML output)  hoelzl@41689  36  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  hoelzl@41689  37 hoelzl@41689  38 translations  hoelzl@41689  39  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"  hoelzl@41689  40 hoelzl@40859  41 abbreviation  hoelzl@40859  42  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"  hoelzl@40859  43  (infixr "->\<^isub>E" 60) where  hoelzl@40859  44  "A ->\<^isub>E B \ Pi\<^isub>E A (%_. B)"  hoelzl@40859  45 hoelzl@40859  46 notation (xsymbols)  hoelzl@40859  47  funcset_extensional (infixr "\\<^isub>E" 60)  hoelzl@40859  48 hoelzl@40859  49 lemma extensional_empty[simp]: "extensional {} = {\x. undefined}"  hoelzl@40859  50  by safe (auto simp add: extensional_def fun_eq_iff)  hoelzl@40859  51 hoelzl@40859  52 lemma extensional_insert[intro, simp]:  hoelzl@40859  53  assumes "a \ extensional (insert i I)"  hoelzl@40859  54  shows "a(i := b) \ extensional (insert i I)"  hoelzl@40859  55  using assms unfolding extensional_def by auto  hoelzl@40859  56 hoelzl@40859  57 lemma extensional_Int[simp]:  hoelzl@40859  58  "extensional I \ extensional I' = extensional (I \ I')"  hoelzl@40859  59  unfolding extensional_def by auto  hoelzl@38656  60 hoelzl@35833  61 definition  hoelzl@40859  62  "merge I x J y = (\i. if i \ I then x i else if i \ J then y i else undefined)"  hoelzl@40859  63 hoelzl@40859  64 lemma merge_apply[simp]:  hoelzl@40859  65  "I \ J = {} \ i \ I \ merge I x J y i = x i"  hoelzl@40859  66  "I \ J = {} \ i \ J \ merge I x J y i = y i"  hoelzl@40859  67  "J \ I = {} \ i \ I \ merge I x J y i = x i"  hoelzl@40859  68  "J \ I = {} \ i \ J \ merge I x J y i = y i"  hoelzl@40859  69  "i \ I \ i \ J \ merge I x J y i = undefined"  hoelzl@40859  70  unfolding merge_def by auto  hoelzl@40859  71 hoelzl@40859  72 lemma merge_commute:  hoelzl@40859  73  "I \ J = {} \ merge I x J y = merge J y I x"  hoelzl@40859  74  by (auto simp: merge_def intro!: ext)  hoelzl@40859  75 hoelzl@40859  76 lemma Pi_cancel_merge_range[simp]:  hoelzl@40859  77  "I \ J = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  hoelzl@40859  78  "I \ J = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  hoelzl@40859  79  "J \ I = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  hoelzl@40859  80  "J \ I = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  hoelzl@40859  81  by (auto simp: Pi_def)  hoelzl@40859  82 hoelzl@40859  83 lemma Pi_cancel_merge[simp]:  hoelzl@40859  84  "I \ J = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  hoelzl@40859  85  "J \ I = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  hoelzl@40859  86  "I \ J = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  hoelzl@40859  87  "J \ I = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  hoelzl@40859  88  by (auto simp: Pi_def)  hoelzl@40859  89 hoelzl@40859  90 lemma extensional_merge[simp]: "merge I x J y \ extensional (I \ J)"  hoelzl@40859  91  by (auto simp: extensional_def)  hoelzl@40859  92 hoelzl@40859  93 lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A"  hoelzl@40859  94  by (auto simp: restrict_def Pi_def)  hoelzl@40859  95 hoelzl@40859  96 lemma restrict_merge[simp]:  hoelzl@40859  97  "I \ J = {} \ restrict (merge I x J y) I = restrict x I"  hoelzl@40859  98  "I \ J = {} \ restrict (merge I x J y) J = restrict y J"  hoelzl@40859  99  "J \ I = {} \ restrict (merge I x J y) I = restrict x I"  hoelzl@40859  100  "J \ I = {} \ restrict (merge I x J y) J = restrict y J"  hoelzl@40859  101  by (auto simp: restrict_def intro!: ext)  hoelzl@40859  102 hoelzl@40859  103 lemma extensional_insert_undefined[intro, simp]:  hoelzl@40859  104  assumes "a \ extensional (insert i I)"  hoelzl@40859  105  shows "a(i := undefined) \ extensional I"  hoelzl@40859  106  using assms unfolding extensional_def by auto  hoelzl@40859  107 hoelzl@40859  108 lemma extensional_insert_cancel[intro, simp]:  hoelzl@40859  109  assumes "a \ extensional I"  hoelzl@40859  110  shows "a \ extensional (insert i I)"  hoelzl@40859  111  using assms unfolding extensional_def by auto  hoelzl@40859  112 hoelzl@41095  113 lemma merge_singleton[simp]: "i \ I \ merge I x {i} y = restrict (x(i := y i)) (insert i I)"  hoelzl@41095  114  unfolding merge_def by (auto simp: fun_eq_iff)  hoelzl@41095  115 hoelzl@41095  116 lemma Pi_Int: "Pi I E \ Pi I F = (\ i\I. E i \ F i)"  hoelzl@41095  117  by auto  hoelzl@41095  118 hoelzl@40859  119 lemma PiE_Int: "(Pi\<^isub>E I A) \ (Pi\<^isub>E I B) = Pi\<^isub>E I (\x. A x \ B x)"  hoelzl@40859  120  by auto  hoelzl@40859  121 hoelzl@40859  122 lemma Pi_cancel_fupd_range[simp]: "i \ I \ x \ Pi I (B(i := b)) \ x \ Pi I B"  hoelzl@40859  123  by (auto simp: Pi_def)  hoelzl@40859  124 hoelzl@40859  125 lemma Pi_split_insert_domain[simp]: "x \ Pi (insert i I) X \ x \ Pi I X \ x i \ X i"  hoelzl@40859  126  by (auto simp: Pi_def)  hoelzl@39088  127 hoelzl@40859  128 lemma Pi_split_domain[simp]: "x \ Pi (I \ J) X \ x \ Pi I X \ x \ Pi J X"  hoelzl@40859  129  by (auto simp: Pi_def)  hoelzl@40859  130 hoelzl@40859  131 lemma Pi_cancel_fupd[simp]: "i \ I \ x(i := a) \ Pi I B \ x \ Pi I B"  hoelzl@40859  132  by (auto simp: Pi_def)  hoelzl@40859  133 hoelzl@41095  134 lemma restrict_vimage:  hoelzl@41095  135  assumes "I \ J = {}"  hoelzl@41095  136  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  137  using assms by (auto simp: restrict_Pi_cancel)  hoelzl@41095  138 hoelzl@41095  139 lemma merge_vimage:  hoelzl@41095  140  assumes "I \ J = {}"  hoelzl@41095  141  shows "(\(x,y). merge I x J y) - Pi\<^isub>E (I \ J) E = Pi I E \ Pi J E"  hoelzl@41095  142  using assms by (auto simp: restrict_Pi_cancel)  hoelzl@41095  143 hoelzl@41095  144 lemma restrict_fupd[simp]: "i \ I \ restrict (f (i := x)) I = restrict f I"  hoelzl@41095  145  by (auto simp: restrict_def intro!: ext)  hoelzl@41095  146 hoelzl@41095  147 lemma merge_restrict[simp]:  hoelzl@41095  148  "merge I (restrict x I) J y = merge I x J y"  hoelzl@41095  149  "merge I x J (restrict y J) = merge I x J y"  hoelzl@41095  150  unfolding merge_def by (auto intro!: ext)  hoelzl@41095  151 hoelzl@41095  152 lemma merge_x_x_eq_restrict[simp]:  hoelzl@41095  153  "merge I x J x = restrict x (I \ J)"  hoelzl@41095  154  unfolding merge_def by (auto intro!: ext)  hoelzl@41095  155 hoelzl@41095  156 lemma Pi_fupd_iff: "i \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ A"  hoelzl@41095  157  apply auto  hoelzl@41095  158  apply (drule_tac x=x in Pi_mem)  hoelzl@41095  159  apply (simp_all split: split_if_asm)  hoelzl@41095  160  apply (drule_tac x=i in Pi_mem)  hoelzl@41095  161  apply (auto dest!: Pi_mem)  hoelzl@41095  162  done  hoelzl@41095  163 hoelzl@41095  164 lemma Pi_UN:  hoelzl@41095  165  fixes A :: "nat \ 'i \ 'a set"  hoelzl@41095  166  assumes "finite I" and mono: "\i n m. i \ I \ n \ m \ A n i \ A m i"  hoelzl@41095  167  shows "(\n. Pi I (A n)) = (\ i\I. \n. A n i)"  hoelzl@41095  168 proof (intro set_eqI iffI)  hoelzl@41095  169  fix f assume "f \ (\ i\I. \n. A n i)"  hoelzl@41095  170  then have "\i\I. \n. f i \ A n i" by auto  hoelzl@41095  171  from bchoice[OF this] obtain n where n: "\i. i \ I \ f i \ (A (n i) i)" by auto  hoelzl@41095  172  obtain k where k: "\i. i \ I \ n i \ k"  hoelzl@41095  173  using finite I finite_nat_set_iff_bounded_le[of "nI"] by auto  hoelzl@41095  174  have "f \ Pi I (A k)"  hoelzl@41095  175  proof (intro Pi_I)  hoelzl@41095  176  fix i assume "i \ I"  hoelzl@41095  177  from mono[OF this, of "n i" k] k[OF this] n[OF this]  hoelzl@41095  178  show "f i \ A k i" by auto  hoelzl@41095  179  qed  hoelzl@41095  180  then show "f \ (\n. Pi I (A n))" by auto  hoelzl@41095  181 qed auto  hoelzl@41095  182 hoelzl@41095  183 lemma PiE_cong:  hoelzl@41095  184  assumes "\i. i\I \ A i = B i"  hoelzl@41095  185  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"  hoelzl@41095  186  using assms by (auto intro!: Pi_cong)  hoelzl@41095  187 hoelzl@41095  188 lemma restrict_upd[simp]:  hoelzl@41095  189  "i \ I \ (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"  hoelzl@41095  190  by (auto simp: fun_eq_iff)  hoelzl@41095  191 hoelzl@41689  192 lemma Pi_eq_subset:  hoelzl@41689  193  assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}"  hoelzl@41689  194  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \ I"  hoelzl@41689  195  shows "F i \ F' i"  hoelzl@41689  196 proof  hoelzl@41689  197  fix x assume "x \ F i"  hoelzl@41689  198  with ne have "\j. \y. ((j \ I \ y \ F j \ (i = j \ x = y)) \ (j \ I \ y = undefined))" by auto  hoelzl@41689  199  from choice[OF this] guess f .. note f = this  hoelzl@41689  200  then have "f \ Pi\<^isub>E I F" by (auto simp: extensional_def)  hoelzl@41689  201  then have "f \ Pi\<^isub>E I F'" using assms by simp  hoelzl@41689  202  then show "x \ F' i" using f i \ I by auto  hoelzl@41689  203 qed  hoelzl@41689  204 hoelzl@41689  205 lemma Pi_eq_iff_not_empty:  hoelzl@41689  206  assumes ne: "\i. i \ I \ F i \ {}" "\i. i \ I \ F' i \ {}"  hoelzl@41689  207  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \ (\i\I. F i = F' i)"  hoelzl@41689  208 proof (intro iffI ballI)  hoelzl@41689  209  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \ I"  hoelzl@41689  210  show "F i = F' i"  hoelzl@41689  211  using Pi_eq_subset[of I F F', OF ne eq i]  hoelzl@41689  212  using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]  hoelzl@41689  213  by auto  hoelzl@41689  214 qed auto  hoelzl@41689  215 hoelzl@41689  216 lemma Pi_eq_empty_iff:  hoelzl@41689  217  "Pi\<^isub>E I F = {} \ (\i\I. F i = {})"  hoelzl@41689  218 proof  hoelzl@41689  219  assume "Pi\<^isub>E I F = {}"  hoelzl@41689  220  show "\i\I. F i = {}"  hoelzl@41689  221  proof (rule ccontr)  hoelzl@41689  222  assume "\ ?thesis"  hoelzl@41689  223  then have "\i. \y. (i \ I \ y \ F i) \ (i \ I \ y = undefined)" by auto  hoelzl@41689  224  from choice[OF this] guess f ..  hoelzl@41689  225  then have "f \ Pi\<^isub>E I F" by (auto simp: extensional_def)  hoelzl@41689  226  with Pi\<^isub>E I F = {} show False by auto  hoelzl@41689  227  qed  hoelzl@41689  228 qed auto  hoelzl@41689  229 hoelzl@41689  230 lemma Pi_eq_iff:  hoelzl@41689  231  "Pi\<^isub>E I F = Pi\<^isub>E I F' \ (\i\I. F i = F' i) \ ((\i\I. F i = {}) \ (\i\I. F' i = {}))"  hoelzl@41689  232 proof (intro iffI disjCI)  hoelzl@41689  233  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"  hoelzl@41689  234  assume "\ ((\i\I. F i = {}) \ (\i\I. F' i = {}))"  hoelzl@41689  235  then have "(\i\I. F i \ {}) \ (\i\I. F' i \ {})"  hoelzl@41689  236  using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto  hoelzl@41689  237  with Pi_eq_iff_not_empty[of I F F'] show "\i\I. F i = F' i" by auto  hoelzl@41689  238 next  hoelzl@41689  239  assume "(\i\I. F i = F' i) \ (\i\I. F i = {}) \ (\i\I. F' i = {})"  hoelzl@41689  240  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"  hoelzl@41689  241  using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto  hoelzl@41689  242 qed  hoelzl@41689  243 hoelzl@40859  244 section "Binary products"  hoelzl@40859  245 hoelzl@40859  246 definition  hoelzl@41689  247  "pair_measure_generator A B =  hoelzl@41689  248  \ space = space A \ space B,  hoelzl@41689  249  sets = {a \ b | a b. a \ sets A \ b \ sets B},  hoelzl@41689  250  measure = \X. \\<^isup>+x. (\\<^isup>+y. indicator X (x,y) \B) \A \"  hoelzl@41689  251 hoelzl@41689  252 definition pair_measure (infixr "\\<^isub>M" 80) where  hoelzl@41689  253  "A \\<^isub>M B = sigma (pair_measure_generator A B)"  hoelzl@40859  254 hoelzl@40859  255 locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2  hoelzl@41689  256  for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"  hoelzl@41689  257 hoelzl@41689  258 abbreviation (in pair_sigma_algebra)  hoelzl@41689  259  "E \ pair_measure_generator M1 M2"  hoelzl@40859  260 hoelzl@40859  261 abbreviation (in pair_sigma_algebra)  hoelzl@41689  262  "P \ M1 \\<^isub>M M2"  hoelzl@40859  263 hoelzl@41689  264 lemma sigma_algebra_pair_measure:  hoelzl@41689  265  "sets M1 \ Pow (space M1) \ sets M2 \ Pow (space M2) \ sigma_algebra (pair_measure M1 M2)"  hoelzl@41689  266  by (force simp: pair_measure_def pair_measure_generator_def intro!: sigma_algebra_sigma)  hoelzl@40859  267 hoelzl@40859  268 sublocale pair_sigma_algebra \ sigma_algebra P  hoelzl@41689  269  using M1.space_closed M2.space_closed  hoelzl@41689  270  by (rule sigma_algebra_pair_measure)  hoelzl@40859  271 hoelzl@41689  272 lemma pair_measure_generatorI[intro, simp]:  hoelzl@41689  273  "x \ sets A \ y \ sets B \ x \ y \ sets (pair_measure_generator A B)"  hoelzl@41689  274  by (auto simp add: pair_measure_generator_def)  hoelzl@40859  275 hoelzl@41689  276 lemma pair_measureI[intro, simp]:  hoelzl@41689  277  "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^isub>M B)"  hoelzl@41689  278  by (auto simp add: pair_measure_def)  hoelzl@40859  279 hoelzl@41689  280 lemma space_pair_measure:  hoelzl@41689  281  "space (A \\<^isub>M B) = space A \ space B"  hoelzl@41689  282  by (simp add: pair_measure_def pair_measure_generator_def)  hoelzl@41095  283 hoelzl@41689  284 lemma sets_pair_measure_generator:  hoelzl@41689  285  "sets (pair_measure_generator N M) = (\(x, y). x \ y)  (sets N \ sets M)"  hoelzl@41689  286  unfolding pair_measure_generator_def by auto  hoelzl@41095  287 hoelzl@41689  288 lemma pair_measure_generator_sets_into_space:  hoelzl@41689  289  assumes "sets M \ Pow (space M)" "sets N \ Pow (space N)"  hoelzl@41689  290  shows "sets (pair_measure_generator M N) \ Pow (space (pair_measure_generator M N))"  hoelzl@41689  291  using assms by (auto simp: pair_measure_generator_def)  hoelzl@41689  292 hoelzl@41689  293 lemma pair_measure_generator_Int_snd:  hoelzl@40859  294  assumes "sets S1 \ Pow (space S1)"  hoelzl@41689  295  shows "sets (pair_measure_generator S1 (algebra.restricted_space S2 A)) =  hoelzl@41689  296  sets (algebra.restricted_space (pair_measure_generator S1 S2) (space S1 \ A))"  hoelzl@40859  297  (is "?L = ?R")  hoelzl@41689  298  apply (auto simp: pair_measure_generator_def image_iff)  hoelzl@41689  299  using assms  hoelzl@41689  300  apply (rule_tac x="a \ xa" in exI)  hoelzl@41689  301  apply force  hoelzl@41689  302  using assms  hoelzl@41689  303  apply (rule_tac x="a" in exI)  hoelzl@41689  304  apply (rule_tac x="b \ A" in exI)  hoelzl@41689  305  apply auto  hoelzl@41689  306  done  hoelzl@40859  307 hoelzl@40859  308 lemma (in pair_sigma_algebra)  hoelzl@40859  309  shows measurable_fst[intro!, simp]:  hoelzl@40859  310  "fst \ measurable P M1" (is ?fst)  hoelzl@40859  311  and measurable_snd[intro!, simp]:  hoelzl@40859  312  "snd \ measurable P M2" (is ?snd)  hoelzl@39088  313 proof -  hoelzl@39088  314  { fix X assume "X \ sets M1"  hoelzl@39088  315  then have "\X1\sets M1. \X2\sets M2. fst - X \ space M1 \ space M2 = X1 \ X2"  hoelzl@39088  316  apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])  hoelzl@39088  317  using M1.sets_into_space by force+ }  hoelzl@39088  318  moreover  hoelzl@39088  319  { fix X assume "X \ sets M2"  hoelzl@39088  320  then have "\X1\sets M1. \X2\sets M2. snd - X \ space M1 \ space M2 = X1 \ X2"  hoelzl@39088  321  apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])  hoelzl@39088  322  using M2.sets_into_space by force+ }  hoelzl@40859  323  ultimately have "?fst \ ?snd"  hoelzl@41689  324  by (fastsimp simp: measurable_def sets_sigma space_pair_measure  hoelzl@40859  325  intro!: sigma_sets.Basic)  hoelzl@40859  326  then show ?fst ?snd by auto  hoelzl@40859  327 qed  hoelzl@40859  328 hoelzl@41095  329 lemma (in pair_sigma_algebra) measurable_pair_iff:  hoelzl@40859  330  assumes "sigma_algebra M"  hoelzl@40859  331  shows "f \ measurable M P \  hoelzl@40859  332  (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2"  hoelzl@40859  333 proof -  hoelzl@40859  334  interpret M: sigma_algebra M by fact  hoelzl@40859  335  from assms show ?thesis  hoelzl@40859  336  proof (safe intro!: measurable_comp[where b=P])  hoelzl@40859  337  assume f: "(fst \ f) \ measurable M M1" and s: "(snd \ f) \ measurable M M2"  hoelzl@41689  338  show "f \ measurable M P" unfolding pair_measure_def  hoelzl@40859  339  proof (rule M.measurable_sigma)  hoelzl@41689  340  show "sets (pair_measure_generator M1 M2) \ Pow (space E)"  hoelzl@41689  341  unfolding pair_measure_generator_def using M1.sets_into_space M2.sets_into_space by auto  hoelzl@40859  342  show "f \ space M \ space E"  hoelzl@41689  343  using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma pair_measure_generator_def)  hoelzl@40859  344  fix A assume "A \ sets E"  hoelzl@40859  345  then obtain B C where "B \ sets M1" "C \ sets M2" "A = B \ C"  hoelzl@41689  346  unfolding pair_measure_generator_def by auto  hoelzl@40859  347  moreover have "(fst \ f) - B \ space M \ sets M"  hoelzl@40859  348  using f B \ sets M1 unfolding measurable_def by auto  hoelzl@40859  349  moreover have "(snd \ f) - C \ space M \ sets M"  hoelzl@40859  350  using s C \ sets M2 unfolding measurable_def by auto  hoelzl@40859  351  moreover have "f - A \ space M = ((fst \ f) - B \ space M) \ ((snd \ f) - C \ space M)"  hoelzl@40859  352  unfolding A = B \ C by (auto simp: vimage_Times)  hoelzl@40859  353  ultimately show "f - A \ space M \ sets M" by auto  hoelzl@40859  354  qed  hoelzl@40859  355  qed  hoelzl@40859  356 qed  hoelzl@40859  357 hoelzl@41095  358 lemma (in pair_sigma_algebra) measurable_pair:  hoelzl@40859  359  assumes "sigma_algebra M"  hoelzl@41095  360  assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2"  hoelzl@40859  361  shows "f \ measurable M P"  hoelzl@41095  362  unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp  hoelzl@40859  363 hoelzl@41689  364 lemma pair_measure_generatorE:  hoelzl@41689  365  assumes "X \ sets (pair_measure_generator M1 M2)"  hoelzl@40859  366  obtains A B where "X = A \ B" "A \ sets M1" "B \ sets M2"  hoelzl@41689  367  using assms unfolding pair_measure_generator_def by auto  hoelzl@40859  368 hoelzl@41689  369 lemma (in pair_sigma_algebra) pair_measure_generator_swap:  hoelzl@41689  370  "(\X. (\(x,y). (y,x)) - X \ space M2 \ space M1)  sets E = sets (pair_measure_generator M2 M1)"  hoelzl@41689  371 proof (safe elim!: pair_measure_generatorE)  hoelzl@40859  372  fix A B assume "A \ sets M1" "B \ sets M2"  hoelzl@40859  373  moreover then have "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 = B \ A"  hoelzl@40859  374  using M1.sets_into_space M2.sets_into_space by auto  hoelzl@41689  375  ultimately show "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 \ sets (pair_measure_generator M2 M1)"  hoelzl@41689  376  by (auto intro: pair_measure_generatorI)  hoelzl@40859  377 next  hoelzl@40859  378  fix A B assume "A \ sets M1" "B \ sets M2"  hoelzl@40859  379  then show "B \ A \ (\X. (\(x, y). (y, x)) - X \ space M2 \ space M1)  sets E"  hoelzl@40859  380  using M1.sets_into_space M2.sets_into_space  hoelzl@41689  381  by (auto intro!: image_eqI[where x="A \ B"] pair_measure_generatorI)  hoelzl@40859  382 qed  hoelzl@40859  383 hoelzl@40859  384 lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap:  hoelzl@40859  385  assumes Q: "Q \ sets P"  hoelzl@41689  386  shows "(\(x,y). (y, x)) - Q \ sets (M2 \\<^isub>M M1)" (is "_ \ sets ?Q")  hoelzl@40859  387 proof -  hoelzl@41689  388  let "?f Q" = "(\(x,y). (y, x)) - Q \ space M2 \ space M1"  hoelzl@41689  389  have *: "(\(x,y). (y, x)) - Q = ?f Q"  hoelzl@41689  390  using sets_into_space[OF Q] by (auto simp: space_pair_measure)  hoelzl@41689  391  have "sets (M2 \\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))"  hoelzl@41689  392  unfolding pair_measure_def ..  hoelzl@41689  393  also have "\ = sigma_sets (space M2 \ space M1) (?f  sets E)"  hoelzl@41689  394  unfolding sigma_def pair_measure_generator_swap[symmetric]  hoelzl@41689  395  by (simp add: pair_measure_generator_def)  hoelzl@41689  396  also have "\ = ?f  sigma_sets (space M1 \ space M2) (sets E)"  hoelzl@41689  397  using M1.sets_into_space M2.sets_into_space  hoelzl@41689  398  by (intro sigma_sets_vimage) (auto simp: pair_measure_generator_def)  hoelzl@41689  399  also have "\ = ?f  sets P"  hoelzl@41689  400  unfolding pair_measure_def pair_measure_generator_def sigma_def by simp  hoelzl@41689  401  finally show ?thesis  hoelzl@41689  402  using Q by (subst *) auto  hoelzl@40859  403 qed  hoelzl@40859  404 hoelzl@40859  405 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable:  hoelzl@41689  406  shows "(\(x,y). (y, x)) \ measurable P (M2 \\<^isub>M M1)"  hoelzl@40859  407  (is "?f \ measurable ?P ?Q")  hoelzl@40859  408  unfolding measurable_def  hoelzl@40859  409 proof (intro CollectI conjI Pi_I ballI)  hoelzl@40859  410  fix x assume "x \ space ?P" then show "(case x of (x, y) \ (y, x)) \ space ?Q"  hoelzl@41689  411  unfolding pair_measure_generator_def pair_measure_def by auto  hoelzl@40859  412 next  hoelzl@41689  413  fix A assume "A \ sets (M2 \\<^isub>M M1)"  hoelzl@40859  414  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@41689  415  with Q.sets_pair_sigma_algebra_swap[OF A \ sets (M2 \\<^isub>M M1)]  hoelzl@40859  416  show "?f - A \ space ?P \ sets ?P" by simp  hoelzl@40859  417 qed  hoelzl@40859  418 hoelzl@41981  419 lemma (in pair_sigma_algebra) measurable_cut_fst[simp,intro]:  hoelzl@40859  420  assumes "Q \ sets P" shows "Pair x - Q \ sets M2"  hoelzl@40859  421 proof -  hoelzl@40859  422  let ?Q' = "{Q. Q \ space P \ Pair x - Q \ sets M2}"  hoelzl@40859  423  let ?Q = "\ space = space P, sets = ?Q' \"  hoelzl@40859  424  interpret Q: sigma_algebra ?Q  hoelzl@41689  425  proof qed (auto simp: vimage_UN vimage_Diff space_pair_measure)  hoelzl@40859  426  have "sets E \ sets ?Q"  hoelzl@40859  427  using M1.sets_into_space M2.sets_into_space  hoelzl@41689  428  by (auto simp: pair_measure_generator_def space_pair_measure)  hoelzl@40859  429  then have "sets P \ sets ?Q"  hoelzl@41689  430  apply (subst pair_measure_def, intro Q.sets_sigma_subset)  hoelzl@41689  431  by (simp add: pair_measure_def)  hoelzl@40859  432  with assms show ?thesis by auto  hoelzl@40859  433 qed  hoelzl@40859  434 hoelzl@40859  435 lemma (in pair_sigma_algebra) measurable_cut_snd:  hoelzl@40859  436  assumes Q: "Q \ sets P" shows "(\x. (x, y)) - Q \ sets M1" (is "?cut Q \ sets M1")  hoelzl@40859  437 proof -  hoelzl@40859  438  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  439  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]  hoelzl@41689  440  show ?thesis by (simp add: vimage_compose[symmetric] comp_def)  hoelzl@40859  441 qed  hoelzl@40859  442 hoelzl@40859  443 lemma (in pair_sigma_algebra) measurable_pair_image_snd:  hoelzl@40859  444  assumes m: "f \ measurable P M" and "x \ space M1"  hoelzl@40859  445  shows "(\y. f (x, y)) \ measurable M2 M"  hoelzl@40859  446  unfolding measurable_def  hoelzl@40859  447 proof (intro CollectI conjI Pi_I ballI)  hoelzl@40859  448  fix y assume "y \ space M2" with f \ measurable P M x \ space M1  hoelzl@41689  449  show "f (x, y) \ space M"  hoelzl@41689  450  unfolding measurable_def pair_measure_generator_def pair_measure_def by auto  hoelzl@40859  451 next  hoelzl@40859  452  fix A assume "A \ sets M"  hoelzl@40859  453  then have "Pair x - (f - A \ space P) \ sets M2" (is "?C \ _")  hoelzl@40859  454  using f \ measurable P M  hoelzl@40859  455  by (intro measurable_cut_fst) (auto simp: measurable_def)  hoelzl@40859  456  also have "?C = (\y. f (x, y)) - A \ space M2"  hoelzl@41689  457  using x \ space M1 by (auto simp: pair_measure_generator_def pair_measure_def)  hoelzl@40859  458  finally show "(\y. f (x, y)) - A \ space M2 \ sets M2" .  hoelzl@40859  459 qed  hoelzl@40859  460 hoelzl@40859  461 lemma (in pair_sigma_algebra) measurable_pair_image_fst:  hoelzl@40859  462  assumes m: "f \ measurable P M" and "y \ space M2"  hoelzl@40859  463  shows "(\x. f (x, y)) \ measurable M1 M"  hoelzl@40859  464 proof -  hoelzl@40859  465  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  466  from Q.measurable_pair_image_snd[OF measurable_comp y \ space M2,  hoelzl@40859  467  OF Q.pair_sigma_algebra_swap_measurable m]  hoelzl@40859  468  show ?thesis by simp  hoelzl@40859  469 qed  hoelzl@40859  470 hoelzl@41689  471 lemma (in pair_sigma_algebra) Int_stable_pair_measure_generator: "Int_stable E"  hoelzl@40859  472  unfolding Int_stable_def  hoelzl@40859  473 proof (intro ballI)  hoelzl@40859  474  fix A B assume "A \ sets E" "B \ sets E"  hoelzl@40859  475  then obtain A1 A2 B1 B2 where "A = A1 \ A2" "B = B1 \ B2"  hoelzl@40859  476  "A1 \ sets M1" "A2 \ sets M2" "B1 \ sets M1" "B2 \ sets M2"  hoelzl@41689  477  unfolding pair_measure_generator_def by auto  hoelzl@40859  478  then show "A \ B \ sets E"  hoelzl@41689  479  by (auto simp add: times_Int_times pair_measure_generator_def)  hoelzl@40859  480 qed  hoelzl@40859  481 hoelzl@40859  482 lemma finite_measure_cut_measurable:  hoelzl@41689  483  fixes M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"  hoelzl@41689  484  assumes "sigma_finite_measure M1" "finite_measure M2"  hoelzl@41689  485  assumes "Q \ sets (M1 \\<^isub>M M2)"  hoelzl@41689  486  shows "(\x. measure M2 (Pair x - Q)) \ borel_measurable M1"  hoelzl@40859  487  (is "?s Q \ _")  hoelzl@40859  488 proof -  hoelzl@41689  489  interpret M1: sigma_finite_measure M1 by fact  hoelzl@41689  490  interpret M2: finite_measure M2 by fact  hoelzl@40859  491  interpret pair_sigma_algebra M1 M2 by default  hoelzl@40859  492  have [intro]: "sigma_algebra M1" by fact  hoelzl@40859  493  have [intro]: "sigma_algebra M2" by fact  hoelzl@40859  494  let ?D = "\ space = space P, sets = {A\sets P. ?s A \ borel_measurable M1} \"  hoelzl@41689  495  note space_pair_measure[simp]  hoelzl@40859  496  interpret dynkin_system ?D  hoelzl@40859  497  proof (intro dynkin_systemI)  hoelzl@40859  498  fix A assume "A \ sets ?D" then show "A \ space ?D"  hoelzl@40859  499  using sets_into_space by simp  hoelzl@40859  500  next  hoelzl@40859  501  from top show "space ?D \ sets ?D"  hoelzl@40859  502  by (auto simp add: if_distrib intro!: M1.measurable_If)  hoelzl@40859  503  next  hoelzl@40859  504  fix A assume "A \ sets ?D"  hoelzl@41689  505  with sets_into_space have "\x. measure M2 (Pair x - (space M1 \ space M2 - A)) =  hoelzl@41689  506  (if x \ space M1 then measure M2 (space M2) - ?s A x else 0)"  hoelzl@41981  507  by (auto intro!: M2.measure_compl simp: vimage_Diff)  hoelzl@40859  508  with A \ sets ?D top show "space ?D - A \ sets ?D"  hoelzl@41981  509  by (auto intro!: Diff M1.measurable_If M1.borel_measurable_extreal_diff)  hoelzl@40859  510  next  hoelzl@40859  511  fix F :: "nat \ ('a\'b) set" assume "disjoint_family F" "range F \ sets ?D"  hoelzl@41981  512  moreover then have "\x. measure M2 (\i. Pair x - F i) = (\i. ?s (F i) x)"  hoelzl@40859  513  by (intro M2.measure_countably_additive[symmetric])  hoelzl@41981  514  (auto simp: disjoint_family_on_def)  hoelzl@40859  515  ultimately show "(\i. F i) \ sets ?D"  hoelzl@40859  516  by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf)  hoelzl@40859  517  qed  hoelzl@41689  518  have "sets P = sets ?D" apply (subst pair_measure_def)  hoelzl@40859  519  proof (intro dynkin_lemma)  hoelzl@41689  520  show "Int_stable E" by (rule Int_stable_pair_measure_generator)  hoelzl@40859  521  from M1.sets_into_space have "\A. A \ sets M1 \ {x \ space M1. x \ A} = A"  hoelzl@40859  522  by auto  hoelzl@40859  523  then show "sets E \ sets ?D"  hoelzl@41689  524  by (auto simp: pair_measure_generator_def sets_sigma if_distrib  hoelzl@40859  525  intro: sigma_sets.Basic intro!: M1.measurable_If)  hoelzl@41689  526  qed (auto simp: pair_measure_def)  hoelzl@40859  527  with Q \ sets P have "Q \ sets ?D" by simp  hoelzl@40859  528  then show "?s Q \ borel_measurable M1" by simp  hoelzl@40859  529 qed  hoelzl@40859  530 hoelzl@40859  531 subsection {* Binary products of \sigma-finite measure spaces *}  hoelzl@40859  532 hoelzl@41689  533 locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2  hoelzl@41689  534  for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"  hoelzl@40859  535 hoelzl@40859  536 sublocale pair_sigma_finite \ pair_sigma_algebra M1 M2  hoelzl@40859  537  by default  hoelzl@40859  538 hoelzl@41689  539 lemma times_eq_iff: "A \ B = C \ D \ A = C \ B = D \ ((A = {} \ B = {}) \ (C = {} \ D = {}))"  hoelzl@41689  540  by auto  hoelzl@41689  541 hoelzl@40859  542 lemma (in pair_sigma_finite) measure_cut_measurable_fst:  hoelzl@41689  543  assumes "Q \ sets P" shows "(\x. measure M2 (Pair x - Q)) \ borel_measurable M1" (is "?s Q \ _")  hoelzl@40859  544 proof -  hoelzl@40859  545  have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+  hoelzl@41689  546  have M1: "sigma_finite_measure M1" by default  hoelzl@40859  547  from M2.disjoint_sigma_finite guess F .. note F = this  hoelzl@41981  548  then have F_sets: "\i. F i \ sets M2" by auto  hoelzl@40859  549  let "?C x i" = "F i \ Pair x - Q"  hoelzl@40859  550  { fix i  hoelzl@40859  551  let ?R = "M2.restricted_space (F i)"  hoelzl@40859  552  have [simp]: "space M1 \ F i \ space M1 \ space M2 = space M1 \ F i"  hoelzl@40859  553  using F M2.sets_into_space by auto  hoelzl@41689  554  let ?R2 = "M2.restricted_space (F i)"  hoelzl@41689  555  have "(\x. measure ?R2 (Pair x - (space M1 \ space ?R2 \ Q))) \ borel_measurable M1"  hoelzl@40859  556  proof (intro finite_measure_cut_measurable[OF M1])  hoelzl@41689  557  show "finite_measure ?R2"  hoelzl@40859  558  using F by (intro M2.restricted_to_finite_measure) auto  hoelzl@41689  559  have "(space M1 \ space ?R2) \ Q \ (op \ (space M1 \ F i))  sets P"  hoelzl@41689  560  using Q \ sets P by (auto simp: image_iff)  hoelzl@41689  561  also have "\ = sigma_sets (space M1 \ F i) ((op \ (space M1 \ F i))  sets E)"  hoelzl@41689  562  unfolding pair_measure_def pair_measure_generator_def sigma_def  hoelzl@41689  563  using F i \ sets M2 M2.sets_into_space  hoelzl@41689  564  by (auto intro!: sigma_sets_Int sigma_sets.Basic)  hoelzl@41689  565  also have "\ \ sets (M1 \\<^isub>M ?R2)"  hoelzl@41689  566  using M1.sets_into_space  hoelzl@41689  567  apply (auto simp: times_Int_times pair_measure_def pair_measure_generator_def sigma_def  hoelzl@41689  568  intro!: sigma_sets_subseteq)  hoelzl@41689  569  apply (rule_tac x="a" in exI)  hoelzl@41689  570  apply (rule_tac x="b \ F i" in exI)  hoelzl@41689  571  by auto  hoelzl@41689  572  finally show "(space M1 \ space ?R2) \ Q \ sets (M1 \\<^isub>M ?R2)" .  hoelzl@40859  573  qed  hoelzl@40859  574  moreover have "\x. Pair x - (space M1 \ F i \ Q) = ?C x i"  hoelzl@41689  575  using Q \ sets P sets_into_space by (auto simp: space_pair_measure)  hoelzl@41689  576  ultimately have "(\x. measure M2 (?C x i)) \ borel_measurable M1"  hoelzl@40859  577  by simp }  hoelzl@40859  578  moreover  hoelzl@40859  579  { fix x  hoelzl@41981  580  have "(\i. measure M2 (?C x i)) = measure M2 (\i. ?C x i)"  hoelzl@40859  581  proof (intro M2.measure_countably_additive)  hoelzl@40859  582  show "range (?C x) \ sets M2"  hoelzl@41981  583  using F Q \ sets P by (auto intro!: M2.Int)  hoelzl@40859  584  have "disjoint_family F" using F by auto  hoelzl@40859  585  show "disjoint_family (?C x)"  hoelzl@40859  586  by (rule disjoint_family_on_bisimulation[OF disjoint_family F]) auto  hoelzl@40859  587  qed  hoelzl@40859  588  also have "(\i. ?C x i) = Pair x - Q"  hoelzl@40859  589  using F sets_into_space Q \ sets P  hoelzl@41689  590  by (auto simp: space_pair_measure)  hoelzl@41981  591  finally have "measure M2 (Pair x - Q) = (\i. measure M2 (?C x i))"  hoelzl@40859  592  by simp }  hoelzl@41981  593  ultimately show ?thesis using Q \ sets P F_sets  hoelzl@41981  594  by (auto intro!: M1.borel_measurable_psuminf M2.Int)  hoelzl@40859  595 qed  hoelzl@40859  596 hoelzl@40859  597 lemma (in pair_sigma_finite) measure_cut_measurable_snd:  hoelzl@41689  598  assumes "Q \ sets P" shows "(\y. M1.\ ((\x. (x, y)) - Q)) \ borel_measurable M2"  hoelzl@40859  599 proof -  hoelzl@41689  600  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@40859  601  note sets_pair_sigma_algebra_swap[OF assms]  hoelzl@40859  602  from Q.measure_cut_measurable_fst[OF this]  hoelzl@41689  603  show ?thesis by (simp add: vimage_compose[symmetric] comp_def)  hoelzl@40859  604 qed  hoelzl@40859  605 hoelzl@40859  606 lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable:  hoelzl@41689  607  assumes "f \ measurable P M" shows "(\(x,y). f (y, x)) \ measurable (M2 \\<^isub>M M1) M"  hoelzl@40859  608 proof -  hoelzl@40859  609  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@40859  610  have *: "(\(x,y). f (y, x)) = f \ (\(x,y). (y, x))" by (simp add: fun_eq_iff)  hoelzl@40859  611  show ?thesis  hoelzl@40859  612  using Q.pair_sigma_algebra_swap_measurable assms  hoelzl@40859  613  unfolding * by (rule measurable_comp)  hoelzl@39088  614 qed  hoelzl@39088  615 hoelzl@40859  616 lemma (in pair_sigma_finite) pair_measure_alt:  hoelzl@40859  617  assumes "A \ sets P"  hoelzl@41689  618  shows "measure (M1 \\<^isub>M M2) A = (\\<^isup>+ x. measure M2 (Pair x - A) \M1)"  hoelzl@41689  619  apply (simp add: pair_measure_def pair_measure_generator_def)  hoelzl@40859  620 proof (rule M1.positive_integral_cong)  hoelzl@40859  621  fix x assume "x \ space M1"  hoelzl@41981  622  have *: "\y. indicator A (x, y) = (indicator (Pair x - A) y :: extreal)"  hoelzl@40859  623  unfolding indicator_def by auto  hoelzl@41689  624  show "(\\<^isup>+ y. indicator A (x, y) \M2) = measure M2 (Pair x - A)"  hoelzl@40859  625  unfolding *  hoelzl@40859  626  apply (subst M2.positive_integral_indicator)  hoelzl@40859  627  apply (rule measurable_cut_fst[OF assms])  hoelzl@40859  628  by simp  hoelzl@40859  629 qed  hoelzl@40859  630 hoelzl@40859  631 lemma (in pair_sigma_finite) pair_measure_times:  hoelzl@40859  632  assumes A: "A \ sets M1" and "B \ sets M2"  hoelzl@41689  633  shows "measure (M1 \\<^isub>M M2) (A \ B) = M1.\ A * measure M2 B"  hoelzl@40859  634 proof -  hoelzl@41689  635  have "measure (M1 \\<^isub>M M2) (A \ B) = (\\<^isup>+ x. measure M2 B * indicator A x \M1)"  hoelzl@41689  636  using assms by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)  hoelzl@40859  637  with assms show ?thesis  hoelzl@40859  638  by (simp add: M1.positive_integral_cmult_indicator ac_simps)  hoelzl@40859  639 qed  hoelzl@40859  640 hoelzl@41981  641 lemma (in measure_space) measure_not_negative[simp,intro]:  hoelzl@41981  642  assumes A: "A \ sets M" shows "\ A \ - \"  hoelzl@41981  643  using positive_measure[OF A] by auto  hoelzl@41981  644 hoelzl@41689  645 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator:  hoelzl@41981  646  "\F::nat \ ('a \ 'b) set. range F \ sets E \ incseq F \ (\i. F i) = space E \  hoelzl@41981  647  (\i. measure (M1 \\<^isub>M M2) (F i) \$$"  hoelzl@40859  648 proof -  hoelzl@40859  649  obtain F1 :: "nat \ 'a set" and F2 :: "nat \ 'b set" where  hoelzl@41981  650  F1: "range F1 \ sets M1" "incseq F1" "(\i. F1 i) = space M1" "\i. M1.\ (F1 i) \ \" and  hoelzl@41981  651  F2: "range F2 \ sets M2" "incseq F2" "(\i. F2 i) = space M2" "\i. M2.\ (F2 i) \ \"  hoelzl@40859  652  using M1.sigma_finite_up M2.sigma_finite_up by auto  hoelzl@41981  653  then have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)" by auto  hoelzl@40859  654  let ?F = "\i. F1 i \ F2 i"  hoelzl@41981  655  show ?thesis unfolding space_pair_measure  hoelzl@40859  656  proof (intro exI[of _ ?F] conjI allI)  hoelzl@40859  657  show "range ?F \ sets E" using F1 F2  hoelzl@41689  658  by (fastsimp intro!: pair_measure_generatorI)  hoelzl@40859  659  next  hoelzl@40859  660  have "space M1 \ space M2 \ (\i. ?F i)"  hoelzl@40859  661  proof (intro subsetI)  hoelzl@40859  662  fix x assume "x \ space M1 \ space M2"  hoelzl@40859  663  then obtain i j where "fst x \ F1 i" "snd x \ F2 j"  hoelzl@40859  664  by (auto simp: space)  hoelzl@40859  665  then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)"  hoelzl@41981  666  using incseq F1 incseq F2 unfolding incseq_def  hoelzl@41981  667  by (force split: split_max)+  hoelzl@40859  668  then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)"  hoelzl@40859  669  by (intro SigmaI) (auto simp add: min_max.sup_commute)  hoelzl@40859  670  then show "x \ (\i. ?F i)" by auto  hoelzl@40859  671  qed  hoelzl@41689  672  then show "(\i. ?F i) = space E"  hoelzl@41689  673  using space by (auto simp: space pair_measure_generator_def)  hoelzl@40859  674  next  hoelzl@41981  675  fix i show "incseq (\i. F1 i \ F2 i)"  hoelzl@41981  676  using incseq F1 incseq F2 unfolding incseq_Suc_iff by auto  hoelzl@40859  677  next  hoelzl@40859  678  fix i  hoelzl@40859  679  from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto  hoelzl@41981  680  with F1 F2 M1.positive_measure[OF this(1)] M2.positive_measure[OF this(2)]  hoelzl@41981  681  show "measure P (F1 i \ F2 i) \ \"  hoelzl@40859  682  by (simp add: pair_measure_times)  hoelzl@40859  683  qed  hoelzl@40859  684 qed  hoelzl@40859  685 hoelzl@41689  686 sublocale pair_sigma_finite \ sigma_finite_measure P  hoelzl@40859  687 proof  hoelzl@41981  688  show "positive P (measure P)"  hoelzl@41981  689  unfolding pair_measure_def pair_measure_generator_def sigma_def positive_def  hoelzl@41981  690  by (auto intro: M1.positive_integral_positive M2.positive_integral_positive)  hoelzl@40859  691 hoelzl@41689  692  show "countably_additive P (measure P)"  hoelzl@40859  693  unfolding countably_additive_def  hoelzl@40859  694  proof (intro allI impI)  hoelzl@40859  695  fix F :: "nat \ ('a \ 'b) set"  hoelzl@40859  696  assume F: "range F \ sets P" "disjoint_family F"  hoelzl@40859  697  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  hoelzl@41689  698  moreover from F have "\i. (\x. measure M2 (Pair x - F i)) \ borel_measurable M1"  hoelzl@40859  699  by (intro measure_cut_measurable_fst) auto  hoelzl@40859  700  moreover have "\x. disjoint_family (\i. Pair x - F i)"  hoelzl@40859  701  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  hoelzl@40859  702  moreover have "\x. x \ space M1 \ range (\i. Pair x - F i) \ sets M2"  hoelzl@41981  703  using F by auto  hoelzl@41981  704  ultimately show "(\n. measure P (F n)) = measure P (\i. F i)"  hoelzl@41981  705  by (simp add: pair_measure_alt vimage_UN M1.positive_integral_suminf[symmetric]  hoelzl@40859  706  M2.measure_countably_additive  hoelzl@40859  707  cong: M1.positive_integral_cong)  hoelzl@40859  708  qed  hoelzl@40859  709 hoelzl@41689  710  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this  hoelzl@41981  711  show "\F::nat \ ('a \ 'b) set. range F \ sets P \ (\i. F i) = space P \ (\i. measure P (F i) \ \)"  hoelzl@40859  712  proof (rule exI[of _ F], intro conjI)  hoelzl@41689  713  show "range F \ sets P" using F by (auto simp: pair_measure_def)  hoelzl@40859  714  show "(\i. F i) = space P"  hoelzl@41981  715  using F by (auto simp: pair_measure_def pair_measure_generator_def)  hoelzl@41981  716  show "\i. measure P (F i) \ \" using F by auto  hoelzl@40859  717  qed  hoelzl@40859  718 qed  hoelzl@39088  719 hoelzl@41661  720 lemma (in pair_sigma_algebra) sets_swap:  hoelzl@41661  721  assumes "A \ sets P"  hoelzl@41689  722  shows "($$x, y). (y, x)) - A \ space (M2 \\<^isub>M M1) \ sets (M2 \\<^isub>M M1)"  hoelzl@41661  723  (is "_ - A \ space ?Q \ sets ?Q")  hoelzl@41661  724 proof -  hoelzl@41689  725  have *: "(\(x, y). (y, x)) - A \ space ?Q = (\(x, y). (y, x)) - A"  hoelzl@41689  726  using A \ sets P sets_into_space by (auto simp: space_pair_measure)  hoelzl@41661  727  show ?thesis  hoelzl@41661  728  unfolding * using assms by (rule sets_pair_sigma_algebra_swap)  hoelzl@41661  729 qed  hoelzl@41661  730 hoelzl@40859  731 lemma (in pair_sigma_finite) pair_measure_alt2:  hoelzl@41706  732  assumes A: "A \ sets P"  hoelzl@41689  733  shows "\ A = (\\<^isup>+y. M1.\ ((\x. (x, y)) - A) \M2)"  hoelzl@40859  734  (is "_ = ?\ A")  hoelzl@40859  735 proof -  hoelzl@41706  736  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41689  737  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this  hoelzl@41689  738  have [simp]: "\m. \ space = space E, sets = sets (sigma E), measure = m \ = P\ measure := m \"  hoelzl@41689  739  unfolding pair_measure_def by simp  hoelzl@41706  740 hoelzl@41706  741  have "\ A = Q.\ ((\(y, x). (x, y)) - A \ space Q.P)"  hoelzl@41706  742  proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator])  hoelzl@41706  743  show "measure_space P" "measure_space Q.P" by default  hoelzl@41706  744  show "(\(y, x). (x, y)) \ measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable)  hoelzl@41706  745  show "sets (sigma E) = sets P" "space E = space P" "A \ sets (sigma E)"  hoelzl@41706  746  using assms unfolding pair_measure_def by auto  hoelzl@41981  747  show "range F \ sets E" "incseq F" "(\i. F i) = space E" "\i. \ (F i) \ \"  hoelzl@41689  748  using F A \ sets P by (auto simp: pair_measure_def)  hoelzl@40859  749  fix X assume "X \ sets E"  hoelzl@41706  750  then obtain A B where X[simp]: "X = A \ B" and AB: "A \ sets M1" "B \ sets M2"  hoelzl@41689  751  unfolding pair_measure_def pair_measure_generator_def by auto  hoelzl@41706  752  then have "(\(y, x). (x, y)) - X \ space Q.P = B \ A"  hoelzl@41706  753  using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure)  hoelzl@41706  754  then show "\ X = Q.\ ((\(y, x). (x, y)) - X \ space Q.P)"  hoelzl@41706  755  using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps)  hoelzl@41689  756  qed  hoelzl@41706  757  then show ?thesis  hoelzl@41706  758  using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]]  hoelzl@41706  759  by (auto simp add: Q.pair_measure_alt space_pair_measure  hoelzl@41706  760  intro!: M2.positive_integral_cong arg_cong[where f="M1.\"])  hoelzl@41689  761 qed  hoelzl@41689  762 hoelzl@41689  763 lemma pair_sigma_algebra_sigma:  hoelzl@41981  764  assumes 1: "incseq S1" "(\i. S1 i) = space E1" "range S1 \ sets E1" and E1: "sets E1 \ Pow (space E1)"  hoelzl@41981  765  assumes 2: "decseq S2" "(\i. S2 i) = space E2" "range S2 \ sets E2" and E2: "sets E2 \ Pow (space E2)"  hoelzl@41689  766  shows "sets (sigma (pair_measure_generator (sigma E1) (sigma E2))) = sets (sigma (pair_measure_generator E1 E2))"  hoelzl@41689  767  (is "sets ?S = sets ?E")  hoelzl@41689  768 proof -  hoelzl@41689  769  interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)  hoelzl@41689  770  interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)  hoelzl@41689  771  have P: "sets (pair_measure_generator E1 E2) \ Pow (space E1 \ space E2)"  hoelzl@41689  772  using E1 E2 by (auto simp add: pair_measure_generator_def)  hoelzl@41689  773  interpret E: sigma_algebra ?E unfolding pair_measure_generator_def  hoelzl@41689  774  using E1 E2 by (intro sigma_algebra_sigma) auto  hoelzl@41689  775  { fix A assume "A \ sets E1"  hoelzl@41689  776  then have "fst - A \ space ?E = A \ (\i. S2 i)"  hoelzl@41981  777  using E1 2 unfolding pair_measure_generator_def by auto  hoelzl@41689  778  also have "\ = (\i. A \ S2 i)" by auto  hoelzl@41689  779  also have "\ \ sets ?E" unfolding pair_measure_generator_def sets_sigma  hoelzl@41689  780  using 2 A \ sets E1  hoelzl@41689  781  by (intro sigma_sets.Union)  hoelzl@41981  782  (force simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@41689  783  finally have "fst - A \ space ?E \ sets ?E" . }  hoelzl@41689  784  moreover  hoelzl@41689  785  { fix B assume "B \ sets E2"  hoelzl@41689  786  then have "snd - B \ space ?E = (\i. S1 i) \ B"  hoelzl@41981  787  using E2 1 unfolding pair_measure_generator_def by auto  hoelzl@41689  788  also have "\ = (\i. S1 i \ B)" by auto  hoelzl@41689  789  also have "\ \ sets ?E"  hoelzl@41689  790  using 1 B \ sets E2 unfolding pair_measure_generator_def sets_sigma  hoelzl@41689  791  by (intro sigma_sets.Union)  hoelzl@41981  792  (force simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@41689  793  finally have "snd - B \ space ?E \ sets ?E" . }  hoelzl@41689  794  ultimately have proj:  hoelzl@41689  795  "fst \ measurable ?E (sigma E1) \ snd \ measurable ?E (sigma E2)"  hoelzl@41689  796  using E1 E2 by (subst (1 2) E.measurable_iff_sigma)  hoelzl@41689  797  (auto simp: pair_measure_generator_def sets_sigma)  hoelzl@41689  798  { fix A B assume A: "A \ sets (sigma E1)" and B: "B \ sets (sigma E2)"  hoelzl@41689  799  with proj have "fst - A \ space ?E \ sets ?E" "snd - B \ space ?E \ sets ?E"  hoelzl@41689  800  unfolding measurable_def by simp_all  hoelzl@41689  801  moreover have "A \ B = (fst - A \ space ?E) \ (snd - B \ space ?E)"  hoelzl@41689  802  using A B M1.sets_into_space M2.sets_into_space  hoelzl@41689  803  by (auto simp: pair_measure_generator_def)  hoelzl@41689  804  ultimately have "A \ B \ sets ?E" by auto }  hoelzl@41689  805  then have "sigma_sets (space ?E) (sets (pair_measure_generator (sigma E1) (sigma E2))) \ sets ?E"  hoelzl@41689  806  by (intro E.sigma_sets_subset) (auto simp add: pair_measure_generator_def sets_sigma)  hoelzl@41689  807  then have subset: "sets ?S \ sets ?E"  hoelzl@41689  808  by (simp add: sets_sigma pair_measure_generator_def)  hoelzl@41689  809  show "sets ?S = sets ?E"  hoelzl@41689  810  proof (intro set_eqI iffI)  hoelzl@41689  811  fix A assume "A \ sets ?E" then show "A \ sets ?S"  hoelzl@41689  812  unfolding sets_sigma  hoelzl@41689  813  proof induct  hoelzl@41689  814  case (Basic A) then show ?case  hoelzl@41689  815  by (auto simp: pair_measure_generator_def sets_sigma intro: sigma_sets.Basic)  hoelzl@41689  816  qed (auto intro: sigma_sets.intros simp: pair_measure_generator_def)  hoelzl@41689  817  next  hoelzl@41689  818  fix A assume "A \ sets ?S" then show "A \ sets ?E" using subset by auto  hoelzl@41689  819  qed  hoelzl@40859  820 qed  hoelzl@40859  821 hoelzl@40859  822 section "Fubinis theorem"  hoelzl@40859  823 hoelzl@40859  824 lemma (in pair_sigma_finite) simple_function_cut:  hoelzl@41981  825  assumes f: "simple_function P f" "\x. 0 \ f x"  hoelzl@41689  826  shows "(\x. \\<^isup>+y. f (x, y) \M2) \ borel_measurable M1"  hoelzl@41689  827  and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P P f"  hoelzl@40859  828 proof -  hoelzl@40859  829  have f_borel: "f \ borel_measurable P"  hoelzl@41981  830  using f(1) by (rule borel_measurable_simple_function)  hoelzl@40859  831  let "?F z" = "f - {z} \ space P"  hoelzl@40859  832  let "?F' x z" = "Pair x - ?F z"  hoelzl@40859  833  { fix x assume "x \ space M1"  hoelzl@40859  834  have [simp]: "\z y. indicator (?F z) (x, y) = indicator (?F' x z) y"  hoelzl@40859  835  by (auto simp: indicator_def)  hoelzl@40859  836  have "\y. y \ space M2 \ (x, y) \ space P" using x \ space M1  hoelzl@41689  837  by (simp add: space_pair_measure)  hoelzl@40859  838  moreover have "\x z. ?F' x z \ sets M2" using f_borel  hoelzl@40859  839  by (intro borel_measurable_vimage measurable_cut_fst)  hoelzl@41689  840  ultimately have "simple_function M2 (\ y. f (x, y))"  hoelzl@40859  841  apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])  hoelzl@41981  842  apply (rule simple_function_indicator_representation[OF f(1)])  hoelzl@40859  843  using x \ space M1 by (auto simp del: space_sigma) }  hoelzl@40859  844  note M2_sf = this  hoelzl@40859  845  { fix x assume x: "x \ space M1"  hoelzl@41689  846  then have "(\\<^isup>+y. f (x, y) \M2) = (\z\f  space P. z * M2.\ (?F' x z))"  hoelzl@41981  847  unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)]  hoelzl@41689  848  unfolding simple_integral_def  hoelzl@40859  849  proof (safe intro!: setsum_mono_zero_cong_left)  hoelzl@41981  850  from f(1) show "finite (f  space P)" by (rule simple_functionD)  hoelzl@40859  851  next  hoelzl@40859  852  fix y assume "y \ space M2" then show "f (x, y) \ f  space P"  hoelzl@41689  853  using x \ space M1 by (auto simp: space_pair_measure)  hoelzl@40859  854  next  hoelzl@40859  855  fix x' y assume "(x', y) \ space P"  hoelzl@40859  856  "f (x', y) \ (\y. f (x, y))  space M2"  hoelzl@40859  857  then have *: "?F' x (f (x', y)) = {}"  hoelzl@41689  858  by (force simp: space_pair_measure)  hoelzl@41689  859  show "f (x', y) * M2.\ (?F' x (f (x', y))) = 0"  hoelzl@40859  860  unfolding * by simp  hoelzl@40859  861  qed (simp add: vimage_compose[symmetric] comp_def  hoelzl@41689  862  space_pair_measure) }  hoelzl@40859  863  note eq = this  hoelzl@40859  864  moreover have "\z. ?F z \ sets P"  hoelzl@40859  865  by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)  hoelzl@41689  866  moreover then have "\z. (\x. M2.\ (?F' x z)) \ borel_measurable M1"  hoelzl@40859  867  by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)  hoelzl@41981  868  moreover have *: "\i x. 0 \ M2.\ (Pair x - (f - {i} \ space P))"  hoelzl@41981  869  using f(1)[THEN simple_functionD(2)] f(2) by (intro M2.positive_measure measurable_cut_fst)  hoelzl@41981  870  moreover { fix i assume "i \ fspace P"  hoelzl@41981  871  with * have "\x. 0 \ i * M2.\ (Pair x - (f - {i} \ space P))"  hoelzl@41981  872  using f(2) by auto }  hoelzl@40859  873  ultimately  hoelzl@41689  874  show "(\x. \\<^isup>+y. f (x, y) \M2) \ borel_measurable M1"  hoelzl@41981  875  and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P P f" using f(2)  hoelzl@40859  876  by (auto simp del: vimage_Int cong: measurable_cong  hoelzl@41981  877  intro!: M1.borel_measurable_extreal_setsum setsum_cong  hoelzl@40859  878  simp add: M1.positive_integral_setsum simple_integral_def  hoelzl@40859  879  M1.positive_integral_cmult  hoelzl@40859  880  M1.positive_integral_cong[OF eq]  hoelzl@40859  881  positive_integral_eq_simple_integral[OF f]  hoelzl@40859  882  pair_measure_alt[symmetric])  hoelzl@40859  883 qed  hoelzl@40859  884 hoelzl@40859  885 lemma (in pair_sigma_finite) positive_integral_fst_measurable:  hoelzl@40859  886  assumes f: "f \ borel_measurable P"  hoelzl@41689  887  shows "(\x. \\<^isup>+ y. f (x, y) \M2) \ borel_measurable M1"  hoelzl@40859  888  (is "?C f \ borel_measurable M1")  hoelzl@41689  889  and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P P f"  hoelzl@40859  890 proof -  hoelzl@41981  891  from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this  hoelzl@40859  892  then have F_borel: "\i. F i \ borel_measurable P"  hoelzl@40859  893  by (auto intro: borel_measurable_simple_function)  hoelzl@41981  894  note sf = simple_function_cut[OF F(1,5)]  hoelzl@41097  895  then have "(\x. SUP i. ?C (F i) x) \ borel_measurable M1"  hoelzl@41097  896  using F(1) by auto  hoelzl@40859  897  moreover  hoelzl@40859  898  { fix x assume "x \ space M1"  hoelzl@41981  899  from F measurable_pair_image_snd[OF F_borelx \ space M1]  hoelzl@41981  900  have "(\\<^isup>+y. (SUP i. F i (x, y)) \M2) = (SUP i. ?C (F i) x)"  hoelzl@41981  901  by (intro M2.positive_integral_monotone_convergence_SUP)  hoelzl@41981  902  (auto simp: incseq_Suc_iff le_fun_def)  hoelzl@41981  903  then have "(SUP i. ?C (F i) x) = ?C f x"  hoelzl@41981  904  unfolding F(4) positive_integral_max_0 by simp }  hoelzl@40859  905  note SUPR_C = this  hoelzl@40859  906  ultimately show "?C f \ borel_measurable M1"  hoelzl@41097  907  by (simp cong: measurable_cong)  hoelzl@41689  908  have "(\\<^isup>+x. (SUP i. F i x) \P) = (SUP i. integral\<^isup>P P (F i))"  hoelzl@41981  909  using F_borel F  hoelzl@41981  910  by (intro positive_integral_monotone_convergence_SUP) auto  hoelzl@41689  911  also have "(SUP i. integral\<^isup>P P (F i)) = (SUP i. \\<^isup>+ x. (\\<^isup>+ y. F i (x, y) \M2) \M1)"  hoelzl@40859  912  unfolding sf(2) by simp  hoelzl@41981  913  also have "\ = \\<^isup>+ x. (SUP i. \\<^isup>+ y. F i (x, y) \M2) \M1" using F sf(1)  hoelzl@41981  914  by (intro M1.positive_integral_monotone_convergence_SUP[symmetric])  hoelzl@41981  915  (auto intro!: M2.positive_integral_mono M2.positive_integral_positive  hoelzl@41981  916  simp: incseq_Suc_iff le_fun_def)  hoelzl@41689  917  also have "\ = \\<^isup>+ x. (\\<^isup>+ y. (SUP i. F i (x, y)) \M2) \M1"  hoelzl@41981  918  using F_borel F(2,5)  hoelzl@41981  919  by (auto intro!: M1.positive_integral_cong M2.positive_integral_monotone_convergence_SUP[symmetric]  hoelzl@41981  920  simp: incseq_Suc_iff le_fun_def measurable_pair_image_snd)  hoelzl@41689  921  finally show "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P P f"  hoelzl@41981  922  using F by (simp add: positive_integral_max_0)  hoelzl@40859  923 qed  hoelzl@40859  924 hoelzl@41831  925 lemma (in pair_sigma_finite) measure_preserving_swap:  hoelzl@41831  926  "(\(x,y). (y, x)) \ measure_preserving (M1 \\<^isub>M M2) (M2 \\<^isub>M M1)"  hoelzl@41831  927 proof  hoelzl@41831  928  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41831  929  show *: "(\(x,y). (y, x)) \ measurable (M1 \\<^isub>M M2) (M2 \\<^isub>M M1)"  hoelzl@41831  930  using pair_sigma_algebra_swap_measurable .  hoelzl@41831  931  fix X assume "X \ sets (M2 \\<^isub>M M1)"  hoelzl@41831  932  from measurable_sets[OF * this] this Q.sets_into_space[OF this]  hoelzl@41831  933  show "measure (M1 \\<^isub>M M2) ((\(x, y). (y, x)) - X \ space P) = measure (M2 \\<^isub>M M1) X"  hoelzl@41831  934  by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\"]  hoelzl@41831  935  simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure)  hoelzl@41831  936 qed  hoelzl@41831  937 hoelzl@41661  938 lemma (in pair_sigma_finite) positive_integral_product_swap:  hoelzl@41661  939  assumes f: "f \ borel_measurable P"  hoelzl@41689  940  shows "(\\<^isup>+x. f (case x of (x,y)\(y,x)) \(M2 \\<^isub>M M1)) = integral\<^isup>P P f"  hoelzl@41661  941 proof -  hoelzl@41689  942  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41689  943  have "sigma_algebra P" by default  hoelzl@41831  944  with f show ?thesis  hoelzl@41831  945  by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto  hoelzl@41661  946 qed  hoelzl@41661  947 hoelzl@40859  948 lemma (in pair_sigma_finite) positive_integral_snd_measurable:  hoelzl@40859  949  assumes f: "f \ borel_measurable P"  hoelzl@41689  950  shows "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = integral\<^isup>P P f"  hoelzl@40859  951 proof -  hoelzl@41689  952  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@40859  953  note pair_sigma_algebra_measurable[OF f]  hoelzl@40859  954  from Q.positive_integral_fst_measurable[OF this]  hoelzl@41689  955  have "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = (\\<^isup>+ (x, y). f (y, x) \Q.P)"  hoelzl@40859  956  by simp  hoelzl@41689  957  also have "(\\<^isup>+ (x, y). f (y, x) \Q.P) = integral\<^isup>P P f"  hoelzl@41661  958  unfolding positive_integral_product_swap[OF f, symmetric]  hoelzl@41661  959  by (auto intro!: Q.positive_integral_cong)  hoelzl@40859  960  finally show ?thesis .  hoelzl@40859  961 qed  hoelzl@40859  962 hoelzl@40859  963 lemma (in pair_sigma_finite) Fubini:  hoelzl@40859  964  assumes f: "f \ borel_measurable P"  hoelzl@41689  965  shows "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = (\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1)"  hoelzl@40859  966  unfolding positive_integral_snd_measurable[OF assms]  hoelzl@40859  967  unfolding positive_integral_fst_measurable[OF assms] ..  hoelzl@40859  968 hoelzl@40859  969 lemma (in pair_sigma_finite) AE_pair:  hoelzl@41981  970  assumes "AE x in P. Q x"  hoelzl@41981  971  shows "AE x in M1. (AE y in M2. Q (x, y))"  hoelzl@40859  972 proof -  hoelzl@41689  973  obtain N where N: "N \ sets P" "\ N = 0" "{x\space P. \ Q x} \ N"  hoelzl@40859  974  using assms unfolding almost_everywhere_def by auto  hoelzl@40859  975  show ?thesis  hoelzl@40859  976  proof (rule M1.AE_I)  hoelzl@40859  977  from N measure_cut_measurable_fst[OF N \ sets P]  hoelzl@41689  978  show "M1.\ {x\space M1. M2.\ (Pair x - N) \ 0} = 0"  hoelzl@41981  979  by (auto simp: pair_measure_alt M1.positive_integral_0_iff)  hoelzl@41689  980  show "{x \ space M1. M2.\ (Pair x - N) \ 0} \ sets M1"  hoelzl@41981  981  by (intro M1.borel_measurable_extreal_neq_const measure_cut_measurable_fst N)  hoelzl@41689  982  { fix x assume "x \ space M1" "M2.\ (Pair x - N) = 0"  hoelzl@40859  983  have "M2.almost_everywhere (\y. Q (x, y))"  hoelzl@40859  984  proof (rule M2.AE_I)  hoelzl@41689  985  show "M2.\ (Pair x - N) = 0" by fact  hoelzl@40859  986  show "Pair x - N \ sets M2" by (intro measurable_cut_fst N)  hoelzl@40859  987  show "{y \ space M2. \ Q (x, y)} \ Pair x - N"  hoelzl@41689  988  using N x \ space M1 unfolding space_sigma space_pair_measure by auto  hoelzl@40859  989  qed }  hoelzl@41689  990  then show "{x \ space M1. \ M2.almost_everywhere (\y. Q (x, y))} \ {x \ space M1. M2.\ (Pair x - N) \ 0}"  hoelzl@40859  991  by auto  hoelzl@39088  992  qed  hoelzl@39088  993 qed  hoelzl@35833  994 hoelzl@41026  995 lemma (in pair_sigma_algebra) measurable_product_swap:  hoelzl@41689  996  "f \ measurable (M2 \\<^isub>M M1) M \ (\(x,y). f (y,x)) \ measurable P M"  hoelzl@41026  997 proof -  hoelzl@41026  998  interpret Q: pair_sigma_algebra M2 M1 by default  hoelzl@41026  999  show ?thesis  hoelzl@41026  1000  using pair_sigma_algebra_measurable[of "\(x,y). f (y, x)"]  hoelzl@41026  1001  by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI)  hoelzl@41026  1002 qed  hoelzl@41026  1003 hoelzl@41026  1004 lemma (in pair_sigma_finite) integrable_product_swap:  hoelzl@41689  1005  assumes "integrable P f"  hoelzl@41689  1006  shows "integrable (M2 \\<^isub>M M1) (\(x,y). f (y,x))"  hoelzl@41026  1007 proof -  hoelzl@41689  1008  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41661  1009  have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff)  hoelzl@41661  1010  show ?thesis unfolding *  hoelzl@41689  1011  using assms unfolding integrable_def  hoelzl@41661  1012  apply (subst (1 2) positive_integral_product_swap)  hoelzl@41689  1013  using integrable P f unfolding integrable_def  hoelzl@41661  1014  by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])  hoelzl@41661  1015 qed  hoelzl@41661  1016 hoelzl@41661  1017 lemma (in pair_sigma_finite) integrable_product_swap_iff:  hoelzl@41689  1018  "integrable (M2 \\<^isub>M M1) (\(x,y). f (y,x)) \ integrable P f"  hoelzl@41661  1019 proof -  hoelzl@41689  1020  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41661  1021  from Q.integrable_product_swap[of "\(x,y). f (y,x)"] integrable_product_swap[of f]  hoelzl@41661  1022  show ?thesis by auto  hoelzl@41026  1023 qed  hoelzl@41026  1024 hoelzl@41026  1025 lemma (in pair_sigma_finite) integral_product_swap:  hoelzl@41689  1026  assumes "integrable P f"  hoelzl@41689  1027  shows "(\(x,y). f (y,x) \(M2 \\<^isub>M M1)) = integral\<^isup>L P f"  hoelzl@41026  1028 proof -  hoelzl@41689  1029  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41661  1030  have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff)  hoelzl@41026  1031  show ?thesis  hoelzl@41689  1032  unfolding lebesgue_integral_def *  hoelzl@41661  1033  apply (subst (1 2) positive_integral_product_swap)  hoelzl@41689  1034  using integrable P f unfolding integrable_def  hoelzl@41661  1035  by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])  hoelzl@41026  1036 qed  hoelzl@41026  1037 hoelzl@41026  1038 lemma (in pair_sigma_finite) integrable_fst_measurable:  hoelzl@41689  1039  assumes f: "integrable P f"  hoelzl@41689  1040  shows "M1.almost_everywhere (\x. integrable M2 (\ y. f (x, y)))" (is "?AE")  hoelzl@41689  1041  and "(\x. (\y. f (x, y) \M2) \M1) = integral\<^isup>L P f" (is "?INT")  hoelzl@41026  1042 proof -  hoelzl@41981  1043  let "?pf x" = "extreal (f x)" and "?nf x" = "extreal (- f x)"  hoelzl@41026  1044  have  hoelzl@41026  1045  borel: "?nf \ borel_measurable P""?pf \ borel_measurable P" and  hoelzl@41981  1046  int: "integral\<^isup>P P ?nf \ \" "integral\<^isup>P P ?pf \ \"  hoelzl@41026  1047  using assms by auto  hoelzl@41981  1048  have "(\\<^isup>+x. (\\<^isup>+y. extreal (f (x, y)) \M2) \M1) \ \"  hoelzl@41981  1049  "(\\<^isup>+x. (\\<^isup>+y. extreal (- f (x, y)) \M2) \M1) \ \"  hoelzl@41026  1050  using borel[THEN positive_integral_fst_measurable(1)] int  hoelzl@41026  1051  unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all  hoelzl@41026  1052  with borel[THEN positive_integral_fst_measurable(1)]  hoelzl@41981  1053  have AE_pos: "AE x in M1. (\\<^isup>+y. extreal (f (x, y)) \M2) \ \"  hoelzl@41981  1054  "AE x in M1. (\\<^isup>+y. extreal (- f (x, y)) \M2) \ \"  hoelzl@41981  1055  by (auto intro!: M1.positive_integral_PInf_AE )  hoelzl@41981  1056  then have AE: "AE x in M1. \\\<^isup>+y. extreal (f (x, y)) \M2\ \ \"  hoelzl@41981  1057  "AE x in M1. \\\<^isup>+y. extreal (- f (x, y)) \M2\ \ \"  hoelzl@41981  1058  by (auto simp: M2.positive_integral_positive)  hoelzl@41981  1059  from AE_pos show ?AE using assms  hoelzl@41705  1060  by (simp add: measurable_pair_image_snd integrable_def)  hoelzl@41981  1061  { fix f have "(\\<^isup>+ x. - \\<^isup>+ y. extreal (f x y) \M2 \M1) = (\\<^isup>+x. 0 \M1)"  hoelzl@41981  1062  using M2.positive_integral_positive  hoelzl@41981  1063  by (intro M1.positive_integral_cong_pos) (auto simp: extreal_uminus_le_reorder)  hoelzl@41981  1064  then have "(\\<^isup>+ x. - \\<^isup>+ y. extreal (f x y) \M2 \M1) = 0" by simp }  hoelzl@41981  1065  note this[simp]  hoelzl@41981  1066  { fix f assume borel: "(\x. extreal (f x)) \ borel_measurable P"  hoelzl@41981  1067  and int: "integral\<^isup>P P (\x. extreal (f x)) \ \"  hoelzl@41981  1068  and AE: "M1.almost_everywhere (\x. (\\<^isup>+y. extreal (f (x, y)) \M2) \$$"  hoelzl@41981  1069  have "integrable M1 (\x. real (\\<^isup>+y. extreal (f (x, y)) \M2))" (is "integrable M1 ?f")  hoelzl@41705  1070  proof (intro integrable_def[THEN iffD2] conjI)  hoelzl@41705  1071  show "?f \ borel_measurable M1"  hoelzl@41981  1072  using borel by (auto intro!: M1.borel_measurable_real_of_extreal positive_integral_fst_measurable)  hoelzl@41981  1073  have "(\\<^isup>+x. extreal (?f x) \M1) = (\\<^isup>+x. (\\<^isup>+y. extreal (f (x, y)) \M2) \M1)"  hoelzl@41981  1074  using AE M2.positive_integral_positive  hoelzl@41981  1075  by (auto intro!: M1.positive_integral_cong_AE simp: extreal_real)  hoelzl@41981  1076  then show "(\\<^isup>+x. extreal (?f x) \M1) \ \"  hoelzl@41705  1077  using positive_integral_fst_measurable[OF borel] int by simp  hoelzl@41981  1078  have "(\\<^isup>+x. extreal (- ?f x) \M1) = (\\<^isup>+x. 0 \M1)"  hoelzl@41981  1079  by (intro M1.positive_integral_cong_pos)  hoelzl@41981  1080  (simp add: M2.positive_integral_positive real_of_extreal_pos)  hoelzl@41981  1081  then show "(\\<^isup>+x. extreal (- ?f x) \M1) \ \" by simp  hoelzl@41705  1082  qed }  hoelzl@41981  1083  with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)]  hoelzl@41705  1084  show ?INT  hoelzl@41689  1085  unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2]  hoelzl@41026  1086  borel[THEN positive_integral_fst_measurable(2), symmetric]  hoelzl@41981  1087  using AE[THEN M1.integral_real]  hoelzl@41981  1088  by simp  hoelzl@41026  1089 qed  hoelzl@41026  1090 hoelzl@41026  1091 lemma (in pair_sigma_finite) integrable_snd_measurable:  hoelzl@41689  1092  assumes f: "integrable P f"  hoelzl@41689  1093  shows "M2.almost_everywhere (\y. integrable M1 (\x. f (x, y)))" (is "?AE")  hoelzl@41689  1094  and "(\y. (\x. f (x, y) \M1) \M2) = integral\<^isup>L P f" (is "?INT")  hoelzl@41026  1095 proof -  hoelzl@41689  1096  interpret Q: pair_sigma_finite M2 M1 by default  hoelzl@41689  1097  have Q_int: "integrable Q.P ($$x, y). f (y, x))"  hoelzl@41661  1098  using f unfolding integrable_product_swap_iff .  hoelzl@41026  1099  show ?INT  hoelzl@41026  1100  using Q.integrable_fst_measurable(2)[OF Q_int]  hoelzl@41661  1101  using integral_product_swap[OF f] by simp  hoelzl@41026  1102  show ?AE  hoelzl@41026  1103  using Q.integrable_fst_measurable(1)[OF Q_int]  hoelzl@41026  1104  by simp  hoelzl@41026  1105 qed  hoelzl@41026  1106 hoelzl@41026  1107 lemma (in pair_sigma_finite) Fubini_integral:  hoelzl@41689  1108  assumes f: "integrable P f"  hoelzl@41689  1109  shows "(\y. (\x. f (x, y) \M1) \M2) = (\x. (\y. f (x, y) \M2) \M1)"  hoelzl@41026  1110  unfolding integrable_snd_measurable[OF assms]  hoelzl@41026  1111  unfolding integrable_fst_measurable[OF assms] ..  hoelzl@41026  1112 hoelzl@40859  1113 section "Finite product spaces"  hoelzl@40859  1114 hoelzl@40859  1115 section "Products"  hoelzl@40859  1116 hoelzl@40859  1117 locale product_sigma_algebra =  hoelzl@41689  1118  fixes M :: "'i \ ('a, 'b) measure_space_scheme"  hoelzl@40859  1119  assumes sigma_algebras: "\i. sigma_algebra (M i)"  hoelzl@40859  1120 hoelzl@41689  1121 locale finite_product_sigma_algebra = product_sigma_algebra M  hoelzl@41689  1122  for M :: "'i \ ('a, 'b) measure_space_scheme" +  hoelzl@40859  1123  fixes I :: "'i set"  hoelzl@40859  1124  assumes finite_index: "finite I"  hoelzl@40859  1125 hoelzl@41689  1126 definition  hoelzl@41689  1127  "product_algebra_generator I M = \ space = (\\<^isub>E i \ I. space (M i)),  hoelzl@41689  1128  sets = Pi\<^isub>E I  (\ i \ I. sets (M i)),  hoelzl@41689  1129  measure = \A. (\i\I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \"  hoelzl@41689  1130 hoelzl@41689  1131 definition product_algebra_def:  hoelzl@41689  1132  "Pi\<^isub>M I M = sigma (product_algebra_generator I M)  hoelzl@41689  1133  \ measure := (SOME \. sigma_finite_measure (sigma (product_algebra_generator I M) \ measure := \$$ \  hoelzl@41689  1134  (\A\\ i\I. sets (M i). \ (Pi\<^isub>E I A) = (\i\I. measure (M i) (A i))))\"  hoelzl@41689  1135 hoelzl@40859  1136 syntax  hoelzl@41689  1137  "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>  hoelzl@41689  1138  ('i => 'a, 'b) measure_space_scheme" ("(3PIM _:_./ _)" 10)  hoelzl@40859  1139 hoelzl@40859  1140 syntax (xsymbols)  hoelzl@41689  1141  "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>  hoelzl@41689  1142  ('i => 'a, 'b) measure_space_scheme" ("(3\\<^isub>M _\_./ _)" 10)  hoelzl@40859  1143 hoelzl@40859  1144 syntax (HTML output)  hoelzl@41689  1145  "_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] =>  hoelzl@41689  1146  ('i => 'a, 'b) measure_space_scheme" ("(3\\<^isub>M _\_./ _)" 10)  hoelzl@40859  1147 hoelzl@40859  1148 translations  hoelzl@41689  1149  "PIM x:I. M" == "CONST Pi\<^isub>M I (%x. M)"  hoelzl@40859  1150 hoelzl@41689  1151 abbreviation (in finite_product_sigma_algebra) "G \ product_algebra_generator I M"  hoelzl@41689  1152 abbreviation (in finite_product_sigma_algebra) "P \ Pi\<^isub>M I M"  hoelzl@40859  1153 hoelzl@40859  1154 sublocale product_sigma_algebra \ M: sigma_algebra "M i" for i by (rule sigma_algebras)  hoelzl@40859  1155 hoelzl@41689  1156 lemma sigma_into_space:  hoelzl@41689  1157  assumes "sets M \ Pow (space M)"  hoelzl@41689  1158  shows "sets (sigma M) \ Pow (space M)"  hoelzl@41689  1159  using sigma_sets_into_sp[OF assms] unfolding sigma_def by auto  hoelzl@41689  1160 hoelzl@41689  1161 lemma (in product_sigma_algebra) product_algebra_generator_into_space:  hoelzl@41689  1162  "sets (product_algebra_generator I M) \ Pow (space (product_algebra_generator I M))"  hoelzl@41689  1163  using M.sets_into_space unfolding product_algebra_generator_def  hoelzl@40859  1164  by auto blast  hoelzl@40859  1165 hoelzl@41689  1166 lemma (in product_sigma_algebra) product_algebra_into_space:  hoelzl@41689  1167  "sets (Pi\<^isub>M I M) \ Pow (space (Pi\<^isub>M I M))"  hoelzl@41689  1168  using product_algebra_generator_into_space  hoelzl@41689  1169  by (auto intro!: sigma_into_space simp add: product_algebra_def)  hoelzl@41689  1170 hoelzl@41689  1171 lemma (in product_sigma_algebra) sigma_algebra_product_algebra: "sigma_algebra (Pi\<^isub>M I M)"  hoelzl@41689  1172  using product_algebra_generator_into_space unfolding product_algebra_def  hoelzl@41689  1173  by (rule sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) simp_all  hoelzl@41689  1174 hoelzl@40859  1175 sublocale finite_product_sigma_algebra \ sigma_algebra P  hoelzl@41689  1176  using sigma_algebra_product_algebra .  hoelzl@40859  1177 hoelzl@41095  1178 lemma product_algebraE:  hoelzl@41689  1179  assumes "A \ sets (product_algebra_generator I M)"  hoelzl@41095  1180  obtains E where "A = Pi\<^isub>E I E" "E \ (\ i\I. sets (M i))"  hoelzl@41689  1181  using assms unfolding product_algebra_generator_def by auto  hoelzl@41095  1182 hoelzl@41689  1183 lemma product_algebra_generatorI[intro]:  hoelzl@41095  1184  assumes "E \ (\ i\I. sets (M i))"  hoelzl@41689  1185  shows "Pi\<^isub>E I E \ sets (product_algebra_generator I M)"  hoelzl@41689  1186  using assms unfolding product_algebra_generator_def by auto  hoelzl@41689  1187 hoelzl@41689  1188 lemma space_product_algebra_generator[simp]:  hoelzl@41689  1189  "space (product_algebra_generator I M) = Pi\<^isub>E I (\i. space (M i))"  hoelzl@41689  1190  unfolding product_algebra_generator_def by simp  hoelzl@41095  1191 hoelzl@40859  1192 lemma space_product_algebra[simp]:  hoelzl@41689  1193  "space (Pi\<^isub>M I M) = (\\<^isub>E i\I. space (M i))"  hoelzl@41689  1194  unfolding product_algebra_def product_algebra_generator_def by simp  hoelzl@40859  1195 hoelzl@41689  1196 lemma sets_product_algebra:  hoelzl@41689  1197  "sets (Pi\<^isub>M I M) = sets (sigma (product_algebra_generator I M))"  hoelzl@41689  1198  unfolding product_algebra_def sigma_def by simp  hoelzl@41689  1199 hoelzl@41689  1200 lemma product_algebra_generator_sets_into_space:  hoelzl@41095  1201  assumes "\i. i\I \ sets (M i) \ Pow (space (M i))"  hoelzl@41689  1202  shows "sets (product_algebra_generator I M) \ Pow (space (product_algebra_generator I M))"  hoelzl@41689  1203  using assms by (auto simp: product_algebra_generator_def) blast  hoelzl@40859  1204 hoelzl@40859  1205 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:  hoelzl@40859  1206  "\ \i. i \ I \ A i \ sets (M i) \ \ Pi\<^isub>E I A \ sets P"  hoelzl@41689  1207  by (auto simp: sets_product_algebra)  hoelzl@41026  1208 hoelzl@40859  1209 section "Generating set generates also product algebra"  hoelzl@40859  1210 hoelzl@40859  1211 lemma sigma_product_algebra_sigma_eq:  hoelzl@40859  1212  assumes "finite I"  hoelzl@41981  1213  assumes mono: "\i. i \ I \ incseq (S i)"  hoelzl@41981  1214  assumes union: "\i. i \ I \ (\j. S i j) = space (E i)"  hoelzl@40859  1215  assumes sets_into: "\i. i \ I \ range (S i) \ sets (E i)"  hoelzl@40859  1216  and E: "\i. sets (E i) \ Pow (space (E i))"  hoelzl@41689  1217  shows "sets (\\<^isub>M i\I. sigma (E i)) = sets (\\<^isub>M i\I. E i)"  hoelzl@41689  1218  (is "sets ?S = sets ?E")  hoelzl@40859  1219 proof cases  hoelzl@41689  1220  assume "I = {}" then show ?thesis  hoelzl@41689  1221  by (simp add: product_algebra_def product_algebra_generator_def)  hoelzl@40859  1222 next  hoelzl@40859  1223  assume "I \ {}"  hoelzl@40859  1224  interpret E: sigma_algebra "sigma (E i)" for i  hoelzl@40859  1225  using E by (rule sigma_algebra_sigma)  hoelzl@40859  1226  have into_space[intro]: "\i x A. A \ sets (E i) \ x i \ A \ x i \ space (E i)"  hoelzl@40859  1227  using E by auto  hoelzl@40859  1228  interpret G: sigma_algebra ?E  hoelzl@41689  1229  unfolding product_algebra_def product_algebra_generator_def using E  hoelzl@41689  1230  by (intro sigma_algebra.sigma_algebra_cong[OF sigma_algebra_sigma]) (auto dest: Pi_mem)  hoelzl@40859  1231  { fix A i assume "i \ I" and A: "A \ sets (E i)"  hoelzl@40859  1232  then have "(\x. x i) - A \ space ?E = (\\<^isub>E j\I. if j = i then A else \n. S j n) \ space ?E"  hoelzl@41981  1233  using mono union unfolding incseq_Suc_iff space_product_algebra  hoelzl@41689  1234  by (auto dest: Pi_mem)  hoelzl@40859  1235  also have "\ = (\n. (\\<^isub>E j\I. if j = i then A else S j n))"  hoelzl@41689  1236  unfolding space_product_algebra  hoelzl@40859  1237  apply simp  hoelzl@40859  1238  apply (subst Pi_UN[OF finite I])  hoelzl@41981  1239  using mono[THEN incseqD] apply simp  hoelzl@40859  1240  apply (simp add: PiE_Int)  hoelzl@40859  1241  apply (intro PiE_cong)  hoelzl@40859  1242  using A sets_into by (auto intro!: into_space)  hoelzl@41689  1243  also have "\ \ sets ?E"  hoelzl@40859  1244  using sets_into A \ sets (E i)  hoelzl@41689  1245  unfolding sets_product_algebra sets_sigma  hoelzl@40859  1246  by (intro sigma_sets.Union)  hoelzl@40859  1247  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  hoelzl@40859  1248  finally have "(\x. x i) - A \ space ?E \ sets ?E" . }  hoelzl@40859  1249  then have proj:  hoelzl@40859  1250  "\i. i\I \ (\x. x i) \ measurable ?E (sigma (E i))"  hoelzl@40859  1251  using E by (subst G.measurable_iff_sigma)  hoelzl@41689  1252  (auto simp: sets_product_algebra sets_sigma)  hoelzl@40859  1253  { fix A assume A: "\i. i \ I \ A i \ sets (sigma (E i))"  hoelzl@40859  1254  with proj have basic: "\i. i \ I \ (\x. x i) - (A i) \ space ?E \ sets ?E"  hoelzl@40859  1255  unfolding measurable_def by simp  hoelzl@40859  1256  have "Pi\<^isub>E I A = (\i\I. (\x. x i) - (A i) \ space ?E)"  hoelzl@40859  1257  using A E.sets_into_space I \ {} unfolding product_algebra_def by auto blast  hoelzl@40859  1258  then have "Pi\<^isub>E I A \ sets ?E"  hoelzl@40859  1259  using G.finite_INT[OF finite I I \ {} basic, of "\i. i"] by simp }  hoelzl@41689  1260  then have "sigma_sets (space ?E) (sets (product_algebra_generator I (\i. sigma (E i)))) \ sets ?E"  hoelzl@41689  1261  by (intro G.sigma_sets_subset) (auto simp add: product_algebra_generator_def)  hoelzl@40859  1262  then have subset: "sets ?S \ sets ?E"  hoelzl@41689  1263  by (simp add: sets_sigma sets_product_algebra)  hoelzl@41689  1264  show "sets ?S = sets ?E"  hoelzl@40859  1265  proof (intro set_eqI iffI)  hoelzl@40859  1266  fix A assume "A \ sets ?E" then show "A \ sets ?S"  hoelzl@41689  1267  unfolding sets_sigma sets_product_algebra  hoelzl@40859  1268  proof induct  hoelzl@40859  1269  case (Basic A) then show ?case  hoelzl@41689  1270  by (auto simp: sets_sigma product_algebra_generator_def intro: sigma_sets.Basic)  hoelzl@41689  1271  qed (auto intro: sigma_sets.intros simp: product_algebra_generator_def)  hoelzl@40859  1272  next  hoelzl@40859  1273  fix A assume "A \ sets ?S" then show "A \ sets ?E" using subset by auto  hoelzl@40859  1274  qed  hoelzl@41689  1275 qed  hoelzl@41689  1276 hoelzl@41689  1277 lemma product_algebraI[intro]:  hoelzl@41689  1278  "E \ (\ i\I. sets (M i)) \ Pi\<^isub>E I E \ sets (Pi\<^isub>M I M)"  hoelzl@41689  1279  using assms unfolding product_algebra_def by (auto intro: product_algebra_generatorI)  hoelzl@41689  1280 hoelzl@41689  1281 lemma (in product_sigma_algebra) measurable_component_update:  hoelzl@41689  1282  assumes "x \ space (Pi\<^isub>M I M)" and "i \ I"  hoelzl@41689  1283  shows "(\v. x(i := v)) \ measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \ _")  hoelzl@41689  1284  unfolding product_algebra_def apply simp  hoelzl@41689  1285 proof (intro measurable_sigma)  hoelzl@41689  1286  let ?G = "product_algebra_generator (insert i I) M"  hoelzl@41689  1287  show "sets ?G \ Pow (space ?G)" using product_algebra_generator_into_space .  hoelzl@41689  1288  show "?f \ space (M i) \ space ?G"  hoelzl@41689  1289  using M.sets_into_space assms by auto  hoelzl@41689  1290  fix A assume "A \ sets ?G"  hoelzl@41689  1291  from product_algebraE[OF this] guess E . note E = this  hoelzl@41689  1292  then have "?f - A \ space (M i) = E i \ ?f - A \ space (M i) = {}"  hoelzl@41689  1293  using M.sets_into_space assms by auto  hoelzl@41689  1294  then show "?f - A \ space (M i) \ sets (M i)"  hoelzl@41689  1295  using E by (auto intro!: product_algebraI)  hoelzl@40859  1296 qed  hoelzl@40859  1297 hoelzl@41689  1298 lemma (in product_sigma_algebra) measurable_add_dim:  hoelzl@41689  1299  assumes "i \ I"  hoelzl@41689  1300  shows "(\(f, y). f(i := y)) \ measurable (Pi\<^isub>M I M \\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"  hoelzl@41689  1301 proof -  hoelzl@41689  1302  let ?f = "(\(f, y). f(i := y))" and ?G = "product_algebra_generator (insert i I) M"  hoelzl@41689  1303  interpret Ii: pair_sigma_algebra "Pi\<^isub>M I M" "M i"  hoelzl@41689  1304  unfolding pair_sigma_algebra_def  hoelzl@41689  1305  by (intro sigma_algebra_product_algebra sigma_algebras conjI)  hoelzl@41689  1306  have "?f \ measurable Ii.P (sigma ?G)"  hoelzl@41689  1307  proof (rule Ii.measurable_sigma)  hoelzl@41689  1308  show "sets ?G \ Pow (space ?G)"  hoelzl@41689  1309  using product_algebra_generator_into_space .  hoelzl@41689  1310  show "?f \ space (Pi\<^isub>M I M \\<^isub>M M i) \ space ?G"  hoelzl@41689  1311  by (auto simp: space_pair_measure)  hoelzl@41689  1312  next  hoelzl@41689  1313  fix A assume "A \ sets ?G"  hoelzl@41689  1314  then obtain F where "A = Pi\<^isub>E (insert i I) F"  hoelzl@41689  1315  and F: "\j. j \ I \ F j \ sets (M j)" "F i \ sets (M i)"  hoelzl@41689  1316  by (auto elim!: product_algebraE)  hoelzl@41689  1317  then have "?f - A \ space (Pi\<^isub>M I M \\<^isub>M M i) = Pi\<^isub>E I F \ (F i)"  hoelzl@41689  1318  using sets_into_space i \ I  hoelzl@41689  1319  by (auto simp add: space_pair_measure) blast+  hoelzl@41689  1320  then show "?f - A \ space (Pi\<^isub>M I M \\<^isub>M M i) \ sets (Pi\<^isub>M I M \\<^isub>M M i)"  hoelzl@41689  1321  using F by (auto intro!: pair_measureI)  hoelzl@41689  1322  qed  hoelzl@41689  1323  then show ?thesis  hoelzl@41689  1324  by (simp add: product_algebra_def)  hoelzl@41689  1325 qed  hoelzl@41095  1326 hoelzl@41095  1327 lemma (in product_sigma_algebra) measurable_merge:  hoelzl@41095  1328  assumes [simp]: "I \ J = {}"  hoelzl@41689  1329  shows "(\(x, y). merge I x J y) \ measurable (Pi\<^isub>M I M \\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \ J) M)"  hoelzl@40859  1330 proof -  hoelzl@41689  1331  let ?I = "Pi\<^isub>M I M" and ?J = "Pi\<^isub>M J M"  hoelzl@41689  1332  interpret P: sigma_algebra "?I \\<^isub>M ?J"  hoelzl@41689  1333  by (intro sigma_algebra_pair_measure product_algebra_into_space)  hoelzl@41689  1334  let ?f = "\(x, y). merge I x J y"  hoelzl@41689  1335  let ?G = "product_algebra_generator (I \ J) M"  hoelzl@41689  1336  have "?f \ measurable (?I \\<^isub>M ?J) (sigma ?G)"  hoelzl@41689  1337  proof (rule P.measurable_sigma)  hoelzl@41689  1338  fix A assume "A \ sets ?G"  hoelzl@41689  1339  from product_algebraE[OF this]  hoelzl@41689  1340  obtain E where E: "A = Pi\<^isub>E (I \ J) E" "E \ (\ i\I \ J. sets (M i))" .  hoelzl@41689  1341  then have *: "?f - A \ space (?I \\<^isub>M ?J) = Pi\<^isub>E I E \ Pi\<^isub>E J E"  hoelzl@41689  1342  using sets_into_space I \ J = {}  hoelzl@41981  134