summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Andreas Lochbihler |

Tue, 14 Apr 2015 14:11:01 +0200 | |

changeset 60063 | 81835db730e8 |

parent 60062 | 4c5de5a860ee |

child 60064 | 63124d48a2ee |

add lemmas about restrict_space

src/HOL/Probability/Measure_Space.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Probability/Sigma_Algebra.thy | file | annotate | diff | comparison | revisions |

--- 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>"

--- 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)