src/HOL/Probability/Borel_Space.thy
 changeset 43923 ab93d0190a5d parent 43920 cedb5cb948fd child 44282 f0de18b62d63
equal inserted replaced
43922:c6f35921056e 43923:ab93d0190a5d
`  1120   have open_real: "open (real -` (B - {0}) :: ereal set)"`
`  1120   have open_real: "open (real -` (B - {0}) :: ereal set)"`
`  1121     unfolding open_ereal_def * using `open B` by auto`
`  1121     unfolding open_ereal_def * using `open B` by auto`
`  1122   show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"`
`  1122   show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"`
`  1123   proof cases`
`  1123   proof cases`
`  1124     assume "0 \<in> B"`
`  1124     assume "0 \<in> B"`
`  1125     then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0}"`
`  1125     then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"`
`  1126       by (auto simp add: real_of_ereal_eq_0)`
`  1126       by (auto simp add: real_of_ereal_eq_0)`
`  1127     then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"`
`  1127     then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"`
`  1128       using open_real by auto`
`  1128       using open_real by auto`
`  1129   next`
`  1129   next`
`  1130     assume "0 \<notin> B"`
`  1130     assume "0 \<notin> B"`
`  1146   from borel_measurable_real_of_ereal[OF this]`
`  1146   from borel_measurable_real_of_ereal[OF this]`
`  1147   show "f \<in> borel_measurable M" by auto`
`  1147   show "f \<in> borel_measurable M" by auto`
`  1148 qed auto`
`  1148 qed auto`
`  1149 `
`  1149 `
`  1150 lemma (in sigma_algebra) borel_measurable_ereal_iff_real:`
`  1150 lemma (in sigma_algebra) borel_measurable_ereal_iff_real:`
`  1151   "f \<in> borel_measurable M \<longleftrightarrow>`
`  1151   fixes f :: "'a \<Rightarrow> ereal"`
`       `
`  1152   shows "f \<in> borel_measurable M \<longleftrightarrow>`
`  1152     ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)"`
`  1153     ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)"`
`  1153 proof safe`
`  1154 proof safe`
`  1154   assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"`
`  1155   assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"`
`  1155   have "f -` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f -` {-\<infinity>} \<inter> space M = {x\<in>space M. f x = -\<infinity>}" by auto`
`  1156   have "f -` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f -` {-\<infinity>} \<inter> space M = {x\<in>space M. f x = -\<infinity>}" by auto`
`  1156   with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = -\<infinity>} \<in> sets M" by simp_all`
`  1157   with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = -\<infinity>} \<in> sets M" by simp_all`
`  1206 proof`
`  1207 proof`
`  1207   assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp`
`  1208   assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp`
`  1208 qed auto`
`  1209 qed auto`
`  1209 `
`  1210 `
`  1210 lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal:`
`  1211 lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal:`
`  1211   "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"`
`  1212   fixes f :: "'a \<Rightarrow> ereal"`
`       `
`  1213   shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"`
`  1212 proof (intro iffI allI)`
`  1214 proof (intro iffI allI)`
`  1213   assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"`
`  1215   assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"`
`  1214   show "f \<in> borel_measurable M"`
`  1216   show "f \<in> borel_measurable M"`
`  1215     unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le`
`  1217     unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le`
`  1216   proof (intro conjI allI)`
`  1218   proof (intro conjI allI)`
`  1224       qed }`
`  1226       qed }`
`  1225     then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"`
`  1227     then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"`
`  1226       by (auto simp: not_le)`
`  1228       by (auto simp: not_le)`
`  1227     then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)`
`  1229     then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)`
`  1228     moreover`
`  1230     moreover`
`  1229     have "{-\<infinity>} = {..-\<infinity>}" by auto`
`  1231     have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto`
`  1230     then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto`
`  1232     then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto`
`  1231     moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"`
`  1233     moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"`
`  1232       using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)`
`  1234       using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)`
`  1233     moreover have "{w \<in> space M. real (f w) \<le> a} =`
`  1235     moreover have "{w \<in> space M. real (f w) \<le> a} =`
`  1234       (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M`
`  1236       (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M`