682 next |
682 next |
683 fix x a b |
683 fix x a b |
684 assume "x \<in> sigma_sets ?prod ?sets" and "(a, b) \<in> x" |
684 assume "x \<in> sigma_sets ?prod ?sets" and "(a, b) \<in> x" |
685 from sigma_sets_into_sp[OF _ this(1)] this(2) |
685 from sigma_sets_into_sp[OF _ this(1)] this(2) |
686 show "a \<in> A" and "b \<in> B" by auto |
686 show "a \<in> A" and "b \<in> B" by auto |
|
687 qed |
|
688 |
|
689 lemma sets_pair_eq: |
|
690 assumes Ea: "Ea \<subseteq> Pow (space A)" "sets A = sigma_sets (space A) Ea" |
|
691 and Ca: "countable Ca" "Ca \<subseteq> Ea" "\<Union>Ca = space A" |
|
692 and Eb: "Eb \<subseteq> Pow (space B)" "sets B = sigma_sets (space B) Eb" |
|
693 and Cb: "countable Cb" "Cb \<subseteq> Eb" "\<Union>Cb = space B" |
|
694 shows "sets (A \<Otimes>\<^sub>M B) = sets (sigma (space A \<times> space B) { a \<times> b | a b. a \<in> Ea \<and> b \<in> Eb })" |
|
695 (is "_ = sets (sigma ?\<Omega> ?E)") |
|
696 proof |
|
697 show "sets (sigma ?\<Omega> ?E) \<subseteq> sets (A \<Otimes>\<^sub>M B)" |
|
698 using Ea(1) Eb(1) by (subst sigma_le_sets) (auto simp: Ea(2) Eb(2)) |
|
699 have "?E \<subseteq> Pow ?\<Omega>" |
|
700 using Ea(1) Eb(1) by auto |
|
701 then have E: "a \<in> Ea \<Longrightarrow> b \<in> Eb \<Longrightarrow> a \<times> b \<in> sets (sigma ?\<Omega> ?E)" for a b |
|
702 by auto |
|
703 have "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets (Sup {vimage_algebra ?\<Omega> fst A, vimage_algebra ?\<Omega> snd B})" |
|
704 unfolding sets_pair_eq_sets_fst_snd .. |
|
705 also have "vimage_algebra ?\<Omega> fst A = vimage_algebra ?\<Omega> fst (sigma (space A) Ea)" |
|
706 by (intro vimage_algebra_cong[OF refl refl]) (simp add: Ea) |
|
707 also have "\<dots> = sigma ?\<Omega> {fst -` A \<inter> ?\<Omega> |A. A \<in> Ea}" |
|
708 by (intro Ea vimage_algebra_sigma) auto |
|
709 also have "vimage_algebra ?\<Omega> snd B = vimage_algebra ?\<Omega> snd (sigma (space B) Eb)" |
|
710 by (intro vimage_algebra_cong[OF refl refl]) (simp add: Eb) |
|
711 also have "\<dots> = sigma ?\<Omega> {snd -` A \<inter> ?\<Omega> |A. A \<in> Eb}" |
|
712 by (intro Eb vimage_algebra_sigma) auto |
|
713 also have "{sigma ?\<Omega> {fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, sigma ?\<Omega> {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}} = |
|
714 sigma ?\<Omega> ` {{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}" |
|
715 by auto |
|
716 also have "sets (SUP S:{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}. sigma ?\<Omega> S) = |
|
717 sets (sigma ?\<Omega> (\<Union>{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}))" |
|
718 using Ea(1) Eb(1) by (intro sets_Sup_sigma) auto |
|
719 also have "\<dots> \<subseteq> sets (sigma ?\<Omega> ?E)" |
|
720 proof (subst sigma_le_sets, safe intro!: space_in_measure_of) |
|
721 fix a assume "a \<in> Ea" |
|
722 then have "fst -` a \<inter> ?\<Omega> = (\<Union>b\<in>Cb. a \<times> b)" |
|
723 using Cb(3)[symmetric] Ea(1) by auto |
|
724 then show "fst -` a \<inter> ?\<Omega> \<in> sets (sigma ?\<Omega> ?E)" |
|
725 using Cb \<open>a \<in> Ea\<close> by (auto intro!: sets.countable_UN' E) |
|
726 next |
|
727 fix b assume "b \<in> Eb" |
|
728 then have "snd -` b \<inter> ?\<Omega> = (\<Union>a\<in>Ca. a \<times> b)" |
|
729 using Ca(3)[symmetric] Eb(1) by auto |
|
730 then show "snd -` b \<inter> ?\<Omega> \<in> sets (sigma ?\<Omega> ?E)" |
|
731 using Ca \<open>b \<in> Eb\<close> by (auto intro!: sets.countable_UN' E) |
|
732 qed |
|
733 finally show "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets (sigma ?\<Omega> ?E)" . |
687 qed |
734 qed |
688 |
735 |
689 lemma borel_prod: |
736 lemma borel_prod: |
690 "(borel \<Otimes>\<^sub>M borel) = (borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)" |
737 "(borel \<Otimes>\<^sub>M borel) = (borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)" |
691 (is "?P = ?B") |
738 (is "?P = ?B") |