equal
deleted
inserted
replaced
85 sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M |
85 sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M |
86 proof |
86 proof |
87 fix J::"'i set" assume "finite J" |
87 fix J::"'i set" assume "finite J" |
88 interpret f: finite_product_prob_space M J proof qed fact |
88 interpret f: finite_product_prob_space M J proof qed fact |
89 show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp |
89 show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp |
|
90 show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and> |
|
91 (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and> |
|
92 (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`] |
|
93 by (auto simp add: sigma_finite_measure_def) |
|
94 show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1) |
90 qed simp_all |
95 qed simp_all |
91 |
96 |
92 lemma (in projective_family) prod_emb_injective: |
97 lemma (in projective_family) prod_emb_injective: |
93 assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)" |
98 assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)" |
94 assumes "prod_emb L M J X = prod_emb L M J Y" |
99 assumes "prod_emb L M J X = prod_emb L M J Y" |