src/HOL/Probability/Borel_Space.thy
 changeset 41026 bea75746dc9d parent 41025 8b2cd85ecf11 child 41080 294956ff285b
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Dec 06 19:54:53 2010 +0100
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Dec 06 19:54:56 2010 +0100
1.3 @@ -847,6 +847,15 @@
1.5  qed
1.6
1.7 +lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
1.8 +  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.9 +  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.10 +  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.11 +proof cases
1.12 +  assume "finite S"
1.13 +  thus ?thesis using assms by induct auto
1.14 +qed simp
1.15 +
1.16  lemma (in sigma_algebra) borel_measurable_square:
1.17    fixes f :: "'a \<Rightarrow> real"
1.18    assumes f: "f \<in> borel_measurable M"
1.19 @@ -930,6 +939,15 @@
1.20      using 1 2 by simp
1.21  qed
1.22
1.23 +lemma (in sigma_algebra) borel_measurable_setprod[simp, intro]:
1.24 +  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.25 +  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.26 +  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
1.27 +proof cases
1.28 +  assume "finite S"
1.29 +  thus ?thesis using assms by induct auto
1.30 +qed simp
1.31 +
1.32  lemma (in sigma_algebra) borel_measurable_diff[simp, intro]:
1.33    fixes f :: "'a \<Rightarrow> real"
1.34    assumes f: "f \<in> borel_measurable M"
1.35 @@ -937,15 +955,6 @@
1.36    shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
1.37    unfolding diff_minus using assms by fast
1.38
1.39 -lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
1.40 -  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
1.41 -  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
1.42 -  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
1.43 -proof cases
1.44 -  assume "finite S"
1.45 -  thus ?thesis using assms by induct auto
1.46 -qed simp
1.47 -
1.48  lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]:
1.49    fixes f :: "'a \<Rightarrow> real"
1.50    assumes "f \<in> borel_measurable M"
1.51 @@ -1007,6 +1016,11 @@
1.52    show ?thesis unfolding * using assms by auto
1.53  qed
1.54
1.55 +lemma borel_measurable_nth[simp, intro]:
1.56 +  "(\<lambda>x::real^'n. x \$ i) \<in> borel_measurable borel"
1.57 +  using borel_measurable_euclidean_component
1.58 +  unfolding nth_conv_component by auto
1.59 +
1.60  section "Borel space over the real line with infinity"
1.61
1.62  lemma borel_Real_measurable:
```