src/HOL/Analysis/Embed_Measure.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69313 b021008c5397 child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Embed_Measure.thy ``` hoelzl@59092 ` 2` ``` Author: Manuel Eberl, TU München ``` hoelzl@59092 ` 3` hoelzl@62975 ` 4` ``` Defines measure embeddings with injective functions, i.e. lifting a measure on some values ``` hoelzl@62975 ` 5` ``` to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a ``` hoelzl@59092 ` 6` ``` measure on the left part of the sum type 'a + 'b) ``` hoelzl@59092 ` 7` ```*) ``` hoelzl@59092 ` 8` eberlm@69180 ` 9` ```section \Embedding Measure Spaces with a Function\ ``` hoelzl@59092 ` 10` hoelzl@59092 ` 11` ```theory Embed_Measure ``` hoelzl@59092 ` 12` ```imports Binary_Product_Measure ``` hoelzl@59092 ` 13` ```begin ``` hoelzl@59092 ` 14` eberlm@69180 ` 15` ```text \ ``` eberlm@69180 ` 16` ``` Given a measure space on some carrier set \\\ and a function \f\, we can define a push-forward ``` eberlm@69180 ` 17` ``` measure on the carrier set \$f(\Omega)\$ whose \\\-algebra is the one generated by mapping \f\ over ``` eberlm@69180 ` 18` ``` the original sigma algebra. ``` eberlm@69180 ` 19` eberlm@69180 ` 20` ``` This is useful e.\,g.\ when \f\ is injective, i.\,e.\ it is some kind of ``tagging'' function. ``` eberlm@69180 ` 21` ``` For instance, suppose we have some algebraaic datatype of values with various constructors, ``` eberlm@69180 ` 22` ``` including a constructor \RealVal\ for real numbers. Then \embed_measure\ allows us to lift a ``` eberlm@69180 ` 23` ``` measure on real numbers to the appropriate subset of that algebraic datatype. ``` eberlm@69180 ` 24` ```\ ``` eberlm@69180 ` 25` ```definition%important embed_measure :: "'a measure \ ('a \ 'b) \ 'b measure" where ``` hoelzl@62975 ` 26` ``` "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \ sets M} ``` hoelzl@59092 ` 27` ``` (\A. emeasure M (f -` A \ space M))" ``` hoelzl@59092 ` 28` hoelzl@59092 ` 29` ```lemma space_embed_measure: "space (embed_measure M f) = f ` space M" ``` hoelzl@62975 ` 30` ``` unfolding embed_measure_def ``` hoelzl@59092 ` 31` ``` by (subst space_measure_of) (auto dest: sets.sets_into_space) ``` hoelzl@59092 ` 32` hoelzl@59092 ` 33` ```lemma sets_embed_measure': ``` hoelzl@62975 ` 34` ``` assumes inj: "inj_on f (space M)" ``` hoelzl@59092 ` 35` ``` shows "sets (embed_measure M f) = {f ` A |A. A \ sets M}" ``` hoelzl@59092 ` 36` ``` unfolding embed_measure_def ``` hoelzl@59092 ` 37` ```proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI) ``` hoelzl@59092 ` 38` ``` fix s assume "s \ {f ` A |A. A \ sets M}" ``` hoelzl@59092 ` 39` ``` then obtain s' where s'_props: "s = f ` s'" "s' \ sets M" by auto ``` hoelzl@59092 ` 40` ``` hence "f ` space M - s = f ` (space M - s')" using inj ``` hoelzl@59092 ` 41` ``` by (auto dest: inj_onD sets.sets_into_space) ``` hoelzl@59092 ` 42` ``` also have "... \ {f ` A |A. A \ sets M}" using s'_props by auto ``` hoelzl@59092 ` 43` ``` finally show "f ` space M - s \ {f ` A |A. A \ sets M}" . ``` hoelzl@59092 ` 44` ```next ``` hoelzl@59092 ` 45` ``` fix A :: "nat \ _" assume "range A \ {f ` A |A. A \ sets M}" ``` wenzelm@63539 ` 46` ``` then obtain A' where A': "\i. A i = f ` A' i" "\i. A' i \ sets M" ``` hoelzl@59092 ` 47` ``` by (auto simp: subset_eq choice_iff) ``` wenzelm@63539 ` 48` ``` then have "(\x. f ` A' x) = f ` (\x. A' x)" by blast ``` wenzelm@63539 ` 49` ``` with A' show "(\i. A i) \ {f ` A |A. A \ sets M}" ``` haftmann@62343 ` 50` ``` by simp blast ``` hoelzl@59092 ` 51` ```qed (auto dest: sets.sets_into_space) ``` hoelzl@59092 ` 52` hoelzl@59092 ` 53` ```lemma the_inv_into_vimage: ``` hoelzl@59092 ` 54` ``` "inj_on f X \ A \ X \ the_inv_into X f -` A \ (f`X) = f ` A" ``` hoelzl@59092 ` 55` ``` by (auto simp: the_inv_into_f_f) ``` hoelzl@59092 ` 56` hoelzl@59092 ` 57` ```lemma sets_embed_eq_vimage_algebra: ``` hoelzl@59092 ` 58` ``` assumes "inj_on f (space M)" ``` hoelzl@59092 ` 59` ``` shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)" ``` hoelzl@63886 ` 60` ``` by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image ``` hoelzl@59092 ` 61` ``` dest: sets.sets_into_space ``` hoelzl@59092 ` 62` ``` intro!: image_cong the_inv_into_vimage[symmetric]) ``` hoelzl@59092 ` 63` hoelzl@59092 ` 64` ```lemma sets_embed_measure: ``` hoelzl@62975 ` 65` ``` assumes inj: "inj f" ``` hoelzl@59092 ` 66` ``` shows "sets (embed_measure M f) = {f ` A |A. A \ sets M}" ``` hoelzl@59092 ` 67` ``` using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD) ``` hoelzl@59092 ` 68` hoelzl@59092 ` 69` ```lemma in_sets_embed_measure: "A \ sets M \ f ` A \ sets (embed_measure M f)" ``` hoelzl@59092 ` 70` ``` unfolding embed_measure_def ``` hoelzl@59092 ` 71` ``` by (intro in_measure_of) (auto dest: sets.sets_into_space) ``` hoelzl@59092 ` 72` hoelzl@59092 ` 73` ```lemma measurable_embed_measure1: ``` hoelzl@62975 ` 74` ``` assumes g: "(\x. g (f x)) \ measurable M N" ``` hoelzl@59092 ` 75` ``` shows "g \ measurable (embed_measure M f) N" ``` hoelzl@59092 ` 76` ``` unfolding measurable_def ``` hoelzl@59092 ` 77` ```proof safe ``` hoelzl@59092 ` 78` ``` fix A assume "A \ sets N" ``` hoelzl@59092 ` 79` ``` with g have "(\x. g (f x)) -` A \ space M \ sets M" ``` hoelzl@59092 ` 80` ``` by (rule measurable_sets) ``` hoelzl@59092 ` 81` ``` then have "f ` ((\x. g (f x)) -` A \ space M) \ sets (embed_measure M f)" ``` hoelzl@59092 ` 82` ``` by (rule in_sets_embed_measure) ``` hoelzl@59092 ` 83` ``` also have "f ` ((\x. g (f x)) -` A \ space M) = g -` A \ space (embed_measure M f)" ``` hoelzl@59092 ` 84` ``` by (auto simp: space_embed_measure) ``` hoelzl@59092 ` 85` ``` finally show "g -` A \ space (embed_measure M f) \ sets (embed_measure M f)" . ``` hoelzl@59092 ` 86` ```qed (insert measurable_space[OF assms], auto simp: space_embed_measure) ``` hoelzl@59092 ` 87` hoelzl@59092 ` 88` ```lemma measurable_embed_measure2': ``` hoelzl@62975 ` 89` ``` assumes "inj_on f (space M)" ``` hoelzl@59092 ` 90` ``` shows "f \ measurable M (embed_measure M f)" ``` hoelzl@59092 ` 91` ```proof- ``` hoelzl@59092 ` 92` ``` { ``` hoelzl@59092 ` 93` ``` fix A assume A: "A \ sets M" ``` wenzelm@63539 ` 94` ``` also from A have "A = A \ space M" by auto ``` hoelzl@59092 ` 95` ``` also have "... = f -` f ` A \ space M" using A assms ``` hoelzl@59092 ` 96` ``` by (auto dest: inj_onD sets.sets_into_space) ``` hoelzl@59092 ` 97` ``` finally have "f -` f ` A \ space M \ sets M" . ``` hoelzl@59092 ` 98` ``` } ``` hoelzl@59092 ` 99` ``` thus ?thesis using assms unfolding embed_measure_def ``` hoelzl@59092 ` 100` ``` by (intro measurable_measure_of) (auto dest: sets.sets_into_space) ``` hoelzl@59092 ` 101` ```qed ``` hoelzl@59092 ` 102` hoelzl@59092 ` 103` ```lemma measurable_embed_measure2: ``` hoelzl@59092 ` 104` ``` assumes [simp]: "inj f" shows "f \ measurable M (embed_measure M f)" ``` hoelzl@59092 ` 105` ``` by (auto simp: inj_vimage_image_eq embed_measure_def ``` hoelzl@59092 ` 106` ``` intro!: measurable_measure_of dest: sets.sets_into_space) ``` hoelzl@59092 ` 107` hoelzl@59092 ` 108` ```lemma embed_measure_eq_distr': ``` hoelzl@59092 ` 109` ``` assumes "inj_on f (space M)" ``` hoelzl@59092 ` 110` ``` shows "embed_measure M f = distr M (embed_measure M f) f" ``` hoelzl@59092 ` 111` ```proof- ``` hoelzl@62975 ` 112` ``` have "distr M (embed_measure M f) f = ``` hoelzl@59092 ` 113` ``` measure_of (f ` space M) {f ` A |A. A \ sets M} ``` hoelzl@59092 ` 114` ``` (\A. emeasure M (f -` A \ space M))" unfolding distr_def ``` hoelzl@59092 ` 115` ``` by (simp add: space_embed_measure sets_embed_measure'[OF assms]) ``` hoelzl@59092 ` 116` ``` also have "... = embed_measure M f" unfolding embed_measure_def .. ``` hoelzl@59092 ` 117` ``` finally show ?thesis .. ``` hoelzl@59092 ` 118` ```qed ``` hoelzl@59092 ` 119` hoelzl@59092 ` 120` ```lemma embed_measure_eq_distr: ``` hoelzl@59092 ` 121` ``` "inj f \ embed_measure M f = distr M (embed_measure M f) f" ``` hoelzl@59092 ` 122` ``` by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD) ``` hoelzl@59092 ` 123` Andreas@60065 ` 124` ```lemma nn_integral_embed_measure': ``` Andreas@60065 ` 125` ``` "inj_on f (space M) \ g \ borel_measurable (embed_measure M f) \ ``` Andreas@60065 ` 126` ``` nn_integral (embed_measure M f) g = nn_integral M (\x. g (f x))" ``` Andreas@60065 ` 127` ``` apply (subst embed_measure_eq_distr', simp) ``` Andreas@60065 ` 128` ``` apply (subst nn_integral_distr) ``` Andreas@60065 ` 129` ``` apply (simp_all add: measurable_embed_measure2') ``` Andreas@60065 ` 130` ``` done ``` Andreas@60065 ` 131` hoelzl@59092 ` 132` ```lemma nn_integral_embed_measure: ``` hoelzl@59092 ` 133` ``` "inj f \ g \ borel_measurable (embed_measure M f) \ ``` hoelzl@59092 ` 134` ``` nn_integral (embed_measure M f) g = nn_integral M (\x. g (f x))" ``` Andreas@60065 ` 135` ``` by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp ``` hoelzl@59092 ` 136` hoelzl@59092 ` 137` ```lemma emeasure_embed_measure': ``` hoelzl@59092 ` 138` ``` assumes "inj_on f (space M)" "A \ sets (embed_measure M f)" ``` hoelzl@59092 ` 139` ``` shows "emeasure (embed_measure M f) A = emeasure M (f -` A \ space M)" ``` hoelzl@59092 ` 140` ``` by (subst embed_measure_eq_distr'[OF assms(1)]) ``` hoelzl@59092 ` 141` ``` (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)]) ``` hoelzl@59092 ` 142` hoelzl@59092 ` 143` ```lemma emeasure_embed_measure: ``` hoelzl@59092 ` 144` ``` assumes "inj f" "A \ sets (embed_measure M f)" ``` hoelzl@59092 ` 145` ``` shows "emeasure (embed_measure M f) A = emeasure M (f -` A \ space M)" ``` hoelzl@59092 ` 146` ``` using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD) ``` hoelzl@59092 ` 147` hoelzl@62975 ` 148` ```lemma embed_measure_comp: ``` hoelzl@59092 ` 149` ``` assumes [simp]: "inj f" "inj g" ``` hoelzl@59092 ` 150` ``` shows "embed_measure (embed_measure M f) g = embed_measure M (g \ f)" ``` hoelzl@59092 ` 151` ```proof- ``` hoelzl@59092 ` 152` ``` have [simp]: "inj (\x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp) ``` hoelzl@59092 ` 153` ``` note measurable_embed_measure2[measurable] ``` hoelzl@62975 ` 154` ``` have "embed_measure (embed_measure M f) g = ``` hoelzl@59092 ` 155` ``` distr M (embed_measure (embed_measure M f) g) (g \ f)" ``` hoelzl@62975 ` 156` ``` by (subst (1 2) embed_measure_eq_distr) ``` hoelzl@59092 ` 157` ``` (simp_all add: distr_distr sets_embed_measure cong: distr_cong) ``` hoelzl@59092 ` 158` ``` also have "... = embed_measure M (g \ f)" ``` hoelzl@59092 ` 159` ``` by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong) ``` hoelzl@62975 ` 160` ``` (auto simp: sets_embed_measure o_def image_image[symmetric] ``` hoelzl@59092 ` 161` ``` intro: inj_comp cong: distr_cong) ``` hoelzl@59092 ` 162` ``` finally show ?thesis . ``` hoelzl@59092 ` 163` ```qed ``` hoelzl@59092 ` 164` hoelzl@59092 ` 165` ```lemma sigma_finite_embed_measure: ``` hoelzl@59092 ` 166` ``` assumes "sigma_finite_measure M" and inj: "inj f" ``` hoelzl@59092 ` 167` ``` shows "sigma_finite_measure (embed_measure M f)" ``` wenzelm@60580 ` 168` ```proof - ``` hoelzl@59092 ` 169` ``` from assms(1) interpret sigma_finite_measure M . ``` hoelzl@59092 ` 170` ``` from sigma_finite_countable obtain A where ``` hoelzl@59092 ` 171` ``` A_props: "countable A" "A \ sets M" "\A = space M" "\X. X\A \ emeasure M X \ \" by blast ``` nipkow@67399 ` 172` ``` from A_props have "countable ((`) f`A)" by auto ``` wenzelm@60580 ` 173` ``` moreover ``` nipkow@67399 ` 174` ``` from inj and A_props have "(`) f`A \ sets (embed_measure M f)" ``` wenzelm@60580 ` 175` ``` by (auto simp: sets_embed_measure) ``` wenzelm@60580 ` 176` ``` moreover ``` nipkow@67399 ` 177` ``` from A_props and inj have "\((`) f`A) = space (embed_measure M f)" ``` wenzelm@60580 ` 178` ``` by (auto simp: space_embed_measure intro!: imageI) ``` wenzelm@60580 ` 179` ``` moreover ``` nipkow@67399 ` 180` ``` from A_props and inj have "\a\(`) f ` A. emeasure (embed_measure M f) a \ \" ``` wenzelm@60580 ` 181` ``` by (intro ballI, subst emeasure_embed_measure) ``` wenzelm@60580 ` 182` ``` (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure) ``` wenzelm@61169 ` 183` ``` ultimately show ?thesis by - (standard, blast) ``` hoelzl@59092 ` 184` ```qed ``` hoelzl@59092 ` 185` Andreas@60065 ` 186` ```lemma embed_measure_count_space': ``` Andreas@60065 ` 187` ``` "inj_on f A \ embed_measure (count_space A) f = count_space (f`A)" ``` hoelzl@59092 ` 188` ``` apply (subst distr_bij_count_space[of f A "f`A", symmetric]) ``` hoelzl@59092 ` 189` ``` apply (simp add: inj_on_def bij_betw_def) ``` Andreas@60065 ` 190` ``` apply (subst embed_measure_eq_distr') ``` hoelzl@59092 ` 191` ``` apply simp ``` Andreas@60065 ` 192` ``` apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff) ``` hoelzl@59092 ` 193` ``` apply (subst (1 2) emeasure_distr) ``` Andreas@60065 ` 194` ``` apply (auto simp: space_embed_measure sets_embed_measure') ``` hoelzl@59092 ` 195` ``` done ``` hoelzl@59092 ` 196` hoelzl@62975 ` 197` ```lemma embed_measure_count_space: ``` Andreas@60065 ` 198` ``` "inj f \ embed_measure (count_space A) f = count_space (f`A)" ``` Andreas@60065 ` 199` ``` by(rule embed_measure_count_space')(erule subset_inj_on, simp) ``` Andreas@60065 ` 200` hoelzl@59092 ` 201` ```lemma sets_embed_measure_alt: ``` nipkow@67399 ` 202` ``` "inj f \ sets (embed_measure M f) = ((`) f) ` sets M" ``` hoelzl@59092 ` 203` ``` by (auto simp: sets_embed_measure) ``` hoelzl@59092 ` 204` hoelzl@59092 ` 205` ```lemma emeasure_embed_measure_image': ``` hoelzl@59092 ` 206` ``` assumes "inj_on f (space M)" "X \ sets M" ``` hoelzl@59092 ` 207` ``` shows "emeasure (embed_measure M f) (f`X) = emeasure M X" ``` hoelzl@59092 ` 208` ```proof- ``` hoelzl@59092 ` 209` ``` from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \ space M)" ``` hoelzl@59092 ` 210` ``` by (subst emeasure_embed_measure') (auto simp: sets_embed_measure') ``` hoelzl@59092 ` 211` ``` also from assms have "f -` f ` X \ space M = X" by (auto dest: inj_onD sets.sets_into_space) ``` hoelzl@59092 ` 212` ``` finally show ?thesis . ``` hoelzl@59092 ` 213` ```qed ``` hoelzl@59092 ` 214` hoelzl@59092 ` 215` ```lemma emeasure_embed_measure_image: ``` hoelzl@59092 ` 216` ``` "inj f \ X \ sets M \ emeasure (embed_measure M f) (f`X) = emeasure M X" ``` hoelzl@59092 ` 217` ``` by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq) ``` hoelzl@59092 ` 218` hoelzl@59092 ` 219` ```lemma embed_measure_eq_iff: ``` hoelzl@59092 ` 220` ``` assumes "inj f" ``` hoelzl@59092 ` 221` ``` shows "embed_measure A f = embed_measure B f \ A = B" (is "?M = ?N \ _") ``` hoelzl@59092 ` 222` ```proof ``` nipkow@67399 ` 223` ``` from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD) ``` hoelzl@59092 ` 224` ``` assume asm: "?M = ?N" ``` hoelzl@59092 ` 225` ``` hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp ``` hoelzl@59092 ` 226` ``` with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt) ``` hoelzl@59092 ` 227` ``` moreover { ``` hoelzl@59092 ` 228` ``` fix X assume "X \ sets A" ``` hoelzl@59092 ` 229` ``` from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp ``` hoelzl@62975 ` 230` ``` with \X \ sets A\ and \sets A = sets B\ and assms ``` hoelzl@59092 ` 231` ``` have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image) ``` hoelzl@59092 ` 232` ``` } ``` hoelzl@59092 ` 233` ``` ultimately show "A = B" by (rule measure_eqI) ``` hoelzl@59092 ` 234` ```qed simp ``` hoelzl@59092 ` 235` hoelzl@59092 ` 236` ```lemma the_inv_into_in_Pi: "inj_on f A \ the_inv_into A f \ f ` A \ A" ``` hoelzl@59092 ` 237` ``` by (auto simp: the_inv_into_f_f) ``` hoelzl@59092 ` 238` hoelzl@59092 ` 239` ```lemma map_prod_image: "map_prod f g ` (A \ B) = (f`A) \ (g`B)" ``` hoelzl@59092 ` 240` ``` using map_prod_surj_on[OF refl refl] . ``` hoelzl@59092 ` 241` hoelzl@59092 ` 242` ```lemma map_prod_vimage: "map_prod f g -` (A \ B) = (f-`A) \ (g-`B)" ``` hoelzl@59092 ` 243` ``` by auto ``` hoelzl@59092 ` 244` hoelzl@59092 ` 245` ```lemma embed_measure_prod: ``` hoelzl@59092 ` 246` ``` assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N" ``` hoelzl@59092 ` 247` ``` shows "embed_measure M f \\<^sub>M embed_measure N g = embed_measure (M \\<^sub>M N) (\(x, y). (f x, g y))" ``` hoelzl@59092 ` 248` ``` (is "?L = _") ``` hoelzl@59092 ` 249` ``` unfolding map_prod_def[symmetric] ``` hoelzl@59092 ` 250` ```proof (rule pair_measure_eqI) ``` hoelzl@59092 ` 251` ``` have fg[simp]: "\A. inj_on (map_prod f g) A" "\A. inj_on f A" "\A. inj_on g A" ``` hoelzl@59092 ` 252` ``` using f g by (auto simp: inj_on_def) ``` hoelzl@62975 ` 253` hoelzl@63333 ` 254` ``` note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del] ``` hoelzl@63333 ` 255` ``` ccSUP_insert[simp del] ``` hoelzl@59092 ` 256` ``` show sets: "sets ?L = sets (embed_measure (M \\<^sub>M N) (map_prod f g))" ``` hoelzl@59092 ` 257` ``` unfolding map_prod_def[symmetric] ``` hoelzl@59092 ` 258` ``` apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra ``` hoelzl@59092 ` 259` ``` cong: vimage_algebra_cong) ``` hoelzl@63333 ` 260` ``` apply (subst sets_vimage_Sup_eq[where Y="space (M \\<^sub>M N)"]) ``` hoelzl@59092 ` 261` ``` apply (simp_all add: space_pair_measure[symmetric]) ``` hoelzl@59092 ` 262` ``` apply (auto simp add: the_inv_into_f_f ``` hoelzl@59092 ` 263` ``` simp del: map_prod_simp ``` hoelzl@59092 ` 264` ``` del: prod_fun_imageE) [] ``` hoelzl@63333 ` 265` ``` apply auto [] ``` hoelzl@63333 ` 266` ``` apply (subst image_insert) ``` hoelzl@63333 ` 267` ``` apply simp ``` hoelzl@59092 ` 268` ``` apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq) ``` hoelzl@59092 ` 269` ``` apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure) ``` hoelzl@59092 ` 270` ``` apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq ``` hoelzl@59092 ` 271` ``` space_pair_measure[symmetric] map_prod_image[symmetric]) ``` hoelzl@63333 ` 272` ``` apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong) ``` hoelzl@59092 ` 273` ``` apply (auto simp: map_prod_image the_inv_into_f_f ``` hoelzl@59092 ` 274` ``` simp del: map_prod_simp del: prod_fun_imageE) ``` hoelzl@59092 ` 275` ``` apply (simp_all add: the_inv_into_f_f space_pair_measure) ``` hoelzl@59092 ` 276` ``` done ``` hoelzl@59092 ` 277` hoelzl@59092 ` 278` ``` note measurable_embed_measure2[measurable] ``` hoelzl@59092 ` 279` ``` fix A B assume AB: "A \ sets (embed_measure M f)" "B \ sets (embed_measure N g)" ``` hoelzl@59092 ` 280` ``` moreover have "f -` A \ g -` B \ space (M \\<^sub>M N) = (f -` A \ space M) \ (g -` B \ space N)" ``` hoelzl@59092 ` 281` ``` by (auto simp: space_pair_measure) ``` hoelzl@59092 ` 282` ``` ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B = ``` hoelzl@59092 ` 283` ``` emeasure (embed_measure (M \\<^sub>M N) (map_prod f g)) (A \ B)" ``` hoelzl@59092 ` 284` ``` by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure ``` hoelzl@59092 ` 285` ``` sigma_finite_measure.emeasure_pair_measure_Times) ``` hoelzl@59092 ` 286` ```qed (insert assms, simp_all add: sigma_finite_embed_measure) ``` hoelzl@59092 ` 287` hoelzl@63333 ` 288` ```lemma mono_embed_measure: ``` hoelzl@63333 ` 289` ``` "space M = space M' \ sets M \ sets M' \ sets (embed_measure M f) \ sets (embed_measure M' f)" ``` hoelzl@63333 ` 290` ``` unfolding embed_measure_def ``` hoelzl@63333 ` 291` ``` apply (subst (1 2) sets_measure_of) ``` hoelzl@63333 ` 292` ``` apply (blast dest: sets.sets_into_space) ``` hoelzl@63333 ` 293` ``` apply (blast dest: sets.sets_into_space) ``` hoelzl@63333 ` 294` ``` apply simp ``` hoelzl@63333 ` 295` ``` apply (intro sigma_sets_mono') ``` hoelzl@63333 ` 296` ``` apply safe ``` hoelzl@63333 ` 297` ``` apply (simp add: subset_eq) ``` hoelzl@63333 ` 298` ``` apply metis ``` hoelzl@63333 ` 299` ``` done ``` hoelzl@63333 ` 300` hoelzl@59092 ` 301` ```lemma density_embed_measure: ``` hoelzl@59092 ` 302` ``` assumes inj: "inj f" and Mg[measurable]: "g \ borel_measurable (embed_measure M f)" ``` hoelzl@59092 ` 303` ``` shows "density (embed_measure M f) g = embed_measure (density M (g \ f)) f" (is "?M1 = ?M2") ``` hoelzl@59092 ` 304` ```proof (rule measure_eqI) ``` hoelzl@59092 ` 305` ``` fix X assume X: "X \ sets ?M1" ``` hoelzl@62975 ` 306` ``` from inj have Mf[measurable]: "f \ measurable M (embed_measure M f)" ``` hoelzl@59092 ` 307` ``` by (rule measurable_embed_measure2) ``` hoelzl@62975 ` 308` ``` from Mg and X have "emeasure ?M1 X = \\<^sup>+ x. g x * indicator X x \embed_measure M f" ``` hoelzl@59092 ` 309` ``` by (subst emeasure_density) simp_all ``` hoelzl@59092 ` 310` ``` also from X have "... = \\<^sup>+ x. g (f x) * indicator X (f x) \M" ``` hoelzl@62975 ` 311` ``` by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto ``` hoelzl@59092 ` 312` ``` also have "... = \\<^sup>+ x. g (f x) * indicator (f -` X \ space M) x \M" ``` hoelzl@59092 ` 313` ``` by (intro nn_integral_cong) (auto split: split_indicator) ``` hoelzl@59092 ` 314` ``` also from X have "... = emeasure (density M (g \ f)) (f -` X \ space M)" ``` hoelzl@59092 ` 315` ``` by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf]) ``` hoelzl@62975 ` 316` ``` also from X and inj have "... = emeasure ?M2 X" ``` hoelzl@59092 ` 317` ``` by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure) ``` hoelzl@59092 ` 318` ``` finally show "emeasure ?M1 X = emeasure ?M2 X" . ``` hoelzl@59092 ` 319` ```qed (simp_all add: sets_embed_measure inj) ``` hoelzl@59092 ` 320` hoelzl@59092 ` 321` ```lemma density_embed_measure': ``` hoelzl@59092 ` 322` ``` assumes inj: "inj f" and inv: "\x. f' (f x) = x" and Mg[measurable]: "g \ borel_measurable M" ``` hoelzl@59092 ` 323` ``` shows "density (embed_measure M f) (g \ f') = embed_measure (density M g) f" ``` hoelzl@59092 ` 324` ```proof- ``` hoelzl@59092 ` 325` ``` have "density (embed_measure M f) (g \ f') = embed_measure (density M (g \ f' \ f)) f" ``` hoelzl@59092 ` 326` ``` by (rule density_embed_measure[OF inj]) ``` hoelzl@62975 ` 327` ``` (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, ``` hoelzl@59092 ` 328` ``` rule inv, rule measurable_ident_sets, simp, rule Mg) ``` hoelzl@59092 ` 329` ``` also have "density M (g \ f' \ f) = density M g" ``` hoelzl@59092 ` 330` ``` by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv) ``` hoelzl@59092 ` 331` ``` finally show ?thesis . ``` hoelzl@59092 ` 332` ```qed ``` hoelzl@59092 ` 333` hoelzl@59092 ` 334` ```lemma inj_on_image_subset_iff: ``` hoelzl@59092 ` 335` ``` assumes "inj_on f C" "A \ C" "B \ C" ``` hoelzl@59092 ` 336` ``` shows "f ` A \ f ` B \ A \ B" ``` hoelzl@59092 ` 337` ```proof (intro iffI subsetI) ``` hoelzl@59092 ` 338` ``` fix x assume A: "f ` A \ f ` B" and B: "x \ A" ``` hoelzl@59092 ` 339` ``` from B have "f x \ f ` A" by blast ``` hoelzl@59092 ` 340` ``` with A have "f x \ f ` B" by blast ``` hoelzl@59092 ` 341` ``` then obtain y where "f x = f y" and "y \ B" by blast ``` hoelzl@59092 ` 342` ``` with assms and B have "x = y" by (auto dest: inj_onD) ``` wenzelm@61808 ` 343` ``` with \y \ B\ show "x \ B" by simp ``` hoelzl@59092 ` 344` ```qed auto ``` hoelzl@62975 ` 345` hoelzl@59092 ` 346` hoelzl@59092 ` 347` ```lemma AE_embed_measure': ``` hoelzl@59092 ` 348` ``` assumes inj: "inj_on f (space M)" ``` hoelzl@59092 ` 349` ``` shows "(AE x in embed_measure M f. P x) \ (AE x in M. P (f x))" ``` hoelzl@59092 ` 350` ```proof ``` hoelzl@59092 ` 351` ``` let ?M = "embed_measure M f" ``` hoelzl@59092 ` 352` ``` assume "AE x in ?M. P x" ``` hoelzl@59092 ` 353` ``` then obtain A where A_props: "A \ sets ?M" "emeasure ?M A = 0" "{x\space ?M. \P x} \ A" ``` hoelzl@59092 ` 354` ``` by (force elim: AE_E) ``` hoelzl@59092 ` 355` ``` then obtain A' where A'_props: "A = f ` A'" "A' \ sets M" by (auto simp: sets_embed_measure' inj) ``` hoelzl@62975 ` 356` ``` moreover have B: "{x\space ?M. \P x} = f ` {x\space M. \P (f x)}" ``` hoelzl@59092 ` 357` ``` by (auto simp: inj space_embed_measure) ``` hoelzl@59092 ` 358` ``` from A_props(3) have "{x\space M. \P (f x)} \ A'" ``` hoelzl@59092 ` 359` ``` by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj]) ``` hoelzl@59092 ` 360` ``` (insert A'_props, auto dest: sets.sets_into_space) ``` hoelzl@59092 ` 361` ``` moreover from A_props A'_props have "emeasure M A' = 0" ``` hoelzl@59092 ` 362` ``` by (simp add: emeasure_embed_measure_image' inj) ``` hoelzl@59092 ` 363` ``` ultimately show "AE x in M. P (f x)" by (intro AE_I) ``` hoelzl@59092 ` 364` ```next ``` hoelzl@59092 ` 365` ``` let ?M = "embed_measure M f" ``` hoelzl@59092 ` 366` ``` assume "AE x in M. P (f x)" ``` hoelzl@59092 ` 367` ``` then obtain A where A_props: "A \ sets M" "emeasure M A = 0" "{x\space M. \P (f x)} \ A" ``` hoelzl@59092 ` 368` ``` by (force elim: AE_E) ``` hoelzl@59092 ` 369` ``` hence "f`A \ sets ?M" "emeasure ?M (f`A) = 0" "{x\space ?M. \P x} \ f`A" ``` hoelzl@59092 ` 370` ``` by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj) ``` hoelzl@59092 ` 371` ``` thus "AE x in ?M. P x" by (intro AE_I) ``` hoelzl@59092 ` 372` ```qed ``` hoelzl@59092 ` 373` hoelzl@59092 ` 374` ```lemma AE_embed_measure: ``` hoelzl@59092 ` 375` ``` assumes inj: "inj f" ``` hoelzl@59092 ` 376` ``` shows "(AE x in embed_measure M f. P x) \ (AE x in M. P (f x))" ``` hoelzl@59092 ` 377` ``` using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD) ``` hoelzl@59092 ` 378` Andreas@60065 ` 379` ```lemma nn_integral_monotone_convergence_SUP_countable: ``` hoelzl@62975 ` 380` ``` fixes f :: "'a \ 'b \ ennreal" ``` Andreas@60065 ` 381` ``` assumes nonempty: "Y \ {}" ``` nipkow@67399 ` 382` ``` and chain: "Complete_Partial_Order.chain (\) (f ` Y)" ``` Andreas@60065 ` 383` ``` and countable: "countable B" ``` haftmann@69260 ` 384` ``` shows "(\\<^sup>+ x. (SUP i\Y. f i x) \count_space B) = (SUP i\Y. (\\<^sup>+ x. f i x \count_space B))" ``` Andreas@60065 ` 385` ``` (is "?lhs = ?rhs") ``` Andreas@60065 ` 386` ```proof - ``` Andreas@60065 ` 387` ``` let ?f = "(\i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)" ``` haftmann@69260 ` 388` ``` have "?lhs = \\<^sup>+ x. (SUP i\Y. f i (from_nat_into B (to_nat_on B x))) \count_space B" ``` Andreas@60065 ` 389` ``` by(rule nn_integral_cong)(simp add: countable) ``` haftmann@69260 ` 390` ``` also have "\ = \\<^sup>+ x. (SUP i\Y. f i (from_nat_into B x)) \count_space (to_nat_on B ` B)" ``` Andreas@60065 ` 391` ``` by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) ``` haftmann@69260 ` 392` ``` also have "\ = \\<^sup>+ x. (SUP i\Y. ?f i x) \count_space UNIV" ``` hoelzl@62975 ` 393` ``` by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty) ``` haftmann@69260 ` 394` ``` also have "\ = (SUP i\Y. \\<^sup>+ x. ?f i x \count_space UNIV)" ``` Andreas@60065 ` 395` ``` proof(rule nn_integral_monotone_convergence_SUP_nat) ``` nipkow@67399 ` 396` ``` show "Complete_Partial_Order.chain (\) (?f ` Y)" ``` Andreas@60065 ` 397` ``` by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD) ``` hoelzl@62975 ` 398` ``` qed fact ``` haftmann@69260 ` 399` ``` also have "\ = (SUP i\Y. \\<^sup>+ x. f i (from_nat_into B x) \count_space (to_nat_on B ` B))" ``` Andreas@60065 ` 400` ``` by(simp add: nn_integral_count_space_indicator) ``` haftmann@69260 ` 401` ``` also have "\ = (SUP i\Y. \\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \count_space B)" ``` Andreas@60065 ` 402` ``` by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) ``` hoelzl@62975 ` 403` ``` also have "\ = ?rhs" ``` haftmann@69313 ` 404` ``` by(intro arg_cong2[where f = "\A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable) ``` Andreas@60065 ` 405` ``` finally show ?thesis . ``` Andreas@60065 ` 406` ```qed ``` Andreas@60065 ` 407` hoelzl@59092 ` 408` ```end ```