the measurable sets with null measure form a ring
authorhoelzl
Tue May 17 14:36:54 2011 +0200 (2011-05-17)
changeset 42866b0746bd57a41
parent 42865 36353d913424
child 42867 760094e49a2c
the measurable sets with null measure form a ring
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
     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