diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Mar 08 09:38:59 2010 +0100
+++ b/src/HOL/Probability/Borel.thy	Mon Mar 08 11:30:55 2010 +0100
@@ -15,11 +15,6 @@
 definition indicator_fn where
   "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
 
-definition mono_convergent where
-  "mono_convergent u f s \<equiv>
-        (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
-        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
-
 lemma in_borel_measurable:
    "f \<in> borel_measurable M \<longleftrightarrow>
     sigma_algebra M \<and>
@@ -375,6 +370,95 @@
   by (fast intro: borel_measurable_add_borel_measurable 
                   borel_measurable_uminus_borel_measurable f g)
 
+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)
+  case empty
+  thus ?case
+    by (simp add: borel_measurable_const)
+next
+  case (insert x s)
+  thus ?case
+    by (auto simp add: borel_measurable_add_borel_measurable) 
+qed
+
+lemma (in measure_space) borel_measurable_cong:
+  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
+  shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
+using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
+
+lemma (in measure_space) borel_measurable_inverse:
+  assumes "f \<in> borel_measurable M"
+  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
+  unfolding borel_measurable_ge_iff
+proof (safe, rule linorder_cases)
+  fix a :: real assume "0 < a"
+  { fix w
+    from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
+      by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
+                linorder_not_le real_le_refl real_le_trans real_less_def
+                xt1(7) zero_less_divide_1_iff) }
+  hence "{w \<in> space M. a \<le> inverse (f w)} =
+    {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
+  with Int assms[unfolded borel_measurable_gr_iff]
+    assms[unfolded borel_measurable_le_iff]
+  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+next
+  fix a :: real assume "0 = a"
+  { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
+      unfolding `0 = a`[symmetric] by auto }
+  thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
+    using assms[unfolded borel_measurable_ge_iff] by simp
+next
+  fix a :: real assume "a < 0"
+  { fix w
+    from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
+      apply (cases "0 \<le> f w")
+      apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
+                   zero_le_divide_1_iff)
+      apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
+                   linorder_not_le real_le_refl real_le_trans)
+      done }
+  hence "{w \<in> space M. a \<le> inverse (f w)} =
+    {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
+  with Un assms[unfolded borel_measurable_ge_iff]
+    assms[unfolded borel_measurable_le_iff]
+  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+qed
+
+lemma (in measure_space) borel_measurable_divide:
+  assumes "f \<in> borel_measurable M"
+  and "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+  unfolding field_divide_inverse
+  by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+
+
+section "Monotone convergence"
+
+definition mono_convergent where
+  "mono_convergent u f s \<equiv>
+        (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
+        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+
+definition "upclose f g x = max (f x) (g x)"
+
+primrec mon_upclose where
+"mon_upclose 0 u = u 0" |
+"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
+
+lemma mono_convergentD:
+  assumes "mono_convergent u f s" and "x \<in> s"
+  shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
+  using assms unfolding mono_convergent_def by auto
+
+lemma mono_convergentI:
+  assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
+  assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
+  shows "mono_convergent u f s"
+  using assms unfolding mono_convergent_def by auto
+
 lemma (in measure_space) mono_convergent_borel_measurable:
   assumes u: "!!n. u n \<in> borel_measurable M"
   assumes mc: "mono_convergent u f (space M)"
@@ -409,44 +493,11 @@
     by (auto simp add: borel_measurable_le_iff) 
 qed
 
-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)
-  case empty
-  thus ?case
-    by (simp add: borel_measurable_const)
-next
-  case (insert x s)
-  thus ?case
-    by (auto simp add: borel_measurable_add_borel_measurable) 
-qed
-
-section "Monotone convergence"
-
-lemma mono_convergentD:
-  assumes "mono_convergent u f s" and "x \<in> s"
-  shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
-  using assms unfolding mono_convergent_def by auto
-
-
-lemma mono_convergentI:
-  assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
-  assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
-  shows "mono_convergent u f s"
-  using assms unfolding mono_convergent_def by auto
-
 lemma mono_convergent_le:
   assumes "mono_convergent u f s" and "t \<in> s"
   shows "u n t \<le> f t"
 using mono_convergentD[OF assms] by (auto intro!: incseq_le)
 
-definition "upclose f g x = max (f x) (g x)"
-
-primrec mon_upclose where
-"mon_upclose 0 u = u 0" |
-"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
-
 lemma mon_upclose_ex:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
   shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
@@ -561,4 +612,19 @@
   qed
 qed
 
+lemma mono_conv_outgrow:
+  assumes "incseq x" "x ----> y" "z < y"
+  shows "\<exists>b. \<forall> a \<ge> b. z < x a"
+using assms
+proof -
+  from assms have "y - z > 0" by simp
+  hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
+    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+    by simp
+  have "\<forall>m. x m \<le> y" using incseq_le assms by auto
+  hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
+    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+  from A B show ?thesis by auto
+qed
+
 end