author paulson Mon, 09 Nov 2009 16:06:08 +0000 changeset 33535 b233f48a4d3d parent 33534 b21c820dfb63 child 33536 fd28b7399f2b child 33541 e716c6ad381b child 33585 8d39394fe5cf
fixed some inappropriate names
```--- a/src/HOL/Probability/Borel.thy	Mon Nov 09 15:50:31 2009 +0000
+++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 16:06:08 2009 +0000
@@ -264,7 +264,7 @@
qed

-lemma (in measure_space) borel_measurable_plus_borel_measurable:
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
@@ -352,18 +352,18 @@
proof -
have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
by (fast intro: affine_borel_measurable borel_measurable_square
-                    borel_measurable_plus_borel_measurable f g)
have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
(\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
also have "... \<in> borel_measurable M"
by (fast intro: affine_borel_measurable borel_measurable_square
-                    borel_measurable_plus_borel_measurable
borel_measurable_uminus_borel_measurable f g)
finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
show ?thesis
-    using 1 2 apply (simp add: borel_measurable_plus_borel_measurable)
done
qed

@@ -372,7 +372,7 @@
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
unfolding real_diff_def
-  by (fast intro: borel_measurable_plus_borel_measurable
borel_measurable_uminus_borel_measurable f g)

lemma (in measure_space) mono_convergent_borel_measurable:
@@ -409,7 +409,7 @@
qed

-lemma (in measure_space) borel_measurable_SIGMA_borel_measurable:
+lemma (in measure_space) borel_measurable_setsum_borel_measurable:
assumes s: "finite s"
shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
proof (induct s)
@@ -419,7 +419,7 @@
next
case (insert x s)
thus ?case
-    by (auto simp add: borel_measurable_plus_borel_measurable)