src/HOL/Probability/Infinite_Product_Measure.thy
 changeset 50040 5da32dc55cd8 parent 50039 bfd5198cbe40 child 50041 afe886a04198
equal inserted replaced
50039:bfd5198cbe40 50040:5da32dc55cd8
`    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"`