summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Borel_Space.thy

changeset 44537 | c10485a6a7af |

parent 44282 | f0de18b62d63 |

child 44666 | 8670a39d4420 |

--- a/src/HOL/Probability/Borel_Space.thy Wed Sep 08 16:10:49 2010 -0700 +++ b/src/HOL/Probability/Borel_Space.thy Fri Aug 26 15:00:00 2011 -0700 @@ -11,7 +11,7 @@ section "Generic Borel spaces" -definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = open\<rparr>" +definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = {S. open S}\<rparr>" abbreviation "borel_measurable M \<equiv> measurable M borel" interpretation borel: sigma_algebra borel @@ -19,7 +19,7 @@ lemma in_borel_measurable: "f \<in> borel_measurable M \<longleftrightarrow> - (\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = open\<rparr>). + (\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = {S. open S}\<rparr>). f -` S \<inter> space M \<in> sets M)" by (auto simp add: measurable_def borel_def) @@ -35,7 +35,7 @@ lemma borel_open[simp]: assumes "open A" shows "A \<in> sets borel" proof - - have "A \<in> open" unfolding mem_def using assms . + have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic) qed @@ -71,8 +71,8 @@ shows "f \<in> borel_measurable M" unfolding borel_def proof (rule measurable_sigma, simp_all) - fix S :: "'x set" assume "S \<in> open" thus "f -` S \<inter> space M \<in> sets M" - using assms[of S] by (simp add: mem_def) + fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M" + using assms[of S] by simp qed lemma borel_singleton[simp, intro]: @@ -391,7 +391,8 @@ proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp then interpret sigma_algebra ?SIGMA . - { fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def . + { fix S :: "'a set" assume "S \<in> {S. open S}" + then have "open S" unfolding mem_Collect_eq . from open_UNION[OF this] obtain I where *: "S = (\<Union>(a, b)\<in>I. @@ -647,8 +648,8 @@ proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . - { fix M :: "'a set" assume "M \<in> open" - then have "open M" by (simp add: mem_def) + { fix M :: "'a set" assume "M \<in> {S. open S}" + then have "open M" by simp have "M \<in> sets ?SIGMA" apply (subst open_UNION[OF `open M`]) apply (safe intro!: countable_UN) @@ -784,7 +785,7 @@ "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma, simp_all) - fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def . + fix S::"real set" assume "open S" from open_vimage_euclidean_component[OF this] show "(\<lambda>x. x $$ i) -` S \<in> sets borel" by (auto intro: borel_open) @@ -815,8 +816,8 @@ show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M" proof cases assume "b \<noteq> 0" - with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open") - by (auto intro!: open_affinity simp: scaleR_add_right mem_def) + with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S") + by (auto intro!: open_affinity simp: scaleR_add_right) hence "?S \<in> sets borel" unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) moreover @@ -1099,8 +1100,8 @@ "ereal \<in> borel_measurable borel" unfolding borel_def[where 'a=ereal] proof (rule borel.measurable_sigma) - fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open \<rparr>" - then have "open X" by (auto simp: mem_def) + fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" + then have "open X" by simp then have "open (ereal -` X \<inter> space borel)" by (simp add: open_ereal_vimage) then show "ereal -` X \<inter> space borel \<in> sets borel" by auto @@ -1114,8 +1115,8 @@ "(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma) - fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = open \<rparr>" - then have "open B" by (auto simp: mem_def) + fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>" + then have "open B" by simp have *: "ereal -` real -` (B - {0}) = B - {0}" by auto have open_real: "open (real -` (B - {0}) :: ereal set)" unfolding open_ereal_def * using `open B` by auto @@ -1190,8 +1191,8 @@ lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal: "(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel" proof (subst borel_def, rule borel.measurable_sigma) - fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open\<rparr>" - then have "open X" by (simp add: mem_def) + fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S}\<rparr>" + then have "open X" by simp have "uminus -` X = uminus ` X" by (force simp: image_iff) then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto then show "uminus -` X \<inter> space borel \<in> sets borel" by auto