736 apply (rule someI_ex[where P="?P"]) |
736 apply (rule someI_ex[where P="?P"]) |
737 apply (rule extend_\<mu>G) |
737 apply (rule extend_\<mu>G) |
738 done |
738 done |
739 qed |
739 qed |
740 |
740 |
741 sublocale product_prob_space \<subseteq> measure_space "Pi\<^isub>P I M" |
741 sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M" |
742 using infprod_spec by auto |
742 using infprod_spec by auto |
743 |
743 |
744 lemma (in product_prob_space) measure_infprod_emb: |
744 lemma (in product_prob_space) measure_infprod_emb: |
745 assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" |
745 assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" |
746 shows "measure (Pi\<^isub>P I M) (emb I J X) = measure (Pi\<^isub>M J M) X" |
746 shows "\<mu> (emb I J X) = measure (Pi\<^isub>M J M) X" |
747 proof - |
747 proof - |
748 have "emb I J X \<in> sets generator" |
748 have "emb I J X \<in> sets generator" |
749 using assms by (rule generatorI') |
749 using assms by (rule generatorI') |
750 with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto |
750 with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto |
751 qed |
751 qed |
752 |
752 |
753 sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M" |
753 sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M" |
754 proof |
754 proof |
755 obtain i where "i \<in> I" using I_not_empty by auto |
755 obtain i where "i \<in> I" using I_not_empty by auto |
756 interpret i: finite_product_sigma_finite M "{i}" by default auto |
756 interpret i: finite_product_sigma_finite M "{i}" by default auto |
757 let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)" |
757 let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)" |
758 have "?X \<in> sets (Pi\<^isub>M {i} M)" |
758 have "?X \<in> sets (Pi\<^isub>M {i} M)" |
759 by auto |
759 by auto |
760 from measure_infprod_emb[OF _ _ _ this] `i \<in> I` |
760 from measure_infprod_emb[OF _ _ _ this] `i \<in> I` |
761 have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))" |
761 have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))" |
762 by (simp add: i.measure_times) |
762 by (simp add: i.measure_times) |
763 also have "emb I {i} ?X = space (Pi\<^isub>P I M)" |
763 also have "emb I {i} ?X = space (Pi\<^isub>P I M)" |
764 using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def) |
764 using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def) |
765 finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1" |
765 finally show "\<mu> (space (Pi\<^isub>P I M)) = 1" |
766 using M.measure_space_1 by simp |
766 using M.measure_space_1 by simp |
767 qed |
767 qed |
768 |
768 |
769 lemma (in product_prob_space) measurable_component: |
769 lemma (in product_prob_space) measurable_component: |
770 assumes "i \<in> I" |
770 assumes "i \<in> I" |
782 from generatorI[OF _ _ _ this] `i \<in> I` |
782 from generatorI[OF _ _ _ this] `i \<in> I` |
783 show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)" |
783 show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)" |
784 unfolding infprod_algebra_def by auto |
784 unfolding infprod_algebra_def by auto |
785 qed |
785 qed |
786 |
786 |
|
787 lemma (in product_prob_space) emb_in_infprod_algebra[intro]: |
|
788 fixes J assumes J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (Pi\<^isub>M J M)" |
|
789 shows "emb I J X \<in> sets (\<Pi>\<^isub>P i\<in>I. M i)" |
|
790 proof cases |
|
791 assume "J = {}" |
|
792 with X have "emb I J X = space (\<Pi>\<^isub>P i\<in>I. M i) \<or> emb I J X = {}" |
|
793 by (auto simp: emb_def infprod_algebra_def generator_def |
|
794 product_algebra_def product_algebra_generator_def image_constant sigma_def) |
|
795 then show ?thesis by auto |
|
796 next |
|
797 assume "J \<noteq> {}" |
|
798 show ?thesis unfolding infprod_algebra_def |
|
799 by simp (intro in_sigma generatorI' `J \<noteq> {}` J X) |
|
800 qed |
|
801 |
|
802 lemma (in product_prob_space) finite_measure_infprod_emb: |
|
803 assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" |
|
804 shows "\<mu>' (emb I J X) = finite_measure.\<mu>' (Pi\<^isub>M J M) X" |
|
805 proof - |
|
806 interpret J: finite_product_prob_space M J by default fact+ |
|
807 from assms have "emb I J X \<in> sets (Pi\<^isub>P I M)" by auto |
|
808 with assms show "\<mu>' (emb I J X) = J.\<mu>' X" |
|
809 unfolding \<mu>'_def J.\<mu>'_def |
|
810 unfolding measure_infprod_emb[OF assms] |
|
811 by auto |
|
812 qed |
|
813 |
|
814 lemma (in finite_product_prob_space) finite_measure_times: |
|
815 assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)" |
|
816 shows "\<mu>' (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu>' i (A i))" |
|
817 using assms |
|
818 unfolding \<mu>'_def M.\<mu>'_def |
|
819 by (subst measure_times[OF assms]) |
|
820 (auto simp: finite_measure_eq M.finite_measure_eq setprod_extreal) |
|
821 |
|
822 lemma (in product_prob_space) finite_measure_infprod_emb_Pi: |
|
823 assumes J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)" |
|
824 shows "\<mu>' (emb I J (Pi\<^isub>E J X)) = (\<Prod>j\<in>J. M.\<mu>' j (X j))" |
|
825 proof cases |
|
826 assume "J = {}" |
|
827 then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra" |
|
828 by (auto simp: infprod_algebra_def generator_def sigma_def emb_def) |
|
829 then show ?thesis using `J = {}` prob_space by simp |
|
830 next |
|
831 assume "J \<noteq> {}" |
|
832 interpret J: finite_product_prob_space M J by default fact+ |
|
833 have "(\<Prod>i\<in>J. M.\<mu>' i (X i)) = J.\<mu>' (Pi\<^isub>E J X)" |
|
834 using J `J \<noteq> {}` by (subst J.finite_measure_times) auto |
|
835 also have "\<dots> = \<mu>' (emb I J (Pi\<^isub>E J X))" |
|
836 using J `J \<noteq> {}` by (intro finite_measure_infprod_emb[symmetric]) auto |
|
837 finally show ?thesis by simp |
|
838 qed |
|
839 |
|
840 lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
841 proof |
|
842 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
843 by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros) |
|
844 qed |
|
845 |
|
846 lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" |
|
847 proof |
|
848 fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" |
|
849 by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros) |
|
850 qed |
|
851 |
|
852 lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A" |
|
853 by (auto intro: sigma_sets.Basic) |
|
854 |
|
855 lemma (in product_prob_space) infprod_algebra_alt: |
|
856 "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M), |
|
857 sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i))), |
|
858 measure = measure (Pi\<^isub>P I M) \<rparr>" |
|
859 (is "_ = sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>") |
|
860 proof (rule measure_space.equality) |
|
861 let ?G = "\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M)" |
|
862 have "sigma_sets ?O ?M = sigma_sets ?O ?G" |
|
863 proof (intro equalityI sigma_sets_mono UN_least) |
|
864 fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}" |
|
865 have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto |
|
866 also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper) |
|
867 also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq) |
|
868 finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" . |
|
869 have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))" |
|
870 by (simp add: sets_sigma product_algebra_generator_def product_algebra_def) |
|
871 also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))" |
|
872 using J M.sets_into_space |
|
873 by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast |
|
874 also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M" |
|
875 using J by (intro sigma_sets_mono') auto |
|
876 finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M" |
|
877 by (simp add: infprod_algebra_def generator_def) |
|
878 qed |
|
879 then show "sets (Pi\<^isub>P I M) = sets (sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>)" |
|
880 by (simp_all add: infprod_algebra_def generator_def sets_sigma) |
|
881 qed simp_all |
|
882 |
|
883 lemma (in product_prob_space) infprod_algebra_alt2: |
|
884 "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M), |
|
885 sets = (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i)), |
|
886 measure = measure (Pi\<^isub>P I M) \<rparr>" |
|
887 (is "_ = ?S") |
|
888 proof (rule measure_space.equality) |
|
889 let "sigma \<lparr> space = ?O, sets = ?A, \<dots> = _ \<rparr>" = ?S |
|
890 let ?G = "(\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))" |
|
891 have "sets (Pi\<^isub>P I M) = sigma_sets ?O ?G" |
|
892 by (subst infprod_algebra_alt) (simp add: sets_sigma) |
|
893 also have "\<dots> = sigma_sets ?O ?A" |
|
894 proof (intro equalityI sigma_sets_mono subsetI) |
|
895 interpret A: sigma_algebra ?S |
|
896 by (rule sigma_algebra_sigma) auto |
|
897 fix A assume "A \<in> ?G" |
|
898 then obtain J B where "finite J" "J \<noteq> {}" "J \<subseteq> I" "A = emb I J (Pi\<^isub>E J B)" |
|
899 and B: "\<And>i. i \<in> J \<Longrightarrow> B i \<in> sets (M i)" |
|
900 by auto |
|
901 then have A: "A = (\<Inter>j\<in>J. (\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M))" |
|
902 by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff) |
|
903 { fix j assume "j\<in>J" |
|
904 with `J \<subseteq> I` have "j \<in> I" by auto |
|
905 with `j \<in> J` B have "(\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M) \<in> sets ?S" |
|
906 by (auto simp: sets_sigma intro: sigma_sets.Basic) } |
|
907 with `finite J` `J \<noteq> {}` have "A \<in> sets ?S" |
|
908 unfolding A by (intro A.finite_INT) auto |
|
909 then show "A \<in> sigma_sets ?O ?A" by (simp add: sets_sigma) |
|
910 next |
|
911 fix A assume "A \<in> ?A" |
|
912 then obtain i B where i: "i \<in> I" "B \<in> sets (M i)" |
|
913 and "A = (\<lambda>x. x i) -` B \<inter> space (Pi\<^isub>P I M)" |
|
914 by auto |
|
915 then have "A = emb I {i} (Pi\<^isub>E {i} (\<lambda>_. B))" |
|
916 by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff) |
|
917 with i show "A \<in> sigma_sets ?O ?G" |
|
918 by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto |
|
919 qed |
|
920 finally show "sets (Pi\<^isub>P I M) = sets ?S" |
|
921 by (simp add: sets_sigma) |
|
922 qed simp_all |
|
923 |
|
924 lemma (in product_prob_space) measurable_into_infprod_algebra: |
|
925 assumes "sigma_algebra N" |
|
926 assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)" |
|
927 assumes ext: "\<And>x. x \<in> space N \<Longrightarrow> f x \<in> extensional I" |
|
928 shows "f \<in> measurable N (Pi\<^isub>P I M)" |
|
929 proof - |
|
930 interpret N: sigma_algebra N by fact |
|
931 have f_in: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> space N \<rightarrow> space (M i)" |
|
932 using f by (auto simp: measurable_def) |
|
933 { fix i A assume i: "i \<in> I" "A \<in> sets (M i)" |
|
934 then have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N = (\<lambda>x. f x i) -` A \<inter> space N" |
|
935 using f_in ext by (auto simp: infprod_algebra_def generator_def) |
|
936 also have "\<dots> \<in> sets N" |
|
937 by (rule measurable_sets f i)+ |
|
938 finally have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N \<in> sets N" . } |
|
939 with f_in ext show ?thesis |
|
940 by (subst infprod_algebra_alt2) |
|
941 (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def) |
|
942 qed |
|
943 |
|
944 subsection {* Sequence space *} |
|
945 |
|
946 locale sequence_space = product_prob_space M "UNIV :: nat set" for M |
|
947 |
|
948 lemma (in sequence_space) infprod_in_sets[intro]: |
|
949 fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)" |
|
950 shows "Pi UNIV E \<in> sets (Pi\<^isub>P UNIV M)" |
|
951 proof - |
|
952 have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))" |
|
953 using E E[THEN M.sets_into_space] |
|
954 by (auto simp: emb_def Pi_iff extensional_def) blast |
|
955 with E show ?thesis |
|
956 by (auto intro: emb_in_infprod_algebra) |
|
957 qed |
|
958 |
|
959 lemma (in sequence_space) measure_infprod: |
|
960 fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)" |
|
961 shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)" |
|
962 proof - |
|
963 let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)" |
|
964 { fix n :: nat |
|
965 interpret n: finite_product_prob_space M "{..n}" by default auto |
|
966 have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)" |
|
967 using E by (subst n.finite_measure_times) auto |
|
968 also have "\<dots> = \<mu>' (?E n)" |
|
969 using E by (intro finite_measure_infprod_emb[symmetric]) auto |
|
970 finally have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = \<mu>' (?E n)" . } |
|
971 moreover have "Pi UNIV E = (\<Inter>n. ?E n)" |
|
972 using E E[THEN M.sets_into_space] |
|
973 by (auto simp: emb_def extensional_def Pi_iff) blast |
|
974 moreover have "range ?E \<subseteq> sets (Pi\<^isub>P UNIV M)" |
|
975 using E by auto |
|
976 moreover have "decseq ?E" |
|
977 by (auto simp: emb_def Pi_iff decseq_def) |
|
978 ultimately show ?thesis |
|
979 by (simp add: finite_continuity_from_above) |
|
980 qed |
|
981 |
787 end |
982 end |