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