698 using A B emeasure by auto |
698 using A B emeasure by auto |
699 finally show "emeasure ?P X = emeasure M X" |
699 finally show "emeasure ?P X = emeasure M X" |
700 by simp |
700 by simp |
701 qed |
701 qed |
702 qed |
702 qed |
|
703 |
|
704 lemma sets_pair_countable: |
|
705 assumes "countable S1" "countable S2" |
|
706 assumes M: "sets M = Pow S1" and N: "sets N = Pow S2" |
|
707 shows "sets (M \<Otimes>\<^sub>M N) = Pow (S1 \<times> S2)" |
|
708 proof auto |
|
709 fix x a b assume x: "x \<in> sets (M \<Otimes>\<^sub>M N)" "(a, b) \<in> x" |
|
710 from sets.sets_into_space[OF x(1)] x(2) |
|
711 sets_eq_imp_space_eq[of N "count_space S2"] sets_eq_imp_space_eq[of M "count_space S1"] M N |
|
712 show "a \<in> S1" "b \<in> S2" |
|
713 by (auto simp: space_pair_measure) |
|
714 next |
|
715 fix X assume X: "X \<subseteq> S1 \<times> S2" |
|
716 then have "countable X" |
|
717 by (metis countable_subset `countable S1` `countable S2` countable_SIGMA) |
|
718 have "X = (\<Union>(a, b)\<in>X. {a} \<times> {b})" by auto |
|
719 also have "\<dots> \<in> sets (M \<Otimes>\<^sub>M N)" |
|
720 using X |
|
721 by (safe intro!: sets.countable_UN' `countable X` subsetI pair_measureI) (auto simp: M N) |
|
722 finally show "X \<in> sets (M \<Otimes>\<^sub>M N)" . |
|
723 qed |
|
724 |
|
725 lemma pair_measure_countable: |
|
726 assumes "countable S1" "countable S2" |
|
727 shows "count_space S1 \<Otimes>\<^sub>M count_space S2 = count_space (S1 \<times> S2)" |
|
728 proof (rule pair_measure_eqI) |
|
729 show "sigma_finite_measure (count_space S1)" "sigma_finite_measure (count_space S2)" |
|
730 using assms by (auto intro!: sigma_finite_measure_count_space_countable) |
|
731 show "sets (count_space S1 \<Otimes>\<^sub>M count_space S2) = sets (count_space (S1 \<times> S2))" |
|
732 by (subst sets_pair_countable[OF assms]) auto |
|
733 next |
|
734 fix A B assume "A \<in> sets (count_space S1)" "B \<in> sets (count_space S2)" |
|
735 then show "emeasure (count_space S1) A * emeasure (count_space S2) B = |
|
736 emeasure (count_space (S1 \<times> S2)) (A \<times> B)" |
|
737 by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff) |
|
738 qed |
703 |
739 |
704 end |
740 end |