src/HOL/Analysis/Binary_Product_Measure.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69517 dc20f278e8f3 child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
 hoelzl@63627  1 (* Title: HOL/Analysis/Binary_Product_Measure.thy  hoelzl@42067  2  Author: Johannes Hölzl, TU München  hoelzl@42067  3 *)  hoelzl@42067  4 nipkow@69517  5 section%important \Binary Product Measure\  hoelzl@42067  6 hoelzl@42146  7 theory Binary_Product_Measure  hoelzl@56993  8 imports Nonnegative_Lebesgue_Integration  hoelzl@35833  9 begin  hoelzl@35833  10 ak2110@68833  11 lemma%unimportant Pair_vimage_times[simp]: "Pair x - (A \ B) = (if x \ A then B else {})"  hoelzl@40859  12  by auto  hoelzl@40859  13 ak2110@68833  14 lemma%unimportant rev_Pair_vimage_times[simp]: "(\x. (x, y)) - (A \ B) = (if y \ B then A else {})"  hoelzl@40859  15  by auto  hoelzl@40859  16 ak2110@68833  17 subsection%important "Binary products"  hoelzl@40859  18 ak2110@68833  19 definition%important pair_measure (infixr "\\<^sub>M" 80) where  wenzelm@53015  20  "A \\<^sub>M B = measure_of (space A \ space B)  hoelzl@47694  21  {a \ b | a b. a \ sets A \ b \ sets B}  wenzelm@53015  22  (\X. \\<^sup>+x. (\\<^sup>+y. indicator X (x,y) \B) \A)"  hoelzl@40859  23 ak2110@68833  24 lemma%important pair_measure_closed: "{a \ b | a b. a \ sets A \ b \ sets B} \ Pow (space A \ space B)"  ak2110@68833  25  using%unimportant sets.space_closed[of A] sets.space_closed[of B] by auto  hoelzl@49789  26 ak2110@68833  27 lemma%important space_pair_measure:  wenzelm@53015  28  "space (A \\<^sub>M B) = space A \ space B"  hoelzl@49789  29  unfolding pair_measure_def using pair_measure_closed[of A B]  ak2110@68833  30  by%unimportant (rule space_measure_of)  hoelzl@47694  31 ak2110@68833  32 lemma%unimportant SIGMA_Collect_eq: "(SIGMA x:space M. {y\space N. P x y}) = {x\space (M \\<^sub>M N). P (fst x) (snd x)}"  hoelzl@59000  33  by (auto simp: space_pair_measure)  hoelzl@59000  34 ak2110@68833  35 lemma%unimportant sets_pair_measure:  wenzelm@53015  36  "sets (A \\<^sub>M B) = sigma_sets (space A \ space B) {a \ b | a b. a \ sets A \ b \ sets B}"  hoelzl@49789  37  unfolding pair_measure_def using pair_measure_closed[of A B]  hoelzl@49789  38  by (rule sets_measure_of)  hoelzl@41095  39 ak2110@68833  40 lemma%unimportant sets_pair_measure_cong[measurable_cong, cong]:  wenzelm@53015  41  "sets M1 = sets M1' \ sets M2 = sets M2' \ sets (M1 \\<^sub>M M2) = sets (M1' \\<^sub>M M2')"  hoelzl@49776  42  unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)  hoelzl@49776  43 ak2110@68833  44 lemma%unimportant pair_measureI[intro, simp, measurable]:  wenzelm@53015  45  "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^sub>M B)"  hoelzl@47694  46  by (auto simp: sets_pair_measure)  hoelzl@41095  47 ak2110@68833  48 lemma%unimportant sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)"  hoelzl@58606  49  using pair_measureI[of "{x}" M1 "{y}" M2] by simp  hoelzl@58606  50 ak2110@68833  51 lemma%unimportant measurable_pair_measureI:  hoelzl@47694  52  assumes 1: "f \ space M \ space M1 \ space M2"  hoelzl@47694  53  assumes 2: "\A B. A \ sets M1 \ B \ sets M2 \ f - (A \ B) \ space M \ sets M"  wenzelm@53015  54  shows "f \ measurable M (M1 \\<^sub>M M2)"  hoelzl@47694  55  unfolding pair_measure_def using 1 2  immler@50244  56  by (intro measurable_measure_of) (auto dest: sets.sets_into_space)  hoelzl@41689  57 ak2110@68833  58 lemma%unimportant measurable_split_replace[measurable (raw)]:  haftmann@61424  59  "(\x. f x (fst (g x)) (snd (g x))) \ measurable M N \ (\x. case_prod (f x) (g x)) \ measurable M N"  hoelzl@50003  60  unfolding split_beta' .  hoelzl@50003  61 ak2110@68833  62 lemma%important measurable_Pair[measurable (raw)]:  hoelzl@49776  63  assumes f: "f \ measurable M M1" and g: "g \ measurable M M2"  wenzelm@53015  64  shows "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)"  ak2110@68833  65 proof%unimportant (rule measurable_pair_measureI)  hoelzl@49776  66  show "(\x. (f x, g x)) \ space M \ space M1 \ space M2"  hoelzl@49776  67  using f g by (auto simp: measurable_def)  hoelzl@49776  68  fix A B assume *: "A \ sets M1" "B \ sets M2"  hoelzl@49776  69  have "(\x. (f x, g x)) - (A \ B) \ space M = (f - A \ space M) \ (g - B \ space M)"  hoelzl@49776  70  by auto  hoelzl@49776  71  also have "\ \ sets M"  immler@50244  72  by (rule sets.Int) (auto intro!: measurable_sets * f g)  hoelzl@49776  73  finally show "(\x. (f x, g x)) - (A \ B) \ space M \ sets M" .  hoelzl@49776  74 qed  hoelzl@49776  75 ak2110@68833  76 lemma%unimportant measurable_fst[intro!, simp, measurable]: "fst \ measurable (M1 \\<^sub>M M2) M1"  immler@50244  77  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times  immler@50244  78  measurable_def)  hoelzl@40859  79 ak2110@68833  80 lemma%unimportant measurable_snd[intro!, simp, measurable]: "snd \ measurable (M1 \\<^sub>M M2) M2"  immler@50244  81  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times  immler@50244  82  measurable_def)  hoelzl@47694  83 ak2110@68833  84 lemma%unimportant measurable_Pair_compose_split[measurable_dest]:  haftmann@61424  85  assumes f: "case_prod f \ measurable (M1 \\<^sub>M M2) N"  hoelzl@59353  86  assumes g: "g \ measurable M M1" and h: "h \ measurable M M2"  hoelzl@59353  87  shows "(\x. f (g x) (h x)) \ measurable M N"  hoelzl@59353  88  using measurable_compose[OF measurable_Pair f, OF g h] by simp  hoelzl@59353  89 ak2110@68833  90 lemma%unimportant measurable_Pair1_compose[measurable_dest]:  hoelzl@59353  91  assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)"  hoelzl@59353  92  assumes [measurable]: "h \ measurable N M"  hoelzl@59353  93  shows "(\x. f (h x)) \ measurable N M1"  hoelzl@59353  94  using measurable_compose[OF f measurable_fst] by simp  hoelzl@59353  95 ak2110@68833  96 lemma%unimportant measurable_Pair2_compose[measurable_dest]:  hoelzl@59353  97  assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)"  hoelzl@59353  98  assumes [measurable]: "h \ measurable N M"  hoelzl@59353  99  shows "(\x. g (h x)) \ measurable N M2"  hoelzl@59353  100  using measurable_compose[OF f measurable_snd] by simp  hoelzl@59353  101 ak2110@68833  102 lemma%unimportant measurable_pair:  hoelzl@59353  103  assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2"  hoelzl@59353  104  shows "f \ measurable M (M1 \\<^sub>M M2)"  hoelzl@59353  105  using measurable_Pair[OF assms] by simp  hoelzl@59353  106 ak2110@68833  107 lemma%unimportant (*FIX ME needs a name *)  hoelzl@62975  108  assumes f[measurable]: "f \ measurable M (N \\<^sub>M P)"  hoelzl@50003  109  shows measurable_fst': "(\x. fst (f x)) \ measurable M N"  hoelzl@50003  110  and measurable_snd': "(\x. snd (f x)) \ measurable M P"  hoelzl@50003  111  by simp_all  hoelzl@40859  112 ak2110@68833  113 lemma%unimportant (*FIX ME needs a name *)  hoelzl@50003  114  assumes f[measurable]: "f \ measurable M N"  wenzelm@53015  115  shows measurable_fst'': "(\x. f (fst x)) \ measurable (M \\<^sub>M P) N"  wenzelm@53015  116  and measurable_snd'': "(\x. f (snd x)) \ measurable (P \\<^sub>M M) N"  hoelzl@50003  117  by simp_all  hoelzl@47694  118 ak2110@68833  119 lemma%unimportant sets_pair_in_sets:  hoelzl@63333  120  assumes "\a b. a \ sets A \ b \ sets B \ a \ b \ sets N"  hoelzl@63333  121  shows "sets (A \\<^sub>M B) \ sets N"  hoelzl@63333  122  unfolding sets_pair_measure  hoelzl@63333  123  by (intro sets.sigma_sets_subset') (auto intro!: assms)  hoelzl@63333  124 ak2110@68833  125 lemma%important sets_pair_eq_sets_fst_snd:  hoelzl@63333  126  "sets (A \\<^sub>M B) = sets (Sup {vimage_algebra (space A \ space B) fst A, vimage_algebra (space A \ space B) snd B})"  hoelzl@63333  127  (is "?P = sets (Sup {?fst, ?snd})")  ak2110@68833  128 proof%unimportant -  hoelzl@58606  129  { fix a b assume ab: "a \ sets A" "b \ sets B"  hoelzl@58606  130  then have "a \ b = (fst - a \ (space A \ space B)) \ (snd - b \ (space A \ space B))"  hoelzl@58606  131  by (auto dest: sets.sets_into_space)  hoelzl@63333  132  also have "\ \ sets (Sup {?fst, ?snd})"  hoelzl@63333  133  apply (rule sets.Int)  hoelzl@63333  134  apply (rule in_sets_Sup)  hoelzl@63333  135  apply auto []  hoelzl@63333  136  apply (rule insertI1)  hoelzl@63333  137  apply (auto intro: ab in_vimage_algebra) []  hoelzl@63333  138  apply (rule in_sets_Sup)  hoelzl@63333  139  apply auto []  hoelzl@63333  140  apply (rule insertI2)  hoelzl@63333  141  apply (auto intro: ab in_vimage_algebra)  hoelzl@63333  142  done  hoelzl@63333  143  finally have "a \ b \ sets (Sup {?fst, ?snd})" . }  hoelzl@58606  144  moreover have "sets ?fst \ sets (A \\<^sub>M B)"  hoelzl@58606  145  by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])  hoelzl@62975  146  moreover have "sets ?snd \ sets (A \\<^sub>M B)"  hoelzl@58606  147  by (rule sets_image_in_sets) (auto simp: space_pair_measure)  hoelzl@58606  148  ultimately show ?thesis  hoelzl@63333  149  apply (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets)  hoelzl@63333  150  apply simp  hoelzl@63333  151  apply simp  hoelzl@63333  152  apply simp  hoelzl@63333  153  apply (elim disjE)  hoelzl@63333  154  apply (simp add: space_pair_measure)  hoelzl@63333  155  apply (simp add: space_pair_measure)  hoelzl@63333  156  apply (auto simp add: space_pair_measure)  hoelzl@63333  157  done  hoelzl@58606  158 qed  hoelzl@58606  159 ak2110@68833  160 lemma%unimportant measurable_pair_iff:  wenzelm@53015  161  "f \ measurable M (M1 \\<^sub>M M2) \ (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2"  hoelzl@62975  162  by (auto intro: measurable_pair[of f M M1 M2])  hoelzl@40859  163 ak2110@68833  164 lemma%unimportant measurable_split_conv:  hoelzl@49776  165  "($$x, y). f x y) \ measurable A B \ (\x. f (fst x) (snd x)) \ measurable A B"  nipkow@67399  166  by (intro arg_cong2[where f="($$"]) auto  hoelzl@40859  167 ak2110@68833  168 lemma%unimportant measurable_pair_swap': "($$x,y). (y, x)) \ measurable (M1 \\<^sub>M M2) (M2 \\<^sub>M M1)"  hoelzl@49776  169  by (auto intro!: measurable_Pair simp: measurable_split_conv)  hoelzl@47694  170 ak2110@68833  171 lemma%unimportant measurable_pair_swap:  wenzelm@53015  172  assumes f: "f \ measurable (M1 \\<^sub>M M2) M" shows "(\(x,y). f (y, x)) \ measurable (M2 \\<^sub>M M1) M"  hoelzl@49776  173  using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def)  hoelzl@40859  174 ak2110@68833  175 lemma%unimportant measurable_pair_swap_iff:  wenzelm@53015  176  "f \ measurable (M2 \\<^sub>M M1) M \ (\(x,y). f (y,x)) \ measurable (M1 \\<^sub>M M2) M"  hoelzl@50003  177  by (auto dest: measurable_pair_swap)  hoelzl@49776  178 ak2110@68833  179 lemma%unimportant measurable_Pair1': "x \ space M1 \ Pair x \ measurable M2 (M1 \\<^sub>M M2)"  hoelzl@50003  180  by simp  hoelzl@40859  181 ak2110@68833  182 lemma%unimportant sets_Pair1[measurable (raw)]:  wenzelm@53015  183  assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "Pair x - A \ sets M2"  hoelzl@40859  184 proof -  hoelzl@47694  185  have "Pair x - A = (if x \ space M1 then Pair x - A \ space M2 else {})"  immler@50244  186  using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)  hoelzl@47694  187  also have "\ \ sets M2"  nipkow@62390  188  using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: if_split_asm)  hoelzl@47694  189  finally show ?thesis .  hoelzl@40859  190 qed  hoelzl@40859  191 ak2110@68833  192 lemma%unimportant measurable_Pair2': "y \ space M2 \ (\x. (x, y)) \ measurable M1 (M1 \\<^sub>M M2)"  hoelzl@49776  193  by (auto intro!: measurable_Pair)  hoelzl@40859  194 ak2110@68833  195 lemma%unimportant sets_Pair2: assumes A: "A \ sets (M1 \\<^sub>M M2)" shows "(\x. (x, y)) - A \ sets M1"  hoelzl@47694  196 proof -  hoelzl@47694  197  have "(\x. (x, y)) - A = (if y \ space M2 then (\x. (x, y)) - A \ space M1 else {})"  immler@50244  198  using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)  hoelzl@47694  199  also have "\ \ sets M1"  nipkow@62390  200  using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: if_split_asm)  hoelzl@47694  201  finally show ?thesis .  hoelzl@40859  202 qed  hoelzl@40859  203 ak2110@68833  204 lemma%unimportant measurable_Pair2:  wenzelm@53015  205  assumes f: "f \ measurable (M1 \\<^sub>M M2) M" and x: "x \ space M1"  hoelzl@47694  206  shows "(\y. f (x, y)) \ measurable M2 M"  hoelzl@47694  207  using measurable_comp[OF measurable_Pair1' f, OF x]  hoelzl@47694  208  by (simp add: comp_def)  hoelzl@62975  209 ak2110@68833  210 lemma%unimportant measurable_Pair1:  wenzelm@53015  211  assumes f: "f \ measurable (M1 \\<^sub>M M2) M" and y: "y \ space M2"  hoelzl@40859  212  shows "(\x. f (x, y)) \ measurable M1 M"  hoelzl@47694  213  using measurable_comp[OF measurable_Pair2' f, OF y]  hoelzl@47694  214  by (simp add: comp_def)  hoelzl@40859  215 ak2110@68833  216 lemma%unimportant Int_stable_pair_measure_generator: "Int_stable {a \ b | a b. a \ sets A \ b \ sets B}"  hoelzl@40859  217  unfolding Int_stable_def  hoelzl@47694  218  by safe (auto simp add: times_Int_times)  hoelzl@40859  219 ak2110@68833  220 lemma%unimportant (in finite_measure) finite_measure_cut_measurable:  wenzelm@53015  221  assumes [measurable]: "Q \ sets (N \\<^sub>M M)"  hoelzl@49776  222  shows "(\x. emeasure M (Pair x - Q)) \ borel_measurable N"  hoelzl@40859  223  (is "?s Q \ _")  hoelzl@49789  224  using Int_stable_pair_measure_generator pair_measure_closed assms  hoelzl@49789  225  unfolding sets_pair_measure  hoelzl@49789  226 proof (induct rule: sigma_sets_induct_disjoint)  hoelzl@49789  227  case (compl A)  immler@50244  228  with sets.sets_into_space have "\x. emeasure M (Pair x - ((space N \ space M) - A)) =  hoelzl@49789  229  (if x \ space N then emeasure M (space M) - ?s A x else 0)"  hoelzl@49789  230  unfolding sets_pair_measure[symmetric]  hoelzl@49789  231  by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)  immler@50244  232  with compl sets.top show ?case  hoelzl@49789  233  by (auto intro!: measurable_If simp: space_pair_measure)  hoelzl@49789  234 next  hoelzl@49789  235  case (union F)  wenzelm@53374  236  then have "\x. emeasure M (Pair x - (\i. F i)) = (\i. ?s (F i) x)"  hoelzl@60727  237  by (simp add: suminf_emeasure disjoint_family_on_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])  wenzelm@53374  238  with union show ?case  hoelzl@50003  239  unfolding sets_pair_measure[symmetric] by simp  hoelzl@49789  240 qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)  hoelzl@49776  241 ak2110@68833  242 lemma%unimportant (in sigma_finite_measure) measurable_emeasure_Pair:  wenzelm@53015  243  assumes Q: "Q \ sets (N \\<^sub>M M)" shows "(\x. emeasure M (Pair x - Q)) \ borel_measurable N" (is "?s Q \ _")  hoelzl@49776  244 proof -  hoelzl@49776  245  from sigma_finite_disjoint guess F . note F = this  hoelzl@49776  246  then have F_sets: "\i. F i \ sets M" by auto  hoelzl@49776  247  let ?C = "\x i. F i \ Pair x - Q"  hoelzl@49776  248  { fix i  hoelzl@49776  249  have [simp]: "space N \ F i \ space N \ space M = space N \ F i"  immler@50244  250  using F sets.sets_into_space by auto  hoelzl@49776  251  let ?R = "density M (indicator (F i))"  hoelzl@49776  252  have "finite_measure ?R"  hoelzl@49776  253  using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)  hoelzl@49776  254  then have "(\x. emeasure ?R (Pair x - (space N \ space ?R \ Q))) \ borel_measurable N"  hoelzl@49776  255  by (rule finite_measure.finite_measure_cut_measurable) (auto intro: Q)  hoelzl@49776  256  moreover have "\x. emeasure ?R (Pair x - (space N \ space ?R \ Q))  hoelzl@49776  257  = emeasure M (F i \ Pair x - (space N \ space ?R \ Q))"  hoelzl@49776  258  using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)  hoelzl@49776  259  moreover have "\x. F i \ Pair x - (space N \ space ?R \ Q) = ?C x i"  immler@50244  260  using sets.sets_into_space[OF Q] by (auto simp: space_pair_measure)  hoelzl@49776  261  ultimately have "(\x. emeasure M (?C x i)) \ borel_measurable N"  hoelzl@49776  262  by simp }  hoelzl@49776  263  moreover  hoelzl@49776  264  { fix x  hoelzl@49776  265  have "(\i. emeasure M (?C x i)) = emeasure M (\i. ?C x i)"  hoelzl@49776  266  proof (intro suminf_emeasure)  hoelzl@49776  267  show "range (?C x) \ sets M"  wenzelm@61808  268  using F \Q \ sets (N \\<^sub>M M)\ by (auto intro!: sets_Pair1)  hoelzl@49776  269  have "disjoint_family F" using F by auto  hoelzl@49776  270  show "disjoint_family (?C x)"  wenzelm@61808  271  by (rule disjoint_family_on_bisimulation[OF \disjoint_family F\]) auto  hoelzl@49776  272  qed  hoelzl@49776  273  also have "(\i. ?C x i) = Pair x - Q"  wenzelm@61808  274  using F sets.sets_into_space[OF \Q \ sets (N \\<^sub>M M)\]  hoelzl@49776  275  by (auto simp: space_pair_measure)  hoelzl@49776  276  finally have "emeasure M (Pair x - Q) = (\i. emeasure M (?C x i))"  hoelzl@49776  277  by simp }  wenzelm@61808  278  ultimately show ?thesis using \Q \ sets (N \\<^sub>M M)\ F_sets  hoelzl@49776  279  by auto  hoelzl@49776  280 qed  hoelzl@49776  281 ak2110@68833  282 lemma%unimportant (in sigma_finite_measure) measurable_emeasure[measurable (raw)]:  hoelzl@50003  283  assumes space: "\x. x \ space N \ A x \ space M"  wenzelm@53015  284  assumes A: "{x\space (N \\<^sub>M M). snd x \ A (fst x)} \ sets (N \\<^sub>M M)"  hoelzl@50003  285  shows "(\x. emeasure M (A x)) \ borel_measurable N"  hoelzl@50003  286 proof -  wenzelm@53015  287  from space have "\x. x \ space N \ Pair x - {x \ space (N \\<^sub>M M). snd x \ A (fst x)} = A x"  hoelzl@50003  288  by (auto simp: space_pair_measure)  hoelzl@50003  289  with measurable_emeasure_Pair[OF A] show ?thesis  hoelzl@50003  290  by (auto cong: measurable_cong)  hoelzl@50003  291 qed  hoelzl@50003  292 ak2110@68833  293 lemma%unimportant (in sigma_finite_measure) emeasure_pair_measure:  wenzelm@53015  294  assumes "X \ sets (N \\<^sub>M M)"  wenzelm@53015  295  shows "emeasure (N \\<^sub>M M) X = (\\<^sup>+ x. \\<^sup>+ y. indicator X (x, y) \M \N)" (is "_ = ?\ X")  hoelzl@49776  296 proof (rule emeasure_measure_of[OF pair_measure_def])  wenzelm@53015  297  show "positive (sets (N \\<^sub>M M)) ?\"  hoelzl@62975  298  by (auto simp: positive_def)  hoelzl@49776  299  have eq[simp]: "\A x y. indicator A (x, y) = indicator (Pair x - A) y"  hoelzl@49776  300  by (auto simp: indicator_def)  wenzelm@53015  301  show "countably_additive (sets (N \\<^sub>M M)) ?\"  hoelzl@49776  302  proof (rule countably_additiveI)  wenzelm@53015  303  fix F :: "nat \ ('b \ 'a) set" assume F: "range F \ sets (N \\<^sub>M M)" "disjoint_family F"  hoelzl@59353  304  from F have *: "\i. F i \ sets (N \\<^sub>M M)" by auto  hoelzl@49776  305  moreover have "\x. disjoint_family (\i. Pair x - F i)"  hoelzl@49776  306  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  hoelzl@49776  307  moreover have "\x. range (\i. Pair x - F i) \ sets M"  hoelzl@49776  308  using F by (auto simp: sets_Pair1)  hoelzl@49776  309  ultimately show "(\n. ?\ (F n)) = ?\ (\i. F i)"  hoelzl@62975  310  by (auto simp add: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure  hoelzl@56996  311  intro!: nn_integral_cong nn_integral_indicator[symmetric])  hoelzl@49776  312  qed  hoelzl@49776  313  show "{a \ b |a b. a \ sets N \ b \ sets M} \ Pow (space N \ space M)"  immler@50244  314  using sets.space_closed[of N] sets.space_closed[of M] by auto  hoelzl@49776  315 qed fact  hoelzl@49776  316 ak2110@68833  317 lemma%unimportant (in sigma_finite_measure) emeasure_pair_measure_alt:  wenzelm@53015  318  assumes X: "X \ sets (N \\<^sub>M M)"  wenzelm@53015  319  shows "emeasure (N \\<^sub>M M) X = (\\<^sup>+x. emeasure M (Pair x - X) \N)"  hoelzl@49776  320 proof -  hoelzl@49776  321  have [simp]: "\x y. indicator X (x, y) = indicator (Pair x - X) y"  hoelzl@49776  322  by (auto simp: indicator_def)  hoelzl@49776  323  show ?thesis  hoelzl@56996  324  using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1)  hoelzl@49776  325 qed  hoelzl@49776  326 ak2110@68833  327 lemma%important (in sigma_finite_measure) emeasure_pair_measure_Times:  hoelzl@49776  328  assumes A: "A \ sets N" and B: "B \ sets M"  wenzelm@53015  329  shows "emeasure (N \\<^sub>M M) (A \ B) = emeasure N A * emeasure M B"  ak2110@68833  330 proof%unimportant -  wenzelm@53015  331  have "emeasure (N \\<^sub>M M) (A \ B) = (\\<^sup>+x. emeasure M B * indicator A x \N)"  hoelzl@56996  332  using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt)  hoelzl@49776  333  also have "\ = emeasure M B * emeasure N A"  hoelzl@62975  334  using A by (simp add: nn_integral_cmult_indicator)  hoelzl@49776  335  finally show ?thesis  hoelzl@49776  336  by (simp add: ac_simps)  hoelzl@40859  337 qed  hoelzl@40859  338 ak2110@68833  339 subsection%important \Binary products of \sigma-finite emeasure spaces\  hoelzl@40859  340 ak2110@68833  341 locale%important pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2  hoelzl@47694  342  for M1 :: "'a measure" and M2 :: "'b measure"  hoelzl@40859  343 ak2110@68833  344 lemma%unimportant (in pair_sigma_finite) measurable_emeasure_Pair1:  wenzelm@53015  345  "Q \ sets (M1 \\<^sub>M M2) \ (\x. emeasure M2 (Pair x - Q)) \ borel_measurable M1"  hoelzl@49776  346  using M2.measurable_emeasure_Pair .  hoelzl@40859  347 ak2110@68833  348 lemma%important (in pair_sigma_finite) measurable_emeasure_Pair2:  wenzelm@53015  349  assumes Q: "Q \ sets (M1 \\<^sub>M M2)" shows "(\y. emeasure M1 ((\x. (x, y)) - Q)) \ borel_measurable M2"  ak2110@68833  350 proof%unimportant -  wenzelm@53015  351  have "(\(x, y). (y, x)) - Q \ space (M2 \\<^sub>M M1) \ sets (M2 \\<^sub>M M1)"  hoelzl@47694  352  using Q measurable_pair_swap' by (auto intro: measurable_sets)  hoelzl@49776  353  note M1.measurable_emeasure_Pair[OF this]  wenzelm@53015  354  moreover have "\y. Pair y - ((\(x, y). (y, x)) - Q \ space (M2 \\<^sub>M M1)) = (\x. (x, y)) - Q"  immler@50244  355  using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure)  hoelzl@47694  356  ultimately show ?thesis by simp  hoelzl@39088  357 qed  hoelzl@39088  358 ak2110@68833  359 lemma%important (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator:  hoelzl@47694  360  defines "E \ {A \ B | A B. A \ sets M1 \ B \ sets M2}"  hoelzl@47694  361  shows "\F::nat \ ('a \ 'b) set. range F \ E \ incseq F \ (\i. F i) = space M1 \ space M2 \  wenzelm@53015  362  (\i. emeasure (M1 \\<^sub>M M2) (F i) \$$"  ak2110@68833  363 proof%unimportant -  hoelzl@47694  364  from M1.sigma_finite_incseq guess F1 . note F1 = this  hoelzl@47694  365  from M2.sigma_finite_incseq guess F2 . note F2 = this  hoelzl@47694  366  from F1 F2 have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)" by auto  hoelzl@40859  367  let ?F = "\i. F1 i \ F2 i"  hoelzl@47694  368  show ?thesis  hoelzl@40859  369  proof (intro exI[of _ ?F] conjI allI)  hoelzl@47694  370  show "range ?F \ E" using F1 F2 by (auto simp: E_def) (metis range_subsetD)  hoelzl@40859  371  next  hoelzl@40859  372  have "space M1 \ space M2 \ (\i. ?F i)"  hoelzl@40859  373  proof (intro subsetI)  hoelzl@40859  374  fix x assume "x \ space M1 \ space M2"  hoelzl@40859  375  then obtain i j where "fst x \ F1 i" "snd x \ F2 j"  hoelzl@40859  376  by (auto simp: space)  hoelzl@40859  377  then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)"  wenzelm@61808  378  using \incseq F1\ \incseq F2\ unfolding incseq_def  hoelzl@41981  379  by (force split: split_max)+  hoelzl@40859  380  then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)"  haftmann@54863  381  by (intro SigmaI) (auto simp add: max.commute)  hoelzl@40859  382  then show "x \ (\i. ?F i)" by auto  hoelzl@40859  383  qed  hoelzl@47694  384  then show "(\i. ?F i) = space M1 \ space M2"  hoelzl@47694  385  using space by (auto simp: space)  hoelzl@40859  386  next  hoelzl@41981  387  fix i show "incseq (\i. F1 i \ F2 i)"  wenzelm@61808  388  using \incseq F1\ \incseq F2\ unfolding incseq_Suc_iff by auto  hoelzl@40859  389  next  hoelzl@40859  390  fix i  hoelzl@40859  391  from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto  hoelzl@62975  392  with F1 F2 show "emeasure (M1 \\<^sub>M M2) (F1 i \ F2 i) \ \"  hoelzl@62975  393  by (auto simp add: emeasure_pair_measure_Times ennreal_mult_eq_top_iff)  hoelzl@47694  394  qed  hoelzl@47694  395 qed  hoelzl@47694  396 ak2110@68833  397 sublocale%important pair_sigma_finite \ P?: sigma_finite_measure "M1 \\<^sub>M M2"  hoelzl@47694  398 proof  hoelzl@57447  399  from M1.sigma_finite_countable guess F1 ..  hoelzl@57447  400  moreover from M2.sigma_finite_countable guess F2 ..  hoelzl@57447  401  ultimately show  hoelzl@57447  402  "\A. countable A \ A \ sets (M1 \\<^sub>M M2) \ \A = space (M1 \\<^sub>M M2) \ (\a\A. emeasure (M1 \\<^sub>M M2) a \ \)"  hoelzl@57447  403  by (intro exI[of _ "($$a, b). a \ b)  (F1 \ F2)"] conjI)  hoelzl@62975  404  (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff)  hoelzl@40859  405 qed  hoelzl@40859  406 ak2110@68833  407 lemma%unimportant sigma_finite_pair_measure:  hoelzl@47694  408  assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B"  wenzelm@53015  409  shows "sigma_finite_measure (A \\<^sub>M B)"  hoelzl@47694  410 proof -  hoelzl@47694  411  interpret A: sigma_finite_measure A by fact  hoelzl@47694  412  interpret B: sigma_finite_measure B by fact  hoelzl@47694  413  interpret AB: pair_sigma_finite A B ..  hoelzl@47694  414  show ?thesis ..  hoelzl@40859  415 qed  hoelzl@39088  416 ak2110@68833  417 lemma%unimportant sets_pair_swap:  wenzelm@53015  418  assumes "A \ sets (M1 \\<^sub>M M2)"  wenzelm@53015  419  shows "(\(x, y). (y, x)) - A \ space (M2 \\<^sub>M M1) \ sets (M2 \\<^sub>M M1)"  hoelzl@47694  420  using measurable_pair_swap' assms by (rule measurable_sets)  hoelzl@41661  421 ak2110@68833  422 lemma%important (in pair_sigma_finite) distr_pair_swap:  wenzelm@53015  423  "M1 \\<^sub>M M2 = distr (M2 \\<^sub>M M1) (M1 \\<^sub>M M2) (\(x, y). (y, x))" (is "?P = ?D")  ak2110@68833  424 proof%unimportant -  hoelzl@41689  425  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this  hoelzl@47694  426  let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}"  hoelzl@47694  427  show ?thesis  hoelzl@47694  428  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])  hoelzl@47694  429  show "?E \ Pow (space ?P)"  immler@50244  430  using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)  hoelzl@47694  431  show "sets ?P = sigma_sets (space ?P) ?E"  hoelzl@47694  432  by (simp add: sets_pair_measure space_pair_measure)  hoelzl@47694  433  then show "sets ?D = sigma_sets (space ?P) ?E"  hoelzl@47694  434  by simp  hoelzl@47694  435  next  hoelzl@49784  436  show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \"  hoelzl@47694  437  using F by (auto simp: space_pair_measure)  hoelzl@47694  438  next  hoelzl@47694  439  fix X assume "X \ ?E"  hoelzl@47694  440  then obtain A B where X[simp]: "X = A \ B" and A: "A \ sets M1" and B: "B \ sets M2" by auto  wenzelm@53015  441  have "(\(y, x). (x, y)) - X \ space (M2 \\<^sub>M M1) = B \ A"  immler@50244  442  using sets.sets_into_space[OF A] sets.sets_into_space[OF B] by (auto simp: space_pair_measure)  wenzelm@53015  443  with A B show "emeasure (M1 \\<^sub>M M2) X = emeasure ?D X"  hoelzl@49776  444  by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr  hoelzl@47694  445  measurable_pair_swap' ac_simps)  hoelzl@41689  446  qed  hoelzl@41689  447 qed  hoelzl@41689  448 ak2110@68833  449 lemma%unimportant (in pair_sigma_finite) emeasure_pair_measure_alt2:  wenzelm@53015  450  assumes A: "A \ sets (M1 \\<^sub>M M2)"  wenzelm@53015  451  shows "emeasure (M1 \\<^sub>M M2) A = (\\<^sup>+y. emeasure M1 ((\x. (x, y)) - A) \M2)"  hoelzl@47694  452  (is "_ = ?\ A")  ak2110@68833  453 proof%unimportant -  wenzelm@53015  454  have [simp]: "\y. (Pair y - ((\(x, y). (y, x)) - A \ space (M2 \\<^sub>M M1))) = (\x. (x, y)) - A"  immler@50244  455  using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)  hoelzl@47694  456  show ?thesis using A  hoelzl@47694  457  by (subst distr_pair_swap)  hoelzl@47694  458  (simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']  hoelzl@49776  459  M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A])  hoelzl@49776  460 qed  hoelzl@49776  461 ak2110@68833  462 lemma%unimportant (in pair_sigma_finite) AE_pair:  wenzelm@53015  463  assumes "AE x in (M1 \\<^sub>M M2). Q x"  hoelzl@49776  464  shows "AE x in M1. (AE y in M2. Q (x, y))"  hoelzl@49776  465 proof -  wenzelm@53015  466  obtain N where N: "N \ sets (M1 \\<^sub>M M2)" "emeasure (M1 \\<^sub>M M2) N = 0" "{x\space (M1 \\<^sub>M M2). \ Q x} \ N"  hoelzl@49776  467  using assms unfolding eventually_ae_filter by auto  hoelzl@49776  468  show ?thesis  hoelzl@49776  469  proof (rule AE_I)  wenzelm@61808  470  from N measurable_emeasure_Pair1[OF \N \ sets (M1 \\<^sub>M M2)\]  hoelzl@49776  471  show "emeasure M1 {x\space M1. emeasure M2 (Pair x - N) \ 0} = 0"  hoelzl@62975  472  by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff)  hoelzl@49776  473  show "{x \ space M1. emeasure M2 (Pair x - N) \ 0} \ sets M1"  hoelzl@62975  474  by (intro borel_measurable_eq measurable_emeasure_Pair1 N sets.sets_Collect_neg N) simp  hoelzl@49776  475  { fix x assume "x \ space M1" "emeasure M2 (Pair x - N) = 0"  hoelzl@49776  476  have "AE y in M2. Q (x, y)"  hoelzl@49776  477  proof (rule AE_I)  hoelzl@49776  478  show "emeasure M2 (Pair x - N) = 0" by fact  hoelzl@49776  479  show "Pair x - N \ sets M2" using N(1) by (rule sets_Pair1)  hoelzl@49776  480  show "{y \ space M2. \ Q (x, y)} \ Pair x - N"  wenzelm@61808  481  using N \x \ space M1\ unfolding space_pair_measure by auto  hoelzl@49776  482  qed }  hoelzl@49776  483  then show "{x \ space M1. \ (AE y in M2. Q (x, y))} \ {x \ space M1. emeasure M2 (Pair x - N) \ 0}"  hoelzl@49776  484  by auto  hoelzl@49776  485  qed  hoelzl@49776  486 qed  hoelzl@49776  487 ak2110@68833  488 lemma%important (in pair_sigma_finite) AE_pair_measure:  wenzelm@53015  489  assumes "{x\space (M1 \\<^sub>M M2). P x} \ sets (M1 \\<^sub>M M2)"  hoelzl@49776  490  assumes ae: "AE x in M1. AE y in M2. P (x, y)"  wenzelm@53015  491  shows "AE x in M1 \\<^sub>M M2. P x"  ak2110@68833  492 proof%unimportant (subst AE_iff_measurable[OF _ refl])  wenzelm@53015  493  show "{x\space (M1 \\<^sub>M M2). \ P x} \ sets (M1 \\<^sub>M M2)"  immler@50244  494  by (rule sets.sets_Collect) fact  wenzelm@53015  495  then have "emeasure (M1 \\<^sub>M M2) {x \ space (M1 \\<^sub>M M2). \ P x} =  wenzelm@53015  496  (\\<^sup>+ x. \\<^sup>+ y. indicator {x \ space (M1 \\<^sub>M M2). \ P x} (x, y) \M2 \M1)"  hoelzl@49776  497  by (simp add: M2.emeasure_pair_measure)  wenzelm@53015  498  also have "\ = (\\<^sup>+ x. \\<^sup>+ y. 0 \M2 \M1)"  hoelzl@49776  499  using ae  hoelzl@56996  500  apply (safe intro!: nn_integral_cong_AE)  hoelzl@49776  501  apply (intro AE_I2)  hoelzl@56996  502  apply (safe intro!: nn_integral_cong_AE)  hoelzl@49776  503  apply auto  hoelzl@49776  504  done  wenzelm@53015  505  finally show "emeasure (M1 \\<^sub>M M2) {x \ space (M1 \\<^sub>M M2). \ P x} = 0" by simp  hoelzl@49776  506 qed  hoelzl@49776  507 ak2110@68833  508 lemma%unimportant (in pair_sigma_finite) AE_pair_iff:  wenzelm@53015  509  "{x\space (M1 \\<^sub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^sub>M M2) \  wenzelm@53015  510  (AE x in M1. AE y in M2. P x y) \ (AE x in (M1 \\<^sub>M M2). P (fst x) (snd x))"  hoelzl@49776  511  using AE_pair[of "\x. P (fst x) (snd x)"] AE_pair_measure[of "\x. P (fst x) (snd x)"] by auto  hoelzl@49776  512 ak2110@68833  513 lemma%unimportant (in pair_sigma_finite) AE_commute:  wenzelm@53015  514  assumes P: "{x\space (M1 \\<^sub>M M2). P (fst x) (snd x)} \ sets (M1 \\<^sub>M M2)"  hoelzl@49776  515  shows "(AE x in M1. AE y in M2. P x y) \ (AE y in M2. AE x in M1. P x y)"  hoelzl@49776  516 proof -  hoelzl@49776  517  interpret Q: pair_sigma_finite M2 M1 ..  hoelzl@49776  518  have [simp]: "\x. (fst (case x of (x, y) \ (y, x))) = snd x" "\x. (snd (case x of (x, y) \ (y, x))) = fst x"  hoelzl@49776  519  by auto  wenzelm@53015  520  have "{x \ space (M2 \\<^sub>M M1). P (snd x) (fst x)} =  wenzelm@53015  521  (\(x, y). (y, x)) - {x \ space (M1 \\<^sub>M M2). P (fst x) (snd x)} \ space (M2 \\<^sub>M M1)"  hoelzl@49776  522  by (auto simp: space_pair_measure)  wenzelm@53015  523  also have "\ \ sets (M2 \\<^sub>M M1)"  hoelzl@49776  524  by (intro sets_pair_swap P)  hoelzl@49776  525  finally show ?thesis  hoelzl@49776  526  apply (subst AE_pair_iff[OF P])  hoelzl@49776  527  apply (subst distr_pair_swap)  hoelzl@49776  528  apply (subst AE_distr_iff[OF measurable_pair_swap' P])  hoelzl@49776  529  apply (subst Q.AE_pair_iff)  hoelzl@49776  530  apply simp_all  hoelzl@49776  531  done  hoelzl@40859  532 qed  hoelzl@40859  533 ak2110@68833  534 subsection%important "Fubinis theorem"  hoelzl@40859  535 ak2110@68833  536 lemma%unimportant measurable_compose_Pair1:  wenzelm@53015  537  "x \ space M1 \ g \ measurable (M1 \\<^sub>M M2) L \ (\y. g (x, y)) \ measurable M2 L"  hoelzl@50003  538  by simp  hoelzl@49800  539 ak2110@68833  540 lemma%unimportant (in sigma_finite_measure) borel_measurable_nn_integral_fst:  hoelzl@62975  541  assumes f: "f \ borel_measurable (M1 \\<^sub>M M)"  wenzelm@53015  542  shows "(\x. \\<^sup>+ y. f (x, y) \M) \ borel_measurable M1"  ak2110@68833  543 using f proof%unimportant induct  hoelzl@49800  544  case (cong u v)  hoelzl@49999  545  then have "\w x. w \ space M1 \ x \ space M \ u (w, x) = v (w, x)"  hoelzl@49800  546  by (auto simp: space_pair_measure)  hoelzl@49800  547  show ?case  hoelzl@49800  548  apply (subst measurable_cong)  hoelzl@56996  549  apply (rule nn_integral_cong)  hoelzl@49800  550  apply fact+  hoelzl@49800  551  done  hoelzl@49800  552 next  hoelzl@49800  553  case (set Q)  hoelzl@49800  554  have [simp]: "\x y. indicator Q (x, y) = indicator (Pair x - Q) y"  hoelzl@49800  555  by (auto simp: indicator_def)  wenzelm@53015  556  have "\x. x \ space M1 \ emeasure M (Pair x - Q) = \\<^sup>+ y. indicator Q (x, y) \M"  hoelzl@49800  557  by (simp add: sets_Pair1[OF set])  hoelzl@49999  558  from this measurable_emeasure_Pair[OF set] show ?case  hoelzl@49800  559  by (rule measurable_cong[THEN iffD1])  hoelzl@56996  560 qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1  hoelzl@56996  561  nn_integral_monotone_convergence_SUP incseq_def le_fun_def  hoelzl@49800  562  cong: measurable_cong)  hoelzl@49800  563 ak2110@68833  564 lemma%unimportant (in sigma_finite_measure) nn_integral_fst:  hoelzl@62975  565  assumes f: "f \ borel_measurable (M1 \\<^sub>M M)"  hoelzl@56996  566  shows "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \M \M1) = integral\<^sup>N (M1 \\<^sub>M M) f" (is "?I f = _")  ak2110@68833  567  using f proof induct  hoelzl@49800  568  case (cong u v)  wenzelm@53374  569  then have "?I u = ?I v"  hoelzl@56996  570  by (intro nn_integral_cong) (auto simp: space_pair_measure)  wenzelm@53374  571  with cong show ?case  hoelzl@56996  572  by (simp cong: nn_integral_cong)  hoelzl@56996  573 qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add  hoelzl@62975  574  nn_integral_monotone_convergence_SUP measurable_compose_Pair1  hoelzl@62975  575  borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def  hoelzl@56996  576  cong: nn_integral_cong)  hoelzl@40859  577 ak2110@68833  578 lemma%unimportant (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:  haftmann@61424  579  "case_prod f \ borel_measurable (N \\<^sub>M M) \ (\x. \\<^sup>+ y. f x y \M) \ borel_measurable N"  hoelzl@62975  580  using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp  hoelzl@50003  581 ak2110@68833  582 lemma%important (in pair_sigma_finite) nn_integral_snd:  hoelzl@62975  583  assumes f[measurable]: "f \ borel_measurable (M1 \\<^sub>M M2)"  hoelzl@56996  584  shows "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = integral\<^sup>N (M1 \\<^sub>M M2) f"  ak2110@68833  585 proof%unimportant -  hoelzl@47694  586  note measurable_pair_swap[OF f]  hoelzl@56996  587  from M1.nn_integral_fst[OF this]  wenzelm@53015  588  have "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = (\\<^sup>+ (x, y). f (y, x) \(M2 \\<^sub>M M1))"  hoelzl@40859  589  by simp  hoelzl@56996  590  also have "(\\<^sup>+ (x, y). f (y, x) \(M2 \\<^sub>M M1)) = integral\<^sup>N (M1 \\<^sub>M M2) f"  hoelzl@62975  591  by (subst distr_pair_swap) (auto simp add: nn_integral_distr intro!: nn_integral_cong)  hoelzl@40859  592  finally show ?thesis .  hoelzl@40859  593 qed  hoelzl@40859  594 ak2110@68833  595 lemma%important (in pair_sigma_finite) Fubini:  wenzelm@53015  596  assumes f: "f \ borel_measurable (M1 \\<^sub>M M2)"  wenzelm@53015  597  shows "(\\<^sup>+ y. (\\<^sup>+ x. f (x, y) \M1) \M2) = (\\<^sup>+ x. (\\<^sup>+ y. f (x, y) \M2) \M1)"  hoelzl@56996  598  unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..  hoelzl@41026  599 ak2110@68833  600 lemma%important (in pair_sigma_finite) Fubini':  haftmann@61424  601  assumes f: "case_prod f \ borel_measurable (M1 \\<^sub>M M2)"  hoelzl@57235  602  shows "(\\<^sup>+ y. (\\<^sup>+ x. f x y \M1) \M2) = (\\<^sup>+ x. (\\<^sup>+ y. f x y \M2) \M1)"  hoelzl@57235  603  using Fubini[OF f] by simp  hoelzl@57235  604 ak2110@68833  605 subsection%important \Products on counting spaces, densities and distributions\  hoelzl@40859  606 ak2110@68833  607 lemma%important sigma_prod:  hoelzl@59088  608  assumes X_cover: "\E\A. countable E \ X = \E" and A: "A \ Pow X"  hoelzl@59088  609  assumes Y_cover: "\E\B. countable E \ Y = \E" and B: "B \ Pow Y"  hoelzl@59088  610  shows "sigma X A \\<^sub>M sigma Y B = sigma (X \ Y) {a \ b | a b. a \ A \ b \ B}"  hoelzl@59088  611  (is "?P = ?S")  ak2110@68833  612 proof%unimportant (rule measure_eqI)  hoelzl@59088  613  have [simp]: "snd \ X \ Y \ Y" "fst \ X \ Y \ X"  hoelzl@59088  614  by auto  hoelzl@59088  615  let ?XY = "{{fst - a \ X \ Y | a. a \ A}, {snd - b \ X \ Y | b. b \ B}}"  haftmann@69260  616  have "sets ?P = sets (SUP xy\?XY. sigma (X \ Y) xy)"  hoelzl@59088  617  by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)  hoelzl@59088  618  also have "\ = sets (sigma (X \ Y) (\?XY))"  hoelzl@63333  619  by (intro Sup_sigma arg_cong[where f=sets]) auto  hoelzl@59088  620  also have "\ = sets ?S"  hoelzl@62975  621  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)  hoelzl@59088  622  show "\?XY \ Pow (X \ Y)" "{a \ b |a b. a \ A \ b \ B} \ Pow (X \ Y)"  hoelzl@59088  623  using A B by auto  hoelzl@59088  624  next  hoelzl@59088  625  interpret XY: sigma_algebra "X \ Y" "sigma_sets (X \ Y) {a \ b |a b. a \ A \ b \ B}"  hoelzl@59088  626  using A B by (intro sigma_algebra_sigma_sets) auto  hoelzl@59088  627  fix Z assume "Z \ \?XY"  hoelzl@59088  628  then show "Z \ sigma_sets (X \ Y) {a \ b |a b. a \ A \ b \ B}"  hoelzl@59088  629  proof safe  hoelzl@59088  630  fix a assume "a \ A"  hoelzl@59088  631  from Y_cover obtain E where E: "E \ B" "countable E" and "Y = \E"  hoelzl@59088  632  by auto  wenzelm@61808  633  with \a \ A\ A have eq: "fst - a \ X \ Y = (\e\E. a \ e)"  hoelzl@59088  634  by auto  hoelzl@59088  635  show "fst - a \ X \ Y \ sigma_sets (X \ Y) {a \ b |a b. a \ A \ b \ B}"  wenzelm@61808  636  using \a \ A\ E unfolding eq by (auto intro!: XY.countable_UN')  hoelzl@59088  637  next  hoelzl@59088  638  fix b assume "b \ B"  hoelzl@59088  639  from X_cover obtain E where E: "E \ A" "countable E" and "X = \E"  hoelzl@59088  640  by auto  wenzelm@61808  641  with \b \ B\ B have eq: "snd - b \ X \ Y = (\e\E. e \ b)"  hoelzl@59088  642  by auto  hoelzl@59088  643  show "snd - b \ X \ Y \ sigma_sets (X \ Y) {a \ b |a b. a \ A \ b \ B}"  wenzelm@61808  644  using \b \ B\ E unfolding eq by (auto intro!: XY.countable_UN')  hoelzl@59088  645  qed  hoelzl@59088  646  next  hoelzl@59088  647  fix Z assume "Z \ {a \ b |a b. a \ A \ b \ B}"  hoelzl@59088  648  then obtain a b where "Z = a \ b" and ab: "a \ A" "b \ B"  hoelzl@59088  649  by auto  hoelzl@59088  650  then have Z: "Z = (fst - a \ X \ Y) \ (snd - b \ X \ Y)"  hoelzl@59088  651  using A B by auto  hoelzl@59088  652  interpret XY: sigma_algebra "X \ Y" "sigma_sets (X \ Y) (\?XY)"  hoelzl@59088  653  by (intro sigma_algebra_sigma_sets) auto  hoelzl@59088  654  show "Z \ sigma_sets (X \ Y) (\?XY)"  hoelzl@59088  655  unfolding Z by (rule XY.Int) (blast intro: ab)+  hoelzl@59088  656  qed  hoelzl@59088  657  finally show "sets ?P = sets ?S" .  hoelzl@59088  658 next  hoelzl@59088  659  interpret finite_measure "sigma X A" for X A  hoelzl@59088  660  proof qed (simp add: emeasure_sigma)  hoelzl@59088  661  fix A assume "A \ sets ?P" then show "emeasure ?P A = emeasure ?S A"  hoelzl@59088  662  by (simp add: emeasure_pair_measure_alt emeasure_sigma)  hoelzl@59088  663 qed  hoelzl@59088  664 ak2110@68833  665 lemma%unimportant sigma_sets_pair_measure_generator_finite:  hoelzl@38656  666  assumes "finite A" and "finite B"  hoelzl@47694  667  shows "sigma_sets (A \ B) { a \ b | a b. a \ A \ b \ B} = Pow (A \ B)"  hoelzl@40859  668  (is "sigma_sets ?prod ?sets = _")  hoelzl@38656  669 proof safe  hoelzl@38656  670  have fin: "finite (A \ B)" using assms by (rule finite_cartesian_product)  hoelzl@38656  671  fix x assume subset: "x \ A \ B"  hoelzl@38656  672  hence "finite x" using fin by (rule finite_subset)  hoelzl@40859  673  from this subset show "x \ sigma_sets ?prod ?sets"  hoelzl@38656  674  proof (induct x)  hoelzl@38656  675  case empty show ?case by (rule sigma_sets.Empty)  hoelzl@38656  676  next  hoelzl@38656  677  case (insert a x)  hoelzl@47694  678  hence "{a} \ sigma_sets ?prod ?sets" by auto  hoelzl@38656  679  moreover have "x \ sigma_sets ?prod ?sets" using insert by auto  hoelzl@38656  680  ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)  hoelzl@38656  681  qed  hoelzl@38656  682 next  hoelzl@38656  683  fix x a b  hoelzl@40859  684  assume "x \ sigma_sets ?prod ?sets" and "(a, b) \ x"  hoelzl@38656  685  from sigma_sets_into_sp[OF _ this(1)] this(2)  hoelzl@40859  686  show "a \ A" and "b \ B" by auto  hoelzl@35833  687 qed  hoelzl@35833  688 ak2110@68833  689 lemma%important sets_pair_eq:  hoelzl@64008  690  assumes Ea: "Ea \ Pow (space A)" "sets A = sigma_sets (space A) Ea"  hoelzl@64008  691  and Ca: "countable Ca" "Ca \ Ea" "\Ca = space A"  hoelzl@64008  692  and Eb: "Eb \ Pow (space B)" "sets B = sigma_sets (space B) Eb"  hoelzl@64008  693  and Cb: "countable Cb" "Cb \ Eb" "\Cb = space B"  hoelzl@64008  694  shows "sets (A \\<^sub>M B) = sets (sigma (space A \ space B) { a \ b | a b. a \ Ea \ b \ Eb })"  hoelzl@64008  695  (is "_ = sets (sigma ?\ ?E)")  ak2110@68833  696 proof%unimportant  hoelzl@64008  697  show "sets (sigma ?\ ?E) \ sets (A \\<^sub>M B)"  hoelzl@64008  698  using Ea(1) Eb(1) by (subst sigma_le_sets) (auto simp: Ea(2) Eb(2))  hoelzl@64008  699  have "?E \ Pow ?\"  hoelzl@64008  700  using Ea(1) Eb(1) by auto  hoelzl@64008  701  then have E: "a \ Ea \ b \ Eb \ a \ b \ sets (sigma ?\ ?E)" for a b  hoelzl@64008  702  by auto  hoelzl@64008  703  have "sets (A \\<^sub>M B) \ sets (Sup {vimage_algebra ?\ fst A, vimage_algebra ?\ snd B})"  hoelzl@64008  704  unfolding sets_pair_eq_sets_fst_snd ..  hoelzl@64008  705  also have "vimage_algebra ?\ fst A = vimage_algebra ?\ fst (sigma (space A) Ea)"  hoelzl@64008  706  by (intro vimage_algebra_cong[OF refl refl]) (simp add: Ea)  hoelzl@64008  707  also have "\ = sigma ?\ {fst - A \ ?\ |A. A \ Ea}"  hoelzl@64008  708  by (intro Ea vimage_algebra_sigma) auto  hoelzl@64008  709  also have "vimage_algebra ?\ snd B = vimage_algebra ?\ snd (sigma (space B) Eb)"  hoelzl@64008  710  by (intro vimage_algebra_cong[OF refl refl]) (simp add: Eb)  hoelzl@64008  711  also have "\ = sigma ?\ {snd - A \ ?\ |A. A \ Eb}"  hoelzl@64008  712  by (intro Eb vimage_algebra_sigma) auto  hoelzl@64008  713  also have "{sigma ?\ {fst - Aa \ ?\ |Aa. Aa \ Ea}, sigma ?\ {snd - Aa \ ?\ |Aa. Aa \ Eb}} =  hoelzl@64008  714  sigma ?\  {{fst - Aa \ ?\ |Aa. Aa \ Ea}, {snd - Aa \ ?\ |Aa. Aa \ Eb}}"  hoelzl@64008  715  by auto  haftmann@69260  716  also have "sets (SUP S\{{fst - Aa \ ?\ |Aa. Aa \ Ea}, {snd - Aa \ ?\ |Aa. Aa \ Eb}}. sigma ?\ S) =  hoelzl@64008  717  sets (sigma ?\ (\{{fst - Aa \ ?\ |Aa. Aa \ Ea}, {snd - Aa \ ?\ |Aa. Aa \ Eb}}))"  hoelzl@64008  718  using Ea(1) Eb(1) by (intro sets_Sup_sigma) auto  hoelzl@64008  719  also have "\ \ sets (sigma ?\ ?E)"  hoelzl@64008  720  proof (subst sigma_le_sets, safe intro!: space_in_measure_of)  hoelzl@64008  721  fix a assume "a \ Ea"  hoelzl@64008  722  then have "fst - a \ ?\ = (\b\Cb. a \ b)"  hoelzl@64008  723  using Cb(3)[symmetric] Ea(1) by auto  hoelzl@64008  724  then show "fst - a \ ?\ \ sets (sigma ?\ ?E)"  hoelzl@64008  725  using Cb \a \ Ea\ by (auto intro!: sets.countable_UN' E)  hoelzl@64008  726  next  hoelzl@64008  727  fix b assume "b \ Eb"  hoelzl@64008  728  then have "snd - b \ ?\ = (\a\Ca. a \ b)"  hoelzl@64008  729  using Ca(3)[symmetric] Eb(1) by auto  hoelzl@64008  730  then show "snd - b \ ?\ \ sets (sigma ?\ ?E)"  hoelzl@64008  731  using Ca \b \ Eb\ by (auto intro!: sets.countable_UN' E)  hoelzl@64008  732  qed  hoelzl@64008  733  finally show "sets (A \\<^sub>M B) \ sets (sigma ?\ ?E)" .  hoelzl@64008  734 qed  hoelzl@64008  735 ak2110@68833  736 lemma%important borel_prod:  hoelzl@59088  737  "(borel \\<^sub>M borel) = (borel :: ('a::second_countable_topology \ 'b::second_countable_topology) measure)"  hoelzl@59088  738  (is "?P = ?B")  ak2110@68833  739 proof%unimportant -  hoelzl@59088  740  have "?B = sigma UNIV {A \ B | A B. open A \ open B}"  hoelzl@59088  741  by (rule second_countable_borel_measurable[OF open_prod_generated])  hoelzl@59088  742  also have "\ = ?P"  hoelzl@59088  743  unfolding borel_def  hoelzl@59088  744  by (subst sigma_prod) (auto intro!: exI[of _ "{UNIV}"])  hoelzl@59088  745  finally show ?thesis ..  hoelzl@59088  746 qed  hoelzl@59088  747 ak2110@68833  748 lemma%important pair_measure_count_space:  hoelzl@47694  749  assumes A: "finite A" and B: "finite B"  wenzelm@53015  750  shows "count_space A \\<^sub>M count_space B = count_space (A \ B)" (is "?P = ?C")  ak2110@68833  751 proof%unimportant (rule measure_eqI)  hoelzl@47694  752  interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact  hoelzl@47694  753  interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact  wenzelm@61169  754  interpret P: pair_sigma_finite "count_space A" "count_space B" ..  hoelzl@47694  755  show eq: "sets ?P = sets ?C"  hoelzl@47694  756  by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B)  hoelzl@47694  757  fix X assume X: "X \ sets ?P"  hoelzl@47694  758  with eq have X_subset: "X \ A \ B" by simp  hoelzl@47694  759  with A B have fin_Pair: "\x. finite (Pair x - X)"  hoelzl@47694  760  by (intro finite_subset[OF _ B]) auto  hoelzl@47694  761  have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)  lp15@67693  762  have card: "0 < card (Pair a - X)" if "(a, b) \ X" for a b  lp15@67693  763  using card_gt_0_iff fin_Pair that by auto  lp15@67693  764  then have "emeasure ?P X = \\<^sup>+ x. emeasure (count_space B) (Pair x - X)  lp15@67693  765  \count_space A"  lp15@67693  766  by (simp add: B.emeasure_pair_measure_alt X)  lp15@67693  767  also have "... = emeasure ?C X"  hoelzl@47694  768  apply (subst emeasure_count_space)  lp15@67693  769  using card X_subset A fin_Pair fin_X  lp15@67693  770  apply (auto simp add: nn_integral_count_space  lp15@67693  771  of_nat_sum[symmetric] card_SigmaI[symmetric]  lp15@67693  772  simp del: card_SigmaI  hoelzl@62975  773  intro!: arg_cong[where f=card])  hoelzl@47694  774  done  lp15@67693  775  finally show "emeasure ?P X = emeasure ?C X" .  hoelzl@45777  776 qed  hoelzl@35833  777 hoelzl@59426  778 ak2110@68833  779 lemma%unimportant emeasure_prod_count_space:  hoelzl@59426  780  assumes A: "A \ sets (count_space UNIV \\<^sub>M M)" (is "A \ sets (?A \\<^sub>M ?B)")  hoelzl@59426  781  shows "emeasure (?A \\<^sub>M ?B) A = (\\<^sup>+ x. \\<^sup>+ y. indicator A (x, y) \?B \?A)"  hoelzl@59426  782  by (rule emeasure_measure_of[OF pair_measure_def])  hoelzl@62975  783  (auto simp: countably_additive_def positive_def suminf_indicator A  hoelzl@59426  784  nn_integral_suminf[symmetric] dest: sets.sets_into_space)  hoelzl@59426  785 ak2110@68833  786 lemma%unimportant emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \\<^sub>M count_space UNIV) {x} = 1"  hoelzl@59426  787 proof -  hoelzl@62975  788  have [simp]: "\a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ennreal)"  hoelzl@59426  789  by (auto split: split_indicator)  hoelzl@59426  790  show ?thesis  hoelzl@62975  791  by (cases x) (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair)  hoelzl@59426  792 qed  hoelzl@59426  793 ak2110@68833  794 lemma%important emeasure_count_space_prod_eq:  hoelzl@59426  795  fixes A :: "('a \ 'b) set"  hoelzl@59426  796  assumes A: "A \ sets (count_space UNIV \\<^sub>M count_space UNIV)" (is "A \ sets (?A \\<^sub>M ?B)")  hoelzl@59426  797  shows "emeasure (?A \\<^sub>M ?B) A = emeasure (count_space UNIV) A"  ak2110@68833  798 proof%unimportant -  hoelzl@59426  799  { fix A :: "('a \ 'b) set" assume "countable A"  hoelzl@59426  800  then have "emeasure (?A \\<^sub>M ?B) (\a\A. {a}) = (\\<^sup>+a. emeasure (?A \\<^sub>M ?B) {a} \count_space A)"  hoelzl@59426  801  by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def)  hoelzl@59426  802  also have "\ = (\\<^sup>+a. indicator A a \count_space UNIV)"  hoelzl@59426  803  by (subst nn_integral_count_space_indicator) auto  hoelzl@59426  804  finally have "emeasure (?A \\<^sub>M ?B) A = emeasure (count_space UNIV) A"  hoelzl@59426  805  by simp }  hoelzl@59426  806  note * = this  hoelzl@59426  807 hoelzl@59426  808  show ?thesis  hoelzl@59426  809  proof cases  hoelzl@59426  810  assume "finite A" then show ?thesis  hoelzl@59426  811  by (intro * countable_finite)  hoelzl@59426  812  next  hoelzl@59426  813  assume "infinite A"  hoelzl@59426  814  then obtain C where "countable C" and "infinite C" and "C \ A"  hoelzl@59426  815  by (auto dest: infinite_countable_subset')  hoelzl@59426  816  with A have "emeasure (?A \\<^sub>M ?B) C \ emeasure (?A \\<^sub>M ?B) A"  hoelzl@59426  817  by (intro emeasure_mono) auto  hoelzl@59426  818  also have "emeasure (?A \\<^sub>M ?B) C = emeasure (count_space UNIV) C"  wenzelm@61808  819  using \countable C\ by (rule *)  hoelzl@59426  820  finally show ?thesis  hoelzl@62975  821  using \infinite C\ \infinite A\ by (simp add: top_unique)  hoelzl@59426  822  qed  hoelzl@59426  823 qed  hoelzl@59426  824 ak2110@68833  825 lemma%unimportant nn_integral_count_space_prod_eq:  hoelzl@62975  826  "nn_integral (count_space UNIV \\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f"  hoelzl@59426  827  (is "nn_integral ?P f = _")  hoelzl@59426  828 proof cases  hoelzl@59426  829  assume cntbl: "countable {x. f x \ 0}"  hoelzl@62975  830  have [simp]: "\x. card ({x} \ {x. f x \ 0}) = (indicator {x. f x \ 0} x::ennreal)"  hoelzl@59426  831  by (auto split: split_indicator)  hoelzl@59426  832  have [measurable]: "\y. (\x. indicator {y} x) \ borel_measurable ?P"  hoelzl@59426  833  by (rule measurable_discrete_difference[of "\x. 0" _ borel "{y}" "\x. indicator {y} x" for y])  hoelzl@59426  834  (auto intro: sets_Pair)  hoelzl@59426  835 hoelzl@59426  836  have "(\\<^sup>+x. f x \?P) = (\\<^sup>+x. \\<^sup>+x'. f x * indicator {x} x' \count_space {x. f x \ 0} \?P)"  hoelzl@59426  837  by (auto simp add: nn_integral_cmult nn_integral_indicator' intro!: nn_integral_cong split: split_indicator)  hoelzl@59426  838  also have "\ = (\\<^sup>+x. \\<^sup>+x'. f x' * indicator {x'} x \count_space {x. f x \ 0} \?P)"  hoelzl@59426  839  by (auto intro!: nn_integral_cong split: split_indicator)  hoelzl@59426  840  also have "\ = (\\<^sup>+x'. \\<^sup>+x. f x' * indicator {x'} x \?P \count_space {x. f x \ 0})"  hoelzl@59426  841  by (intro nn_integral_count_space_nn_integral cntbl) auto  hoelzl@59426  842  also have "\ = (\\<^sup>+x'. f x' \count_space {x. f x \ 0})"  hoelzl@59426  843  by (intro nn_integral_cong) (auto simp: nn_integral_cmult sets_Pair)  hoelzl@59426  844  finally show ?thesis  hoelzl@59426  845  by (auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)  hoelzl@59426  846 next  hoelzl@59426  847  { fix x assume "f x \ 0"  hoelzl@62975  848  then have "(\r\0. 0 < r \ f x = ennreal r) \ f x = \"  hoelzl@62975  849  by (cases "f x" rule: ennreal_cases) (auto simp: less_le)  hoelzl@62975  850  then have "\n. ennreal (1 / real (Suc n)) \ f x"  hoelzl@59426  851  by (auto elim!: nat_approx_posE intro!: less_imp_le) }  hoelzl@59426  852  note * = this  hoelzl@59426  853 hoelzl@59426  854  assume cntbl: "uncountable {x. f x \ 0}"  hoelzl@59426  855  also have "{x. f x \ 0} = (\n. {x. 1/Suc n \ f x})"  hoelzl@59426  856  using * by auto  hoelzl@59426  857  finally obtain n where "infinite {x. 1/Suc n \ f x}"  hoelzl@59426  858  by (meson countableI_type countable_UN uncountable_infinite)  hoelzl@59426  859  then obtain C where C: "C \ {x. 1/Suc n \ f x}" and "countable C" "infinite C"  hoelzl@59426  860  by (metis infinite_countable_subset')  hoelzl@59426  861 hoelzl@59426  862  have [measurable]: "C \ sets ?P"  wenzelm@61808  863  using sets.countable[OF _ \countable C\, of ?P] by (auto simp: sets_Pair)  hoelzl@59426  864 hoelzl@62975  865  have "(\\<^sup>+x. ennreal (1/Suc n) * indicator C x \?P) \ nn_integral ?P f"  hoelzl@59426  866  using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])  hoelzl@62975  867  moreover have "(\\<^sup>+x. ennreal (1/Suc n) * indicator C x \?P) = \"  hoelzl@62975  868  using \infinite C\ by (simp add: nn_integral_cmult emeasure_count_space_prod_eq ennreal_mult_top)  hoelzl@62975  869  moreover have "(\\<^sup>+x. ennreal (1/Suc n) * indicator C x \count_space UNIV) \ nn_integral (count_space UNIV) f"  hoelzl@59426  870  using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])  hoelzl@62975  871  moreover have "(\\<^sup>+x. ennreal (1/Suc n) * indicator C x \count_space UNIV) = \"  hoelzl@62975  872  using \infinite C\ by (simp add: nn_integral_cmult ennreal_mult_top)  hoelzl@59426  873  ultimately show ?thesis  hoelzl@62975  874  by (simp add: top_unique)  hoelzl@59426  875 qed  hoelzl@59426  876 ak2110@68833  877 lemma%important pair_measure_density:  hoelzl@62975  878  assumes f: "f \ borel_measurable M1"  hoelzl@62975  879  assumes g: "g \ borel_measurable M2"  hoelzl@50003  880  assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"  wenzelm@53015  881  shows "density M1 f \\<^sub>M density M2 g = density (M1 \\<^sub>M M2) (\(x,y). f x * g y)" (is "?L = ?R")  ak2110@68833  882 proof%unimportant (rule measure_eqI)  hoelzl@47694  883  interpret M2: sigma_finite_measure M2 by fact  hoelzl@47694  884  interpret D2: sigma_finite_measure "density M2 g" by fact  hoelzl@47694  885 hoelzl@47694  886  fix A assume A: "A \ sets ?L"  wenzelm@53015  887  with f g have "(\\<^sup>+ x. f x * \\<^sup>+ y. g y * indicator A (x, y) \M2 \M1) =  wenzelm@53015  888  (\\<^sup>+ x. \\<^sup>+ y. f x * g y * indicator A (x, y) \M2 \M1)"  hoelzl@56996  889  by (intro nn_integral_cong_AE)  hoelzl@56996  890  (auto simp add: nn_integral_cmult[symmetric] ac_simps)  hoelzl@50003  891  with A f g show "emeasure ?L A = emeasure ?R A"  hoelzl@56996  892  by (simp add: D2.emeasure_pair_measure emeasure_density nn_integral_density  hoelzl@56996  893  M2.nn_integral_fst[symmetric]  hoelzl@56996  894  cong: nn_integral_cong)  hoelzl@47694  895 qed simp  hoelzl@47694  896 ak2110@68833  897 lemma%unimportant sigma_finite_measure_distr:  hoelzl@47694  898  assumes "sigma_finite_measure (distr M N f)" and f: "f \ measurable M N"  hoelzl@47694  899  shows "sigma_finite_measure M"  hoelzl@40859  900 proof -  hoelzl@47694  901  interpret sigma_finite_measure "distr M N f" by fact  hoelzl@57447  902  from sigma_finite_countable guess A .. note A = this  hoelzl@47694  903  show ?thesis  hoelzl@57447  904  proof  hoelzl@57447  905  show "\A. countable A \ A \ sets M \ \A = space M \ (\a\A. emeasure M a \$$"  hoelzl@57447  906  using A f  hoelzl@57447  907  by (intro exI[of _ "(\a. f - a \ space M)  A"])  hoelzl@57447  908  (auto simp: emeasure_distr set_eq_iff subset_eq intro: measurable_space)  hoelzl@47694  909  qed  hoelzl@38656  910 qed  hoelzl@38656  911 ak2110@68833  912 lemma%unimportant pair_measure_distr:  hoelzl@47694  913  assumes f: "f \ measurable M S" and g: "g \ measurable N T"  hoelzl@50003  914  assumes "sigma_finite_measure (distr N T g)"  wenzelm@53015  915  shows "distr M S f \\<^sub>M distr N T g = distr (M \\<^sub>M N) (S \\<^sub>M T) (\(x, y). (f x, g y))" (is "?P = ?D")  hoelzl@47694  916 proof (rule measure_eqI)  hoelzl@47694  917  interpret T: sigma_finite_measure "distr N T g" by fact  hoelzl@47694  918  interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+  hoelzl@50003  919 hoelzl@47694  920  fix A assume A: "A \ sets ?P"  hoelzl@50003  921  with f g show "emeasure ?P A = emeasure ?D A"  hoelzl@50003  922  by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr  hoelzl@56996  923  T.emeasure_pair_measure_alt nn_integral_distr  hoelzl@56996  924  intro!: nn_integral_cong arg_cong[where f="emeasure N"])  hoelzl@50003  925 qed simp  hoelzl@39097  926 ak2110@68833  927 lemma%important pair_measure_eqI:  hoelzl@50104  928  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"  wenzelm@53015  929  assumes sets: "sets (M1 \\<^sub>M M2) = sets M"  hoelzl@50104  930  assumes emeasure: "\A B. A \ sets M1 \ B \ sets M2 \ emeasure M1 A * emeasure M2 B = emeasure M (A \ B)"  wenzelm@53015  931  shows "M1 \\<^sub>M M2 = M"  ak2110@68833  932 proof%unimportant -  hoelzl@50104  933  interpret M1: sigma_finite_measure M1 by fact  hoelzl@50104  934  interpret M2: sigma_finite_measure M2 by fact  wenzelm@61169  935  interpret pair_sigma_finite M1 M2 ..  hoelzl@50104  936  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this  hoelzl@50104  937  let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}"  wenzelm@53015  938  let ?P = "M1 \\<^sub>M M2"  hoelzl@50104  939  show ?thesis  hoelzl@50104  940  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])  hoelzl@50104  941  show "?E \ Pow (space ?P)"  immler@50244  942  using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)  hoelzl@50104  943  show "sets ?P = sigma_sets (space ?P) ?E"  hoelzl@50104  944  by (simp add: sets_pair_measure space_pair_measure)  hoelzl@50104  945  then show "sets M = sigma_sets (space ?P) ?E"  hoelzl@50104  946  using sets[symmetric] by simp  hoelzl@50104  947  next  hoelzl@50104  948  show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \"  hoelzl@50104  949  using F by (auto simp: space_pair_measure)  hoelzl@50104  950  next  hoelzl@50104  951  fix X assume "X \ ?E"  hoelzl@50104  952  then obtain A B where X[simp]: "X = A \ B" and A: "A \ sets M1" and B: "B \ sets M2" by auto  hoelzl@50104  953  then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"  hoelzl@50104  954  by (simp add: M2.emeasure_pair_measure_Times)  hoelzl@50104  955  also have "\ = emeasure M (A \ B)"  hoelzl@50104  956  using A B emeasure by auto  hoelzl@50104  957  finally show "emeasure ?P X = emeasure M X"  hoelzl@50104  958  by simp  hoelzl@50104  959  qed  hoelzl@50104  960 qed  hoelzl@62975  961 ak2110@68833  962 lemma%important sets_pair_countable:  hoelzl@57025  963  assumes "countable S1" "countable S2"  hoelzl@57025  964  assumes M: "sets M = Pow S1" and N: "sets N = Pow S2"  hoelzl@57025  965  shows "sets (M \\<^sub>M N) = Pow (S1 \ S2)"  ak2110@68833  966 proof%unimportant auto  hoelzl@57025  967  fix x a b assume x: "x \ sets (M \\<^sub>M N)" "(a, b) \ x"  hoelzl@57025  968  from sets.sets_into_space[OF x(1)] x(2)  hoelzl@57025  969  sets_eq_imp_space_eq[of N "count_space S2"] sets_eq_imp_space_eq[of M "count_space S1"] M N  hoelzl@57025  970  show "a \ S1" "b \ S2"  hoelzl@57025  971  by (auto simp: space_pair_measure)  hoelzl@57025  972 next  hoelzl@57025  973  fix X assume X: "X \ S1 \ S2"  hoelzl@57025  974  then have "countable X"  wenzelm@61808  975  by (metis countable_subset \countable S1\ \countable S2\ countable_SIGMA)  hoelzl@57025  976  have "X = (\(a, b)\X. {a} \ {b})" by auto  hoelzl@57025  977  also have "\ \ sets (M \\<^sub>M N)"  hoelzl@57025  978  using X  wenzelm@61808  979  by (safe intro!: sets.countable_UN' \countable X\ subsetI pair_measureI) (auto simp: M N)  hoelzl@57025  980  finally show "X \ sets (M \\<^sub>M N)" .  hoelzl@57025  981 qed  hoelzl@57025  982 ak2110@68833  983 lemma%important pair_measure_countable:  hoelzl@57025  984  assumes "countable S1" "countable S2"  hoelzl@57025  985  shows "count_space S1 \\<^sub>M count_space S2 = count_space (S1 \ S2)"  ak2110@68833  986 proof%unimportant (rule pair_measure_eqI)  hoelzl@57025  987  show "sigma_finite_measure (count_space S1)" "sigma_finite_measure (count_space S2)"  hoelzl@57025  988  using assms by (auto intro!: sigma_finite_measure_count_space_countable)  hoelzl@57025  989  show "sets (count_space S1 \\<^sub>M count_space S2) = sets (count_space (S1 \ S2))"  hoelzl@57025  990  by (subst sets_pair_countable[OF assms]) auto  hoelzl@57025  991 next  hoelzl@57025  992  fix A B assume "A \ sets (count_space S1)" "B \ sets (count_space S2)"  hoelzl@62975  993  then show "emeasure (count_space S1) A * emeasure (count_space S2) B =  hoelzl@57025  994  emeasure (count_space (S1 \ S2)) (A \ B)"  hoelzl@62975  995  by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff ennreal_mult_top ennreal_top_mult)  hoelzl@57025  996 qed  hoelzl@50104  997 ak2110@68833  998 lemma%important nn_integral_fst_count_space:  hoelzl@62975  999  "(\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f"  Andreas@59489  1000  (is "?lhs = ?rhs")  ak2110@68833  1001 proof%unimportant(cases)  Andreas@59489  1002  assume *: "countable {xy. f xy \ 0}"  Andreas@59489  1003  let ?A = "fst  {xy. f xy \ 0}"  Andreas@59489  1004  let ?B = "snd  {xy. f xy \ 0}"  Andreas@59489  1005  from * have [simp]: "countable ?A" "countable ?B" by(rule countable_image)+  Andreas@59489  1006  have "?lhs = (\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space UNIV \count_space ?A)"  Andreas@59489  1007  by(rule nn_integral_count_space_eq)  hoelzl@62975  1008  (auto simp add: nn_integral_0_iff_AE AE_count_space not_le intro: rev_image_eqI)  Andreas@59489  1009  also have "\ = (\\<^sup>+ x. \\<^sup>+ y. f (x, y) \count_space ?B \count_space ?A)"  Andreas@59489  1010  by(intro nn_integral_count_space_eq nn_integral_cong)(auto intro: rev_image_eqI)  Andreas@59489  1011  also have "\ = (\\<^sup>+ xy. f xy \count_space (?A \ ?B))"  Andreas@59489  1012  by(subst sigma_finite_measure.nn_integral_fst)  Andreas@59489  1013  (simp_all add: sigma_finite_measure_count_space_countable pair_measure_countable)  Andreas@59489  1014  also have "\ = ?rhs"  Andreas@59489  1015  by(rule nn_integral_count_space_eq)(auto intro: rev_image_eqI)  Andreas@59489  1016  finally show ?thesis .  Andreas@59489  1017 next  Andreas@59489  1018  { fix xy assume "f xy \ 0"  hoelzl@62975  1019  then have "(\r\0. 0 < r \ f xy = ennreal r) \ f xy = \"  hoelzl@62975  1020  by (cases "f xy" rule: ennreal_cases) (auto simp: less_le)  hoelzl@62975  1021  then have "\n. ennreal (1 / real (Suc n)) \ f xy"  Andreas@59489  1022  by (auto elim!: nat_approx_posE intro!: less_imp_le) }  Andreas@59489  1023  note * = this  Andreas@59489  1024 Andreas@59489  1025  assume cntbl: "uncountable {xy. f xy \ 0}"  Andreas@59489  1026  also have "{xy. f xy \ 0} = (\n. {xy. 1/Suc n \ f xy})"  Andreas@59489  1027  using * by auto  Andreas@59489  1028  finally obtain n where "infinite {xy. 1/Suc n \ f xy}"  Andreas@59489  1029  by (meson countableI_type countable_UN uncountable_infinite)  Andreas@59489  1030  then obtain C where C: "C \ {xy. 1/Suc n \ f xy}" and "countable C" "infinite C"  Andreas@59489  1031  by (metis infinite_countable_subset')  Andreas@59489  1032 hoelzl@62975  1033  have "\ = (\\<^sup>+ xy. ennreal (1 / Suc n) * indicator C xy \count_space UNIV)"  hoelzl@62975  1034  using \infinite C\ by(simp add: nn_integral_cmult ennreal_mult_top)  Andreas@59489  1035  also have "\ \ ?rhs" using C  hoelzl@62975  1036  by(intro nn_integral_mono)(auto split: split_indicator)  hoelzl@62975  1037  finally have "?rhs = \" by (simp add: top_unique)  Andreas@59489  1038  moreover have "?lhs = \"  Andreas@59489  1039  proof(cases "finite (fst  C)")  Andreas@59489  1040  case True  hoelzl@62975  1041  then obtain x C' where x: "x \ fst  C"  Andreas@59489  1042  and C': "C' = fst - {x} \ C"  Andreas@59489  1043  and "infinite C'"  Andreas@59489  1044  using \infinite C\ by(auto elim!: inf_img_fin_domE')  Andreas@59489  1045  from x C C' have **: "C' \ {xy. 1 / Suc n \ f xy}" by auto  Andreas@59489  1046 Andreas@59489  1047  from C' \infinite C'\ have "infinite (snd  C')"  Andreas@59489  1048  by(auto dest!: finite_imageD simp add: inj_on_def)  hoelzl@62975  1049  then have "\ = (\\<^sup>+ y. ennreal (1 / Suc n) * indicator (snd  C') y \count_space UNIV)"  hoelzl@62975  1050  by(simp add: nn_integral_cmult ennreal_mult_top)  hoelzl@62975  1051  also have "\ = (\\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \count_space UNIV)"  Andreas@59489  1052  by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C')  hoelzl@62975  1053  also have "\ = (\\<^sup>+ x'. (\\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \count_space UNIV) * indicator {x} x' \count_space UNIV)"  hoelzl@62975  1054  by(simp add: one_ereal_def[symmetric])  hoelzl@62975  1055  also have "\ \ (\\<^sup>+ x. \\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \count_space UNIV \count_space UNIV)"  hoelzl@62975  1056  by(rule nn_integral_mono)(simp split: split_indicator)  Andreas@59489  1057  also have "\ \ ?lhs" using **  hoelzl@62975  1058  by(intro nn_integral_mono)(auto split: split_indicator)  hoelzl@62975  1059  finally show ?thesis by (simp add: top_unique)  Andreas@59489  1060  next  Andreas@59489  1061  case False  wenzelm@63040  1062  define C' where "C' = fst  C"  hoelzl@62975  1063  have "\ = \\<^sup>+ x. ennreal (1 / Suc n) * indicator C' x \count_space UNIV"  hoelzl@62975  1064  using C'_def False by(simp add: nn_integral_cmult ennreal_mult_top)  hoelzl@62975  1065  also have "\ = \\<^sup>+ x. \\<^sup>+ y. ennreal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \ C} y \count_space UNIV \count_space UNIV"  hoelzl@62083  1066  by(auto simp add: one_ereal_def[symmetric] max_def intro: nn_integral_cong)  hoelzl@62975  1067  also have "\ \ \\<^sup>+ x. \\<^sup>+ y. ennreal (1 / Suc n) * indicator C (x, y) \count_space UNIV \count_space UNIV"  Andreas@59489  1068  by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI)  Andreas@59489  1069  also have "\ \ ?lhs" using C  hoelzl@62975  1070  by(intro nn_integral_mono)(auto split: split_indicator)  hoelzl@62975  1071  finally show ?thesis by (simp add: top_unique)  Andreas@59489  1072  qed  Andreas@59489  1073  ultimately show ?thesis by simp  Andreas@59489  1074 qed  Andreas@59489  1075 Andreas@59491  1076 lemma nn_integral_snd_count_space:  Andreas@59491  1077  "(\\<^sup>+ y. \\<^sup>+ x. f (x, y) \count_space UNIV \count_space UNIV) = integral\<^sup>N (count_space UNIV) f"  Andreas@59491  1078  (is "?lhs = ?rhs")  Andreas@59491  1079 proof -  Andreas@59491  1080  have "?lhs = (\\<^sup>+ y. \\<^sup>+ x. (\(y, x). f (x, y)) (y, x) \count_space UNIV \count_space UNIV)"  Andreas@59491  1081  by(simp)  Andreas@59491  1082  also have "\ = \\<^sup>+ yx. (\(y, x). f (x, y)) yx \count_space UNIV"  Andreas@59491  1083  by(rule nn_integral_fst_count_space)  Andreas@59491  1084  also have "\ = \\<^sup>+ xy. f xy \count_space ((\(x, y). (y, x))  UNIV)"  Andreas@59491  1085  by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])  Andreas@59491  1086  (simp_all add: inj_on_def split_def)  Andreas@59491  1087  also have "\ = ?rhs" by(rule nn_integral_count_space_eq) auto  Andreas@59491  1088  finally show ?thesis .  Andreas@59491  1089 qed  Andreas@59491  1090 ak2110@68833  1091 lemma%unimportant measurable_pair_measure_countable1:  Andreas@60066  1092  assumes "countable A"  Andreas@60066  1093  and [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N K"  Andreas@60066  1094  shows "f \ measurable (count_space A \\<^sub>M N) K"  Andreas@60066  1095 using _ _ assms(1)  Andreas@60066  1096 by(rule measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all  Andreas@60066  1097 ak2110@68833  1098 subsection%important \Product of Borel spaces\  hoelzl@57235  1099 ak2110@68833  1100 lemma%important borel_Times:  hoelzl@57235  1101  fixes A :: "'a::topological_space set" and B :: "'b::topological_space set"  hoelzl@57235  1102  assumes A: "A \ sets borel" and B: "B \ sets borel"  hoelzl@57235  1103  shows "A \ B \ sets borel"  ak2110@68833  1104 proof%unimportant -  hoelzl@57235  1105  have "A \ B = (A\UNIV) \ (UNIV \ B)"  hoelzl@57235  1106  by auto  hoelzl@57235  1107  moreover  hoelzl@57235  1108  { have "A \ sigma_sets UNIV {S. open S}" using A by (simp add: sets_borel)  hoelzl@57235  1109  then have "A\UNIV \ sets borel"  hoelzl@57235  1110  proof (induct A)  hoelzl@57235  1111  case (Basic S) then show ?case  hoelzl@57235  1112  by (auto intro!: borel_open open_Times)  hoelzl@57235  1113  next  hoelzl@57235  1114  case (Compl A)  hoelzl@57235  1115  moreover have *: "(UNIV - A) \ UNIV = UNIV - (A \ UNIV)"  hoelzl@57235  1116  by auto  hoelzl@57235  1117  ultimately show ?case  hoelzl@57235  1118  unfolding * by auto  hoelzl@57235  1119  next  hoelzl@57235  1120  case (Union A)  haftmann@69313  1121  moreover have *: "(\(A  UNIV)) \ UNIV = \((\i. A i \ UNIV)  UNIV)"  hoelzl@57235  1122  by auto  hoelzl@57235  1123  ultimately show ?case  hoelzl@57235  1124  unfolding * by auto  hoelzl@57235  1125  qed simp }  hoelzl@57235  1126  moreover  hoelzl@57235  1127  { have "B \ sigma_sets UNIV {S. open S}" using B by (simp add: sets_borel)  hoelzl@57235  1128  then have "UNIV\B \ sets borel"  hoelzl@57235  1129  proof (induct B)  hoelzl@57235  1130  case (Basic S) then show ?case  hoelzl@57235  1131  by (auto intro!: borel_open open_Times)  hoelzl@57235  1132  next  hoelzl@57235  1133  case (Compl B)  hoelzl@57235  1134  moreover have *: "UNIV \ (UNIV - B) = UNIV - (UNIV \ B)"  hoelzl@57235  1135  by auto  hoelzl@57235  1136  ultimately show ?case  hoelzl@57235  1137  unfolding * by auto  hoelzl@57235  1138  next  hoelzl@57235  1139  case (Union B)  haftmann@69313  1140  moreover have *: "UNIV \ (\(B  UNIV)) = \((\i. UNIV \ B i)  UNIV)"  hoelzl@57235  1141  by auto  hoelzl@57235  1142  ultimately show ?case  hoelzl@57235  1143  unfolding * by auto  hoelzl@57235  1144  qed simp }  hoelzl@57235  1145  ultimately show ?thesis  hoelzl@57235  1146  by auto  hoelzl@57235  1147 qed  hoelzl@57235  1148 ak2110@68833  1149 lemma%unimportant finite_measure_pair_measure:  hoelzl@57235  1150  assumes "finite_measure M" "finite_measure N"  hoelzl@57235  1151  shows "finite_measure (N \\<^sub>M M)"  hoelzl@57235  1152 proof (rule finite_measureI)  hoelzl@57235  1153  interpret M: finite_measure M by fact  hoelzl@57235  1154  interpret N: finite_measure N by fact  hoelzl@57235  1155  show "emeasure (N \\<^sub>M M) (space (N \\<^sub>M M)) \ \"  hoelzl@62975  1156  by (auto simp: space_pair_measure M.emeasure_pair_measure_Times ennreal_mult_eq_top_iff)  hoelzl@57235  1157 qed  hoelzl@57235  1158 hoelzl@62083  1159 end