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.4      by (simp add: borel_measurable_iff_ge)
     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: