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

author | hoelzl |

Mon, 13 Jul 2015 14:40:16 +0200 | |

changeset 60715 | ee0afee54b1d |

parent 60714 | ff8aa76d6d1c |

child 60716 | 8e82a83757df |

add emeasure_add_AE

--- a/src/HOL/Probability/Measure_Space.thy Mon Jul 13 14:39:50 2015 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Mon Jul 13 14:40:16 2015 +0200 @@ -1112,6 +1112,21 @@ using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets) +lemma emeasure_add_AE: + assumes [measurable]: "A \<in> sets M" "B \<in> sets M" "C \<in> sets M" + assumes 1: "AE x in M. x \<in> C \<longleftrightarrow> x \<in> A \<or> x \<in> B" + assumes 2: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" + shows "emeasure M C = emeasure M A + emeasure M B" +proof - + have "emeasure M C = emeasure M (A \<union> B)" + by (rule emeasure_eq_AE) (insert 1, auto) + also have "\<dots> = emeasure M A + emeasure M (B - A)" + by (subst plus_emeasure) auto + also have "emeasure M (B - A) = emeasure M B" + by (rule emeasure_eq_AE) (insert 2, auto) + finally show ?thesis . +qed + subsection {* @{text \<sigma>}-finite Measures *} locale sigma_finite_measure =