# HG changeset patch # User Andreas Lochbihler # Date 1380011737 -7200 # Node ID 3245d5f11f6ab0cf804251c756e9d2117768a163 # Parent 255a2929c137561fac5d7343fc021f2d9abf55ef make measure_of total diff -r 255a2929c137 -r 3245d5f11f6a src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 24 09:12:09 2013 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 24 10:35:37 2013 +0200 @@ -74,6 +74,9 @@ qed qed +lemma disjoint_singleton [simp]: "disjoint {A}" +by(simp add: disjoint_def) + locale semiring_of_sets = subset_class + assumes empty_sets[iff]: "{} \ M" assumes Int[intro]: "\a b. a \ M \ b \ M \ a \ b \ M" @@ -1085,7 +1088,7 @@ using measure_space[of M] by (auto simp: measure_space_def) definition measure_of :: "'a set \ 'a set set \ ('a set \ ereal) \ 'a measure" where - "measure_of \ A \ = Abs_measure (\, sigma_sets \ A, + "measure_of \ A \ = Abs_measure (\, if A \ Pow \ then sigma_sets \ A else {{}, \}, \a. if a \ sigma_sets \ A \ measure_space \ (sigma_sets \ A) \ then \ a else 0)" abbreviation "sigma \ A \ measure_of \ A (\x. 0)" @@ -1094,6 +1097,20 @@ unfolding measure_space_def by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def) +lemma sigma_algebra_trivial: "sigma_algebra \ {{}, \}" +by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\}"])+ + +lemma measure_space_0': "measure_space \ {{}, \} (\x. 0)" +by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial) + +lemma measure_space_closed: + assumes "measure_space \ M \" + shows "M \ Pow \" +proof - + interpret sigma_algebra \ M using assms by(simp add: measure_space_def) + show ?thesis by(rule space_closed) +qed + lemma (in ring_of_sets) positive_cong_eq: "(\a. a \ M \ \' a = \ a) \ positive M \' = positive M \" by (auto simp add: positive_def) @@ -1123,26 +1140,37 @@ qed lemma - assumes A: "A \ Pow \" - shows sets_measure_of[simp]: "sets (measure_of \ A \) = sigma_sets \ A" (is ?sets) - and space_measure_of[simp]: "space (measure_of \ A \) = \" (is ?space) + shows space_measure_of_conv: "space (measure_of \ A \) = \" (is ?space) + and sets_measure_of_conv: + "sets (measure_of \ A \) = (if A \ Pow \ then sigma_sets \ A else {{}, \})" (is ?sets) + and emeasure_measure_of_conv: + "emeasure (measure_of \ A \) = + (\B. if B \ sigma_sets \ A \ measure_space \ (sigma_sets \ A) \ then \ B else 0)" (is ?emeasure) proof - - have "?sets \ ?space" - proof cases - assume "measure_space \ (sigma_sets \ A) \" - moreover have "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) - (\a. if a \ sigma_sets \ A then \ a else 0)" - using A by (rule measure_space_eq) auto - ultimately show "?sets \ ?space" - by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def) + have "?space \ ?sets \ ?emeasure" + proof(cases "measure_space \ (sigma_sets \ A) \") + case True + from measure_space_closed[OF this] sigma_sets_superset_generator[of A \] + have "A \ Pow \" by simp + hence "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) + (\a. if a \ sigma_sets \ A then \ a else 0)" + by(rule measure_space_eq) auto + with True `A \ Pow \` show ?thesis + by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse) next - assume "\ measure_space \ (sigma_sets \ A) \" - with A show "?sets \ ?space" - by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def measure_space_0) + case False thus ?thesis + by(cases "A \ Pow \")(simp_all add: Abs_measure_inverse measure_of_def sets_def space_def emeasure_def measure_space_0 measure_space_0') qed - then show ?sets ?space by auto + thus ?space ?sets ?emeasure by simp_all qed +lemma [simp]: + assumes A: "A \ Pow \" + shows sets_measure_of: "sets (measure_of \ A \) = sigma_sets \ A" + and space_measure_of: "space (measure_of \ A \) = \" +using assms +by(simp_all add: sets_measure_of_conv space_measure_of_conv) + lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \ M \) = M" using space_closed by (auto intro!: sigma_sets_eq) @@ -1193,14 +1221,8 @@ interpret sigma_algebra \ "sigma_sets \ A" by (rule sigma_algebra_sigma_sets) fact have "measure_space \ (sigma_sets \ A) \" using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets) - moreover have "measure_space \ (sigma_sets \ A) (\a. if a \ sigma_sets \ A then \ a else 0) - = measure_space \ (sigma_sets \ A) \" - using ms(1) by (rule measure_space_eq) auto - moreover have "X \ sigma_sets \ A" - using X M ms by simp - ultimately show ?thesis - unfolding emeasure_def measure_of_def M - by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) + thus ?thesis using X ms + by(simp add: M emeasure_measure_of_conv sets_measure_of_conv) qed lemma emeasure_measure_of_sigma: @@ -1211,12 +1233,7 @@ interpret sigma_algebra \ M by fact have "measure_space \ (sigma_sets \ M) \" using ms sigma_sets_eq by (simp add: measure_space_def) - moreover have "measure_space \ (sigma_sets \ M) (\a. if a \ sigma_sets \ M then \ a else 0) - = measure_space \ (sigma_sets \ M) \" - using space_closed by (rule measure_space_eq) auto - ultimately show ?thesis using A - unfolding emeasure_def measure_of_def - by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) + thus ?thesis by(simp add: emeasure_measure_of_conv A) qed lemma measure_cases[cases type: measure]: