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