src/HOL/Probability/Borel_Space.thy
 changeset 40870 94427db32392 parent 40869 251df82c0088 child 41023 9118eb4eb8dc
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:09:41 2010 +0100
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:12:53 2010 +0100
1.3 @@ -1016,7 +1016,6 @@
1.4    then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B - {\<omega>}" and
1.5      x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B"
1.6      unfolding open_pinfreal_def by blast
1.7 -
1.8    have "Real -` B = Real -` (B - {\<omega>})" by auto
1.9    also have "\<dots> = Real -` (Real ` (T \<inter> {0..}))" using T by simp
1.10    also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})"
1.11 @@ -1222,12 +1221,10 @@
1.12    hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M"
1.13      unfolding less_eq_le_pinfreal_measurable
1.14      unfolding greater_eq_le_measurable .
1.15 -
1.16    show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater
1.17    proof safe
1.18      have "f -` {\<omega>} \<inter> space M = space M - {x\<in>space M. f x < \<omega>}" by auto
1.19      then show \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" using ** by auto
1.20 -
1.21      fix a
1.22      have "{w \<in> space M. a < real (f w)} =
1.23        (if 0 \<le> a then {w\<in>space M. Real a < f w} - (f -` {\<omega>} \<inter> space M) else space M)"
1.24 @@ -1358,14 +1355,14 @@
1.25      by induct auto
1.27
1.28 -lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]:
1.29 +lemma (in sigma_algebra) borel_measurable_pinfreal_min[simp, intro]:
1.30    fixes f g :: "'a \<Rightarrow> pinfreal"
1.31    assumes "f \<in> borel_measurable M"
1.32    assumes "g \<in> borel_measurable M"
1.33    shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
1.34    using assms unfolding min_def by (auto intro!: measurable_If)
1.35
1.36 -lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]:
1.37 +lemma (in sigma_algebra) borel_measurable_pinfreal_max[simp, intro]:
1.38    fixes f g :: "'a \<Rightarrow> pinfreal"
1.39    assumes "f \<in> borel_measurable M"
1.40    and "g \<in> borel_measurable M"
1.41 @@ -1412,7 +1409,7 @@
1.42      using assms by auto
1.43  qed
1.44
1.45 -lemma (in sigma_algebra) borel_measurable_psuminf:
1.46 +lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
1.47    assumes "\<And>i. f i \<in> borel_measurable M"
1.48    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
1.49    using assms unfolding psuminf_def
1.50 @@ -1428,7 +1425,6 @@
1.51  proof -
1.52    let "?pu x i" = "max (u i x) 0"
1.53    let "?nu x i" = "max (- u i x) 0"
1.54 -
1.55    { fix x assume x: "x \<in> space M"
1.56      have "(?pu x) ----> max (u' x) 0"
1.57        "(?nu x) ----> max (- u' x) 0"
1.58 @@ -1438,10 +1434,8 @@
1.59        "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)"
1.60        by (simp_all add: Real_max'[symmetric]) }
1.61    note eq = this
1.62 -
1.63    have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
1.64      by auto
1.65 -
1.66    have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
1.67         "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
1.68      using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
```