256 show "f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))" |
248 show "f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))" |
257 using csa[unfolded countably_subadditive_def] A'' disj U_in by auto |
249 using csa[unfolded countably_subadditive_def] A'' disj U_in by auto |
258 have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto |
250 have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto |
259 have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto |
251 have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto |
260 show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)" |
252 show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)" |
261 using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] |
253 using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A'' |
262 using A'' |
|
263 by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN) |
254 by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN) |
264 qed |
255 qed |
265 { |
256 have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a" |
266 fix a |
257 if a [iff]: "a \<in> M" for a |
267 assume a [iff]: "a \<in> M" |
258 proof (rule antisym) |
268 have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a" |
259 have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A'' |
269 proof - |
260 by blast |
270 show ?thesis |
261 moreover |
271 proof (rule antisym) |
262 have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
272 have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A'' |
263 by (auto simp add: disjoint_family_on_def) |
273 by blast |
264 moreover |
274 moreover |
265 have "a \<inter> (\<Union>i. A i) \<in> M" |
275 have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
266 by (metis Int U_in a) |
276 by (auto simp add: disjoint_family_on_def) |
267 ultimately |
277 moreover |
268 have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))" |
278 have "a \<inter> (\<Union>i. A i) \<in> M" |
269 using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"] |
279 by (metis Int U_in a) |
270 by (simp add: o_def) |
280 ultimately |
271 hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))" |
281 have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))" |
272 by (rule add_right_mono) |
282 using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"] |
273 also have "\<dots> \<le> f a" |
283 by (simp add: o_def) |
274 proof (intro suminf_bound_add allI) |
284 hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> |
275 fix n |
285 (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))" |
276 have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M" |
286 by (rule add_right_mono) |
277 by (metis A'' UNION_in_sets) |
287 moreover |
278 have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
288 have "(\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
279 by (blast intro: increasingD [OF inc] A'' UNION_in_sets) |
289 proof (intro suminf_bound_add allI) |
280 have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f" |
290 fix n |
281 using ls.UNION_in_sets by (simp add: A) |
291 have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M" |
282 hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))" |
292 by (metis A'' UNION_in_sets) |
283 by (simp add: lambda_system_eq UNION_in) |
293 have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
284 have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
294 by (blast intro: increasingD [OF inc] A'' UNION_in_sets) |
285 by (blast intro: increasingD [OF inc] UNION_in U_in) |
295 have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f" |
286 thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
296 using ls.UNION_in_sets by (simp add: A) |
287 by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) |
297 hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))" |
288 next |
298 by (simp add: lambda_system_eq UNION_in) |
289 have "\<And>i. a \<inter> A i \<in> M" using A'' by auto |
299 have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
290 then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto |
300 by (blast intro: increasingD [OF inc] UNION_in U_in) |
291 have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto |
301 thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
292 then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto |
302 by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) |
293 then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto |
303 next |
294 qed |
304 have "\<And>i. a \<inter> A i \<in> M" using A'' by auto |
295 finally show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" . |
305 then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto |
296 next |
306 have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto |
297 have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
307 then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto |
298 by (blast intro: increasingD [OF inc] U_in) |
308 then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto |
299 also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
309 qed |
300 by (blast intro: subadditiveD [OF sa] U_in) |
310 ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
301 finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" . |
311 by (rule order_trans) |
302 qed |
312 next |
|
313 have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
|
314 by (blast intro: increasingD [OF inc] U_in) |
|
315 also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
|
316 by (blast intro: subadditiveD [OF sa] U_in) |
|
317 finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" . |
|
318 qed |
|
319 qed |
|
320 } |
|
321 thus ?thesis |
303 thus ?thesis |
322 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
304 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
323 qed |
305 qed |
324 |
306 |
325 lemma (in sigma_algebra) caratheodory_lemma: |
307 lemma (in sigma_algebra) caratheodory_lemma: |
343 ultimately |
325 ultimately |
344 show ?thesis |
326 show ?thesis |
345 using pos by (simp add: measure_space_def) |
327 using pos by (simp add: measure_space_def) |
346 qed |
328 qed |
347 |
329 |
348 lemma inf_measure_nonempty: |
330 definition outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a set \<Rightarrow> ereal" where |
349 assumes f: "positive M f" and b: "b \<in> M" and a: "a \<subseteq> b" "{} \<in> M" |
331 "outer_measure M f X = |
350 shows "f b \<in> measure_set M f a" |
332 (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))" |
351 proof - |
333 |
352 let ?A = "\<lambda>i::nat. (if i = 0 then b else {})" |
334 lemma (in ring_of_sets) outer_measure_agrees: |
353 have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))" |
335 assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M" |
354 by (rule suminf_finite) (simp_all add: f[unfolded positive_def]) |
336 shows "outer_measure M f s = f s" |
355 also have "... = f b" |
337 unfolding outer_measure_def |
356 by simp |
338 proof (safe intro!: antisym INF_greatest) |
357 finally show ?thesis using assms |
339 fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" and dA: "disjoint_family A" and sA: "s \<subseteq> (\<Union>x. A x)" |
358 by (auto intro!: exI [of _ ?A] |
|
359 simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) |
|
360 qed |
|
361 |
|
362 lemma (in ring_of_sets) inf_measure_agrees: |
|
363 assumes posf: "positive M f" and ca: "countably_additive M f" |
|
364 and s: "s \<in> M" |
|
365 shows "Inf (measure_set M f s) = f s" |
|
366 proof (intro Inf_eqI) |
|
367 fix z |
|
368 assume z: "z \<in> measure_set M f s" |
|
369 from this obtain A where |
|
370 A: "range A \<subseteq> M" and disj: "disjoint_family A" |
|
371 and "s \<subseteq> (\<Union>x. A x)" and si: "(\<Sum>i. f (A i)) = z" |
|
372 by (auto simp add: measure_set_def comp_def) |
|
373 hence seq: "s = (\<Union>i. A i \<inter> s)" by blast |
|
374 have inc: "increasing M f" |
340 have inc: "increasing M f" |
375 by (metis additive_increasing ca countably_additive_additive posf) |
341 by (metis additive_increasing ca countably_additive_additive posf) |
376 have sums: "(\<Sum>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)" |
342 have "f s = f (\<Union>i. A i \<inter> s)" |
377 proof (rule ca[unfolded countably_additive_def, rule_format]) |
343 using sA by (auto simp: Int_absorb1) |
378 show "range (\<lambda>n. A n \<inter> s) \<subseteq> M" using A s |
344 also have "\<dots> = (\<Sum>i. f (A i \<inter> s))" |
379 by blast |
345 using sA dA A s |
380 show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj |
346 by (intro ca[unfolded countably_additive_def, rule_format, symmetric]) |
381 by (auto simp add: disjoint_family_on_def) |
347 (auto simp: Int_absorb1 disjoint_family_on_def) |
382 show "(\<Union>i. A i \<inter> s) \<in> M" using A s |
|
383 by (metis UN_extend_simps(4) s seq) |
|
384 qed |
|
385 hence "f s = (\<Sum>i. f (A i \<inter> s))" |
|
386 using seq [symmetric] by (simp add: sums_iff) |
|
387 also have "... \<le> (\<Sum>i. f (A i))" |
348 also have "... \<le> (\<Sum>i. f (A i))" |
388 proof (rule suminf_le_pos) |
349 using A s by (intro suminf_le_pos increasingD[OF inc] positiveD2[OF posf]) auto |
389 fix n show "f (A n \<inter> s) \<le> f (A n)" using A s |
350 finally show "f s \<le> (\<Sum>i. f (A i))" . |
390 by (force intro: increasingD [OF inc]) |
351 next |
391 fix N have "A N \<inter> s \<in> M" using A s by auto |
352 have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s" |
392 then show "0 \<le> f (A N \<inter> s)" using posf unfolding positive_def by auto |
353 using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto |
393 qed |
354 with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s" |
394 also have "... = z" by (rule si) |
355 by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"]) |
395 finally show "f s \<le> z" . |
356 (auto simp: disjoint_family_on_def) |
396 qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl]) |
357 qed |
397 |
358 |
398 lemma measure_set_pos: |
359 lemma outer_measure_nonneg: "positive M f \<Longrightarrow> 0 \<le> outer_measure M f X" |
399 assumes posf: "positive M f" "r \<in> measure_set M f X" |
360 by (auto intro!: INF_greatest suminf_0_le intro: positiveD2 simp: outer_measure_def) |
400 shows "0 \<le> r" |
361 |
401 proof - |
362 lemma outer_measure_empty: |
402 obtain A where "range A \<subseteq> M" and r: "r = (\<Sum>i. f (A i))" |
|
403 using `r \<in> measure_set M f X` unfolding measure_set_def by auto |
|
404 then show "0 \<le> r" using posf unfolding r positive_def |
|
405 by (intro suminf_0_le) auto |
|
406 qed |
|
407 |
|
408 lemma inf_measure_pos: |
|
409 assumes posf: "positive M f" |
|
410 shows "0 \<le> Inf (measure_set M f X)" |
|
411 proof (rule complete_lattice_class.Inf_greatest) |
|
412 fix r assume "r \<in> measure_set M f X" with posf show "0 \<le> r" |
|
413 by (rule measure_set_pos) |
|
414 qed |
|
415 |
|
416 lemma inf_measure_empty: |
|
417 assumes posf: "positive M f" and "{} \<in> M" |
363 assumes posf: "positive M f" and "{} \<in> M" |
418 shows "Inf (measure_set M f {}) = 0" |
364 shows "outer_measure M f {} = 0" |
419 proof (rule antisym) |
365 proof (rule antisym) |
420 show "Inf (measure_set M f {}) \<le> 0" |
366 show "outer_measure M f {} \<le> 0" |
421 by (metis complete_lattice_class.Inf_lower `{} \<in> M` |
367 using assms by (auto intro!: INF_lower2[of "\<lambda>_. {}"] simp: outer_measure_def disjoint_family_on_def positive_def) |
422 inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) |
368 qed (intro outer_measure_nonneg posf) |
423 qed (rule inf_measure_pos[OF posf]) |
369 |
424 |
370 lemma (in ring_of_sets) positive_outer_measure: |
425 lemma (in ring_of_sets) inf_measure_positive: |
371 assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)" |
426 assumes p: "positive M f" and "{} \<in> M" |
372 unfolding positive_def by (auto simp: assms outer_measure_empty outer_measure_nonneg) |
427 shows "positive M (\<lambda>x. Inf (measure_set M f x))" |
373 |
428 proof (unfold positive_def, intro conjI ballI) |
374 lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)" |
429 show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto |
375 by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) |
430 fix A assume "A \<in> M" |
376 |
431 qed (rule inf_measure_pos[OF p]) |
377 lemma (in ring_of_sets) outer_measure_le: |
432 |
378 assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \<subseteq> M" and X: "X \<subseteq> (\<Union>i. A i)" |
433 lemma (in ring_of_sets) inf_measure_increasing: |
379 shows "outer_measure M f X \<le> (\<Sum>i. f (A i))" |
434 assumes posf: "positive M f" |
380 unfolding outer_measure_def |
435 shows "increasing (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" |
381 proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) |
436 apply (clarsimp simp add: increasing_def) |
382 show dA: "range (disjointed A) \<subseteq> M" |
437 apply (rule complete_lattice_class.Inf_greatest) |
383 by (auto intro!: A range_disjointed_sets) |
438 apply (rule complete_lattice_class.Inf_lower) |
384 have "\<forall>n. f (disjointed A n) \<le> f (A n)" |
439 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) |
385 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) |
440 done |
386 moreover have "\<forall>i. 0 \<le> f (disjointed A i)" |
441 |
387 using pos dA unfolding positive_def by auto |
442 lemma (in ring_of_sets) inf_measure_le: |
388 ultimately show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))" |
|
389 by (blast intro!: suminf_le_pos) |
|
390 qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) |
|
391 |
|
392 lemma (in ring_of_sets) outer_measure_close: |
|
393 assumes posf: "positive M f" and "0 < e" and "outer_measure M f X \<noteq> \<infinity>" |
|
394 shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) \<le> outer_measure M f X + e" |
|
395 proof - |
|
396 from `outer_measure M f X \<noteq> \<infinity>` have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>" |
|
397 using outer_measure_nonneg[OF posf, of X] by auto |
|
398 show ?thesis |
|
399 using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>] |
|
400 unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le) |
|
401 qed |
|
402 |
|
403 lemma (in ring_of_sets) countably_subadditive_outer_measure: |
443 assumes posf: "positive M f" and inc: "increasing M f" |
404 assumes posf: "positive M f" and inc: "increasing M f" |
444 and x: "x \<in> {r . \<exists>A. range A \<subseteq> M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}" |
405 shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)" |
445 shows "Inf (measure_set M f s) \<le> x" |
|
446 proof - |
|
447 obtain A where A: "range A \<subseteq> M" and ss: "s \<subseteq> (\<Union>i. A i)" |
|
448 and xeq: "(\<Sum>i. f (A i)) = x" |
|
449 using x by auto |
|
450 have dA: "range (disjointed A) \<subseteq> M" |
|
451 by (metis A range_disjointed_sets) |
|
452 have "\<forall>n. f (disjointed A n) \<le> f (A n)" |
|
453 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) |
|
454 moreover have "\<forall>i. 0 \<le> f (disjointed A i)" |
|
455 using posf dA unfolding positive_def by auto |
|
456 ultimately have sda: "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))" |
|
457 by (blast intro!: suminf_le_pos) |
|
458 hence ley: "(\<Sum>i. f (disjointed A i)) \<le> x" |
|
459 by (metis xeq) |
|
460 hence y: "(\<Sum>i. f (disjointed A i)) \<in> measure_set M f s" |
|
461 apply (auto simp add: measure_set_def) |
|
462 apply (rule_tac x="disjointed A" in exI) |
|
463 apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def) |
|
464 done |
|
465 show ?thesis |
|
466 by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower) |
|
467 qed |
|
468 |
|
469 lemma (in ring_of_sets) inf_measure_close: |
|
470 fixes e :: ereal |
|
471 assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (\<Omega>)" and "Inf (measure_set M f s) \<noteq> \<infinity>" |
|
472 shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and> |
|
473 (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e" |
|
474 proof - |
|
475 from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>" |
|
476 using inf_measure_pos[OF posf, of s] by auto |
|
477 obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e" |
|
478 using Inf_ereal_close[OF fin e] by auto |
|
479 thus ?thesis |
|
480 by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) |
|
481 qed |
|
482 |
|
483 lemma (in ring_of_sets) inf_measure_countably_subadditive: |
|
484 assumes posf: "positive M f" and inc: "increasing M f" |
|
485 shows "countably_subadditive (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" |
|
486 proof (simp add: countably_subadditive_def, safe) |
406 proof (simp add: countably_subadditive_def, safe) |
487 fix A :: "nat \<Rightarrow> 'a set" |
407 fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> Pow (\<Omega>)" and sb: "(\<Union>i. A i) \<subseteq> \<Omega>" |
488 let ?outer = "\<lambda>B. Inf (measure_set M f B)" |
408 let ?O = "outer_measure M f" |
489 assume A: "range A \<subseteq> Pow (\<Omega>)" |
409 |
490 and disj: "disjoint_family A" |
410 { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?O (A i) \<noteq> \<infinity>" |
491 and sb: "(\<Union>i. A i) \<subseteq> \<Omega>" |
411 hence "\<exists>B. \<forall>n. range (B n) \<subseteq> M \<and> disjoint_family (B n) \<and> A n \<subseteq> (\<Union>i. B n i) \<and> |
492 |
412 (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)" |
493 { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>" |
413 using e sb by (auto intro!: choice outer_measure_close [of f, OF posf] simp: ereal_zero_less_0_iff one_ereal_def) |
494 hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> M \<and> disjoint_family (BB n) \<and> |
414 then obtain B |
495 A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)" |
415 where B: "\<And>n. range (B n) \<subseteq> M" |
496 apply (safe intro!: choice inf_measure_close [of f, OF posf]) |
416 and sbB: "\<And>n. A n \<subseteq> (\<Union>i. B n i)" |
497 using e sb by (auto simp: ereal_zero_less_0_iff one_ereal_def) |
417 and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)" |
498 then obtain BB |
|
499 where BB: "\<And>n. (range (BB n) \<subseteq> M)" |
|
500 and disjBB: "\<And>n. disjoint_family (BB n)" |
|
501 and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)" |
|
502 and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)" |
|
503 by auto blast |
418 by auto blast |
504 have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e" |
419 |
505 proof - |
420 def C \<equiv> "split B o prod_decode" |
506 have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e" |
421 from B have B_in_M: "\<And>i j. B i j \<in> M" |
507 using suminf_half_series_ereal e |
|
508 by (simp add: ereal_zero_le_0_iff zero_le_divide_ereal suminf_cmult_ereal) |
|
509 have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto |
|
510 then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le) |
|
511 then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)" |
|
512 by (rule suminf_le_pos[OF BBle]) |
|
513 also have "... = (\<Sum>n. ?outer (A n)) + e" |
|
514 using sum_eq_1 inf_measure_pos[OF posf] e |
|
515 by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff) |
|
516 finally show ?thesis . |
|
517 qed |
|
518 def C \<equiv> "(split BB) o prod_decode" |
|
519 from BB have "\<And>i j. BB i j \<in> M" |
|
520 by (rule range_subsetD) |
422 by (rule range_subsetD) |
521 then have C: "\<And>n. C n \<in> M" |
423 then have C: "range C \<subseteq> M" |
522 by (simp add: C_def split_def) |
424 by (auto simp add: C_def split_def) |
523 have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
425 have A_C: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
524 proof (auto simp add: C_def) |
426 using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse) |
525 fix x i |
427 |
526 assume x: "x \<in> A i" |
428 have "?O (\<Union>i. A i) \<le> ?O (\<Union>i. C i)" |
527 with sbBB [of i] obtain j where "x \<in> BB i j" |
429 using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space) |
528 by blast |
430 also have "\<dots> \<le> (\<Sum>i. f (C i))" |
529 thus "\<exists>i. x \<in> split BB (prod_decode i)" |
431 using C by (intro outer_measure_le[OF posf inc]) auto |
530 by (metis prod_encode_inverse prod.case) |
432 also have "\<dots> = (\<Sum>n. \<Sum>i. f (B n i))" |
531 qed |
433 using B_in_M unfolding C_def comp_def by (intro suminf_ereal_2dimen positiveD2[OF posf]) auto |
532 have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" |
434 also have "\<dots> \<le> (\<Sum>n. ?O (A n) + e*(1/2) ^ Suc n)" |
533 by (rule ext) (auto simp add: C_def) |
435 using B_in_M by (intro suminf_le_pos[OF Ble] suminf_0_le posf[THEN positiveD2]) auto |
534 moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle |
436 also have "... = (\<Sum>n. ?O (A n)) + (\<Sum>n. e*(1/2) ^ Suc n)" |
535 using BB posf[unfolded positive_def] |
437 using e by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff outer_measure_nonneg posf) |
536 by (force intro!: suminf_ereal_2dimen simp: o_def) |
438 also have "(\<Sum>n. e*(1/2) ^ Suc n) = e" |
537 ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def) |
439 using suminf_half_series_ereal e by (simp add: ereal_zero_le_0_iff suminf_cmult_ereal) |
538 have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))" |
440 finally have "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . } |
539 apply (rule inf_measure_le [OF posf(1) inc], auto) |
441 note * = this |
540 apply (rule_tac x="C" in exI) |
442 |
541 apply (auto simp add: C sbC Csums) |
443 show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n))" |
542 done |
|
543 also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll |
|
544 by blast |
|
545 finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . } |
|
546 note for_finite_Inf = this |
|
547 |
|
548 show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))" |
|
549 proof cases |
444 proof cases |
550 assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>" |
445 assume "\<forall>i. ?O (A i) \<noteq> \<infinity>" with * show ?thesis |
551 with for_finite_Inf show ?thesis |
|
552 by (intro ereal_le_epsilon) auto |
446 by (intro ereal_le_epsilon) auto |
553 next |
447 qed (metis suminf_PInfty[OF outer_measure_nonneg, OF posf] ereal_less_eq(1)) |
554 assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)" |
448 qed |
555 then have "\<exists>i. ?outer (A i) = \<infinity>" |
449 |
556 by auto |
450 lemma (in ring_of_sets) outer_measure_space_outer_measure: |
557 then have "(\<Sum>n. ?outer (A n)) = \<infinity>" |
451 "positive M f \<Longrightarrow> increasing M f \<Longrightarrow> outer_measure_space (Pow \<Omega>) (outer_measure M f)" |
558 using suminf_PInfty[OF inf_measure_pos, OF posf] |
452 by (simp add: outer_measure_space_def |
559 by metis |
453 positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) |
560 then show ?thesis by simp |
|
561 qed |
|
562 qed |
|
563 |
|
564 lemma (in ring_of_sets) inf_measure_outer: |
|
565 "\<lbrakk> positive M f ; increasing M f \<rbrakk> \<Longrightarrow> |
|
566 outer_measure_space (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" |
|
567 using inf_measure_pos[of M f] |
|
568 by (simp add: outer_measure_space_def inf_measure_empty |
|
569 inf_measure_increasing inf_measure_countably_subadditive positive_def) |
|
570 |
454 |
571 lemma (in ring_of_sets) algebra_subset_lambda_system: |
455 lemma (in ring_of_sets) algebra_subset_lambda_system: |
572 assumes posf: "positive M f" and inc: "increasing M f" |
456 assumes posf: "positive M f" and inc: "increasing M f" |
573 and add: "additive M f" |
457 and add: "additive M f" |
574 shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" |
458 shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)" |
575 proof (auto dest: sets_into_space |
459 proof (auto dest: sets_into_space |
576 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
460 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
577 fix x s |
461 fix x s assume x: "x \<in> M" and s: "s \<subseteq> \<Omega>" |
578 assume x: "x \<in> M" |
462 have [simp]: "\<And>x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s - x" using s |
579 and s: "s \<subseteq> \<Omega>" |
|
580 have [simp]: "!!x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s-x" using s |
|
581 by blast |
463 by blast |
582 have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
464 have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> outer_measure M f s" |
583 \<le> Inf (measure_set M f s)" |
465 unfolding outer_measure_def[of M f s] |
584 proof cases |
466 proof (safe intro!: INF_greatest) |
585 assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp |
467 fix A :: "nat \<Rightarrow> 'a set" assume A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)" |
586 next |
468 have "outer_measure M f (s \<inter> x) \<le> (\<Sum>i. f (A i \<inter> x))" |
587 assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>" |
469 unfolding outer_measure_def |
588 then have "measure_set M f s \<noteq> {}" |
470 proof (safe intro!: INF_lower2[of "\<lambda>i. A i \<inter> x"]) |
589 by (auto simp: top_ereal_def) |
471 from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)" |
590 show ?thesis |
472 by (rule disjoint_family_on_bisimulation) auto |
591 proof (rule complete_lattice_class.Inf_greatest) |
473 qed (insert x A, auto) |
592 fix r assume "r \<in> measure_set M f s" |
474 moreover |
593 then obtain A where A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)" |
475 have "outer_measure M f (s - x) \<le> (\<Sum>i. f (A i - x))" |
594 and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto |
476 unfolding outer_measure_def |
595 have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))" |
477 proof (safe intro!: INF_lower2[of "\<lambda>i. A i - x"]) |
596 unfolding measure_set_def |
478 from A(1) show "disjoint_family (\<lambda>i. A i - x)" |
597 proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"]) |
479 by (rule disjoint_family_on_bisimulation) auto |
598 from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)" |
480 qed (insert x A, auto) |
599 by (rule disjoint_family_on_bisimulation) auto |
481 ultimately have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> |
600 qed (insert x A, auto) |
482 (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono) |
601 moreover |
483 also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))" |
602 have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))" |
484 using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def) |
603 unfolding measure_set_def |
485 also have "\<dots> = (\<Sum>i. f (A i))" |
604 proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"]) |
486 using A x |
605 from A(1) show "disjoint_family (\<lambda>i. A i - x)" |
487 by (subst add[THEN additiveD, symmetric]) |
606 by (rule disjoint_family_on_bisimulation) auto |
488 (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) |
607 qed (insert x A, auto) |
489 finally show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> (\<Sum>i. f (A i))" . |
608 ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> |
|
609 (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono) |
|
610 also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))" |
|
611 using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def) |
|
612 also have "\<dots> = (\<Sum>i. f (A i))" |
|
613 using A x |
|
614 by (subst add[THEN additiveD, symmetric]) |
|
615 (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) |
|
616 finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r" |
|
617 using r by simp |
|
618 qed |
|
619 qed |
490 qed |
620 moreover |
491 moreover |
621 have "Inf (measure_set M f s) |
492 have "outer_measure M f s \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)" |
622 \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
|
623 proof - |
493 proof - |
624 have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))" |
494 have "outer_measure M f s = outer_measure M f ((s \<inter> x) \<union> (s - x))" |
625 by (metis Un_Diff_Int Un_commute) |
495 by (metis Un_Diff_Int Un_commute) |
626 also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
496 also have "... \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)" |
627 apply (rule subadditiveD) |
497 apply (rule subadditiveD) |
628 apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) |
498 apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) |
629 apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf]) |
499 apply (simp add: positive_def outer_measure_empty[OF posf] outer_measure_nonneg[OF posf]) |
630 apply (rule inf_measure_countably_subadditive) |
500 apply (rule countably_subadditive_outer_measure) |
631 using s by (auto intro!: posf inc) |
501 using s by (auto intro!: posf inc) |
632 finally show ?thesis . |
502 finally show ?thesis . |
633 qed |
503 qed |
634 ultimately |
504 ultimately |
635 show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
505 show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s" |
636 = Inf (measure_set M f s)" |
|
637 by (rule order_antisym) |
506 by (rule order_antisym) |
638 qed |
507 qed |
639 |
508 |
640 lemma measure_down: |
509 lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
641 "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
|
642 by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) |
510 by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) |
643 |
511 |
644 subsection {* Caratheodory's theorem *} |
512 subsection {* Caratheodory's theorem *} |
645 |
513 |
646 theorem (in ring_of_sets) caratheodory': |
514 theorem (in ring_of_sets) caratheodory': |
647 assumes posf: "positive M f" and ca: "countably_additive M f" |
515 assumes posf: "positive M f" and ca: "countably_additive M f" |
648 shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" |
516 shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" |
649 proof - |
517 proof - |
650 have inc: "increasing M f" |
518 have inc: "increasing M f" |
651 by (metis additive_increasing ca countably_additive_additive posf) |
519 by (metis additive_increasing ca countably_additive_additive posf) |
652 let ?infm = "(\<lambda>x. Inf (measure_set M f x))" |
520 let ?O = "outer_measure M f" |
653 def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?infm" |
521 def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?O" |
654 have mls: "measure_space \<Omega> ls ?infm" |
522 have mls: "measure_space \<Omega> ls ?O" |
655 using sigma_algebra.caratheodory_lemma |
523 using sigma_algebra.caratheodory_lemma |
656 [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] |
524 [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]] |
657 by (simp add: ls_def) |
525 by (simp add: ls_def) |
658 hence sls: "sigma_algebra \<Omega> ls" |
526 hence sls: "sigma_algebra \<Omega> ls" |
659 by (simp add: measure_space_def) |
527 by (simp add: measure_space_def) |
660 have "M \<subseteq> ls" |
528 have "M \<subseteq> ls" |
661 by (simp add: ls_def) |
529 by (simp add: ls_def) |
662 (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
530 (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
663 hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls" |
531 hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls" |
664 using sigma_algebra.sigma_sets_subset [OF sls, of "M"] |
532 using sigma_algebra.sigma_sets_subset [OF sls, of "M"] |
665 by simp |
533 by simp |
666 have "measure_space \<Omega> (sigma_sets \<Omega> M) ?infm" |
534 have "measure_space \<Omega> (sigma_sets \<Omega> M) ?O" |
667 by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
535 by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
668 (simp_all add: sgs_sb space_closed) |
536 (simp_all add: sgs_sb space_closed) |
669 thus ?thesis using inf_measure_agrees [OF posf ca] |
537 thus ?thesis using outer_measure_agrees [OF posf ca] |
670 by (intro exI[of _ ?infm]) auto |
538 by (intro exI[of _ ?O]) auto |
671 qed |
539 qed |
672 |
540 |
673 lemma (in ring_of_sets) caratheodory_empty_continuous: |
541 lemma (in ring_of_sets) caratheodory_empty_continuous: |
674 assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>" |
542 assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>" |
675 assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0" |
543 assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0" |