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)