src/HOL/Probability/Borel_Space.thy
changeset 41830 719b0a517c33
parent 41545 9c869baf1c66
child 41969 1cf3e4107a2a
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Feb 22 16:07:23 2011 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Feb 23 11:33:45 2011 +0100
     1.3 @@ -48,6 +48,9 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
     1.8 +  unfolding Compl_eq_Diff_UNIV by (intro borel.Diff) auto
     1.9 +
    1.10  lemma (in sigma_algebra) borel_measurable_vimage:
    1.11    fixes f :: "'a \<Rightarrow> 'x::t2_space"
    1.12    assumes borel: "f \<in> borel_measurable M"
    1.13 @@ -1118,6 +1121,73 @@
    1.14      using * ** by auto
    1.15  qed
    1.16  
    1.17 +lemma borel_measurable_continuous_on1:
    1.18 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
    1.19 +  assumes "continuous_on UNIV f"
    1.20 +  shows "f \<in> borel_measurable borel"
    1.21 +  apply(rule borel.borel_measurableI)
    1.22 +  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
    1.23 +
    1.24 +lemma borel_measurable_continuous_on:
    1.25 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
    1.26 +  assumes cont: "continuous_on A f" "open A" and f: "f -` {c} \<inter> A \<in> sets borel"
    1.27 +  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
    1.28 +proof (rule borel.borel_measurableI)
    1.29 +  fix S :: "'b set" assume "open S"
    1.30 +  then have "open {x\<in>A. f x \<in> S - {c}}"
    1.31 +    by (intro continuous_open_preimage[OF cont]) auto
    1.32 +  then have *: "{x\<in>A. f x \<in> S - {c}} \<in> sets borel" by auto
    1.33 +  show "?f -` S \<inter> space borel \<in> sets borel"
    1.34 +  proof cases
    1.35 +    assume "c \<in> S"
    1.36 +    then have "?f -` S = {x\<in>A. f x \<in> S - {c}} \<union> (f -` {c} \<inter> A) \<union> -A"
    1.37 +      by auto
    1.38 +    with * show "?f -` S \<inter> space borel \<in> sets borel"
    1.39 +      using `open A` f by (auto intro!: borel.Un)
    1.40 +  next
    1.41 +    assume "c \<notin> S"
    1.42 +    then have "?f -` S = {x\<in>A. f x \<in> S - {c}}" by (auto split: split_if_asm)
    1.43 +    with * show "?f -` S \<inter> space borel \<in> sets borel" by auto
    1.44 +  qed
    1.45 +qed
    1.46 +
    1.47 +lemma borel_measurable_borel_log: assumes "1 < b" shows "log b \<in> borel_measurable borel"
    1.48 +proof -
    1.49 +  { fix x :: real assume x: "x \<le> 0"
    1.50 +    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
    1.51 +    from this[of x] x this[of 0] have "log b 0 = log b x"
    1.52 +      by (auto simp: ln_def log_def) }
    1.53 +  note log_imp = this
    1.54 +  have "(\<lambda>x. if x \<in> {0<..} then log b x else log b 0) \<in> borel_measurable borel"
    1.55 +  proof (rule borel_measurable_continuous_on)
    1.56 +    show "continuous_on {0<..} (log b)"
    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)
    1.74 +  finally show ?thesis .
    1.75 +qed
    1.76 +
    1.77 +lemma (in sigma_algebra) borel_measurable_log[simp,intro]:
    1.78 +  assumes f: "f \<in> borel_measurable M" and "1 < b"
    1.79 +  shows "(\<lambda>x. log b (f x)) \<in> borel_measurable M"
    1.80 +  using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
    1.81 +  by (simp add: comp_def)
    1.82 +
    1.83 +
    1.84  lemma (in sigma_algebra) less_eq_ge_measurable:
    1.85    fixes f :: "'a \<Rightarrow> 'c::linorder"
    1.86    shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M"