better support for restrict_space
authorhoelzl
Fri May 30 15:56:30 2014 +0200 (2014-05-30)
changeset 57137f174712d0a84
parent 57136 653e56c6c963
child 57138 7b3146180291
better support for restrict_space
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Fri May 30 18:13:40 2014 +0200
     1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Fri May 30 15:56:30 2014 +0200
     1.3 @@ -856,6 +856,32 @@
     1.4      by (rule has_bochner_integral_eq)
     1.5  qed
     1.6  
     1.7 +lemma simple_bochner_integrable_restrict_space:
     1.8 +  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
     1.9 +  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
    1.10 +  shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
    1.11 +    simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    1.12 +  by (simp add: simple_bochner_integrable.simps space_restrict_space
    1.13 +    simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
    1.14 +    indicator_eq_0_iff conj_ac)
    1.15 +
    1.16 +lemma simple_bochner_integral_restrict_space:
    1.17 +  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.18 +  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
    1.19 +  assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
    1.20 +  shows "simple_bochner_integral (restrict_space M \<Omega>) f =
    1.21 +    simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    1.22 +proof -
    1.23 +  have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
    1.24 +    using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
    1.25 +    by (simp add: simple_bochner_integrable.simps simple_function_def)
    1.26 +  then show ?thesis
    1.27 +    by (auto simp: space_restrict_space measure_restrict_space[OF \<Omega>(1)] le_infI2
    1.28 +                   simple_bochner_integral_def Collect_restrict
    1.29 +             split: split_indicator split_indicator_asm
    1.30 +             intro!: setsum_mono_zero_cong_left arg_cong2[where f=measure])
    1.31 +qed
    1.32 +
    1.33  inductive integrable for M f where
    1.34    "has_bochner_integral M f x \<Longrightarrow> integrable M f"
    1.35  
    1.36 @@ -1251,14 +1277,14 @@
    1.37    by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
    1.38             cong: conj_cong)
    1.39  
    1.40 -lemma integral_dominated_convergence:
    1.41 +lemma
    1.42    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
    1.43    assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
    1.44    assumes lim: "AE x in M. (\<lambda>i. s i x) ----> f x"
    1.45    assumes bound: "\<And>i. AE x in M. norm (s i x) \<le> w x"
    1.46 -  shows "integrable M f"
    1.47 -    and "\<And>i. integrable M (s i)"
    1.48 -    and "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
    1.49 +  shows integrable_dominated_convergence: "integrable M f"
    1.50 +    and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
    1.51 +    and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f"
    1.52  proof -
    1.53    have "AE x in M. 0 \<le> w x"
    1.54      using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
    1.55 @@ -1421,13 +1447,14 @@
    1.56      finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
    1.57    qed
    1.58  
    1.59 -  note int = integral_dominated_convergence(1,3)[OF _ _ 1 2 3]
    1.60 +  note ibl = integrable_dominated_convergence[OF _ _ 1 2 3]
    1.61 +  note int = integral_dominated_convergence[OF _ _ 1 2 3]
    1.62  
    1.63    show "integrable M ?S"
    1.64 -    by (rule int) measurable
    1.65 +    by (rule ibl) measurable
    1.66  
    1.67    show "?f sums ?x" unfolding sums_def
    1.68 -    using int(2) by (simp add: integrable)
    1.69 +    using int by (simp add: integrable)
    1.70    then show "?x = suminf ?f" "summable ?f"
    1.71      unfolding sums_iff by auto
    1.72  qed
    1.73 @@ -1600,6 +1627,49 @@
    1.74      by simp
    1.75  qed
    1.76  
    1.77 +subsection {* Restricted measure spaces *}
    1.78 +
    1.79 +lemma integrable_restrict_space:
    1.80 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.81 +  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
    1.82 +  shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    1.83 +  unfolding integrable_iff_bounded
    1.84 +    borel_measurable_restrict_space_iff[OF \<Omega>]
    1.85 +    nn_integral_restrict_space[OF \<Omega>]
    1.86 +  by (simp add: ac_simps ereal_indicator times_ereal.simps(1)[symmetric] del: times_ereal.simps)
    1.87 +
    1.88 +lemma integral_restrict_space:
    1.89 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.90 +  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
    1.91 +  shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    1.92 +proof (rule integral_eq_cases)
    1.93 +  assume "integrable (restrict_space M \<Omega>) f"
    1.94 +  then show ?thesis
    1.95 +  proof induct
    1.96 +    case (base A c) then show ?case
    1.97 +      by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff
    1.98 +                    emeasure_restrict_space Int_absorb1 measure_restrict_space)
    1.99 +  next
   1.100 +    case (add g f) then show ?case
   1.101 +      by (simp add: scaleR_add_right integrable_restrict_space)
   1.102 +  next
   1.103 +    case (lim f s)
   1.104 +    show ?case
   1.105 +    proof (rule LIMSEQ_unique)
   1.106 +      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> integral\<^sup>L (restrict_space M \<Omega>) f"
   1.107 +        using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) simp_all
   1.108 +      
   1.109 +      show "(\<lambda>i. integral\<^sup>L (restrict_space M \<Omega>) (s i)) ----> (\<integral> x. indicator \<Omega> x *\<^sub>R f x \<partial>M)"
   1.110 +        unfolding lim
   1.111 +        using lim
   1.112 +        by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (indicator \<Omega> x *\<^sub>R f x)"])
   1.113 +           (auto simp add: space_restrict_space integrable_restrict_space
   1.114 +                 simp del: norm_scaleR
   1.115 +                 split: split_indicator)
   1.116 +    qed
   1.117 +  qed
   1.118 +qed (simp add: integrable_restrict_space)
   1.119 +
   1.120  subsection {* Measure spaces with an associated density *}
   1.121  
   1.122  lemma integrable_density:
   1.123 @@ -1653,7 +1723,7 @@
   1.124      show ?case
   1.125      proof (rule LIMSEQ_unique)
   1.126        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)"
   1.127 -      proof (rule integral_dominated_convergence(3))
   1.128 +      proof (rule integral_dominated_convergence)
   1.129          show "integrable M (\<lambda>x. 2 * norm (g x *\<^sub>R f x))"
   1.130            by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto
   1.131          show "AE x in M. (\<lambda>i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x"
   1.132 @@ -1663,7 +1733,7 @@
   1.133        qed auto
   1.134        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
   1.135          unfolding lim(2)[symmetric]
   1.136 -        by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
   1.137 +        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
   1.138             (insert lim(3-5), auto)
   1.139      qed
   1.140    qed
   1.141 @@ -1732,7 +1802,7 @@
   1.142      show ?case
   1.143      proof (rule LIMSEQ_unique)
   1.144        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
   1.145 -      proof (rule integral_dominated_convergence(3))
   1.146 +      proof (rule integral_dominated_convergence)
   1.147          show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
   1.148            using lim by (auto simp: integrable_distr_eq) 
   1.149          show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
   1.150 @@ -1742,7 +1812,7 @@
   1.151        qed auto
   1.152        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
   1.153          unfolding lim(2)[symmetric]
   1.154 -        by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
   1.155 +        by (rule integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"])
   1.156             (insert lim(3-5), auto)
   1.157      qed
   1.158    qed
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri May 30 18:13:40 2014 +0200
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri May 30 15:56:30 2014 +0200
     2.3 @@ -119,6 +119,52 @@
     2.4    shows "f \<in> borel_measurable M"
     2.5    using assms unfolding measurable_def by auto
     2.6  
     2.7 +lemma borel_measurable_restrict_space_iff_ereal:
     2.8 +  fixes f :: "'a \<Rightarrow> ereal"
     2.9 +  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
    2.10 +  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
    2.11 +    (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
    2.12 +proof -
    2.13 +  { fix X :: "ereal set" assume "X \<in> sets borel"
    2.14 +    have 1: "(\<lambda>x. f x * indicator \<Omega> x) -` X \<inter> space M = 
    2.15 +      (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))" 
    2.16 +      by (auto split: split_if_asm simp: indicator_def)
    2.17 +    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
    2.18 +      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
    2.19 +      by auto
    2.20 +    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
    2.21 +      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
    2.22 +      by (subst *) auto
    2.23 +    note this 1 }
    2.24 +  note 1 = this(1) and 2 = this(2)
    2.25 +
    2.26 +  from 2 show ?thesis
    2.27 +    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
    2.28 +qed
    2.29 +
    2.30 +lemma borel_measurable_restrict_space_iff:
    2.31 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    2.32 +  assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
    2.33 +  shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
    2.34 +    (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
    2.35 +proof -
    2.36 +  { fix X :: "'b set" assume "X \<in> sets borel"
    2.37 +    have 1: "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) -` X \<inter> space M = 
    2.38 +      (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))" 
    2.39 +      by (auto split: split_if_asm simp: indicator_def)
    2.40 +    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
    2.41 +      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
    2.42 +      by auto
    2.43 +    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
    2.44 +      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
    2.45 +      by (subst *) auto
    2.46 +    note this 1 }
    2.47 +  note 1 = this(1) and 2 = this(2)
    2.48 +
    2.49 +  from 2 show ?thesis
    2.50 +    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
    2.51 +qed
    2.52 +
    2.53  lemma borel_measurable_continuous_on1:
    2.54    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    2.55    assumes "continuous_on UNIV f"
     3.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 18:13:40 2014 +0200
     3.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 15:56:30 2014 +0200
     3.3 @@ -740,7 +740,7 @@
     3.4      show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) ----> f x"
     3.5        using lim by auto
     3.6      show "(\<lambda>k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f"
     3.7 -      using lim by (intro integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"]) auto
     3.8 +      using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
     3.9    qed
    3.10  qed
    3.11  
     4.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri May 30 18:13:40 2014 +0200
     4.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri May 30 15:56:30 2014 +0200
     4.3 @@ -1693,6 +1693,29 @@
     4.4      by (simp add: emeasure_notin_sets)
     4.5  qed
     4.6  
     4.7 +lemma measure_restrict_space:
     4.8 +  assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
     4.9 +  shows "measure (restrict_space M \<Omega>) A = measure M A"
    4.10 +  using emeasure_restrict_space[OF assms] by (simp add: measure_def)
    4.11 +
    4.12 +lemma AE_restrict_space_iff:
    4.13 +  assumes "\<Omega> \<inter> space M \<in> sets M"
    4.14 +  shows "(AE x in restrict_space M \<Omega>. P x) \<longleftrightarrow> (AE x in M. x \<in> \<Omega> \<longrightarrow> P x)"
    4.15 +proof -
    4.16 +  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)"
    4.17 +    by auto
    4.18 +  { fix X assume X: "X \<in> sets M" "emeasure M X = 0"
    4.19 +    then have "emeasure M (\<Omega> \<inter> space M \<inter> X) \<le> emeasure M X"
    4.20 +      by (intro emeasure_mono) auto
    4.21 +    then have "emeasure M (\<Omega> \<inter> space M \<inter> X) = 0"
    4.22 +      using X by (auto intro!: antisym) }
    4.23 +  with assms show ?thesis
    4.24 +    unfolding eventually_ae_filter
    4.25 +    by (auto simp add: space_restrict_space null_sets_def sets_restrict_space_iff
    4.26 +                       emeasure_restrict_space cong: conj_cong
    4.27 +             intro!: ex_cong[where f="\<lambda>X. (\<Omega> \<inter> space M) \<inter> X"])
    4.28 +qed  
    4.29 +
    4.30  lemma restrict_restrict_space:
    4.31    assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
    4.32    shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
    4.33 @@ -1718,5 +1741,18 @@
    4.34      by (cases "finite X") (auto simp add: emeasure_restrict_space)
    4.35  qed
    4.36  
    4.37 +lemma restrict_distr: 
    4.38 +  assumes [measurable]: "f \<in> measurable M N"
    4.39 +  assumes [simp]: "\<Omega> \<inter> space N \<in> sets N" and restrict: "f \<in> space M \<rightarrow> \<Omega>"
    4.40 +  shows "restrict_space (distr M N f) \<Omega> = distr M (restrict_space N \<Omega>) f"
    4.41 +  (is "?l = ?r")
    4.42 +proof (rule measure_eqI)
    4.43 +  fix A assume "A \<in> sets (restrict_space (distr M N f) \<Omega>)"
    4.44 +  with restrict show "emeasure ?l A = emeasure ?r A"
    4.45 +    by (subst emeasure_distr)
    4.46 +       (auto simp: sets_restrict_space_iff emeasure_restrict_space emeasure_distr
    4.47 +             intro!: measurable_restrict_space2)
    4.48 +qed (simp add: sets_restrict_space)
    4.49 +
    4.50  end
    4.51  
     5.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 30 18:13:40 2014 +0200
     5.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 30 15:56:30 2014 +0200
     5.3 @@ -1733,32 +1733,102 @@
     5.4  
     5.5  subsubsection {* Measures with Restricted Space *}
     5.6  
     5.7 +lemma simple_function_iff_borel_measurable:
     5.8 +  fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
     5.9 +  shows "simple_function M f \<longleftrightarrow> finite (f ` space M) \<and> f \<in> borel_measurable M"
    5.10 +  by (metis borel_measurable_simple_function simple_functionD(1) simple_function_borel_measurable)
    5.11 +
    5.12 +lemma simple_function_restrict_space_ereal:
    5.13 +  fixes f :: "'a \<Rightarrow> ereal"
    5.14 +  assumes "\<Omega> \<inter> space M \<in> sets M"
    5.15 +  shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator \<Omega> x)"
    5.16 +proof -
    5.17 +  { assume "finite (f ` space (restrict_space M \<Omega>))"
    5.18 +    then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp
    5.19 +    then have "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)"
    5.20 +      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
    5.21 +  moreover
    5.22 +  { assume "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)"
    5.23 +    then have "finite (f ` space (restrict_space M \<Omega>))"
    5.24 +      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
    5.25 +  ultimately show ?thesis
    5.26 +    unfolding simple_function_iff_borel_measurable
    5.27 +      borel_measurable_restrict_space_iff_ereal[OF assms]
    5.28 +    by auto
    5.29 +qed
    5.30 +
    5.31 +lemma simple_function_restrict_space:
    5.32 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.33 +  assumes "\<Omega> \<inter> space M \<in> sets M"
    5.34 +  shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    5.35 +proof -
    5.36 +  { assume "finite (f ` space (restrict_space M \<Omega>))"
    5.37 +    then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp
    5.38 +    then have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)"
    5.39 +      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
    5.40 +  moreover
    5.41 +  { assume "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)"
    5.42 +    then have "finite (f ` space (restrict_space M \<Omega>))"
    5.43 +      by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) }
    5.44 +  ultimately show ?thesis
    5.45 +    unfolding simple_function_iff_borel_measurable
    5.46 +      borel_measurable_restrict_space_iff[OF assms]
    5.47 +    by auto
    5.48 +qed
    5.49 +
    5.50 +
    5.51 +lemma split_indicator_asm: "P (indicator Q x) = (\<not> (x \<in> Q \<and> \<not> P 1 \<or> x \<notin> Q \<and> \<not> P 0))"
    5.52 +  by (auto split: split_indicator)
    5.53 +
    5.54 +lemma simple_integral_restrict_space:
    5.55 +  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" "simple_function (restrict_space M \<Omega>) f"
    5.56 +  shows "simple_integral (restrict_space M \<Omega>) f = simple_integral M (\<lambda>x. f x * indicator \<Omega> x)"
    5.57 +  using simple_function_restrict_space_ereal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)]
    5.58 +  by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def
    5.59 +           split: split_indicator split_indicator_asm
    5.60 +           intro!: setsum_mono_zero_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure])
    5.61 +
    5.62 +lemma one_not_less_zero[simp]: "\<not> 1 < (0::ereal)"
    5.63 +  by (simp add: zero_ereal_def one_ereal_def) 
    5.64 +
    5.65  lemma nn_integral_restrict_space:
    5.66 -  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"
    5.67 -  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M f"
    5.68 -using f proof (induct rule: borel_measurable_induct)
    5.69 -  case (cong f g) then show ?case
    5.70 -    using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \<Omega>" f g]
    5.71 -      sets.sets_into_space[OF `\<Omega> \<in> sets M`]
    5.72 -    by (simp add: subset_eq space_restrict_space)
    5.73 -next
    5.74 -  case (set A)
    5.75 -  then have "A \<subseteq> \<Omega>"
    5.76 -    unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
    5.77 -  with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
    5.78 -    by (subst nn_integral_indicator')
    5.79 -       (auto simp add: sets_restrict_space_iff space_restrict_space
    5.80 -                  emeasure_restrict_space Int_absorb2
    5.81 -                dest: sets.sets_into_space)
    5.82 -next
    5.83 -  case (mult f c) then show ?case
    5.84 -    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> nn_integral_cmult)
    5.85 -next
    5.86 -  case (add f g) then show ?case
    5.87 -    by (simp add: measurable_restrict_space1 \<Omega> nn_integral_add ereal_add_nonneg_eq_0_iff)
    5.88 -next
    5.89 -  case (seq F) then show ?case
    5.90 -    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> nn_integral_monotone_convergence_SUP)
    5.91 +  assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
    5.92 +  shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M (\<lambda>x. f x * indicator \<Omega> x)"
    5.93 +proof -
    5.94 +  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>}}"
    5.95 +  have "integral\<^sup>S ?R ` ?X ?R f = integral\<^sup>S M ` ?X M (\<lambda>x. f x * indicator \<Omega> x)"
    5.96 +  proof (safe intro!: image_eqI)
    5.97 +    fix s assume s: "simple_function ?R s" "s \<le> max 0 \<circ> f" "range s \<subseteq> {0..<\<infinity>}"
    5.98 +    from s show "integral\<^sup>S (restrict_space M \<Omega>) s = integral\<^sup>S M (\<lambda>x. s x * indicator \<Omega> x)"
    5.99 +      by (intro simple_integral_restrict_space) auto
   5.100 +    from s show "simple_function M (\<lambda>x. s x * indicator \<Omega> x)"
   5.101 +      by (simp add: simple_function_restrict_space_ereal)
   5.102 +    from s show "(\<lambda>x. s x * indicator \<Omega> x) \<le> max 0 \<circ> (\<lambda>x. f x * indicator \<Omega> x)"
   5.103 +      "\<And>x. s x * indicator \<Omega> x \<in> {0..<\<infinity>}"
   5.104 +      by (auto split: split_indicator simp: le_fun_def image_subset_iff)
   5.105 +  next
   5.106 +    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>}"
   5.107 +    then have "simple_function M (\<lambda>x. s x * indicator (\<Omega> \<inter> space M) x)" (is ?s')
   5.108 +      by (intro simple_function_mult simple_function_indicator) auto
   5.109 +    also have "?s' \<longleftrightarrow> simple_function M (\<lambda>x. s x * indicator \<Omega> x)"
   5.110 +      by (rule simple_function_cong) (auto split: split_indicator)
   5.111 +    finally show sf: "simple_function (restrict_space M \<Omega>) s"
   5.112 +      by (simp add: simple_function_restrict_space_ereal)
   5.113 +
   5.114 +    from s have s_eq: "s = (\<lambda>x. s x * indicator \<Omega> x)"
   5.115 +      by (auto simp add: fun_eq_iff le_fun_def image_subset_iff
   5.116 +                  split: split_indicator split_indicator_asm
   5.117 +                  intro: antisym)
   5.118 +
   5.119 +    show "integral\<^sup>S M s = integral\<^sup>S (restrict_space M \<Omega>) s"
   5.120 +      by (subst s_eq) (rule simple_integral_restrict_space[symmetric, OF \<Omega> sf])
   5.121 +    show "\<And>x. s x \<in> {0..<\<infinity>}"
   5.122 +      using s by (auto simp: image_subset_iff)
   5.123 +    from s show "s \<le> max 0 \<circ> f" 
   5.124 +      by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
   5.125 +  qed
   5.126 +  then show ?thesis
   5.127 +    unfolding nn_integral_def_finite SUP_def by simp
   5.128  qed
   5.129  
   5.130  subsubsection {* Measure spaces with an associated density *}
     6.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 18:13:40 2014 +0200
     6.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 15:56:30 2014 +0200
     6.3 @@ -2351,9 +2351,9 @@
     6.4  qed
     6.5  
     6.6  lemma measurable_restrict_space2:
     6.7 -  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     6.8 +  "\<Omega> \<inter> space N \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     6.9      f \<in> measurable M (restrict_space N \<Omega>)"
    6.10 -  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
    6.11 +  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric])
    6.12  
    6.13  end
    6.14