src/HOL/Probability/Borel_Space.thy
changeset 57275 0ddb5b755cdc
parent 57259 3a448982a74a
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -159,6 +159,18 @@
     1.4      using A by auto
     1.5  qed
     1.6  
     1.7 +lemma borel_measurable_continuous_countable_exceptions:
     1.8 +  fixes f :: "'a::t1_space \<Rightarrow> 'b::topological_space"
     1.9 +  assumes X: "countable X"
    1.10 +  assumes "continuous_on (- X) f"
    1.11 +  shows "f \<in> borel_measurable borel"
    1.12 +proof (rule measurable_discrete_difference[OF _ X])
    1.13 +  have "X \<in> sets borel"
    1.14 +    by (rule sets.countable[OF _ X]) auto
    1.15 +  then show "(\<lambda>x. if x \<in> X then undefined else f x) \<in> borel_measurable borel"
    1.16 +    by (intro borel_measurable_continuous_on_if assms continuous_intros)
    1.17 +qed auto
    1.18 +
    1.19  lemma borel_measurable_continuous_on1:
    1.20    "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
    1.21    using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
    1.22 @@ -691,6 +703,10 @@
    1.23  lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
    1.24    by (intro borel_measurable_continuous_on1 continuous_intros)
    1.25  
    1.26 +lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel"
    1.27 +  by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
    1.28 +     (auto intro!: continuous_on_sgn continuous_on_id)
    1.29 +
    1.30  lemma borel_measurable_uminus[measurable (raw)]:
    1.31    fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
    1.32    assumes g: "g \<in> borel_measurable M"
    1.33 @@ -780,21 +796,18 @@
    1.34    using affine_borel_measurable_vector[of f M a 1] by simp
    1.35  
    1.36  lemma borel_measurable_inverse[measurable (raw)]:
    1.37 -  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
    1.38 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
    1.39    assumes f: "f \<in> borel_measurable M"
    1.40    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
    1.41 -proof -
    1.42 -  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
    1.43 -    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
    1.44 -  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
    1.45 -    by (intro ext) auto
    1.46 -  finally show ?thesis using f by simp
    1.47 -qed
    1.48 +  apply (rule measurable_compose[OF f])
    1.49 +  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
    1.50 +  apply (auto intro!: continuous_on_inverse continuous_on_id)
    1.51 +  done
    1.52  
    1.53  lemma borel_measurable_divide[measurable (raw)]:
    1.54    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
    1.55 -    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
    1.56 -  by (simp add: field_divide_inverse)
    1.57 +    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M"
    1.58 +  by (simp add: divide_inverse)
    1.59  
    1.60  lemma borel_measurable_max[measurable (raw)]:
    1.61    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    1.62 @@ -846,19 +859,10 @@
    1.63  lemma borel_measurable_ln[measurable (raw)]:
    1.64    assumes f: "f \<in> borel_measurable M"
    1.65    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
    1.66 -proof -
    1.67 -  { fix x :: real assume x: "x \<le> 0"
    1.68 -    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
    1.69 -    from this[of x] x this[of 0] have "ln 0 = ln x"
    1.70 -      by (auto simp: ln_def) }
    1.71 -  note ln_imp = this
    1.72 -  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
    1.73 -    by (rule borel_measurable_continuous_on_open[OF _ _ f])
    1.74 -       (auto intro!: continuous_intros)
    1.75 -  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
    1.76 -    by (simp add: fun_eq_iff not_less ln_imp)
    1.77 -  finally show ?thesis .
    1.78 -qed
    1.79 +  apply (rule measurable_compose[OF f])
    1.80 +  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
    1.81 +  apply (auto intro!: continuous_on_ln continuous_on_id)
    1.82 +  done
    1.83  
    1.84  lemma borel_measurable_log[measurable (raw)]:
    1.85    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"