# 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)) \ \" 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 \ 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 \ sets M" "(\C) = space M" "\a\C. emeasure M a \ \" + by blast + let ?C = "op \ A ` C" + from C have "countable ?C" "?C \ sets (restrict_space M A)" "(\?C) = space (restrict_space M A)" + by(auto simp add: sets_restrict_space space_restrict_space) + moreover { + fix a + assume "a \ ?C" + then obtain a' where "a = A \ a'" "a' \ C" .. + then have "emeasure (restrict_space M A) a \ emeasure M a'" + using A C by(auto simp add: emeasure_restrict_space intro: emeasure_mono) + also have "\ < \" using C(4)[rule_format, of a'] \a' \ C\ by simp + finally have "emeasure (restrict_space M A) a \ \" 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 \ 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 \ measurable M N" assumes [simp]: "\ \ space N \ sets N" and restrict: "f \ space M \ \" 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 \ 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)