9 imports Finite_Product_Measure Probability_Measure |
9 imports Finite_Product_Measure Probability_Measure |
10 begin |
10 begin |
11 |
11 |
12 lemma (in product_prob_space) distr_restrict: |
12 lemma (in product_prob_space) distr_restrict: |
13 assumes "J \<noteq> {}" "J \<subseteq> K" "finite K" |
13 assumes "J \<noteq> {}" "J \<subseteq> K" "finite K" |
14 shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D") |
14 shows "(\<Pi>\<^sub>M i\<in>J. M i) = distr (\<Pi>\<^sub>M i\<in>K. M i) (\<Pi>\<^sub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D") |
15 proof (rule measure_eqI_generator_eq) |
15 proof (rule measure_eqI_generator_eq) |
16 have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset) |
16 have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset) |
17 interpret J: finite_product_prob_space M J proof qed fact |
17 interpret J: finite_product_prob_space M J proof qed fact |
18 interpret K: finite_product_prob_space M K proof qed fact |
18 interpret K: finite_product_prob_space M K proof qed fact |
19 |
19 |
20 let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}" |
20 let ?J = "{Pi\<^sub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}" |
21 let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)" |
21 let ?F = "\<lambda>i. \<Pi>\<^sub>E k\<in>J. space (M k)" |
22 let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" |
22 let ?\<Omega> = "(\<Pi>\<^sub>E k\<in>J. space (M k))" |
23 show "Int_stable ?J" |
23 show "Int_stable ?J" |
24 by (rule Int_stable_PiE) |
24 by (rule Int_stable_PiE) |
25 show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>" |
25 show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>" |
26 using `finite J` by (auto intro!: prod_algebraI_finite) |
26 using `finite J` by (auto intro!: prod_algebraI_finite) |
27 { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp } |
27 { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp } |
28 show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space) |
28 show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space) |
29 show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J" |
29 show "sets (\<Pi>\<^sub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J" |
30 using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) |
30 using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) |
31 |
31 |
32 fix X assume "X \<in> ?J" |
32 fix X assume "X \<in> ?J" |
33 then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto |
33 then obtain E where [simp]: "X = Pi\<^sub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto |
34 with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" |
34 with `finite J` have X: "X \<in> sets (Pi\<^sub>M J M)" |
35 by simp |
35 by simp |
36 |
36 |
37 have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))" |
37 have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))" |
38 using E by (simp add: J.measure_times) |
38 using E by (simp add: J.measure_times) |
39 also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))" |
39 also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))" |
40 by simp |
40 by simp |
41 also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))" |
41 also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))" |
42 using `finite K` `J \<subseteq> K` |
42 using `finite K` `J \<subseteq> K` |
43 by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1) |
43 by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1) |
44 also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))" |
44 also have "\<dots> = emeasure (Pi\<^sub>M K M) (\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i))" |
45 using E by (simp add: K.measure_times) |
45 using E by (simp add: K.measure_times) |
46 also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))" |
46 also have "(\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^sub>E J E \<inter> (\<Pi>\<^sub>E i\<in>K. space (M i))" |
47 using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm) |
47 using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm) |
48 finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X" |
48 finally show "emeasure (Pi\<^sub>M J M) X = emeasure ?D X" |
49 using X `J \<subseteq> K` apply (subst emeasure_distr) |
49 using X `J \<subseteq> K` apply (subst emeasure_distr) |
50 by (auto intro!: measurable_restrict_subset simp: space_PiM) |
50 by (auto intro!: measurable_restrict_subset simp: space_PiM) |
51 qed |
51 qed |
52 |
52 |
53 lemma (in product_prob_space) emeasure_prod_emb[simp]: |
53 lemma (in product_prob_space) emeasure_prod_emb[simp]: |
54 assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)" |
54 assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)" |
55 shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X" |
55 shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X" |
56 by (subst distr_restrict[OF L]) |
56 by (subst distr_restrict[OF L]) |
57 (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) |
57 (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) |
58 |
58 |
59 definition |
59 definition |
60 limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where |
60 limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where |
61 "limP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i)) |
61 "limP I M P = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i)) |
62 {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} |
62 {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} |
63 (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j)) |
63 (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j)) |
64 (\<lambda>(J, X). emeasure (P J) (Pi\<^isub>E J X))" |
64 (\<lambda>(J, X). emeasure (P J) (Pi\<^sub>E J X))" |
65 |
65 |
66 abbreviation "lim\<^isub>P \<equiv> limP" |
66 abbreviation "lim\<^sub>P \<equiv> limP" |
67 |
67 |
68 lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)" |
68 lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)" |
69 by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure) |
69 by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure) |
70 |
70 |
71 lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)" |
71 lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)" |
72 by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure) |
72 by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure) |
73 |
73 |
74 lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'" |
74 lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^sub>M i\<in>I. M i) M'" |
75 unfolding measurable_def by auto |
75 unfolding measurable_def by auto |
76 |
76 |
77 lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)" |
77 lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^sub>M i\<in>I. M i)" |
78 unfolding measurable_def by auto |
78 unfolding measurable_def by auto |
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> |
88 |
88 |
89 lemma emeasure_limP: |
89 lemma emeasure_limP: |
90 assumes "finite J" |
90 assumes "finite J" |
91 assumes "J \<subseteq> I" |
91 assumes "J \<subseteq> I" |
92 assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)" |
92 assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)" |
93 shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)" |
93 shows "emeasure (limP J M P) (Pi\<^sub>E J A) = emeasure (P J) (Pi\<^sub>E J A)" |
94 proof - |
94 proof - |
95 have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
95 have "Pi\<^sub>E J (restrict A J) \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" |
96 using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast |
96 using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast |
97 hence "emeasure (limP J M P) (Pi\<^isub>E J A) = |
97 hence "emeasure (limP J M P) (Pi\<^sub>E J A) = |
98 emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))" |
98 emeasure (limP J M P) (prod_emb J M J (Pi\<^sub>E J A))" |
99 using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def) |
99 using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def) |
100 also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)" |
100 also have "\<dots> = emeasure (P J) (Pi\<^sub>E J A)" |
101 proof (rule emeasure_extend_measure_Pair[OF limP_def]) |
101 proof (rule emeasure_extend_measure_Pair[OF limP_def]) |
102 show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto |
102 show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto |
103 show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def |
103 show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def |
104 by (auto simp: suminf_emeasure proj_sets[OF `finite J`]) |
104 by (auto simp: suminf_emeasure proj_sets[OF `finite J`]) |
105 show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))" |
105 show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))" |
106 using assms by auto |
106 using assms by auto |
107 fix K and X::"'i \<Rightarrow> 'a set" |
107 fix K and X::"'i \<Rightarrow> 'a set" |
108 show "prod_emb J M K (Pi\<^isub>E K X) \<in> Pow (\<Pi>\<^isub>E i\<in>J. space (M i))" |
108 show "prod_emb J M K (Pi\<^sub>E K X) \<in> Pow (\<Pi>\<^sub>E i\<in>J. space (M i))" |
109 by (auto simp: prod_emb_def) |
109 by (auto simp: prod_emb_def) |
110 assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))" |
110 assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))" |
111 thus "emeasure (P J) (prod_emb J M K (Pi\<^isub>E K X)) = emeasure (P K) (Pi\<^isub>E K X)" |
111 thus "emeasure (P J) (prod_emb J M K (Pi\<^sub>E K X)) = emeasure (P K) (Pi\<^sub>E K X)" |
112 using assms |
112 using assms |
113 apply (cases "J = {}") |
113 apply (cases "J = {}") |
114 apply (simp add: prod_emb_id) |
114 apply (simp add: prod_emb_id) |
115 apply (fastforce simp add: intro!: projective sets_PiM_I_finite) |
115 apply (fastforce simp add: intro!: projective sets_PiM_I_finite) |
116 done |
116 done |
148 |
148 |
149 abbreviation |
149 abbreviation |
150 "emb L K X \<equiv> prod_emb L M K X" |
150 "emb L K X \<equiv> prod_emb L M K X" |
151 |
151 |
152 lemma prod_emb_injective: |
152 lemma prod_emb_injective: |
153 assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)" |
153 assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^sub>M J M)" "Y \<in> sets (Pi\<^sub>M J M)" |
154 assumes "emb L J X = emb L J Y" |
154 assumes "emb L J X = emb L J Y" |
155 shows "X = Y" |
155 shows "X = Y" |
156 proof (rule injective_vimage_restrict) |
156 proof (rule injective_vimage_restrict) |
157 show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
157 show "X \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" |
158 using sets[THEN sets.sets_into_space] by (auto simp: space_PiM) |
158 using sets[THEN sets.sets_into_space] by (auto simp: space_PiM) |
159 have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)" |
159 have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)" |
160 proof |
160 proof |
161 fix i assume "i \<in> L" |
161 fix i assume "i \<in> L" |
162 interpret prob_space "P {i}" using proj_prob_space by simp |
162 interpret prob_space "P {i}" using proj_prob_space by simp |
163 from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM) |
163 from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM) |
164 qed |
164 qed |
165 from bchoice[OF this] |
165 from bchoice[OF this] |
166 show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def) |
166 show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def) |
167 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))" |
167 show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i))" |
168 using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def) |
168 using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def) |
169 qed fact |
169 qed fact |
170 |
170 |
171 definition generator :: "('i \<Rightarrow> 'a) set set" where |
171 definition generator :: "('i \<Rightarrow> 'a) set set" where |
172 "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))" |
172 "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^sub>M J M))" |
173 |
173 |
174 lemma generatorI': |
174 lemma generatorI': |
175 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator" |
175 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator" |
176 unfolding generator_def by auto |
176 unfolding generator_def by auto |
177 |
177 |
178 lemma algebra_generator: |
178 lemma algebra_generator: |
179 assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G") |
179 assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G") |
180 unfolding algebra_def algebra_axioms_def ring_of_sets_iff |
180 unfolding algebra_def algebra_axioms_def ring_of_sets_iff |
181 proof (intro conjI ballI) |
181 proof (intro conjI ballI) |
182 let ?G = generator |
182 let ?G = generator |
183 show "?G \<subseteq> Pow ?\<Omega>" |
183 show "?G \<subseteq> Pow ?\<Omega>" |
184 by (auto simp: generator_def prod_emb_def) |
184 by (auto simp: generator_def prod_emb_def) |
185 from `I \<noteq> {}` obtain i where "i \<in> I" by auto |
185 from `I \<noteq> {}` obtain i where "i \<in> I" by auto |
186 then show "{} \<in> ?G" |
186 then show "{} \<in> ?G" |
187 by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"] |
187 by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"] |
188 simp: sigma_sets.Empty generator_def prod_emb_def) |
188 simp: sigma_sets.Empty generator_def prod_emb_def) |
189 from `i \<in> I` show "?\<Omega> \<in> ?G" |
189 from `i \<in> I` show "?\<Omega> \<in> ?G" |
190 by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"] |
190 by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^sub>E {i} (\<lambda>i. space (M i))"] |
191 simp: generator_def prod_emb_def) |
191 simp: generator_def prod_emb_def) |
192 fix A assume "A \<in> ?G" |
192 fix A assume "A \<in> ?G" |
193 then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA" |
193 then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^sub>M JA M)" and A: "A = emb I JA XA" |
194 by (auto simp: generator_def) |
194 by (auto simp: generator_def) |
195 fix B assume "B \<in> ?G" |
195 fix B assume "B \<in> ?G" |
196 then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB" |
196 then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^sub>M JB M)" and B: "B = emb I JB XB" |
197 by (auto simp: generator_def) |
197 by (auto simp: generator_def) |
198 let ?RA = "emb (JA \<union> JB) JA XA" |
198 let ?RA = "emb (JA \<union> JB) JA XA" |
199 let ?RB = "emb (JA \<union> JB) JB XB" |
199 let ?RB = "emb (JA \<union> JB) JB XB" |
200 have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)" |
200 have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)" |
201 using XA A XB B by auto |
201 using XA A XB B by auto |
202 show "A - B \<in> ?G" "A \<union> B \<in> ?G" |
202 show "A - B \<in> ?G" "A \<union> B \<in> ?G" |
203 unfolding * using XA XB by (safe intro!: generatorI') auto |
203 unfolding * using XA XB by (safe intro!: generatorI') auto |
204 qed |
204 qed |
205 |
205 |
206 lemma sets_PiM_generator: |
206 lemma sets_PiM_generator: |
207 "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" |
207 "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator" |
208 proof cases |
208 proof cases |
209 assume "I = {}" then show ?thesis |
209 assume "I = {}" then show ?thesis |
210 unfolding generator_def |
210 unfolding generator_def |
211 by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong) |
211 by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong) |
212 next |
212 next |
213 assume "I \<noteq> {}" |
213 assume "I \<noteq> {}" |
214 show ?thesis |
214 show ?thesis |
215 proof |
215 proof |
216 show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" |
216 show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator" |
217 unfolding sets_PiM |
217 unfolding sets_PiM |
218 proof (safe intro!: sigma_sets_subseteq) |
218 proof (safe intro!: sigma_sets_subseteq) |
219 fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator" |
219 fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator" |
220 by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE) |
220 by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE) |
221 qed |
221 qed |
222 qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset) |
222 qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset) |
223 qed |
223 qed |
224 |
224 |
225 lemma generatorI: |
225 lemma generatorI: |
226 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator" |
226 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator" |
227 unfolding generator_def by auto |
227 unfolding generator_def by auto |
228 |
228 |
229 definition mu_G ("\<mu>G") where |
229 definition mu_G ("\<mu>G") where |
230 "\<mu>G A = |
230 "\<mu>G A = |
231 (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (limP J M P) X))" |
231 (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^sub>M J M). A = emb I J X \<longrightarrow> x = emeasure (limP J M P) X))" |
232 |
232 |
233 lemma mu_G_spec: |
233 lemma mu_G_spec: |
234 assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)" |
234 assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)" |
235 shows "\<mu>G A = emeasure (limP J M P) X" |
235 shows "\<mu>G A = emeasure (limP J M P) X" |
236 unfolding mu_G_def |
236 unfolding mu_G_def |
237 proof (intro the_equality allI impI ballI) |
237 proof (intro the_equality allI impI ballI) |
238 fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)" |
238 fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^sub>M K M)" |
239 have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)" |
239 have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)" |
240 using K J by simp |
240 using K J by simp |
241 also have "emb (K \<union> J) K Y = emb (K \<union> J) J X" |
241 also have "emb (K \<union> J) K Y = emb (K \<union> J) J X" |
242 using K J by (simp add: prod_emb_injective[of "K \<union> J" I]) |
242 using K J by (simp add: prod_emb_injective[of "K \<union> J" I]) |
243 also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X" |
243 also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X" |
244 using K J by simp |
244 using K J by simp |
245 finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" .. |
245 finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" .. |
246 qed (insert J, force) |
246 qed (insert J, force) |
247 |
247 |
248 lemma mu_G_eq: |
248 lemma mu_G_eq: |
249 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (limP J M P) X" |
249 "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (limP J M P) X" |
250 by (intro mu_G_spec) auto |
250 by (intro mu_G_spec) auto |
251 |
251 |
252 lemma generator_Ex: |
252 lemma generator_Ex: |
253 assumes *: "A \<in> generator" |
253 assumes *: "A \<in> generator" |
254 shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (limP J M P) X" |
254 shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^sub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (limP J M P) X" |
255 proof - |
255 proof - |
256 from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)" |
256 from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)" |
257 unfolding generator_def by auto |
257 unfolding generator_def by auto |
258 with mu_G_spec[OF this] show ?thesis by auto |
258 with mu_G_spec[OF this] show ?thesis by auto |
259 qed |
259 qed |
260 |
260 |
261 lemma generatorE: |
261 lemma generatorE: |
262 assumes A: "A \<in> generator" |
262 assumes A: "A \<in> generator" |
263 obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X" |
263 obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X" |
264 using generator_Ex[OF A] by atomize_elim auto |
264 using generator_Ex[OF A] by atomize_elim auto |
265 |
265 |
266 lemma merge_sets: |
266 lemma merge_sets: |
267 "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)" |
267 "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^sub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^sub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^sub>M K M) \<in> sets (Pi\<^sub>M K M)" |
268 by simp |
268 by simp |
269 |
269 |
270 lemma merge_emb: |
270 lemma merge_emb: |
271 assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)" |
271 assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^sub>M J M)" |
272 shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = |
272 shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^sub>M I M)) = |
273 emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))" |
273 emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^sub>M (K - J) M))" |
274 proof - |
274 proof - |
275 have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)" |
275 have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)" |
276 by (auto simp: restrict_def merge_def) |
276 by (auto simp: restrict_def merge_def) |
277 have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)" |
277 have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)" |
278 by (auto simp: restrict_def merge_def) |
278 by (auto simp: restrict_def merge_def) |