# HG changeset patch
# User hoelzl
# Date 1401458190 -7200
# Node ID f174712d0a843ca25c6ffc20443dea152443f963
# Parent  653e56c6c963b096c294f90421a839dd8f77db0a
better support for restrict_space

diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Fri May 30 15:56:30 2014 +0200
@@ -856,6 +856,32 @@
     by (rule has_bochner_integral_eq)
 qed
 
+lemma simple_bochner_integrable_restrict_space:
+  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
+  shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
+    simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+  by (simp add: simple_bochner_integrable.simps space_restrict_space
+    simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
+    indicator_eq_0_iff conj_ac)
+
+lemma simple_bochner_integral_restrict_space:
+  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
+  assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
+  shows "simple_bochner_integral (restrict_space M \<Omega>) f =
+    simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+proof -
+  have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
+    using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
+    by (simp add: simple_bochner_integrable.simps simple_function_def)
+  then show ?thesis
+    by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
+                   simple_bochner_integral_def Collect_restrict
+             split: split_indicator split_indicator_asm
+             intro!: setsum_mono_zero_cong_left arg_cong2[where f=measure])
+qed
+
 inductive integrable for M f where
   "has_bochner_integral M f x \<Longrightarrow> integrable M f"
 
@@ -1251,14 +1277,14 @@
   by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
            cong: conj_cong)
 
-lemma integral_dominated_convergence:
+lemma
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
   assumes lim: "AE x in M. (\<lambda>i. s i x) ----> f x"
   assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
-  shows "integrable M f"
-    and "\<And>i. integrable M (s i)"
-    and "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
+  shows integrable_dominated_convergence: "integrable M f"
+    and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
+    and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
 proof -
   have "AE x in M. 0 \<le> w x"
     using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
@@ -1421,13 +1447,14 @@
     finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
   qed
 
-  note int = integral_dominated_convergence(1,3)[OF _ _ 1 2 3]
+  note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
+  note int = integral_dominated_convergence[OF _ _ 1 2 3]
 
   show "integrable M ?S"
-    by (rule int) measurable
+    by (rule ibl) measurable
 
   show "?f sums ?x" unfolding sums_def
-    using int(2) by (simp add: integrable)
+    using int by (simp add: integrable)
   then show "?x = suminf ?f" "summable ?f"
     unfolding sums_iff by auto
 qed
@@ -1600,6 +1627,49 @@
     by simp
 qed
 
+subsection {* Restricted measure spaces *}
+
+lemma integrable_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
+  shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+  unfolding integrable_iff_bounded
+    borel_measurable_restrict_space_iff[OF \<Omega>]
+    nn_integral_restrict_space[OF \<Omega>]
+  by (simp add: ac_simps ereal_indicator times_ereal.simps(1)[symmetric] del: times_ereal.simps)
+
+lemma integral_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
+  shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+proof (rule integral_eq_cases)
+  assume "integrable (restrict_space M \<Omega>) f"
+  then show ?thesis
+  proof induct
+    case (base A c) then show ?case
+      by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
+                    emeasure_restrict_space Int_absorb1 measure_restrict_space)
+  next
+    case (add g f) then show ?case
+      by (simp add: scaleR_add_right integrable_restrict_space)
+  next
+    case (lim f s)
+    show ?case
+    proof (rule LIMSEQ_unique)
+      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> integral\<^sup>L (restrict_space M \<Omega>) f"
+        using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
+      
+      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
+        unfolding lim
+        using lim
+        by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
+           (auto simp add: space_restrict_space integrable_restrict_space
+                 simp del: norm_scaleR
+                 split: split_indicator)
+    qed
+  qed
+qed (simp add: integrable_restrict_space)
+
 subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density:
@@ -1653,7 +1723,7 @@
     show ?case
     proof (rule LIMSEQ_unique)
       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
-      proof (rule integral_dominated_convergence(3))
+      proof (rule integral_dominated_convergence)
         show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
           by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
         show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x"
