--- a/src/HOL/Probability/Borel_Space.thy Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Thu Jun 12 15:47:36 2014 +0200
@@ -35,6 +35,9 @@
lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
unfolding borel_def by auto
+lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
+ unfolding borel_def by (rule sets_measure_of) simp
+
lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
unfolding borel_def pred_def by auto
@@ -801,6 +804,20 @@
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
by (simp add: min_def)
+lemma borel_measurable_Min[measurable (raw)]:
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
+proof (induct I rule: finite_induct)
+ case (insert i I) then show ?case
+ by (cases "I = {}") auto
+qed auto
+
+lemma borel_measurable_Max[measurable (raw)]:
+ "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
+proof (induct I rule: finite_induct)
+ case (insert i I) then show ?case
+ by (cases "I = {}") auto
+qed auto
+
lemma borel_measurable_abs[measurable (raw)]:
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
unfolding abs_real_def by simp
@@ -874,6 +891,36 @@
"f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
by simp
+lemma borel_measurable_root [measurable]: "(root n) \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_power [measurable (raw)]:
+ fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
+ assumes f: "f \<in> borel_measurable M"
+ shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M"
+ by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
+
+lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_sin [measurable]: "sin \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_cos [measurable]: "cos \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
+ by (intro borel_measurable_continuous_on1 continuous_intros)
+
subsection "Borel space on the extended reals"
lemma borel_measurable_ereal[measurable (raw)]: