src/HOL/Probability/Embed_Measure.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 60065 390de6d3a7b8
child 60580 7e741e22d7fc
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (*  Title:      HOL/Probability/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 {* Embed Measure Spaces with a Function *}
    10 
    11 theory Embed_Measure
    12 imports Binary_Product_Measure
    13 begin
    14 
    15 definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    16   "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M} 
    17                            (\<lambda>A. emeasure M (f -` A \<inter> space M))"
    18 
    19 lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
    20   unfolding embed_measure_def 
    21   by (subst space_measure_of) (auto dest: sets.sets_into_space)
    22 
    23 lemma sets_embed_measure':
    24   assumes inj: "inj_on f (space M)" 
    25   shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    26   unfolding embed_measure_def
    27 proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
    28   fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
    29   then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
    30   hence "f ` space M - s = f ` (space M - s')" using inj
    31     by (auto dest: inj_onD sets.sets_into_space)
    32   also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
    33   finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
    34 next
    35   fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
    36   then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
    37     by (auto simp: subset_eq choice_iff)
    38   moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
    39   ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
    40 qed (auto dest: sets.sets_into_space)
    41 
    42 lemma the_inv_into_vimage:
    43   "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
    44   by (auto simp: the_inv_into_f_f)
    45 
    46 lemma sets_embed_eq_vimage_algebra:
    47   assumes "inj_on f (space M)"
    48   shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
    49   by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
    50            dest: sets.sets_into_space
    51            intro!: image_cong the_inv_into_vimage[symmetric])
    52 
    53 lemma sets_embed_measure:
    54   assumes inj: "inj f" 
    55   shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    56   using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
    57 
    58 lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
    59   unfolding embed_measure_def
    60   by (intro in_measure_of) (auto dest: sets.sets_into_space)
    61 
    62 lemma measurable_embed_measure1:
    63   assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N" 
    64   shows "g \<in> measurable (embed_measure M f) N"
    65   unfolding measurable_def
    66 proof safe
    67   fix A assume "A \<in> sets N"
    68   with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
    69     by (rule measurable_sets)
    70   then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
    71     by (rule in_sets_embed_measure)
    72   also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
    73     by (auto simp: space_embed_measure)
    74   finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
    75 qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
    76 
    77 lemma measurable_embed_measure2':
    78   assumes "inj_on f (space M)" 
    79   shows "f \<in> measurable M (embed_measure M f)"
    80 proof-
    81   {
    82     fix A assume A: "A \<in> sets M"
    83     also from this have "A = A \<inter> space M" by auto
    84     also have "... = f -` f ` A \<inter> space M" using A assms
    85       by (auto dest: inj_onD sets.sets_into_space)
    86     finally have "f -` f ` A \<inter> space M \<in> sets M" .
    87   }
    88   thus ?thesis using assms unfolding embed_measure_def
    89     by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    90 qed
    91 
    92 lemma measurable_embed_measure2:
    93   assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
    94   by (auto simp: inj_vimage_image_eq embed_measure_def
    95            intro!: measurable_measure_of dest: sets.sets_into_space)
    96 
    97 lemma embed_measure_eq_distr':
    98   assumes "inj_on f (space M)"
    99   shows "embed_measure M f = distr M (embed_measure M f) f"
   100 proof-
   101   have "distr M (embed_measure M f) f = 
   102             measure_of (f ` space M) {f ` A |A. A \<in> sets M}
   103                        (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
   104       by (simp add: space_embed_measure sets_embed_measure'[OF assms])
   105   also have "... = embed_measure M f" unfolding embed_measure_def ..
   106   finally show ?thesis ..
   107 qed
   108 
   109 lemma embed_measure_eq_distr:
   110     "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
   111   by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
   112 
   113 lemma nn_integral_embed_measure':
   114   "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   115   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   116   apply (subst embed_measure_eq_distr', simp)
   117   apply (subst nn_integral_distr)
   118   apply (simp_all add: measurable_embed_measure2')
   119   done
   120 
   121 lemma nn_integral_embed_measure:
   122   "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   123   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   124   by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
   125 
   126 lemma emeasure_embed_measure':
   127     assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
   128     shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   129   by (subst embed_measure_eq_distr'[OF assms(1)])
   130      (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
   131 
   132 lemma emeasure_embed_measure:
   133     assumes "inj f" "A \<in> sets (embed_measure M f)"
   134     shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   135  using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
   136 
   137 lemma embed_measure_comp: 
   138   assumes [simp]: "inj f" "inj g"
   139   shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
   140 proof-
   141   have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
   142   note measurable_embed_measure2[measurable]
   143   have "embed_measure (embed_measure M f) g = 
   144             distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
   145       by (subst (1 2) embed_measure_eq_distr) 
   146          (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
   147   also have "... = embed_measure M (g \<circ> f)"
   148       by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
   149          (auto simp: sets_embed_measure o_def image_image[symmetric] 
   150                intro: inj_comp cong: distr_cong)
   151   finally show ?thesis .
   152 qed
   153 
   154 lemma sigma_finite_embed_measure:
   155   assumes "sigma_finite_measure M" and inj: "inj f"
   156   shows "sigma_finite_measure (embed_measure M f)"
   157 proof
   158   case goal1
   159   from assms(1) interpret sigma_finite_measure M .
   160   from sigma_finite_countable obtain A where
   161       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
   162   show ?case
   163   proof (intro exI[of _ "op ` f`A"] conjI allI)
   164     from A_props show "countable (op ` f`A)" by auto
   165     from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
   166       by (auto simp: sets_embed_measure)
   167     from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
   168       by (auto simp: space_embed_measure intro!: imageI)
   169     from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   170       by (intro ballI, subst emeasure_embed_measure)
   171          (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   172   qed
   173 qed
   174 
   175 lemma embed_measure_count_space':
   176     "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   177   apply (subst distr_bij_count_space[of f A "f`A", symmetric])
   178   apply (simp add: inj_on_def bij_betw_def)
   179   apply (subst embed_measure_eq_distr')
   180   apply simp
   181   apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
   182   apply (subst (1 2) emeasure_distr)
   183   apply (auto simp: space_embed_measure sets_embed_measure')
   184   done
   185 
   186 lemma embed_measure_count_space: 
   187     "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   188   by(rule embed_measure_count_space')(erule subset_inj_on, simp)
   189 
   190 lemma sets_embed_measure_alt:
   191     "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
   192   by (auto simp: sets_embed_measure)
   193 
   194 lemma emeasure_embed_measure_image':
   195   assumes "inj_on f (space M)" "X \<in> sets M"
   196   shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
   197 proof-
   198   from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
   199     by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
   200   also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
   201   finally show ?thesis .
   202 qed
   203 
   204 lemma emeasure_embed_measure_image:
   205     "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
   206   by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
   207 
   208 lemma embed_measure_eq_iff:
   209   assumes "inj f"
   210   shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
   211 proof
   212   from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
   213   assume asm: "?M = ?N"
   214   hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
   215   with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
   216   moreover {
   217     fix X assume "X \<in> sets A"
   218     from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
   219     with `X \<in> sets A` and `sets A = sets B` and assms 
   220         have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
   221   }
   222   ultimately show "A = B" by (rule measure_eqI)
   223 qed simp
   224 
   225 lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
   226   by (auto simp: the_inv_into_f_f)
   227 
   228 lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
   229   using map_prod_surj_on[OF refl refl] .
   230 
   231 lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
   232   by auto
   233 
   234 lemma embed_measure_prod:
   235   assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
   236   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))"
   237     (is "?L = _")
   238   unfolding map_prod_def[symmetric]
   239 proof (rule pair_measure_eqI)
   240   have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
   241     using f g by (auto simp: inj_on_def)
   242   
   243   show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
   244     unfolding map_prod_def[symmetric]
   245     apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
   246       cong: vimage_algebra_cong)
   247     apply (subst vimage_algebra_Sup_sigma)
   248     apply (simp_all add: space_pair_measure[symmetric])
   249     apply (auto simp add: the_inv_into_f_f
   250                 simp del: map_prod_simp
   251                 del: prod_fun_imageE) []
   252     apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
   253     apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
   254     apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
   255        space_pair_measure[symmetric] map_prod_image[symmetric])
   256     apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)
   257     apply (auto simp: map_prod_image the_inv_into_f_f
   258                 simp del: map_prod_simp del: prod_fun_imageE)
   259     apply (simp_all add: the_inv_into_f_f space_pair_measure)
   260     done
   261 
   262   note measurable_embed_measure2[measurable]
   263   fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
   264   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)"
   265     by (auto simp: space_pair_measure)
   266   ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
   267                      emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
   268     by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
   269                   sigma_finite_measure.emeasure_pair_measure_Times)
   270 qed (insert assms, simp_all add: sigma_finite_embed_measure)
   271 
   272 lemma density_embed_measure:
   273   assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
   274   shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
   275 proof (rule measure_eqI)
   276   fix X assume X: "X \<in> sets ?M1"
   277   from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)" 
   278     by (rule measurable_embed_measure2)
   279   from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f" 
   280     by (subst emeasure_density) simp_all
   281   also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
   282     by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr)
   283        (auto intro!: borel_measurable_ereal_times borel_measurable_indicator)
   284   also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
   285     by (intro nn_integral_cong) (auto split: split_indicator)
   286   also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
   287     by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
   288   also from X and inj have "... = emeasure ?M2 X" 
   289     by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
   290   finally show "emeasure ?M1 X = emeasure ?M2 X" .
   291 qed (simp_all add: sets_embed_measure inj)
   292 
   293 lemma density_embed_measure':
   294   assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
   295   shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
   296 proof-
   297   have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
   298     by (rule density_embed_measure[OF inj])
   299        (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, 
   300         rule inv, rule measurable_ident_sets, simp, rule Mg)
   301   also have "density M (g \<circ> f' \<circ> f) = density M g"
   302     by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
   303   finally show ?thesis .
   304 qed
   305 
   306 lemma inj_on_image_subset_iff:
   307   assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
   308   shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   309 proof (intro iffI subsetI)
   310   fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
   311   from B have "f x \<in> f ` A" by blast
   312   with A have "f x \<in> f ` B" by blast
   313   then obtain y where "f x = f y" and "y \<in> B" by blast
   314   with assms and B have "x = y" by (auto dest: inj_onD)
   315   with `y \<in> B` show "x \<in> B" by simp
   316 qed auto
   317   
   318 
   319 lemma AE_embed_measure':
   320   assumes inj: "inj_on f (space M)"
   321   shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   322 proof
   323   let ?M = "embed_measure M f"
   324   assume "AE x in ?M. P x"
   325   then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
   326     by (force elim: AE_E)
   327   then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
   328   moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}" 
   329     by (auto simp: inj space_embed_measure)
   330   from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
   331     by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
   332        (insert A'_props, auto dest: sets.sets_into_space)
   333   moreover from A_props A'_props have "emeasure M A' = 0"
   334     by (simp add: emeasure_embed_measure_image' inj)
   335   ultimately show "AE x in M. P (f x)" by (intro AE_I)
   336 next
   337   let ?M = "embed_measure M f"
   338   assume "AE x in M. P (f x)"
   339   then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
   340     by (force elim: AE_E)
   341   hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
   342     by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
   343   thus "AE x in ?M. P x" by (intro AE_I)
   344 qed
   345 
   346 lemma AE_embed_measure:
   347   assumes inj: "inj f"
   348   shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   349   using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
   350 
   351 lemma nn_integral_monotone_convergence_SUP_countable:
   352   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
   353   assumes nonempty: "Y \<noteq> {}"
   354   and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
   355   and countable: "countable B"
   356   shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
   357   (is "?lhs = ?rhs")
   358 proof -
   359   let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
   360   have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
   361     by(rule nn_integral_cong)(simp add: countable)
   362   also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
   363     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   364   also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
   365     by(simp add: nn_integral_count_space_indicator ereal_indicator[symmetric] Sup_ereal_mult_right' nonempty)
   366   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" using nonempty
   367   proof(rule nn_integral_monotone_convergence_SUP_nat)
   368     show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
   369       by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
   370   qed
   371   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
   372     by(simp add: nn_integral_count_space_indicator)
   373   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
   374     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   375   also have "\<dots> = ?rhs" 
   376     by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
   377   finally show ?thesis .
   378 qed
   379 
   380 end