diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Oct 07 10:34:24 2014 +0200 @@ -34,6 +34,12 @@ unfolding pair_measure_def using pair_measure_closed[of A B] by (rule sets_measure_of) +lemma sets_pair_in_sets: + assumes N: "space A \ space B = space N" + assumes "\a b. a \ sets A \ b \ sets B \ a \ b \ sets N" + shows "sets (A \\<^sub>M B) \ sets N" + using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N) + lemma sets_pair_measure_cong[cong]: "sets M1 = sets M1' \ sets M2 = sets M2' \ sets (M1 \\<^sub>M M2) = sets (M1' \\<^sub>M M2')" unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) @@ -42,6 +48,9 @@ "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^sub>M B)" by (auto simp: sets_pair_measure) +lemma sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)" + using pair_measureI[of "{x}" M1 "{y}" M2] by simp + lemma measurable_pair_measureI: assumes 1: "f \ space M \ space M1 \ space M2" assumes 2: "\A B. A \ sets M1 \ B \ sets M2 \ f -` (A \ B) \ space M \ sets M" @@ -98,6 +107,25 @@ and measurable_snd'': "(\x. f (snd x)) \ measurable (P \\<^sub>M M) N" by simp_all +lemma sets_pair_eq_sets_fst_snd: + "sets (A \\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \ space B) fst A, vimage_algebra (space A \ space B) snd B})" + (is "?P = sets (Sup_sigma {?fst, ?snd})") +proof - + { fix a b assume ab: "a \ sets A" "b \ sets B" + then have "a \ b = (fst -` a \ (space A \ space B)) \ (snd -` b \ (space A \ space B))" + by (auto dest: sets.sets_into_space) + also have "\ \ sets (Sup_sigma {?fst, ?snd})" + using ab by (auto intro: in_Sup_sigma in_vimage_algebra) + finally have "a \ b \ sets (Sup_sigma {?fst, ?snd})" . } + moreover have "sets ?fst \ sets (A \\<^sub>M B)" + by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric]) + moreover have "sets ?snd \ sets (A \\<^sub>M B)" + by (rule sets_image_in_sets) (auto simp: space_pair_measure) + ultimately show ?thesis + by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets ) + (auto simp add: space_Sup_sigma space_pair_measure) +qed + lemma measurable_pair_iff: "f \ measurable M (M1 \\<^sub>M M2) \ (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2" by (auto intro: measurable_pair[of f M M1 M2])