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