equal
deleted
inserted
replaced
79 |
79 |
80 locale projective_family = |
80 locale projective_family = |
81 fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)" |
81 fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)" |
82 assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> |
82 assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> |
83 (P H) (prod_emb H M J X) = (P J) X" |
83 (P H) (prod_emb H M J X) = (P J) X" |
84 assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)" |
84 assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)" |
85 assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)" |
85 assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)" |
86 assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)" |
86 assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)" |
87 begin |
87 begin |
88 |
88 |
89 lemma emeasure_limP: |
89 lemma emeasure_limP: |
131 let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}" |
131 let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}" |
132 let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)" |
132 let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)" |
133 let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" |
133 let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" |
134 show "Int_stable ?J" |
134 show "Int_stable ?J" |
135 by (rule Int_stable_PiE) |
135 by (rule Int_stable_PiE) |
136 interpret prob_space "P J" using prob_space `finite J` by simp |
136 interpret prob_space "P J" using proj_prob_space `finite J` by simp |
137 show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP) |
137 show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP) |
138 show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space) |
138 show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space) |
139 show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J" |
139 show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J" |
140 using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) |
140 using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) |
141 fix X assume "X \<in> ?J" |
141 fix X assume "X \<in> ?J" |
163 show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
163 show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
164 using sets[THEN sets_into_space] by (auto simp: space_PiM) |
164 using sets[THEN sets_into_space] by (auto simp: space_PiM) |
165 have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)" |
165 have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)" |
166 proof |
166 proof |
167 fix i assume "i \<in> L" |
167 fix i assume "i \<in> L" |
168 interpret prob_space "P {i}" using prob_space by simp |
168 interpret prob_space "P {i}" using proj_prob_space by simp |
169 from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM) |
169 from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM) |
170 qed |
170 qed |
171 from bchoice[OF this] |
171 from bchoice[OF this] |
172 show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto |
172 show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto |
173 show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))" |
173 show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))" |