summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Borel_Space.thy

changeset 42990 | 3706951a6421 |

parent 42950 | 6e5c2a3c69da |

child 43920 | cedb5cb948fd |

1.1 --- a/src/HOL/Probability/Borel_Space.thy Thu May 26 17:59:39 2011 +0200 1.2 +++ b/src/HOL/Probability/Borel_Space.thy Thu May 26 20:49:56 2011 +0200 1.3 @@ -1034,25 +1034,38 @@ 1.4 1.5 lemma borel_measurable_continuous_on: 1.6 fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space" 1.7 - assumes cont: "continuous_on A f" "open A" and f: "f -` {c} \<inter> A \<in> sets borel" 1.8 + assumes cont: "continuous_on A f" "open A" 1.9 shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _") 1.10 proof (rule borel.borel_measurableI) 1.11 fix S :: "'b set" assume "open S" 1.12 - then have "open {x\<in>A. f x \<in> S - {c}}" 1.13 + then have "open {x\<in>A. f x \<in> S}" 1.14 by (intro continuous_open_preimage[OF cont]) auto 1.15 - then have *: "{x\<in>A. f x \<in> S - {c}} \<in> sets borel" by auto 1.16 - show "?f -` S \<inter> space borel \<in> sets borel" 1.17 - proof cases 1.18 - assume "c \<in> S" 1.19 - then have "?f -` S = {x\<in>A. f x \<in> S - {c}} \<union> (f -` {c} \<inter> A) \<union> -A" 1.20 - by auto 1.21 - with * show "?f -` S \<inter> space borel \<in> sets borel" 1.22 - using `open A` f by (auto intro!: borel.Un) 1.23 - next 1.24 - assume "c \<notin> S" 1.25 - then have "?f -` S = {x\<in>A. f x \<in> S - {c}}" by (auto split: split_if_asm) 1.26 - with * show "?f -` S \<inter> space borel \<in> sets borel" by auto 1.27 + then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto 1.28 + have "?f -` S \<inter> space borel = 1.29 + {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})" 1.30 + by (auto split: split_if_asm) 1.31 + also have "\<dots> \<in> sets borel" 1.32 + using * `open A` by (auto simp del: space_borel intro!: borel.Un) 1.33 + finally show "?f -` S \<inter> space borel \<in> sets borel" . 1.34 +qed 1.35 + 1.36 +lemma (in sigma_algebra) convex_measurable: 1.37 + fixes a b :: real 1.38 + assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}" 1.39 + assumes q: "convex_on { a <..< b} q" 1.40 + shows "q \<circ> X \<in> borel_measurable M" 1.41 +proof - 1.42 + have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<in> borel_measurable borel" 1.43 + proof (rule borel_measurable_continuous_on) 1.44 + show "open {a<..<b}" by auto 1.45 + from this q show "continuous_on {a<..<b} q" 1.46 + by (rule convex_on_continuous) 1.47 qed 1.48 + then have "(\<lambda>x. if x \<in> {a <..< b} then q x else 0) \<circ> X \<in> borel_measurable M" (is ?qX) 1.49 + using X by (intro measurable_comp) auto 1.50 + moreover have "?qX \<longleftrightarrow> q \<circ> X \<in> borel_measurable M" 1.51 + using X by (intro measurable_cong) auto 1.52 + ultimately show ?thesis by simp 1.53 qed 1.54 1.55 lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel" 1.56 @@ -1068,17 +1081,6 @@ 1.57 by (auto intro!: continuous_at_imp_continuous_on DERIV_log DERIV_isCont 1.58 simp: continuous_isCont[symmetric]) 1.59 show "open ({0<..}::real set)" by auto 1.60 - show "log b -` {log b 0} \<inter> {0<..} \<in> sets borel" 1.61 - proof cases 1.62 - assume "log b -` {log b 0} \<inter> {0<..} = {}" 1.63 - then show ?thesis by simp 1.64 - next 1.65 - assume "log b -` {log b 0} \<inter> {0<..} \<noteq> {}" 1.66 - then obtain x where "0 < x" "log b x = log b 0" by auto 1.67 - with log_inj[OF `1 < b`] have "log b -` {log b 0} \<inter> {0<..} = {x}" 1.68 - by (auto simp: inj_on_def) 1.69 - then show ?thesis by simp 1.70 - qed 1.71 qed 1.72 also have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) = log b" 1.73 by (simp add: fun_eq_iff not_less log_imp)