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

src/HOL/Analysis/Embed_Measure.thy

author | wenzelm |

Mon Mar 25 17:21:26 2019 +0100 (3 months ago) | |

changeset 69981 | 3dced198b9ec |

parent 69768 | 7e4966eaf781 |

child 70136 | f03a01a18c6e |

permissions | -rw-r--r-- |

more strict AFP properties;

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>Embedding Measure Spaces with a Function\<close>

11 theory Embed_Measure

12 imports Binary_Product_Measure

13 begin

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 \<open>f(\<Omega>)\<close> whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over

18 the original sigma algebra.

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))"

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)

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)

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)

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])

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)

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)

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)

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

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)

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

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)

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

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

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)])

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)

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_compose)

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_compose cong: distr_cong)

162 finally show ?thesis .

163 qed

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

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

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)

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)

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

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)

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

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)

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] .

242 lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"

243 by auto

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)

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 (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)

267 apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)

268 apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq

269 space_pair_measure[symmetric] map_prod_image[symmetric])

270 apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong)

271 apply (auto simp: map_prod_image the_inv_into_f_f

272 simp del: map_prod_simp del: prod_fun_imageE)

273 apply (simp_all add: the_inv_into_f_f space_pair_measure)

274 done

276 note measurable_embed_measure2[measurable]

277 fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"

278 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)"

279 by (auto simp: space_pair_measure)

280 ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =

281 emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"

282 by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure

283 sigma_finite_measure.emeasure_pair_measure_Times)

284 qed (insert assms, simp_all add: sigma_finite_embed_measure)

286 lemma mono_embed_measure:

287 "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)"

288 unfolding embed_measure_def

289 apply (subst (1 2) sets_measure_of)

290 apply (blast dest: sets.sets_into_space)

291 apply (blast dest: sets.sets_into_space)

292 apply simp

293 apply (intro sigma_sets_mono')

294 apply safe

295 apply (simp add: subset_eq)

296 apply metis

297 done

299 lemma density_embed_measure:

300 assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"

301 shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")

302 proof (rule measure_eqI)

303 fix X assume X: "X \<in> sets ?M1"

304 from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)"

305 by (rule measurable_embed_measure2)

306 from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f"

307 by (subst emeasure_density) simp_all

308 also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"

309 by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto

310 also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"

311 by (intro nn_integral_cong) (auto split: split_indicator)

312 also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"

313 by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])

314 also from X and inj have "... = emeasure ?M2 X"

315 by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)

316 finally show "emeasure ?M1 X = emeasure ?M2 X" .

317 qed (simp_all add: sets_embed_measure inj)

319 lemma density_embed_measure':

320 assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"

321 shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"

322 proof-

323 have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"

324 by (rule density_embed_measure[OF inj])

325 (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong,

326 rule inv, rule measurable_ident_sets, simp, rule Mg)

327 also have "density M (g \<circ> f' \<circ> f) = density M g"

328 by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)

329 finally show ?thesis .

330 qed

332 lemma inj_on_image_subset_iff:

333 assumes "inj_on f C" "A \<subseteq> C" "B \<subseteq> C"

334 shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"

335 proof (intro iffI subsetI)

336 fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"

337 from B have "f x \<in> f ` A" by blast

338 with A have "f x \<in> f ` B" by blast

339 then obtain y where "f x = f y" and "y \<in> B" by blast

340 with assms and B have "x = y" by (auto dest: inj_onD)

341 with \<open>y \<in> B\<close> show "x \<in> B" by simp

342 qed auto

345 lemma AE_embed_measure':

346 assumes inj: "inj_on f (space M)"

347 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"

348 proof

349 let ?M = "embed_measure M f"

350 assume "AE x in ?M. P x"

351 then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"

352 by (force elim: AE_E)

353 then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)

354 moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}"

355 by (auto simp: inj space_embed_measure)

356 from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"

357 by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])

358 (insert A'_props, auto dest: sets.sets_into_space)

359 moreover from A_props A'_props have "emeasure M A' = 0"

360 by (simp add: emeasure_embed_measure_image' inj)

361 ultimately show "AE x in M. P (f x)" by (intro AE_I)

362 next

363 let ?M = "embed_measure M f"

364 assume "AE x in M. P (f x)"

365 then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"

366 by (force elim: AE_E)

367 hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"

368 by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)

369 thus "AE x in ?M. P x" by (intro AE_I)

370 qed

372 lemma AE_embed_measure:

373 assumes inj: "inj f"

374 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"

375 using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)

377 lemma nn_integral_monotone_convergence_SUP_countable:

378 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"

379 assumes nonempty: "Y \<noteq> {}"

380 and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"

381 and countable: "countable B"

382 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))"

383 (is "?lhs = ?rhs")

384 proof -

385 let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"

386 have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"

387 by(rule nn_integral_cong)(simp add: countable)

388 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)"

389 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)

390 also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"

391 by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)

392 also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"

393 proof(rule nn_integral_monotone_convergence_SUP_nat)

394 show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"

395 by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)

396 qed fact

397 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))"

398 by(simp add: nn_integral_count_space_indicator)

399 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)"

400 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)

401 also have "\<dots> = ?rhs"

402 by(intro arg_cong2[where f = "\<lambda>A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)

403 finally show ?thesis .

404 qed

406 end