596 have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto |
596 have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto |
597 show ?thesis |
597 show ?thesis |
598 using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto |
598 using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto |
599 qed |
599 qed |
600 |
600 |
|
601 lemma (in product_finite_prob_space) singleton_eq_product: |
|
602 assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})" |
|
603 proof (safe intro!: ext[of _ x]) |
|
604 fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I" |
|
605 with x show "y i = x i" |
|
606 by (cases "i \<in> I") (auto simp: extensional_def) |
|
607 qed (insert x, auto) |
|
608 |
601 sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M" |
609 sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M" |
602 proof |
610 proof |
603 show "finite (space P)" |
611 show "finite (space P)" |
604 using finite_index M.finite_space by auto |
612 using finite_index M.finite_space by auto |
605 |
613 |
606 { fix x assume "x \<in> space P" |
614 { fix x assume "x \<in> space P" |
607 then have x: "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})" |
615 with this[THEN singleton_eq_product] |
608 proof safe |
616 have "{x} \<in> sets P" |
609 fix y assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I" |
|
610 show "y = x" |
|
611 proof |
|
612 fix i show "y i = x i" |
|
613 using * `x \<in> space P` by (cases "i \<in> I") (auto simp: extensional_def) |
|
614 qed |
|
615 qed auto |
|
616 with `x \<in> space P` have "{x} \<in> sets P" |
|
617 by (auto intro!: in_P) } |
617 by (auto intro!: in_P) } |
618 note x_in_P = this |
618 note x_in_P = this |
619 |
619 |
620 have "Pow (space P) \<subseteq> sets P" |
620 have "Pow (space P) \<subseteq> sets P" |
621 proof |
621 proof |
626 by (intro finite_UN x_in_P) auto |
626 by (intro finite_UN x_in_P) auto |
627 then show "X \<in> sets P" by simp |
627 then show "X \<in> sets P" by simp |
628 qed |
628 qed |
629 with space_closed show [simp]: "sets P = Pow (space P)" .. |
629 with space_closed show [simp]: "sets P = Pow (space P)" .. |
630 |
630 |
631 |
|
632 { fix x assume "x \<in> space P" |
631 { fix x assume "x \<in> space P" |
633 from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto |
632 from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto |
634 then show "\<mu> {x} \<noteq> \<infinity>" |
633 then show "\<mu> {x} \<noteq> \<infinity>" |
635 using measure_space_1 by auto } |
634 using measure_space_1 by auto } |
636 qed |
635 qed |
637 |
636 |
638 lemma (in product_finite_prob_space) measure_finite_times: |
637 lemma (in product_finite_prob_space) measure_finite_times: |
639 "(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))" |
638 "(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))" |
640 by (rule measure_times) simp |
639 by (rule measure_times) simp |
641 |
640 |
642 lemma (in product_finite_prob_space) prob_times: |
641 lemma (in product_finite_prob_space) measure_singleton_times: |
|
642 assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})" |
|
643 unfolding singleton_eq_product[OF x] using x |
|
644 by (intro measure_finite_times) auto |
|
645 |
|
646 lemma (in product_finite_prob_space) prob_finite_times: |
643 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)" |
647 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)" |
644 shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" |
648 shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" |
645 proof - |
649 proof - |
646 have "extreal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)" |
650 have "extreal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)" |
647 using X by (intro finite_measure_eq[symmetric] in_P) auto |
651 using X by (intro finite_measure_eq[symmetric] in_P) auto |
649 using measure_finite_times X by simp |
653 using measure_finite_times X by simp |
650 also have "\<dots> = extreal (\<Prod>i\<in>I. M.\<mu>' i (X i))" |
654 also have "\<dots> = extreal (\<Prod>i\<in>I. M.\<mu>' i (X i))" |
651 using X by (simp add: M.finite_measure_eq setprod_extreal) |
655 using X by (simp add: M.finite_measure_eq setprod_extreal) |
652 finally show ?thesis by simp |
656 finally show ?thesis by simp |
653 qed |
657 qed |
|
658 |
|
659 lemma (in product_finite_prob_space) prob_singleton_times: |
|
660 assumes x: "x \<in> space P" |
|
661 shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})" |
|
662 unfolding singleton_eq_product[OF x] using x |
|
663 by (intro prob_finite_times) auto |
|
664 |
|
665 lemma (in product_finite_prob_space) prob_finite_product: |
|
666 "A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})" |
|
667 by (auto simp add: finite_measure_singleton prob_singleton_times |
|
668 simp del: space_product_algebra |
|
669 intro!: setsum_cong prob_singleton_times) |
654 |
670 |
655 lemma (in prob_space) joint_distribution_finite_prob_space: |
671 lemma (in prob_space) joint_distribution_finite_prob_space: |
656 assumes X: "finite_random_variable MX X" |
672 assumes X: "finite_random_variable MX X" |
657 assumes Y: "finite_random_variable MY Y" |
673 assumes Y: "finite_random_variable MY Y" |
658 shows "finite_prob_space ((MX \<Otimes>\<^isub>M MY)\<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |
674 shows "finite_prob_space ((MX \<Otimes>\<^isub>M MY)\<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)" |