author | hoelzl |

Tue May 17 14:36:54 2011 +0200 (2011-05-17) | |

changeset 42866 | b0746bd57a41 |

parent 42865 | 36353d913424 |

child 42867 | 760094e49a2c |

the measurable sets with null measure form a ring

1.1 --- a/src/HOL/Probability/Complete_Measure.thy Tue May 17 12:24:48 2011 +0200 1.2 +++ b/src/HOL/Probability/Complete_Measure.thy Tue May 17 14:36:54 2011 +0200 1.3 @@ -144,7 +144,7 @@ 1.4 have "(\<Union>i. S i) \<in> sets completion" using S by auto 1.5 from null_part[OF this] guess N' .. note N' = this 1.6 let ?N = "(\<Union>i. N i) \<union> N'" 1.7 - have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto 1.8 + have null_set: "?N \<in> null_sets" using N' UN_N by (intro nullsets.Un) auto 1.9 have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N" 1.10 using N' by auto 1.11 also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N" 1.12 @@ -212,7 +212,7 @@ 1.13 from choice[OF this] obtain N where 1.14 N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto 1.15 let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x" 1.16 - have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto 1.17 + have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto 1.18 show ?thesis unfolding simple_function_def 1.19 proof (safe intro!: exI[of _ ?f']) 1.20 have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto

2.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 12:24:48 2011 +0200 2.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 14:36:54 2011 +0200 2.3 @@ -917,8 +917,9 @@ 2.4 with i show "A \<in> sigma_sets ?O ?G" 2.5 by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto 2.6 qed 2.7 - finally show "sets (Pi\<^isub>P I M) = sets ?S" 2.8 + also have "\<dots> = sets ?S" 2.9 by (simp add: sets_sigma) 2.10 + finally show "sets (Pi\<^isub>P I M) = sets ?S" . 2.11 qed simp_all 2.12 2.13 lemma (in product_prob_space) measurable_into_infprod_algebra:

3.1 --- a/src/HOL/Probability/Measure.thy Tue May 17 12:24:48 2011 +0200 3.2 +++ b/src/HOL/Probability/Measure.thy Tue May 17 14:36:54 2011 +0200 3.3 @@ -552,16 +552,20 @@ 3.4 3.5 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}" 3.6 3.7 -lemma (in measure_space) null_sets_Un[intro]: 3.8 - assumes "N \<in> null_sets" "N' \<in> null_sets" 3.9 - shows "N \<union> N' \<in> null_sets" 3.10 -proof (intro conjI CollectI) 3.11 - show "N \<union> N' \<in> sets M" using assms by auto 3.12 - then have "0 \<le> \<mu> (N \<union> N')" by simp 3.13 - moreover have "\<mu> (N \<union> N') \<le> \<mu> N + \<mu> N'" 3.14 - using assms by (intro measure_subadditive) auto 3.15 - ultimately show "\<mu> (N \<union> N') = 0" using assms by auto 3.16 -qed 3.17 +sublocale measure_space \<subseteq> nullsets!: ring_of_sets "\<lparr> space = space M, sets = null_sets \<rparr>" 3.18 + where "space \<lparr> space = space M, sets = null_sets \<rparr> = space M" 3.19 + and "sets \<lparr> space = space M, sets = null_sets \<rparr> = null_sets" 3.20 +proof - 3.21 + { fix A B assume sets: "A \<in> sets M" "B \<in> sets M" 3.22 + moreover then have "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B" "\<mu> (A - B) \<le> \<mu> A" 3.23 + by (auto intro!: measure_subadditive measure_mono) 3.24 + moreover assume "\<mu> B = 0" "\<mu> A = 0" 3.25 + ultimately have "\<mu> (A - B) = 0" "\<mu> (A \<union> B) = 0" 3.26 + by (auto intro!: antisym) } 3.27 + note null = this 3.28 + show "ring_of_sets \<lparr> space = space M, sets = null_sets \<rparr>" 3.29 + by default (insert sets_into_space null, auto) 3.30 +qed simp_all 3.31 3.32 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))" 3.33 proof - 3.34 @@ -583,17 +587,6 @@ 3.35 ultimately show "\<mu> (\<Union>i. N i) = 0" using assms by auto 3.36 qed 3.37 3.38 -lemma (in measure_space) null_sets_finite_UN: 3.39 - assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets" 3.40 - shows "(\<Union>i\<in>S. A i) \<in> null_sets" 3.41 -proof (intro CollectI conjI) 3.42 - show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto 3.43 - then have "0 \<le> \<mu> (\<Union>i\<in>S. A i)" by simp 3.44 - moreover have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))" 3.45 - using assms by (intro measure_finitely_subadditive) auto 3.46 - ultimately show "\<mu> (\<Union>i\<in>S. A i) = 0" using assms by auto 3.47 -qed 3.48 - 3.49 lemma (in measure_space) null_set_Int1: 3.50 assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets" 3.51 using assms proof (intro CollectI conjI)

4.1 --- a/src/HOL/Probability/Radon_Nikodym.thy Tue May 17 12:24:48 2011 +0200 4.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy Tue May 17 14:36:54 2011 +0200 4.3 @@ -975,7 +975,7 @@ 4.4 finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" by simp } 4.5 from this[OF borel(1) refl] this[OF borel(2) f] 4.6 have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>} \<in> null_sets" by simp_all 4.7 - then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule null_sets_Un) 4.8 + then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule nullsets.Un) 4.9 show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq> 4.10 (Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def) 4.11 qed