author hoelzl
Fri Sep 16 13:56:51 2016 +0200 (2016-09-16)
changeset 63886 685fb01256af
parent 63627 6ddb43c6b711
child 67241 73635a5bfa5c
permissions -rw-r--r--
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
     1 (*  Title:      HOL/Analysis/Embed_Measure.thy
     2     Author:     Manuel Eberl, TU M√ľnchen
     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 *)
     9 section \<open>Embed Measure Spaces with a Function\<close>
    11 theory Embed_Measure
    12 imports Binary_Product_Measure
    13 begin
    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))"
    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)
    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 A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
    37     by (auto simp: subset_eq choice_iff)
    38   then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
    39   with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
    40     by simp blast
    41 qed (auto dest: sets.sets_into_space)
    43 lemma the_inv_into_vimage:
    44   "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
    45   by (auto simp: the_inv_into_f_f)
    47 lemma sets_embed_eq_vimage_algebra:
    48   assumes "inj_on f (space M)"
    49   shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
    50   by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
    51            dest: sets.sets_into_space
    52            intro!: image_cong the_inv_into_vimage[symmetric])
    54 lemma sets_embed_measure:
    55   assumes inj: "inj f"
    56   shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    57   using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
    59 lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
    60   unfolding embed_measure_def
    61   by (intro in_measure_of) (auto dest: sets.sets_into_space)
    63 lemma measurable_embed_measure1:
    64   assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N"
    65   shows "g \<in> measurable (embed_measure M f) N"
    66   unfolding measurable_def
    67 proof safe
    68   fix A assume "A \<in> sets N"
    69   with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
    70     by (rule measurable_sets)
    71   then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
    72     by (rule in_sets_embed_measure)
    73   also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
    74     by (auto simp: space_embed_measure)
    75   finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
    76 qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
    78 lemma measurable_embed_measure2':
    79   assumes "inj_on f (space M)"
    80   shows "f \<in> measurable M (embed_measure M f)"
    81 proof-
    82   {
    83     fix A assume A: "A \<in> sets M"
    84     also from A have "A = A \<inter> space M" by auto
    85     also have "... = f -` f ` A \<inter> space M" using A assms
    86       by (auto dest: inj_onD sets.sets_into_space)
    87     finally have "f -` f ` A \<inter> space M \<in> sets M" .
    88   }
    89   thus ?thesis using assms unfolding embed_measure_def
    90     by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    91 qed
    93 lemma measurable_embed_measure2:
    94   assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
    95   by (auto simp: inj_vimage_image_eq embed_measure_def
    96            intro!: measurable_measure_of dest: sets.sets_into_space)
    98 lemma embed_measure_eq_distr':
    99   assumes "inj_on f (space M)"
   100   shows "embed_measure M f = distr M (embed_measure M f) f"
   101 proof-
   102   have "distr M (embed_measure M f) f =
   103             measure_of (f ` space M) {f ` A |A. A \<in> sets M}
   104                        (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
   105       by (simp add: space_embed_measure sets_embed_measure'[OF assms])
   106   also have "... = embed_measure M f" unfolding embed_measure_def ..
   107   finally show ?thesis ..
   108 qed
   110 lemma embed_measure_eq_distr:
   111     "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
   112   by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
   114 lemma nn_integral_embed_measure':
   115   "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   116   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   117   apply (subst embed_measure_eq_distr', simp)
   118   apply (subst nn_integral_distr)
   119   apply (simp_all add: measurable_embed_measure2')
   120   done
   122 lemma nn_integral_embed_measure:
   123   "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   124   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   125   by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
   127 lemma emeasure_embed_measure':
   128     assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
   129     shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   130   by (subst embed_measure_eq_distr'[OF assms(1)])
   131      (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
   133 lemma emeasure_embed_measure:
   134     assumes "inj f" "A \<in> sets (embed_measure M f)"
   135     shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   136  using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
   138 lemma embed_measure_comp:
   139   assumes [simp]: "inj f" "inj g"
   140   shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
   141 proof-
   142   have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
   143   note measurable_embed_measure2[measurable]
   144   have "embed_measure (embed_measure M f) g =
   145             distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
   146       by (subst (1 2) embed_measure_eq_distr)
   147          (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
   148   also have "... = embed_measure M (g \<circ> f)"
   149       by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
   150          (auto simp: sets_embed_measure o_def image_image[symmetric]
   151                intro: inj_comp cong: distr_cong)
   152   finally show ?thesis .
   153 qed
   155 lemma sigma_finite_embed_measure:
   156   assumes "sigma_finite_measure M" and inj: "inj f"
   157   shows "sigma_finite_measure (embed_measure M f)"
   158 proof -
   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   from A_props have "countable (op ` f`A)" by auto
   163   moreover
   164   from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)"
   165     by (auto simp: sets_embed_measure)
   166   moreover
   167   from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
   168     by (auto simp: space_embed_measure intro!: imageI)
   169   moreover
   170   from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   171     by (intro ballI, subst emeasure_embed_measure)
   172        (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   173   ultimately show ?thesis by - (standard, blast)
   174 qed
   176 lemma embed_measure_count_space':
   177     "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   178   apply (subst distr_bij_count_space[of f A "f`A", symmetric])
   179   apply (simp add: inj_on_def bij_betw_def)
   180   apply (subst embed_measure_eq_distr')
   181   apply simp
   182   apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
   183   apply (subst (1 2) emeasure_distr)
   184   apply (auto simp: space_embed_measure sets_embed_measure')
   185   done
   187 lemma embed_measure_count_space:
   188     "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   189   by(rule embed_measure_count_space')(erule subset_inj_on, simp)
   191 lemma sets_embed_measure_alt:
   192     "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
   193   by (auto simp: sets_embed_measure)
   195 lemma emeasure_embed_measure_image':
   196   assumes "inj_on f (space M)" "X \<in> sets M"
   197   shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
   198 proof-
   199   from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
   200     by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
   201   also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
   202   finally show ?thesis .
   203 qed
   205 lemma emeasure_embed_measure_image:
   206     "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
   207   by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
   209 lemma embed_measure_eq_iff:
   210   assumes "inj f"
   211   shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
   212 proof
   213   from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
   214   assume asm: "?M = ?N"
   215   hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
   216   with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
   217   moreover {
   218     fix X assume "X \<in> sets A"
   219     from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
   220     with \<open>X \<in> sets A\<close> and \<open>sets A = sets B\<close> and assms
   221         have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
   222   }
   223   ultimately show "A = B" by (rule measure_eqI)
   224 qed simp
   226 lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
   227   by (auto simp: the_inv_into_f_f)
   229 lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
   230   using map_prod_surj_on[OF refl refl] .
   232 lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
   233   by auto
   235 lemma embed_measure_prod:
   236   assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
   237   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))"
   238     (is "?L = _")
   239   unfolding map_prod_def[symmetric]
   240 proof (rule pair_measure_eqI)
   241   have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
   242     using f g by (auto simp: inj_on_def)
   244   note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del]
   245      ccSUP_insert[simp del]
   246   show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
   247     unfolding map_prod_def[symmetric]
   248     apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
   249       cong: vimage_algebra_cong)
   250     apply (subst sets_vimage_Sup_eq[where Y="space (M \<Otimes>\<^sub>M N)"])
   251     apply (simp_all add: space_pair_measure[symmetric])
   252     apply (auto simp add: the_inv_into_f_f
   253                 simp del: map_prod_simp
   254                 del: prod_fun_imageE) []
   255     apply auto []
   256     apply (subst image_insert)
   257     apply simp
   258     apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
   259     apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
   260     apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
   261        space_pair_measure[symmetric] map_prod_image[symmetric])
   262     apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong)
   263     apply (auto simp: map_prod_image the_inv_into_f_f
   264                 simp del: map_prod_simp del: prod_fun_imageE)
   265     apply (simp_all add: the_inv_into_f_f space_pair_measure)
   266     done
   268   note measurable_embed_measure2[measurable]
   269   fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
   270   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)"
   271     by (auto simp: space_pair_measure)
   272   ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
   273                      emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
   274     by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
   275                   sigma_finite_measure.emeasure_pair_measure_Times)
   276 qed (insert assms, simp_all add: sigma_finite_embed_measure)
   278 lemma mono_embed_measure:
   279   "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)"
   280   unfolding embed_measure_def
   281   apply (subst (1 2) sets_measure_of)
   282   apply (blast dest: sets.sets_into_space)
   283   apply (blast dest: sets.sets_into_space)
   284   apply simp
   285   apply (intro sigma_sets_mono')
   286   apply safe
   287   apply (simp add: subset_eq)
   288   apply metis
   289   done
   291 lemma density_embed_measure:
   292   assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
   293   shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
   294 proof (rule measure_eqI)
   295   fix X assume X: "X \<in> sets ?M1"
   296   from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)"
   297     by (rule measurable_embed_measure2)
   298   from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f"
   299     by (subst emeasure_density) simp_all
   300   also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
   301     by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto
   302   also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
   303     by (intro nn_integral_cong) (auto split: split_indicator)
   304   also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
   305     by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
   306   also from X and inj have "... = emeasure ?M2 X"
   307     by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
   308   finally show "emeasure ?M1 X = emeasure ?M2 X" .
   309 qed (simp_all add: sets_embed_measure inj)
   311 lemma density_embed_measure':
   312   assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
   313   shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
   314 proof-
   315   have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
   316     by (rule density_embed_measure[OF inj])
   317        (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong,
   318         rule inv, rule measurable_ident_sets, simp, rule Mg)
   319   also have "density M (g \<circ> f' \<circ> f) = density M g"
   320     by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
   321   finally show ?thesis .
   322 qed
   324 lemma inj_on_image_subset_iff:
   325   assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
   326   shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   327 proof (intro iffI subsetI)
   328   fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
   329   from B have "f x \<in> f ` A" by blast
   330   with A have "f x \<in> f ` B" by blast
   331   then obtain y where "f x = f y" and "y \<in> B" by blast
   332   with assms and B have "x = y" by (auto dest: inj_onD)
   333   with \<open>y \<in> B\<close> show "x \<in> B" by simp
   334 qed auto
   337 lemma AE_embed_measure':
   338   assumes inj: "inj_on f (space M)"
   339   shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   340 proof
   341   let ?M = "embed_measure M f"
   342   assume "AE x in ?M. P x"
   343   then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
   344     by (force elim: AE_E)
   345   then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
   346   moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}"
   347     by (auto simp: inj space_embed_measure)
   348   from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
   349     by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
   350        (insert A'_props, auto dest: sets.sets_into_space)
   351   moreover from A_props A'_props have "emeasure M A' = 0"
   352     by (simp add: emeasure_embed_measure_image' inj)
   353   ultimately show "AE x in M. P (f x)" by (intro AE_I)
   354 next
   355   let ?M = "embed_measure M f"
   356   assume "AE x in M. P (f x)"
   357   then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
   358     by (force elim: AE_E)
   359   hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
   360     by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
   361   thus "AE x in ?M. P x" by (intro AE_I)
   362 qed
   364 lemma AE_embed_measure:
   365   assumes inj: "inj f"
   366   shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   367   using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
   369 lemma nn_integral_monotone_convergence_SUP_countable:
   370   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"
   371   assumes nonempty: "Y \<noteq> {}"
   372   and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
   373   and countable: "countable B"
   374   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))"
   375   (is "?lhs = ?rhs")
   376 proof -
   377   let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
   378   have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
   379     by(rule nn_integral_cong)(simp add: countable)
   380   also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
   381     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   382   also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
   383     by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
   384   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
   385   proof(rule nn_integral_monotone_convergence_SUP_nat)
   386     show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
   387       by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
   388   qed fact
   389   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
   390     by(simp add: nn_integral_count_space_indicator)
   391   also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
   392     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   393   also have "\<dots> = ?rhs"
   394     by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
   395   finally show ?thesis .
   396 qed
   398 end