--- a/src/HOL/Probability/Measure_Space.thy Tue Apr 14 13:57:25 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Tue Apr 14 14:11:01 2015 +0200
@@ -1650,7 +1650,6 @@
with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
qed
-
subsection {* Counting space *}
lemma strict_monoI_Suc:
@@ -1882,6 +1881,40 @@
by (cases "finite X") (auto simp add: emeasure_restrict_space)
qed
+lemma sigma_finite_measure_restrict_space:
+ assumes "sigma_finite_measure M"
+ and A: "A \<in> sets M"
+ shows "sigma_finite_measure (restrict_space M A)"
+proof -
+ interpret sigma_finite_measure M by fact
+ from sigma_finite_countable obtain C
+ where C: "countable C" "C \<subseteq> sets M" "(\<Union>C) = space M" "\<forall>a\<in>C. emeasure M a \<noteq> \<infinity>"
+ by blast
+ let ?C = "op \<inter> A ` C"
+ from C have "countable ?C" "?C \<subseteq> sets (restrict_space M A)" "(\<Union>?C) = space (restrict_space M A)"
+ by(auto simp add: sets_restrict_space space_restrict_space)
+ moreover {
+ fix a
+ assume "a \<in> ?C"
+ then obtain a' where "a = A \<inter> a'" "a' \<in> C" ..
+ then have "emeasure (restrict_space M A) a \<le> emeasure M a'"
+ using A C by(auto simp add: emeasure_restrict_space intro: emeasure_mono)
+ also have "\<dots> < \<infinity>" using C(4)[rule_format, of a'] \<open>a' \<in> C\<close> by simp
+ finally have "emeasure (restrict_space M A) a \<noteq> \<infinity>" by simp }
+ ultimately show ?thesis
+ by unfold_locales (rule exI conjI|assumption|blast)+
+qed
+
+lemma finite_measure_restrict_space:
+ assumes "finite_measure M"
+ and A: "A \<in> sets M"
+ shows "finite_measure (restrict_space M A)"
+proof -
+ interpret finite_measure M by fact
+ show ?thesis
+ by(rule finite_measureI)(simp add: emeasure_restrict_space A space_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>"