@@ -1663,7 +1733,7 @@
       qed auto
       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
         unfolding lim(2)[symmetric]
-        by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
+        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
            (insert lim(3-5), auto)
     qed
   qed
@@ -1732,7 +1802,7 @@
     show ?case
     proof (rule LIMSEQ_unique)
       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
-      proof (rule integral_dominated_convergence(3))
+      proof (rule integral_dominated_convergence)
         show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
           using lim by (auto simp: integrable_distr_eq) 
         show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
@@ -1742,7 +1812,7 @@
       qed auto
       show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
         unfolding lim(2)[symmetric]
-        by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
+        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
            (insert lim(3-5), auto)
     qed
   qed
diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Fri May 30 15:56:30 2014 +0200
@@ -119,6 +119,52 @@
   shows "f \<in> borel_measurable M"
   using assms unfolding measurable_def by auto
 
+lemma borel_measurable_restrict_space_iff_ereal:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
+  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
+    (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
+proof -
+  { fix X :: "ereal set" assume "X \<in> sets borel"
+    have 1: "(\<lambda>x. f x * indicator \<Omega> x) -` X \<inter> space M = 
+      (if 0 \<in> X then (f -` X \<inter> (\<Omega> \<inter> space M)) \<union> (space M - (\<Omega> \<inter> space M)) else f -` X \<inter> (\<Omega> \<inter> space M))" 
+      by (auto split: split_if_asm simp: indicator_def)
+    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
+      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
+      by auto
+    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
+      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
+      by (subst *) auto
+    note this 1 }
+  note 1 = this(1) and 2 = this(2)
+
+  from 2 show ?thesis
+    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
+qed
+
+lemma borel_measurable_restrict_space_iff:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
+  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
+    (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
+proof -
+  { fix X :: "'b set" assume "X \<in> sets borel"
+    have 1: "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) -` X \<inter> space M = 
+      (if 0 \<in> X then (f -` X \<inter> (\<Omega> \<inter> space M)) \<union> (space M - (\<Omega> \<inter> space M)) else f -` X \<inter> (\<Omega> \<inter> space M))" 
+      by (auto split: split_if_asm simp: indicator_def)
+    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
+      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
+      by auto
+    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
+      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
+      by (subst *) auto
+    note this 1 }
+  note 1 = this(1) and 2 = this(2)
+
+  from 2 show ?thesis
+    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
+qed
+
 lemma borel_measurable_continuous_on1:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes "continuous_on UNIV f"
diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 15:56:30 2014 +0200
@@ -740,7 +740,7 @@
     show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) ----> f x"
       using lim by auto
     show "(\<lambda>k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f"
-      using lim by (intro integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"]) auto
+      using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
   qed
 qed
 
diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Fri May 30 15:56:30 2014 +0200
@@ -1693,6 +1693,29 @@
     by (simp add: emeasure_notin_sets)
 qed
 
+lemma measure_restrict_space:
+  assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
+  shows "measure (restrict_space M \<Omega>) A = measure M A"
+  using emeasure_restrict_space[OF assms] by (simp add: measure_def)
+
+lemma AE_restrict_space_iff:
+  assumes "\<Omega> \<inter> space M \<in> sets M"
+  shows "(AE x in restrict_space M \<Omega>. P x) \<longleftrightarrow> (AE x in M. x \<in> \<Omega> \<longrightarrow> P x)"
+proof -
+  have ex_cong: "\<And>P Q f. (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> P (f x)) \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> (\<exists>x. Q x)"
+    by auto
+  { fix X assume X: "X \<in> sets M" "emeasure M X = 0"
+    then have "emeasure M (\<Omega> \<inter> space M \<inter> X) \<le> emeasure M X"
+      by (intro emeasure_mono) auto
+    then have "emeasure M (\<Omega> \<inter> space M \<inter> X) = 0"
+      using X by (auto intro!: antisym) }
+  with assms show ?thesis
+    unfolding eventually_ae_filter
+    by (auto simp add: space_restrict_space null_sets_def sets_restrict_space_iff
+                       emeasure_restrict_space cong: conj_cong
+             intro!: ex_cong[where f="\<lambda>X. (\<Omega> \<inter> space M) \<inter> X"])
+qed  
+
 lemma restrict_restrict_space:
   assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
   shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
@@ -1718,5 +1741,18 @@
     by (cases "finite X") (auto simp add: emeasure_restrict_space)
 qed
 
+lemma restrict_distr: 
+  assumes [measurable]: "f \<in> measurable M N"
+  assumes [simp]: "\<Omega> \<inter> space N \<in> sets N" and restrict: "f \<in> space M \<rightarrow> \<Omega>"
+  shows "restrict_space (distr M N f) \<Omega> = distr M (restrict_space N \<Omega>) f"
+  (is "?l = ?r")
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets (restrict_space (distr M N f) \<Omega>)"
+  with restrict show "emeasure ?l A = emeasure ?r A"
+    by (subst emeasure_distr)
+       (auto simp: sets_restrict_space_iff emeasure_restrict_space emeasure_distr
+             intro!: measurable_restrict_space2)
+qed (simp add: sets_restrict_space)
+
 end
 
diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 30 15:56:30 2014 +0200
@@ -1733,32 +1733,102 @@
 
 subsubsection {* Measures with Restricted Space *}
 
+lemma simple_function_iff_borel_measurable:
+  fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
+  shows "simple_function M f \<longleftrightarrow> finite (f ` space M) \<and> f \<in> borel_measurable M"
+  by (metis borel_measurable_simple_function simple_functionD(1) simple_function_borel_measurable)
+
+lemma simple_function_restrict_space_ereal:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "\<Omega> \<inter> space M \<in> sets M"
+  shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator \<Omega> x)"
+proof -
+  { assume "finite (f ` space (restrict_space M \<Omega>))"
+    then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp
+    then have "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)"
+      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
+  moreover
+  { assume "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)"
+    then have "finite (f ` space (restrict_space M \<Omega>))"
+      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
+  ultimately show ?thesis
+    unfolding simple_function_iff_borel_measurable
+      borel_measurable_restrict_space_iff_ereal[OF assms]
+    by auto
+qed
+
+lemma simple_function_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<Omega> \<inter> space M \<in> sets M"
+  shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
+proof -
+  { assume "finite (f ` space (restrict_space M \<Omega>))"
+    then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp
+    then have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)"
+      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
+  moreover
+  { assume "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)"
+    then have "finite (f ` space (restrict_space M \<Omega>))"
+      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
+  ultimately show ?thesis
+    unfolding simple_function_iff_borel_measurable
+      borel_measurable_restrict_space_iff[OF assms]
+    by auto
+qed
+
+
+lemma split_indicator_asm: "P (indicator Q x) = (\<not> (x \<in> Q \<and> \<not> P 1 \<or> x \<notin> Q \<and> \<not> P 0))"
+  by (auto split: split_indicator)
+
+lemma simple_integral_restrict_space:
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" "simple_function (restrict_space M \<Omega>) f"
+  shows "simple_integral (restrict_space M \<Omega>) f = simple_integral M (\<lambda>x. f x * indicator \<Omega> x)"
+  using simple_function_restrict_space_ereal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)]
+  by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def
+           split: split_indicator split_indicator_asm
+           intro!: setsum_mono_zero_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure])
+
+lemma one_not_less_zero[simp]: "\<not> 1 < (0::ereal)"
+  by (simp add: zero_ereal_def one_ereal_def) 
+
 lemma nn_integral_restrict_space:
-  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "\<And>x. x \<in> space M - \<Omega> \<Longrightarrow> f x = 0"
-  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M f"
-using f proof (induct rule: borel_measurable_induct)
-  case (cong f g) then show ?case
-    using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \<Omega>" f g]
-      sets.sets_into_space[OF `\<Omega> \<in> sets M`]
-    by (simp add: subset_eq space_restrict_space)
-next
-  case (set A)
-  then have "A \<subseteq> \<Omega>"
-    unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
-  with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
-    by (subst nn_integral_indicator')
-       (auto simp add: sets_restrict_space_iff space_restrict_space
-                  emeasure_restrict_space Int_absorb2
-                dest: sets.sets_into_space)
-next
-  case (mult f c) then show ?case
-    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> nn_integral_cmult)
-next
-  case (add f g) then show ?case
-    by (simp add: measurable_restrict_space1 \<Omega> nn_integral_add ereal_add_nonneg_eq_0_iff)
-next
-  case (seq F) then show ?case
-    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> nn_integral_monotone_convergence_SUP)
+  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
+  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M (\<lambda>x. f x * indicator \<Omega> x)"
+proof -
+  let ?R = "restrict_space M \<Omega>" and ?X = "\<lambda>M f. {s. simple_function M s \<and> s \<le> max 0 \<circ> f \<and> range s \<subseteq> {0 ..< \<infinity>}}"
+  have "integral\<^sup>S ?R ` ?X ?R f = integral\<^sup>S M ` ?X M (\<lambda>x. f x * indicator \<Omega> x)"
+  proof (safe intro!: image_eqI)
+    fix s assume s: "simple_function ?R s" "s \<le> max 0 \<circ> f" "range s \<subseteq> {0..<\<infinity>}"
+    from s show "integral\<^sup>S (restrict_space M \<Omega>) s = integral\<^sup>S M (\<lambda>x. s x * indicator \<Omega> x)"
+      by (intro simple_integral_restrict_space) auto
+    from s show "simple_function M (\<lambda>x. s x * indicator \<Omega> x)"
+      by (simp add: simple_function_restrict_space_ereal)
+    from s show "(\<lambda>x. s x * indicator \<Omega> x) \<le> max 0 \<circ> (\<lambda>x. f x * indicator \<Omega> x)"
+      "\<And>x. s x * indicator \<Omega> x \<in> {0..<\<infinity>}"
+      by (auto split: split_indicator simp: le_fun_def image_subset_iff)
+  next
+    fix s assume s: "simple_function M s" "s \<le> max 0 \<circ> (\<lambda>x. f x * indicator \<Omega> x)" "range s \<subseteq> {0..<\<infinity>}"
+    then have "simple_function M (\<lambda>x. s x * indicator (\<Omega> \<inter> space M) x)" (is ?s')
+      by (intro simple_function_mult simple_function_indicator) auto
+    also have "?s' \<longleftrightarrow> simple_function M (\<lambda>x. s x * indicator \<Omega> x)"
+      by (rule simple_function_cong) (auto split: split_indicator)
+    finally show sf: "simple_function (restrict_space M \<Omega>) s"
+      by (simp add: simple_function_restrict_space_ereal)
+
+    from s have s_eq: "s = (\<lambda>x. s x * indicator \<Omega> x)"
+      by (auto simp add: fun_eq_iff le_fun_def image_subset_iff
+                  split: split_indicator split_indicator_asm
+                  intro: antisym)
+
+    show "integral\<^sup>S M s = integral\<^sup>S (restrict_space M \<Omega>) s"
+      by (subst s_eq) (rule simple_integral_restrict_space[symmetric, OF \<Omega> sf])
+    show "\<And>x. s x \<in> {0..<\<infinity>}"
+      using s by (auto simp: image_subset_iff)
+    from s show "s \<le> max 0 \<circ> f" 
+      by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
+  qed
+  then show ?thesis
+    unfolding nn_integral_def_finite SUP_def by simp
 qed
 
 subsubsection {* Measure spaces with an associated density *}
diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 18:13:40 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 15:56:30 2014 +0200
@@ -2351,9 +2351,9 @@
 qed
 
 lemma measurable_restrict_space2:
-  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
+  "\<Omega> \<inter> space N \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     f \<in> measurable M (restrict_space N \<Omega>)"
-  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
+  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric])
 
 end