summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Embed_Measure.thy

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