# HG changeset patch
# User hoelzl
# Date 1268044255 -3600
# Node ID f1315bbf1bc9b91d27b59142e2b9a3b72d7f9538
# Parent  74e4542d0a4a04175869988f1d59c61dbc5cb7ed
Moved theorems in Lebesgue to the right places

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
diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Mon Mar 08 09:38:59 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy	Mon Mar 08 11:30:55 2010 +0100
@@ -25,9 +25,58 @@
   shows "nonneg (neg_part f)"
   unfolding nonneg_def neg_part_def min_def by auto
 
+lemma (in measure_space)
+  assumes "f \<in> borel_measurable M"
+  shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"
+  and neg_part_borel_measurable: "neg_part f \<in> borel_measurable M"
+using assms
+proof -
+  { fix a :: real
+    { assume asm: "0 \<le> a"
+      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
+      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
+        unfolding pos_part_def using assms borel_measurable_le_iff by auto
+      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
+    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
+      unfolding pos_part_def using empty_sets by auto
+    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
+      using le_less_linear by auto
+  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+  { fix a :: real
+    { assume asm: "0 \<le> a"
+      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
+      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
+        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
+      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
+    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
+    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
+    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
+      using le_less_linear by auto
+  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
+qed
+
+lemma (in measure_space) pos_part_neg_part_borel_measurable_iff:
+  "f \<in> borel_measurable M \<longleftrightarrow>
+  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
+proof -
+  { fix x
+    have "f x = pos_part f x - neg_part f x"
+      unfolding pos_part_def neg_part_def unfolding max_def min_def
+      by auto }
+  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
+  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
+  from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]
+    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
+    this
+  show ?thesis by auto
+qed
+
 context measure_space
 begin
 
+section "Simple discrete step function"
+
 definition
  "pos_simple f =
   { (s :: nat set, a, x).
@@ -40,29 +89,6 @@
 definition
   "psfis f = pos_simple_integral ` (pos_simple f)"
 
-definition
-  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
-                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
-
-definition
-  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
-
-definition
-  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
-
-definition
-  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
-
-definition
-  "countable_space_integral f \<equiv>
-    let e = enumerate (f ` space M) in
-      suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
-
-definition
-  "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
-    f \<in> borel_measurable M \<and>
-    (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
-
 lemma pos_simpleE[consumes 1]:
   assumes ps: "(s, a, x) \<in> pos_simple f"
   obtains "finite s" and "nonneg f" and "nonneg x"
@@ -105,6 +131,11 @@
   shows "psfis f = psfis g"
   unfolding psfis_def using pos_simple_cong[OF assms] by simp
 
+lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
+  unfolding psfis_def pos_simple_def pos_simple_integral_def
+  by (auto simp: nonneg_def
+      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
+
 lemma pos_simple_setsum_indicator_fn:
   assumes ps: "(s, a, x) \<in> pos_simple f"
   and "t \<in> space M"
@@ -121,28 +152,7 @@
     using `i \<in> s` by simp
 qed
 
-lemma (in measure_space) measure_setsum_split:
-  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
-  assumes "(\<Union>i \<in> r. b i) = space M"
-  assumes "disjoint_family_on b r"
-  shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
-proof -
-  have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
-    using assms by auto
-  show ?thesis unfolding *
-  proof (rule measure_finitely_additive''[symmetric])
-    show "finite r" using `finite r` by auto
-    { fix i assume "i \<in> r"
-      hence "b i \<in> sets M" using br_in_M by auto
-      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
-    }
-    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
-      using `disjoint_family_on b r`
-      unfolding disjoint_family_on_def by auto
-  qed
-qed
-
-lemma (in measure_space) pos_simple_common_partition:
+lemma pos_simple_common_partition:
   assumes psf: "(s, a, x) \<in> pos_simple f"
   assumes psg: "(s', b, y) \<in> pos_simple g"
   obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
@@ -229,7 +239,7 @@
   qed
 qed
 
-lemma (in measure_space) pos_simple_integral_equal:
+lemma pos_simple_integral_equal:
   assumes psx: "(s, a, x) \<in> pos_simple f"
   assumes psy: "(s', b, y) \<in> pos_simple f"
   shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
@@ -269,7 +279,7 @@
   finally show "?left = ?right" .
 qed
 
-lemma (in measure_space)psfis_present:
+lemma psfis_present:
   assumes "A \<in> psfis f"
   assumes "B \<in> psfis g"
   obtains z z' c k where
@@ -295,7 +305,7 @@
   qed
 qed
 
-lemma (in measure_space) pos_simple_integral_add:
+lemma pos_simple_integral_add:
   assumes "(s, a, x) \<in> pos_simple f"
   assumes "(s', b, y) \<in> pos_simple g"
   obtains s'' c z where
@@ -468,70 +478,6 @@
   thus ?thesis using r unfolding psfis_def image_def by auto
 qed
 
-lemma pos_simple_integral_setsum_image:
-  assumes "finite P"
-  assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
-  obtains s' a' x' where
-  "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
-  "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
-using assms that
-proof (induct P arbitrary:thesis rule:finite.induct)
-  case emptyI note asms = this
-  def s' == "{0 :: nat}"
-  def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
-  def x' == "\<lambda> x :: nat. (0 :: real)"
-  have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
-    unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
-  moreover have "pos_simple_integral (s', a', x') = 0"
-    unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
-  ultimately show ?case using asms by auto
-next
-
-  case (insertI P c) note asms = this
-  then obtain s' a' x' where
-    sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
-         "pos_simple_integral (s', a', x') =
-             (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
-    by auto
-
-  { assume "c \<in> P"
-    hence "P = insert c P" by auto
-    hence thesis using asms sax by auto
-  }
-  moreover
-  { assume "c \<notin> P"
-    from asms obtain s'' a'' x'' where
-      sax': "s'' = s c" "a'' = a c" "x'' = x c"
-            "(s'', a'', x'') \<in> pos_simple (f c)" by auto
-    from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
-      tybbie:
-      "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
-      "(pos_simple_integral (s', a', x') +
-      pos_simple_integral (s'', a'', x'') =
-      pos_simple_integral (k, b, z))"
-      using pos_simple_integral_add by blast
-
-    from tybbie have
-      "pos_simple_integral (k, b, z) =
-      pos_simple_integral (s', a', x') +
-      pos_simple_integral (s'', a'', x'')" by simp
-    also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
-                  + pos_simple_integral (s c, a c, x c)"
-      using sax sax' by auto
-    also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
-      using asms `c \<notin> P` by auto
-    finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
-      by simp
-
-    have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
-      using `c \<notin> P` `finite P` by auto
-    hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
-      using tybbie by simp
-
-    from A B have thesis using asms by auto
-    } ultimately show thesis by blast
-qed
-
 lemma psfis_setsum_image:
   assumes "finite P"
   assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
@@ -577,57 +523,6 @@
 unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
 using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
 
-lemma pos_part_neg_part_borel_measurable:
-  assumes "f \<in> borel_measurable M"
-  shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
-using assms
-proof -
-  { fix a :: real
-    { assume asm: "0 \<le> a"
-      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
-      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
-        unfolding pos_part_def using assms borel_measurable_le_iff by auto
-      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
-    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
-      unfolding pos_part_def using empty_sets by auto
-    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
-      using le_less_linear by auto
-  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
-  { fix a :: real
-    { assume asm: "0 \<le> a"
-      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
-      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
-        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
-      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
-    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
-    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
-    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
-      using le_less_linear by auto
-  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
-  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
-qed
-
-lemma pos_part_neg_part_borel_measurable_iff:
-  "f \<in> borel_measurable M \<longleftrightarrow>
-  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
-proof -
-  { fix x
-    have "f x = pos_part f x - neg_part f x"
-      unfolding pos_part_def neg_part_def unfolding max_def min_def
-      by auto }
-  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
-  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
-  from pos_part_neg_part_borel_measurable[of f]
-    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
-    this
-  show ?thesis by auto
-qed
-
-lemma 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 psfis_borel_measurable:
   assumes "a \<in> psfis f"
   shows "f \<in> borel_measurable M"
@@ -654,21 +549,6 @@
   show ?thesis by simp
 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
-
 lemma psfis_mono_conv_mono:
   assumes mono: "mono_convergent u f (space M)"
   and ps_u: "\<And>n. x n \<in> psfis (u n)"
@@ -679,7 +559,6 @@
 proof (rule field_le_mult_one_interval)
   fix z :: real assume "0 < z" and "z < 1"
   hence "0 \<le> z" by auto
-(*  def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
   let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
 
   have "incseq x" unfolding incseq_def
@@ -783,6 +662,12 @@
   qed
 qed
 
+section "Continuous posititve integration"
+
+definition
+  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
+                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
+
 lemma psfis_nnfis:
   "a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
   unfolding nnfis_def mono_convergent_def incseq_def
@@ -1136,11 +1021,6 @@
   show ?thesis unfolding nnfis_def by auto
 qed
 
-lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
-  unfolding psfis_def pos_simple_def pos_simple_integral_def
-  by (auto simp: nonneg_def
-      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
-
 lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
   by (auto intro: the_equality nnfis_unique)
 
@@ -1158,6 +1038,14 @@
   show ?thesis by safe
 qed
 
+section "Lebesgue Integral"
+
+definition
+  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
+
+definition
+  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
+
 lemma integral_cong:
   assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
   shows "integral f = integral g"
@@ -1203,7 +1091,7 @@
     (is "\<exists>x. x \<in> nnfis ?pp \<and> _")
   proof (rule nnfis_dom_conv)
     show "?pp \<in> borel_measurable M"
-      using borel by (rule pos_part_neg_part_borel_measurable)
+      using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
     show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
     fix t assume "t \<in> space M"
     with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1217,7 +1105,7 @@
     (is "\<exists>x. x \<in> nnfis ?np \<and> _")
   proof (rule nnfis_dom_conv)
     show "?np \<in> borel_measurable M"
-      using borel by (rule pos_part_neg_part_borel_measurable)
+      using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
     show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
     fix t assume "t \<in> space M"
     with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1419,6 +1307,8 @@
     by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
 qed
 
+section "Lebesgue integration on finite space"
+
 lemma integral_finite_on_sets:
   assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
   shows "integral (\<lambda>x. f x * indicator_fn a x) =
@@ -1489,51 +1379,12 @@
   qed (auto intro!: image_eqI inj_onI)
 qed
 
-lemma 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
+section "Radon–Nikodym derivative"
 
-lemma 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)+
+definition
+  "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
+    f \<in> borel_measurable M \<and>
+    (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
 
 lemma RN_deriv_finite_singleton:
   fixes v :: "'a set \<Rightarrow> real"
@@ -1577,6 +1428,11 @@
     using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
 qed fact
 
+section "Lebesgue integration on countable spaces"
+
+definition
+  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
+
 lemma countable_space_integral_reduce:
   assumes "positive M (measure M)" and "f \<in> borel_measurable M"
   and "countable (f ` space M)"
diff -r 74e4542d0a4a -r f1315bbf1bc9 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Mon Mar 08 09:38:59 2010 +0100
+++ b/src/HOL/Probability/Measure.thy	Mon Mar 08 11:30:55 2010 +0100
@@ -997,4 +997,25 @@
       \<Longrightarrow> measure_space M"
   by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
 
+lemma (in measure_space) measure_setsum_split:
+  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
+  assumes "(\<Union>i \<in> r. b i) = space M"
+  assumes "disjoint_family_on b r"
+  shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
+proof -
+  have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
+    using assms by auto
+  show ?thesis unfolding *
+  proof (rule measure_finitely_additive''[symmetric])
+    show "finite r" using `finite r` by auto
+    { fix i assume "i \<in> r"
+      hence "b i \<in> sets M" using br_in_M by auto
+      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
+    }
+    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
+      using `disjoint_family_on b r`
+      unfolding disjoint_family_on_def by auto
+  qed
+qed
+
 end
\ No newline at end of file