1 (* Title: HOL/Probability/Caratheodory.thy |
|
2 Author: Lawrence C Paulson |
|
3 Author: Johannes Hölzl, TU München |
|
4 *) |
|
5 |
|
6 section \<open>Caratheodory Extension Theorem\<close> |
|
7 |
|
8 theory Caratheodory |
|
9 imports Measure_Space |
|
10 begin |
|
11 |
|
12 text \<open> |
|
13 Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. |
|
14 \<close> |
|
15 |
|
16 lemma suminf_ennreal_2dimen: |
|
17 fixes f:: "nat \<times> nat \<Rightarrow> ennreal" |
|
18 assumes "\<And>m. g m = (\<Sum>n. f (m,n))" |
|
19 shows "(\<Sum>i. f (prod_decode i)) = suminf g" |
|
20 proof - |
|
21 have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))" |
|
22 using assms by (simp add: fun_eq_iff) |
|
23 have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = setsum f (prod_decode ` B)" |
|
24 by (simp add: setsum.reindex[OF inj_prod_decode] comp_def) |
|
25 have "(SUP n. \<Sum>i<n. f (prod_decode i)) = (SUP p : UNIV \<times> UNIV. \<Sum>i<fst p. \<Sum>n<snd p. f (i, n))" |
|
26 proof (intro SUP_eq; clarsimp simp: setsum.cartesian_product reindex) |
|
27 fix n |
|
28 let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))" |
|
29 { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x" |
|
30 then have "a < ?M fst" "b < ?M snd" |
|
31 by (auto intro!: Max_ge le_imp_less_Suc image_eqI) } |
|
32 then have "setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<?M fst} \<times> {..<?M snd})" |
|
33 by (auto intro!: setsum_mono3) |
|
34 then show "\<exists>a b. setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<a} \<times> {..<b})" by auto |
|
35 next |
|
36 fix a b |
|
37 let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} \<times> {..<b})))}" |
|
38 { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M" |
|
39 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
|
40 then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" |
|
41 by (auto intro!: setsum_mono3) |
|
42 then show "\<exists>n. setsum f ({..<a} \<times> {..<b}) \<le> setsum f (prod_decode ` {..<n})" |
|
43 by auto |
|
44 qed |
|
45 also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))" |
|
46 unfolding suminf_setsum[OF summableI, symmetric] |
|
47 by (simp add: suminf_eq_SUP SUP_pair setsum.commute[of _ "{..< fst _}"]) |
|
48 finally show ?thesis unfolding g_def |
|
49 by (simp add: suminf_eq_SUP) |
|
50 qed |
|
51 |
|
52 subsection \<open>Characterizations of Measures\<close> |
|
53 |
|
54 definition outer_measure_space where |
|
55 "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f" |
|
56 |
|
57 subsubsection \<open>Lambda Systems\<close> |
|
58 |
|
59 definition lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set" |
|
60 where |
|
61 "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}" |
|
62 |
|
63 lemma (in algebra) lambda_system_eq: |
|
64 "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}" |
|
65 proof - |
|
66 have [simp]: "\<And>l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l" |
|
67 by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) |
|
68 show ?thesis |
|
69 by (auto simp add: lambda_system_def) (metis Int_commute)+ |
|
70 qed |
|
71 |
|
72 lemma (in algebra) lambda_system_empty: "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f" |
|
73 by (auto simp add: positive_def lambda_system_eq) |
|
74 |
|
75 lemma lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M" |
|
76 by (simp add: lambda_system_def) |
|
77 |
|
78 lemma (in algebra) lambda_system_Compl: |
|
79 fixes f:: "'a set \<Rightarrow> ennreal" |
|
80 assumes x: "x \<in> lambda_system \<Omega> M f" |
|
81 shows "\<Omega> - x \<in> lambda_system \<Omega> M f" |
|
82 proof - |
|
83 have "x \<subseteq> \<Omega>" |
|
84 by (metis sets_into_space lambda_system_sets x) |
|
85 hence "\<Omega> - (\<Omega> - x) = x" |
|
86 by (metis double_diff equalityE) |
|
87 with x show ?thesis |
|
88 by (force simp add: lambda_system_def ac_simps) |
|
89 qed |
|
90 |
|
91 lemma (in algebra) lambda_system_Int: |
|
92 fixes f:: "'a set \<Rightarrow> ennreal" |
|
93 assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" |
|
94 shows "x \<inter> y \<in> lambda_system \<Omega> M f" |
|
95 proof - |
|
96 from xl yl show ?thesis |
|
97 proof (auto simp add: positive_def lambda_system_eq Int) |
|
98 fix u |
|
99 assume x: "x \<in> M" and y: "y \<in> M" and u: "u \<in> M" |
|
100 and fx: "\<forall>z\<in>M. f (z \<inter> x) + f (z - x) = f z" |
|
101 and fy: "\<forall>z\<in>M. f (z \<inter> y) + f (z - y) = f z" |
|
102 have "u - x \<inter> y \<in> M" |
|
103 by (metis Diff Diff_Int Un u x y) |
|
104 moreover |
|
105 have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast |
|
106 moreover |
|
107 have "u - x \<inter> y - y = u - y" by blast |
|
108 ultimately |
|
109 have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy |
|
110 by force |
|
111 have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) |
|
112 = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)" |
|
113 by (simp add: ey ac_simps) |
|
114 also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)" |
|
115 by (simp add: Int_ac) |
|
116 also have "... = f (u \<inter> y) + f (u - y)" |
|
117 using fx [THEN bspec, of "u \<inter> y"] Int y u |
|
118 by force |
|
119 also have "... = f u" |
|
120 by (metis fy u) |
|
121 finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" . |
|
122 qed |
|
123 qed |
|
124 |
|
125 lemma (in algebra) lambda_system_Un: |
|
126 fixes f:: "'a set \<Rightarrow> ennreal" |
|
127 assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" |
|
128 shows "x \<union> y \<in> lambda_system \<Omega> M f" |
|
129 proof - |
|
130 have "(\<Omega> - x) \<inter> (\<Omega> - y) \<in> M" |
|
131 by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) |
|
132 moreover |
|
133 have "x \<union> y = \<Omega> - ((\<Omega> - x) \<inter> (\<Omega> - y))" |
|
134 by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ |
|
135 ultimately show ?thesis |
|
136 by (metis lambda_system_Compl lambda_system_Int xl yl) |
|
137 qed |
|
138 |
|
139 lemma (in algebra) lambda_system_algebra: |
|
140 "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)" |
|
141 apply (auto simp add: algebra_iff_Un) |
|
142 apply (metis lambda_system_sets set_mp sets_into_space) |
|
143 apply (metis lambda_system_empty) |
|
144 apply (metis lambda_system_Compl) |
|
145 apply (metis lambda_system_Un) |
|
146 done |
|
147 |
|
148 lemma (in algebra) lambda_system_strong_additive: |
|
149 assumes z: "z \<in> M" and disj: "x \<inter> y = {}" |
|
150 and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" |
|
151 shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" |
|
152 proof - |
|
153 have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
|
154 moreover |
|
155 have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast |
|
156 moreover |
|
157 have "(z \<inter> (x \<union> y)) \<in> M" |
|
158 by (metis Int Un lambda_system_sets xl yl z) |
|
159 ultimately show ?thesis using xl yl |
|
160 by (simp add: lambda_system_eq) |
|
161 qed |
|
162 |
|
163 lemma (in algebra) lambda_system_additive: "additive (lambda_system \<Omega> M f) f" |
|
164 proof (auto simp add: additive_def) |
|
165 fix x and y |
|
166 assume disj: "x \<inter> y = {}" |
|
167 and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" |
|
168 hence "x \<in> M" "y \<in> M" by (blast intro: lambda_system_sets)+ |
|
169 thus "f (x \<union> y) = f x + f y" |
|
170 using lambda_system_strong_additive [OF top disj xl yl] |
|
171 by (simp add: Un) |
|
172 qed |
|
173 |
|
174 lemma lambda_system_increasing: "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f" |
|
175 by (simp add: increasing_def lambda_system_def) |
|
176 |
|
177 lemma lambda_system_positive: "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f" |
|
178 by (simp add: positive_def lambda_system_def) |
|
179 |
|
180 lemma (in algebra) lambda_system_strong_sum: |
|
181 fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ennreal" |
|
182 assumes f: "positive M f" and a: "a \<in> M" |
|
183 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
|
184 and disj: "disjoint_family A" |
|
185 shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))" |
|
186 proof (induct n) |
|
187 case 0 show ?case using f by (simp add: positive_def) |
|
188 next |
|
189 case (Suc n) |
|
190 have 2: "A n \<inter> UNION {0..<n} A = {}" using disj |
|
191 by (force simp add: disjoint_family_on_def neq_iff) |
|
192 have 3: "A n \<in> lambda_system \<Omega> M f" using A |
|
193 by blast |
|
194 interpret l: algebra \<Omega> "lambda_system \<Omega> M f" |
|
195 using f by (rule lambda_system_algebra) |
|
196 have 4: "UNION {0..<n} A \<in> lambda_system \<Omega> M f" |
|
197 using A l.UNION_in_sets by simp |
|
198 from Suc.hyps show ?case |
|
199 by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) |
|
200 qed |
|
201 |
|
202 lemma (in sigma_algebra) lambda_system_caratheodory: |
|
203 assumes oms: "outer_measure_space M f" |
|
204 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
|
205 and disj: "disjoint_family A" |
|
206 shows "(\<Union>i. A i) \<in> lambda_system \<Omega> M f \<and> (\<Sum>i. f (A i)) = f (\<Union>i. A i)" |
|
207 proof - |
|
208 have pos: "positive M f" and inc: "increasing M f" |
|
209 and csa: "countably_subadditive M f" |
|
210 by (metis oms outer_measure_space_def)+ |
|
211 have sa: "subadditive M f" |
|
212 by (metis countably_subadditive_subadditive csa pos) |
|
213 have A': "\<And>S. A`S \<subseteq> (lambda_system \<Omega> M f)" using A |
|
214 by auto |
|
215 interpret ls: algebra \<Omega> "lambda_system \<Omega> M f" |
|
216 using pos by (rule lambda_system_algebra) |
|
217 have A'': "range A \<subseteq> M" |
|
218 by (metis A image_subset_iff lambda_system_sets) |
|
219 |
|
220 have U_in: "(\<Union>i. A i) \<in> M" |
|
221 by (metis A'' countable_UN) |
|
222 have U_eq: "f (\<Union>i. A i) = (\<Sum>i. f (A i))" |
|
223 proof (rule antisym) |
|
224 show "f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))" |
|
225 using csa[unfolded countably_subadditive_def] A'' disj U_in by auto |
|
226 have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto |
|
227 show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)" |
|
228 using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A'' |
|
229 by (intro suminf_le_const[OF summableI]) (auto intro!: increasingD[OF inc] countable_UN) |
|
230 qed |
|
231 have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a" |
|
232 if a [iff]: "a \<in> M" for a |
|
233 proof (rule antisym) |
|
234 have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A'' |
|
235 by blast |
|
236 moreover |
|
237 have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
|
238 by (auto simp add: disjoint_family_on_def) |
|
239 moreover |
|
240 have "a \<inter> (\<Union>i. A i) \<in> M" |
|
241 by (metis Int U_in a) |
|
242 ultimately |
|
243 have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))" |
|
244 using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"] |
|
245 by (simp add: o_def) |
|
246 hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))" |
|
247 by (rule add_right_mono) |
|
248 also have "\<dots> \<le> f a" |
|
249 proof (intro ennreal_suminf_bound_add) |
|
250 fix n |
|
251 have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M" |
|
252 by (metis A'' UNION_in_sets) |
|
253 have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
|
254 by (blast intro: increasingD [OF inc] A'' UNION_in_sets) |
|
255 have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f" |
|
256 using ls.UNION_in_sets by (simp add: A) |
|
257 hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))" |
|
258 by (simp add: lambda_system_eq UNION_in) |
|
259 have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
|
260 by (blast intro: increasingD [OF inc] UNION_in U_in) |
|
261 thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
|
262 by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) |
|
263 qed |
|
264 finally show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
|
265 by simp |
|
266 next |
|
267 have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
|
268 by (blast intro: increasingD [OF inc] U_in) |
|
269 also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
|
270 by (blast intro: subadditiveD [OF sa] U_in) |
|
271 finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" . |
|
272 qed |
|
273 thus ?thesis |
|
274 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
|
275 qed |
|
276 |
|
277 lemma (in sigma_algebra) caratheodory_lemma: |
|
278 assumes oms: "outer_measure_space M f" |
|
279 defines "L \<equiv> lambda_system \<Omega> M f" |
|
280 shows "measure_space \<Omega> L f" |
|
281 proof - |
|
282 have pos: "positive M f" |
|
283 by (metis oms outer_measure_space_def) |
|
284 have alg: "algebra \<Omega> L" |
|
285 using lambda_system_algebra [of f, OF pos] |
|
286 by (simp add: algebra_iff_Un L_def) |
|
287 then |
|
288 have "sigma_algebra \<Omega> L" |
|
289 using lambda_system_caratheodory [OF oms] |
|
290 by (simp add: sigma_algebra_disjoint_iff L_def) |
|
291 moreover |
|
292 have "countably_additive L f" "positive L f" |
|
293 using pos lambda_system_caratheodory [OF oms] |
|
294 by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def) |
|
295 ultimately |
|
296 show ?thesis |
|
297 using pos by (simp add: measure_space_def) |
|
298 qed |
|
299 |
|
300 definition outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where |
|
301 "outer_measure M f X = |
|
302 (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))" |
|
303 |
|
304 lemma (in ring_of_sets) outer_measure_agrees: |
|
305 assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M" |
|
306 shows "outer_measure M f s = f s" |
|
307 unfolding outer_measure_def |
|
308 proof (safe intro!: antisym INF_greatest) |
|
309 fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" and dA: "disjoint_family A" and sA: "s \<subseteq> (\<Union>x. A x)" |
|
310 have inc: "increasing M f" |
|
311 by (metis additive_increasing ca countably_additive_additive posf) |
|
312 have "f s = f (\<Union>i. A i \<inter> s)" |
|
313 using sA by (auto simp: Int_absorb1) |
|
314 also have "\<dots> = (\<Sum>i. f (A i \<inter> s))" |
|
315 using sA dA A s |
|
316 by (intro ca[unfolded countably_additive_def, rule_format, symmetric]) |
|
317 (auto simp: Int_absorb1 disjoint_family_on_def) |
|
318 also have "... \<le> (\<Sum>i. f (A i))" |
|
319 using A s by (auto intro!: suminf_le increasingD[OF inc]) |
|
320 finally show "f s \<le> (\<Sum>i. f (A i))" . |
|
321 next |
|
322 have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s" |
|
323 using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto |
|
324 with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s" |
|
325 by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"]) |
|
326 (auto simp: disjoint_family_on_def) |
|
327 qed |
|
328 |
|
329 lemma outer_measure_empty: |
|
330 "positive M f \<Longrightarrow> {} \<in> M \<Longrightarrow> outer_measure M f {} = 0" |
|
331 unfolding outer_measure_def |
|
332 by (intro antisym INF_lower2[of "\<lambda>_. {}"]) (auto simp: disjoint_family_on_def positive_def) |
|
333 |
|
334 lemma (in ring_of_sets) positive_outer_measure: |
|
335 assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)" |
|
336 unfolding positive_def by (auto simp: assms outer_measure_empty) |
|
337 |
|
338 lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)" |
|
339 by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) |
|
340 |
|
341 lemma (in ring_of_sets) outer_measure_le: |
|
342 assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \<subseteq> M" and X: "X \<subseteq> (\<Union>i. A i)" |
|
343 shows "outer_measure M f X \<le> (\<Sum>i. f (A i))" |
|
344 unfolding outer_measure_def |
|
345 proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) |
|
346 show dA: "range (disjointed A) \<subseteq> M" |
|
347 by (auto intro!: A range_disjointed_sets) |
|
348 have "\<forall>n. f (disjointed A n) \<le> f (A n)" |
|
349 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) |
|
350 then show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))" |
|
351 by (blast intro!: suminf_le) |
|
352 qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) |
|
353 |
|
354 lemma (in ring_of_sets) outer_measure_close: |
|
355 "outer_measure M f X < e \<Longrightarrow> \<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) < e" |
|
356 unfolding outer_measure_def INF_less_iff by auto |
|
357 |
|
358 lemma (in ring_of_sets) countably_subadditive_outer_measure: |
|
359 assumes posf: "positive M f" and inc: "increasing M f" |
|
360 shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)" |
|
361 proof (simp add: countably_subadditive_def, safe) |
|
362 fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> Pow (\<Omega>)" and sb: "(\<Union>i. A i) \<subseteq> \<Omega>" |
|
363 let ?O = "outer_measure M f" |
|
364 show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n))" |
|
365 proof (rule ennreal_le_epsilon) |
|
366 fix b and e :: real assume "0 < e" "(\<Sum>n. outer_measure M f (A n)) < top" |
|
367 then have *: "\<And>n. outer_measure M f (A n) < outer_measure M f (A n) + e * (1/2)^Suc n" |
|
368 by (auto simp add: less_top dest!: ennreal_suminf_lessD) |
|
369 obtain B |
|
370 where B: "\<And>n. range (B n) \<subseteq> M" |
|
371 and sbB: "\<And>n. A n \<subseteq> (\<Union>i. B n i)" |
|
372 and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)" |
|
373 by (metis less_imp_le outer_measure_close[OF *]) |
|
374 |
|
375 define C where "C = case_prod B o prod_decode" |
|
376 from B have B_in_M: "\<And>i j. B i j \<in> M" |
|
377 by (rule range_subsetD) |
|
378 then have C: "range C \<subseteq> M" |
|
379 by (auto simp add: C_def split_def) |
|
380 have A_C: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
|
381 using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse) |
|
382 |
|
383 have "?O (\<Union>i. A i) \<le> ?O (\<Union>i. C i)" |
|
384 using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space) |
|
385 also have "\<dots> \<le> (\<Sum>i. f (C i))" |
|
386 using C by (intro outer_measure_le[OF posf inc]) auto |
|
387 also have "\<dots> = (\<Sum>n. \<Sum>i. f (B n i))" |
|
388 using B_in_M unfolding C_def comp_def by (intro suminf_ennreal_2dimen) auto |
|
389 also have "\<dots> \<le> (\<Sum>n. ?O (A n) + e * (1/2) ^ Suc n)" |
|
390 using B_in_M by (intro suminf_le suminf_nonneg allI Ble) auto |
|
391 also have "... = (\<Sum>n. ?O (A n)) + (\<Sum>n. ennreal e * ennreal ((1/2) ^ Suc n))" |
|
392 using \<open>0 < e\<close> by (subst suminf_add[symmetric]) |
|
393 (auto simp del: ennreal_suminf_cmult simp add: ennreal_mult[symmetric]) |
|
394 also have "\<dots> = (\<Sum>n. ?O (A n)) + e" |
|
395 unfolding ennreal_suminf_cmult |
|
396 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
|
397 finally show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . |
|
398 qed |
|
399 qed |
|
400 |
|
401 lemma (in ring_of_sets) outer_measure_space_outer_measure: |
|
402 "positive M f \<Longrightarrow> increasing M f \<Longrightarrow> outer_measure_space (Pow \<Omega>) (outer_measure M f)" |
|
403 by (simp add: outer_measure_space_def |
|
404 positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) |
|
405 |
|
406 lemma (in ring_of_sets) algebra_subset_lambda_system: |
|
407 assumes posf: "positive M f" and inc: "increasing M f" |
|
408 and add: "additive M f" |
|
409 shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)" |
|
410 proof (auto dest: sets_into_space |
|
411 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
|
412 fix x s assume x: "x \<in> M" and s: "s \<subseteq> \<Omega>" |
|
413 have [simp]: "\<And>x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s - x" using s |
|
414 by blast |
|
415 have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> outer_measure M f s" |
|
416 unfolding outer_measure_def[of M f s] |
|
417 proof (safe intro!: INF_greatest) |
|
418 fix A :: "nat \<Rightarrow> 'a set" assume A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)" |
|
419 have "outer_measure M f (s \<inter> x) \<le> (\<Sum>i. f (A i \<inter> x))" |
|
420 unfolding outer_measure_def |
|
421 proof (safe intro!: INF_lower2[of "\<lambda>i. A i \<inter> x"]) |
|
422 from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)" |
|
423 by (rule disjoint_family_on_bisimulation) auto |
|
424 qed (insert x A, auto) |
|
425 moreover |
|
426 have "outer_measure M f (s - x) \<le> (\<Sum>i. f (A i - x))" |
|
427 unfolding outer_measure_def |
|
428 proof (safe intro!: INF_lower2[of "\<lambda>i. A i - x"]) |
|
429 from A(1) show "disjoint_family (\<lambda>i. A i - x)" |
|
430 by (rule disjoint_family_on_bisimulation) auto |
|
431 qed (insert x A, auto) |
|
432 ultimately have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> |
|
433 (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono) |
|
434 also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))" |
|
435 using A(2) x posf by (subst suminf_add) (auto simp: positive_def) |
|
436 also have "\<dots> = (\<Sum>i. f (A i))" |
|
437 using A x |
|
438 by (subst add[THEN additiveD, symmetric]) |
|
439 (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) |
|
440 finally show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> (\<Sum>i. f (A i))" . |
|
441 qed |
|
442 moreover |
|
443 have "outer_measure M f s \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)" |
|
444 proof - |
|
445 have "outer_measure M f s = outer_measure M f ((s \<inter> x) \<union> (s - x))" |
|
446 by (metis Un_Diff_Int Un_commute) |
|
447 also have "... \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)" |
|
448 apply (rule subadditiveD) |
|
449 apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) |
|
450 apply (simp add: positive_def outer_measure_empty[OF posf]) |
|
451 apply (rule countably_subadditive_outer_measure) |
|
452 using s by (auto intro!: posf inc) |
|
453 finally show ?thesis . |
|
454 qed |
|
455 ultimately |
|
456 show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s" |
|
457 by (rule order_antisym) |
|
458 qed |
|
459 |
|
460 lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
|
461 by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) |
|
462 |
|
463 subsection \<open>Caratheodory's theorem\<close> |
|
464 |
|
465 theorem (in ring_of_sets) caratheodory': |
|
466 assumes posf: "positive M f" and ca: "countably_additive M f" |
|
467 shows "\<exists>\<mu> :: 'a set \<Rightarrow> ennreal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" |
|
468 proof - |
|
469 have inc: "increasing M f" |
|
470 by (metis additive_increasing ca countably_additive_additive posf) |
|
471 let ?O = "outer_measure M f" |
|
472 define ls where "ls = lambda_system \<Omega> (Pow \<Omega>) ?O" |
|
473 have mls: "measure_space \<Omega> ls ?O" |
|
474 using sigma_algebra.caratheodory_lemma |
|
475 [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]] |
|
476 by (simp add: ls_def) |
|
477 hence sls: "sigma_algebra \<Omega> ls" |
|
478 by (simp add: measure_space_def) |
|
479 have "M \<subseteq> ls" |
|
480 by (simp add: ls_def) |
|
481 (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
|
482 hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls" |
|
483 using sigma_algebra.sigma_sets_subset [OF sls, of "M"] |
|
484 by simp |
|
485 have "measure_space \<Omega> (sigma_sets \<Omega> M) ?O" |
|
486 by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
|
487 (simp_all add: sgs_sb space_closed) |
|
488 thus ?thesis using outer_measure_agrees [OF posf ca] |
|
489 by (intro exI[of _ ?O]) auto |
|
490 qed |
|
491 |
|
492 lemma (in ring_of_sets) caratheodory_empty_continuous: |
|
493 assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>" |
|
494 assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0" |
|
495 shows "\<exists>\<mu> :: 'a set \<Rightarrow> ennreal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" |
|
496 proof (intro caratheodory' empty_continuous_imp_countably_additive f) |
|
497 show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto |
|
498 qed (rule cont) |
|
499 |
|
500 subsection \<open>Volumes\<close> |
|
501 |
|
502 definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
|
503 "volume M f \<longleftrightarrow> |
|
504 (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and> |
|
505 (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))" |
|
506 |
|
507 lemma volumeI: |
|
508 assumes "f {} = 0" |
|
509 assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a" |
|
510 assumes "\<And>C. C \<subseteq> M \<Longrightarrow> disjoint C \<Longrightarrow> finite C \<Longrightarrow> \<Union>C \<in> M \<Longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c)" |
|
511 shows "volume M f" |
|
512 using assms by (auto simp: volume_def) |
|
513 |
|
514 lemma volume_positive: |
|
515 "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a" |
|
516 by (auto simp: volume_def) |
|
517 |
|
518 lemma volume_empty: |
|
519 "volume M f \<Longrightarrow> f {} = 0" |
|
520 by (auto simp: volume_def) |
|
521 |
|
522 lemma volume_finite_additive: |
|
523 assumes "volume M f" |
|
524 assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M" |
|
525 shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))" |
|
526 proof - |
|
527 have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M" |
|
528 using A by (auto simp: disjoint_family_on_disjoint_image) |
|
529 with \<open>volume M f\<close> have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)" |
|
530 unfolding volume_def by blast |
|
531 also have "\<dots> = (\<Sum>i\<in>I. f (A i))" |
|
532 proof (subst setsum.reindex_nontrivial) |
|
533 fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j" |
|
534 with \<open>disjoint_family_on A I\<close> have "A i = {}" |
|
535 by (auto simp: disjoint_family_on_def) |
|
536 then show "f (A i) = 0" |
|
537 using volume_empty[OF \<open>volume M f\<close>] by simp |
|
538 qed (auto intro: \<open>finite I\<close>) |
|
539 finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))" |
|
540 by simp |
|
541 qed |
|
542 |
|
543 lemma (in ring_of_sets) volume_additiveI: |
|
544 assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" |
|
545 assumes [simp]: "\<mu> {} = 0" |
|
546 assumes add: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> \<mu> (a \<union> b) = \<mu> a + \<mu> b" |
|
547 shows "volume M \<mu>" |
|
548 proof (unfold volume_def, safe) |
|
549 fix C assume "finite C" "C \<subseteq> M" "disjoint C" |
|
550 then show "\<mu> (\<Union>C) = setsum \<mu> C" |
|
551 proof (induct C) |
|
552 case (insert c C) |
|
553 from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)" |
|
554 by (auto intro!: add simp: disjoint_def) |
|
555 with insert show ?case |
|
556 by (simp add: disjoint_def) |
|
557 qed simp |
|
558 qed fact+ |
|
559 |
|
560 lemma (in semiring_of_sets) extend_volume: |
|
561 assumes "volume M \<mu>" |
|
562 shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)" |
|
563 proof - |
|
564 let ?R = generated_ring |
|
565 have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)" |
|
566 by (auto simp: generated_ring_def) |
|
567 from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this |
|
568 |
|
569 { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" |
|
570 fix D assume D: "D \<subseteq> M" "finite D" "disjoint D" |
|
571 assume "\<Union>C = \<Union>D" |
|
572 have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))" |
|
573 proof (intro setsum.cong refl) |
|
574 fix d assume "d \<in> D" |
|
575 have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d" |
|
576 using \<open>d \<in> D\<close> \<open>\<Union>C = \<Union>D\<close> by auto |
|
577 moreover have "\<mu> (\<Union>c\<in>C. c \<inter> d) = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" |
|
578 proof (rule volume_finite_additive) |
|
579 { fix c assume "c \<in> C" then show "c \<inter> d \<in> M" |
|
580 using C D \<open>d \<in> D\<close> by auto } |
|
581 show "(\<Union>a\<in>C. a \<inter> d) \<in> M" |
|
582 unfolding Un_eq_d using \<open>d \<in> D\<close> D by auto |
|
583 show "disjoint_family_on (\<lambda>a. a \<inter> d) C" |
|
584 using \<open>disjoint C\<close> by (auto simp: disjoint_family_on_def disjoint_def) |
|
585 qed fact+ |
|
586 ultimately show "\<mu> d = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" by simp |
|
587 qed } |
|
588 note split_sum = this |
|
589 |
|
590 { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" |
|
591 fix D assume D: "D \<subseteq> M" "finite D" "disjoint D" |
|
592 assume "\<Union>C = \<Union>D" |
|
593 with split_sum[OF C D] split_sum[OF D C] |
|
594 have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)" |
|
595 by (simp, subst setsum.commute, simp add: ac_simps) } |
|
596 note sum_eq = this |
|
597 |
|
598 { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" |
|
599 then have "\<Union>C \<in> ?R" by (auto simp: generated_ring_def) |
|
600 with \<mu>'_spec[THEN bspec, of "\<Union>C"] |
|
601 obtain D where |
|
602 D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)" |
|
603 by auto |
|
604 with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp } |
|
605 note \<mu>' = this |
|
606 |
|
607 show ?thesis |
|
608 proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI) |
|
609 fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a" |
|
610 by (simp add: disjoint_def) |
|
611 next |
|
612 fix a assume "a \<in> ?R" then guess Ca .. note Ca = this |
|
613 with \<mu>'[of Ca] \<open>volume M \<mu>\<close>[THEN volume_positive] |
|
614 show "0 \<le> \<mu>' a" |
|
615 by (auto intro!: setsum_nonneg) |
|
616 next |
|
617 show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto |
|
618 next |
|
619 fix a assume "a \<in> ?R" then guess Ca .. note Ca = this |
|
620 fix b assume "b \<in> ?R" then guess Cb .. note Cb = this |
|
621 assume "a \<inter> b = {}" |
|
622 with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto |
|
623 then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto |
|
624 |
|
625 from \<open>a \<inter> b = {}\<close> have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)" |
|
626 using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union) |
|
627 also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)" |
|
628 using C_Int_cases volume_empty[OF \<open>volume M \<mu>\<close>] by (elim disjE) simp_all |
|
629 also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)" |
|
630 using Ca Cb by (simp add: setsum.union_inter) |
|
631 also have "\<dots> = \<mu>' a + \<mu>' b" |
|
632 using Ca Cb by (simp add: \<mu>') |
|
633 finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b" |
|
634 using Ca Cb by simp |
|
635 qed |
|
636 qed |
|
637 |
|
638 subsubsection \<open>Caratheodory on semirings\<close> |
|
639 |
|
640 theorem (in semiring_of_sets) caratheodory: |
|
641 assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>" |
|
642 shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ennreal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'" |
|
643 proof - |
|
644 have "volume M \<mu>" |
|
645 proof (rule volumeI) |
|
646 { fix a assume "a \<in> M" then show "0 \<le> \<mu> a" |
|
647 using pos unfolding positive_def by auto } |
|
648 note p = this |
|
649 |
|
650 fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C" |
|
651 have "\<exists>F'. bij_betw F' {..<card C} C" |
|
652 by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto |
|
653 then guess F' .. note F' = this |
|
654 then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}" |
|
655 by (auto simp: bij_betw_def) |
|
656 { fix i j assume *: "i < card C" "j < card C" "i \<noteq> j" |
|
657 with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j" |
|
658 unfolding inj_on_def by auto |
|
659 with \<open>disjoint C\<close>[THEN disjointD] |
|
660 have "F' i \<inter> F' j = {}" |
|
661 by auto } |
|
662 note F'_disj = this |
|
663 define F where "F i = (if i < card C then F' i else {})" for i |
|
664 then have "disjoint_family F" |
|
665 using F'_disj by (auto simp: disjoint_family_on_def) |
|
666 moreover from F' have "(\<Union>i. F i) = \<Union>C" |
|
667 by (auto simp add: F_def split: if_split_asm) blast |
|
668 moreover have sets_F: "\<And>i. F i \<in> M" |
|
669 using F' sets_C by (auto simp: F_def) |
|
670 moreover note sets_C |
|
671 ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))" |
|
672 using ca[unfolded countably_additive_def, THEN spec, of F] by auto |
|
673 also have "\<dots> = (\<Sum>i<card C. \<mu> (F' i))" |
|
674 proof - |
|
675 have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) sums (\<Sum>i<card C. \<mu> (F' i))" |
|
676 by (rule sums_If_finite_set) auto |
|
677 also have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) = (\<lambda>i. \<mu> (F i))" |
|
678 using pos by (auto simp: positive_def F_def) |
|
679 finally show "(\<Sum>i. \<mu> (F i)) = (\<Sum>i<card C. \<mu> (F' i))" |
|
680 by (simp add: sums_iff) |
|
681 qed |
|
682 also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)" |
|
683 using F'(2) by (subst (2) F') (simp add: setsum.reindex) |
|
684 finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" . |
|
685 next |
|
686 show "\<mu> {} = 0" |
|
687 using \<open>positive M \<mu>\<close> by (rule positiveD1) |
|
688 qed |
|
689 from extend_volume[OF this] obtain \<mu>_r where |
|
690 V: "volume generated_ring \<mu>_r" "\<And>a. a \<in> M \<Longrightarrow> \<mu> a = \<mu>_r a" |
|
691 by auto |
|
692 |
|
693 interpret G: ring_of_sets \<Omega> generated_ring |
|
694 by (rule generating_ring) |
|
695 |
|
696 have pos: "positive generated_ring \<mu>_r" |
|
697 using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty) |
|
698 |
|
699 have "countably_additive generated_ring \<mu>_r" |
|
700 proof (rule countably_additiveI) |
|
701 fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'" |
|
702 and Un_A: "(\<Union>i. A' i) \<in> generated_ring" |
|
703 |
|
704 from generated_ringE[OF Un_A] guess C' . note C' = this |
|
705 |
|
706 { fix c assume "c \<in> C'" |
|
707 moreover define A where [abs_def]: "A i = A' i \<inter> c" for i |
|
708 ultimately have A: "range A \<subseteq> generated_ring" "disjoint_family A" |
|
709 and Un_A: "(\<Union>i. A i) \<in> generated_ring" |
|
710 using A' C' |
|
711 by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def) |
|
712 from A C' \<open>c \<in> C'\<close> have UN_eq: "(\<Union>i. A i) = c" |
|
713 by (auto simp: A_def) |
|
714 |
|
715 have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)" |
|
716 (is "\<forall>i. ?P i") |
|
717 proof |
|
718 fix i |
|
719 from A have Ai: "A i \<in> generated_ring" by auto |
|
720 from generated_ringE[OF this] guess C . note C = this |
|
721 |
|
722 have "\<exists>F'. bij_betw F' {..<card C} C" |
|
723 by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto |
|
724 then guess F .. note F = this |
|
725 define f where [abs_def]: "f i = (if i < card C then F i else {})" for i |
|
726 then have f: "bij_betw f {..< card C} C" |
|
727 by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto |
|
728 with C have "\<forall>j. f j \<in> M" |
|
729 by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset) |
|
730 moreover |
|
731 from f C have d_f: "disjoint_family_on f {..<card C}" |
|
732 by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def) |
|
733 then have "disjoint_family f" |
|
734 by (auto simp: disjoint_family_on_def f_def) |
|
735 moreover |
|
736 have Ai_eq: "A i = (\<Union>x<card C. f x)" |
|
737 using f C Ai unfolding bij_betw_def by auto |
|
738 then have "\<Union>range f = A i" |
|
739 using f C Ai unfolding bij_betw_def |
|
740 by (auto simp add: f_def cong del: strong_SUP_cong) |
|
741 moreover |
|
742 { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)" |
|
743 using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def) |
|
744 also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))" |
|
745 by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp |
|
746 also have "\<dots> = \<mu>_r (A i)" |
|
747 using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq |
|
748 by (intro volume_finite_additive[OF V(1) _ d_f, symmetric]) |
|
749 (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic) |
|
750 finally have "\<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j))" .. } |
|
751 ultimately show "?P i" |
|
752 by blast |
|
753 qed |
|
754 from choice[OF this] guess f .. note f = this |
|
755 then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)" |
|
756 unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff) |
|
757 |
|
758 have d: "disjoint_family (\<lambda>i. case_prod f (prod_decode i))" |
|
759 unfolding disjoint_family_on_def |
|
760 proof (intro ballI impI) |
|
761 fix m n :: nat assume "m \<noteq> n" |
|
762 then have neq: "prod_decode m \<noteq> prod_decode n" |
|
763 using inj_prod_decode[of UNIV] by (auto simp: inj_on_def) |
|
764 show "case_prod f (prod_decode m) \<inter> case_prod f (prod_decode n) = {}" |
|
765 proof cases |
|
766 assume "fst (prod_decode m) = fst (prod_decode n)" |
|
767 then show ?thesis |
|
768 using neq f by (fastforce simp: disjoint_family_on_def) |
|
769 next |
|
770 assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)" |
|
771 have "case_prod f (prod_decode m) \<subseteq> A (fst (prod_decode m))" |
|
772 "case_prod f (prod_decode n) \<subseteq> A (fst (prod_decode n))" |
|
773 using f[THEN spec, of "fst (prod_decode m)"] |
|
774 using f[THEN spec, of "fst (prod_decode n)"] |
|
775 by (auto simp: set_eq_iff) |
|
776 with f A neq show ?thesis |
|
777 by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff) |
|
778 qed |
|
779 qed |
|
780 from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (case_prod f (prod_decode n)))" |
|
781 by (intro suminf_ennreal_2dimen[symmetric] generated_ringI_Basic) |
|
782 (auto split: prod.split) |
|
783 also have "\<dots> = (\<Sum>n. \<mu> (case_prod f (prod_decode n)))" |
|
784 using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split) |
|
785 also have "\<dots> = \<mu> (\<Union>i. case_prod f (prod_decode i))" |
|
786 using f \<open>c \<in> C'\<close> C' |
|
787 by (intro ca[unfolded countably_additive_def, rule_format]) |
|
788 (auto split: prod.split simp: UN_f_eq d UN_eq) |
|
789 finally have "(\<Sum>n. \<mu>_r (A' n \<inter> c)) = \<mu> c" |
|
790 using UN_f_eq UN_eq by (simp add: A_def) } |
|
791 note eq = this |
|
792 |
|
793 have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))" |
|
794 using C' A' |
|
795 by (subst volume_finite_additive[symmetric, OF V(1)]) |
|
796 (auto simp: disjoint_def disjoint_family_on_def |
|
797 intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext |
|
798 intro: generated_ringI_Basic) |
|
799 also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))" |
|
800 using C' A' |
|
801 by (intro suminf_setsum G.Int G.finite_Union) (auto intro: generated_ringI_Basic) |
|
802 also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)" |
|
803 using eq V C' by (auto intro!: setsum.cong) |
|
804 also have "\<dots> = \<mu>_r (\<Union>C')" |
|
805 using C' Un_A |
|
806 by (subst volume_finite_additive[symmetric, OF V(1)]) |
|
807 (auto simp: disjoint_family_on_def disjoint_def |
|
808 intro: generated_ringI_Basic) |
|
809 finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)" |
|
810 using C' by simp |
|
811 qed |
|
812 from G.caratheodory'[OF \<open>positive generated_ring \<mu>_r\<close> \<open>countably_additive generated_ring \<mu>_r\<close>] |
|
813 guess \<mu>' .. |
|
814 with V show ?thesis |
|
815 unfolding sigma_sets_generated_ring_eq |
|
816 by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic) |
|
817 qed |
|
818 |
|
819 lemma extend_measure_caratheodory: |
|
820 fixes G :: "'i \<Rightarrow> 'a set" |
|
821 assumes M: "M = extend_measure \<Omega> I G \<mu>" |
|
822 assumes "i \<in> I" |
|
823 assumes "semiring_of_sets \<Omega> (G ` I)" |
|
824 assumes empty: "\<And>i. i \<in> I \<Longrightarrow> G i = {} \<Longrightarrow> \<mu> i = 0" |
|
825 assumes inj: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> G i = G j \<Longrightarrow> \<mu> i = \<mu> j" |
|
826 assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> \<mu> i" |
|
827 assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>j. A \<in> UNIV \<rightarrow> I \<Longrightarrow> j \<in> I \<Longrightarrow> disjoint_family (G \<circ> A) \<Longrightarrow> |
|
828 (\<Union>i. G (A i)) = G j \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> j" |
|
829 shows "emeasure M (G i) = \<mu> i" |
|
830 proof - |
|
831 interpret semiring_of_sets \<Omega> "G ` I" |
|
832 by fact |
|
833 have "\<forall>g\<in>G`I. \<exists>i\<in>I. g = G i" |
|
834 by auto |
|
835 then obtain sel where sel: "\<And>g. g \<in> G ` I \<Longrightarrow> sel g \<in> I" "\<And>g. g \<in> G ` I \<Longrightarrow> G (sel g) = g" |
|
836 by metis |
|
837 |
|
838 have "\<exists>\<mu>'. (\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'" |
|
839 proof (rule caratheodory) |
|
840 show "positive (G ` I) (\<lambda>s. \<mu> (sel s))" |
|
841 by (auto simp: positive_def intro!: empty sel nonneg) |
|
842 show "countably_additive (G ` I) (\<lambda>s. \<mu> (sel s))" |
|
843 proof (rule countably_additiveI) |
|
844 fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> G ` I" "disjoint_family A" "(\<Union>i. A i) \<in> G ` I" |
|
845 then show "(\<Sum>i. \<mu> (sel (A i))) = \<mu> (sel (\<Union>i. A i))" |
|
846 by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel) |
|
847 qed |
|
848 qed |
|
849 then obtain \<mu>' where \<mu>': "\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)" "measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'" |
|
850 by metis |
|
851 |
|
852 show ?thesis |
|
853 proof (rule emeasure_extend_measure[OF M]) |
|
854 { fix i assume "i \<in> I" then show "\<mu>' (G i) = \<mu> i" |
|
855 using \<mu>' by (auto intro!: inj sel) } |
|
856 show "G ` I \<subseteq> Pow \<Omega>" |
|
857 by fact |
|
858 then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'" |
|
859 using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def) |
|
860 qed fact |
|
861 qed |
|
862 |
|
863 lemma extend_measure_caratheodory_pair: |
|
864 fixes G :: "'i \<Rightarrow> 'j \<Rightarrow> 'a set" |
|
865 assumes M: "M = extend_measure \<Omega> {(a, b). P a b} (\<lambda>(a, b). G a b) (\<lambda>(a, b). \<mu> a b)" |
|
866 assumes "P i j" |
|
867 assumes semiring: "semiring_of_sets \<Omega> {G a b | a b. P a b}" |
|
868 assumes empty: "\<And>i j. P i j \<Longrightarrow> G i j = {} \<Longrightarrow> \<mu> i j = 0" |
|
869 assumes inj: "\<And>i j k l. P i j \<Longrightarrow> P k l \<Longrightarrow> G i j = G k l \<Longrightarrow> \<mu> i j = \<mu> k l" |
|
870 assumes nonneg: "\<And>i j. P i j \<Longrightarrow> 0 \<le> \<mu> i j" |
|
871 assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>B::nat \<Rightarrow> 'j. \<And>j k. |
|
872 (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow> |
|
873 (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k" |
|
874 shows "emeasure M (G i j) = \<mu> i j" |
|
875 proof - |
|
876 have "emeasure M ((\<lambda>(a, b). G a b) (i, j)) = (\<lambda>(a, b). \<mu> a b) (i, j)" |
|
877 proof (rule extend_measure_caratheodory[OF M]) |
|
878 show "semiring_of_sets \<Omega> ((\<lambda>(a, b). G a b) ` {(a, b). P a b})" |
|
879 using semiring by (simp add: image_def conj_commute) |
|
880 next |
|
881 fix A :: "nat \<Rightarrow> ('i \<times> 'j)" and j assume "A \<in> UNIV \<rightarrow> {(a, b). P a b}" "j \<in> {(a, b). P a b}" |
|
882 "disjoint_family ((\<lambda>(a, b). G a b) \<circ> A)" |
|
883 "(\<Union>i. case A i of (a, b) \<Rightarrow> G a b) = (case j of (a, b) \<Rightarrow> G a b)" |
|
884 then show "(\<Sum>n. case A n of (a, b) \<Rightarrow> \<mu> a b) = (case j of (a, b) \<Rightarrow> \<mu> a b)" |
|
885 using add[of "\<lambda>i. fst (A i)" "\<lambda>i. snd (A i)" "fst j" "snd j"] |
|
886 by (simp add: split_beta' comp_def Pi_iff) |
|
887 qed (auto split: prod.splits intro: assms) |
|
888 then show ?thesis by simp |
|
889 qed |
|
890 |
|
891 end |
|