# HG changeset patch
# User Andreas Lochbihler
# Date 1429013461 -7200
# Node ID 81835db730e8ade7a41d89f4b565f53951b00947
# Parent  4c5de5a860ee4677bd89d0945463f6298073a5ff
add lemmas about restrict_space

diff -r 4c5de5a860ee -r 81835db730e8 src/HOL/Probability/Measure_Space.thy
--- 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>"
diff -r 4c5de5a860ee -r 81835db730e8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Apr 14 13:57:25 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Apr 14 14:11:01 2015 +0200
@@ -2361,6 +2361,10 @@
     by simp
 qed
 
+lemma sets_restrict_space_count_space :
+  "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))"
+by(auto simp add: sets_restrict_space)
+
 lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
   by (auto simp add: sets_restrict_space)