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.26  qed (simp add: borel_measurable_const)
    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)