11 |
11 |
12 text \<open> |
12 text \<open> |
13 Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. |
13 Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. |
14 \<close> |
14 \<close> |
15 |
15 |
16 lemma%unimportant suminf_ennreal_2dimen: |
16 lemma suminf_ennreal_2dimen: |
17 fixes f:: "nat \<times> nat \<Rightarrow> ennreal" |
17 fixes f:: "nat \<times> nat \<Rightarrow> ennreal" |
18 assumes "\<And>m. g m = (\<Sum>n. f (m,n))" |
18 assumes "\<And>m. g m = (\<Sum>n. f (m,n))" |
19 shows "(\<Sum>i. f (prod_decode i)) = suminf g" |
19 shows "(\<Sum>i. f (prod_decode i)) = suminf g" |
20 proof - |
20 proof - |
21 have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))" |
21 have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))" |
58 |
58 |
59 definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set" |
59 definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set" |
60 where |
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}" |
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 |
62 |
63 lemma%unimportant (in algebra) lambda_system_eq: |
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}" |
64 "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}" |
65 proof - |
65 proof - |
66 have [simp]: "\<And>l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l" |
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) |
67 by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) |
68 show ?thesis |
68 show ?thesis |
69 by (auto simp add: lambda_system_def) (metis Int_commute)+ |
69 by (auto simp add: lambda_system_def) (metis Int_commute)+ |
70 qed |
70 qed |
71 |
71 |
72 lemma%unimportant (in algebra) lambda_system_empty: "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f" |
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) |
73 by (auto simp add: positive_def lambda_system_eq) |
74 |
74 |
75 lemma%unimportant lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M" |
75 lemma lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M" |
76 by (simp add: lambda_system_def) |
76 by (simp add: lambda_system_def) |
77 |
77 |
78 lemma%unimportant (in algebra) lambda_system_Compl: |
78 lemma (in algebra) lambda_system_Compl: |
79 fixes f:: "'a set \<Rightarrow> ennreal" |
79 fixes f:: "'a set \<Rightarrow> ennreal" |
80 assumes x: "x \<in> lambda_system \<Omega> M f" |
80 assumes x: "x \<in> lambda_system \<Omega> M f" |
81 shows "\<Omega> - x \<in> lambda_system \<Omega> M f" |
81 shows "\<Omega> - x \<in> lambda_system \<Omega> M f" |
82 proof - |
82 proof - |
83 have "x \<subseteq> \<Omega>" |
83 have "x \<subseteq> \<Omega>" |
86 by (metis double_diff equalityE) |
86 by (metis double_diff equalityE) |
87 with x show ?thesis |
87 with x show ?thesis |
88 by (force simp add: lambda_system_def ac_simps) |
88 by (force simp add: lambda_system_def ac_simps) |
89 qed |
89 qed |
90 |
90 |
91 lemma%unimportant (in algebra) lambda_system_Int: |
91 lemma (in algebra) lambda_system_Int: |
92 fixes f:: "'a set \<Rightarrow> ennreal" |
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" |
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" |
94 shows "x \<inter> y \<in> lambda_system \<Omega> M f" |
95 proof - |
95 proof - |
96 from xl yl show ?thesis |
96 from xl yl show ?thesis |
120 by (metis fy u) |
120 by (metis fy u) |
121 finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" . |
121 finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" . |
122 qed |
122 qed |
123 qed |
123 qed |
124 |
124 |
125 lemma%unimportant (in algebra) lambda_system_Un: |
125 lemma (in algebra) lambda_system_Un: |
126 fixes f:: "'a set \<Rightarrow> ennreal" |
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" |
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" |
128 shows "x \<union> y \<in> lambda_system \<Omega> M f" |
129 proof - |
129 proof - |
130 have "(\<Omega> - x) \<inter> (\<Omega> - y) \<in> M" |
130 have "(\<Omega> - x) \<inter> (\<Omega> - y) \<in> M" |
134 by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ |
134 by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ |
135 ultimately show ?thesis |
135 ultimately show ?thesis |
136 by (metis lambda_system_Compl lambda_system_Int xl yl) |
136 by (metis lambda_system_Compl lambda_system_Int xl yl) |
137 qed |
137 qed |
138 |
138 |
139 lemma%unimportant (in algebra) lambda_system_algebra: |
139 lemma (in algebra) lambda_system_algebra: |
140 "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)" |
140 "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)" |
141 apply (auto simp add: algebra_iff_Un) |
141 apply (auto simp add: algebra_iff_Un) |
142 apply (metis lambda_system_sets set_mp sets_into_space) |
142 apply (metis lambda_system_sets set_mp sets_into_space) |
143 apply (metis lambda_system_empty) |
143 apply (metis lambda_system_empty) |
144 apply (metis lambda_system_Compl) |
144 apply (metis lambda_system_Compl) |
145 apply (metis lambda_system_Un) |
145 apply (metis lambda_system_Un) |
146 done |
146 done |
147 |
147 |
148 lemma%unimportant (in algebra) lambda_system_strong_additive: |
148 lemma (in algebra) lambda_system_strong_additive: |
149 assumes z: "z \<in> M" and disj: "x \<inter> y = {}" |
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" |
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)" |
151 shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" |
152 proof - |
152 proof - |
153 have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
153 have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
158 by (metis Int Un lambda_system_sets xl yl z) |
158 by (metis Int Un lambda_system_sets xl yl z) |
159 ultimately show ?thesis using xl yl |
159 ultimately show ?thesis using xl yl |
160 by (simp add: lambda_system_eq) |
160 by (simp add: lambda_system_eq) |
161 qed |
161 qed |
162 |
162 |
163 lemma%unimportant (in algebra) lambda_system_additive: "additive (lambda_system \<Omega> M f) f" |
163 lemma (in algebra) lambda_system_additive: "additive (lambda_system \<Omega> M f) f" |
164 proof (auto simp add: additive_def) |
164 proof (auto simp add: additive_def) |
165 fix x and y |
165 fix x and y |
166 assume disj: "x \<inter> 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" |
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)+ |
168 hence "x \<in> M" "y \<in> M" by (blast intro: lambda_system_sets)+ |
169 thus "f (x \<union> y) = f x + f y" |
169 thus "f (x \<union> y) = f x + f y" |
170 using lambda_system_strong_additive [OF top disj xl yl] |
170 using lambda_system_strong_additive [OF top disj xl yl] |
171 by (simp add: Un) |
171 by (simp add: Un) |
172 qed |
172 qed |
173 |
173 |
174 lemma%unimportant lambda_system_increasing: "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f" |
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) |
175 by (simp add: increasing_def lambda_system_def) |
176 |
176 |
177 lemma%unimportant lambda_system_positive: "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f" |
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) |
178 by (simp add: positive_def lambda_system_def) |
179 |
179 |
180 lemma%unimportant (in algebra) lambda_system_strong_sum: |
180 lemma (in algebra) lambda_system_strong_sum: |
181 fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ennreal" |
181 fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ennreal" |
182 assumes f: "positive M f" and a: "a \<in> M" |
182 assumes f: "positive M f" and a: "a \<in> M" |
183 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
183 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
184 and disj: "disjoint_family A" |
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))" |
185 shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))" |
197 using A l.UNION_in_sets by simp |
197 using A l.UNION_in_sets by simp |
198 from Suc.hyps show ?case |
198 from Suc.hyps show ?case |
199 by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) |
199 by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) |
200 qed |
200 qed |
201 |
201 |
202 lemma%important (in sigma_algebra) lambda_system_caratheodory: |
202 proposition (in sigma_algebra) lambda_system_caratheodory: |
203 assumes oms: "outer_measure_space M f" |
203 assumes oms: "outer_measure_space M f" |
204 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
204 and A: "range A \<subseteq> lambda_system \<Omega> M f" |
205 and disj: "disjoint_family A" |
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)" |
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%unimportant - |
207 proof - |
208 have pos: "positive M f" and inc: "increasing M f" |
208 have pos: "positive M f" and inc: "increasing M f" |
209 and csa: "countably_subadditive M f" |
209 and csa: "countably_subadditive M f" |
210 by (metis oms outer_measure_space_def)+ |
210 by (metis oms outer_measure_space_def)+ |
211 have sa: "subadditive M f" |
211 have sa: "subadditive M f" |
212 by (metis countably_subadditive_subadditive csa pos) |
212 by (metis countably_subadditive_subadditive csa pos) |
272 qed |
272 qed |
273 thus ?thesis |
273 thus ?thesis |
274 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
274 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
275 qed |
275 qed |
276 |
276 |
277 lemma%important (in sigma_algebra) caratheodory_lemma: |
277 proposition (in sigma_algebra) caratheodory_lemma: |
278 assumes oms: "outer_measure_space M f" |
278 assumes oms: "outer_measure_space M f" |
279 defines "L \<equiv> lambda_system \<Omega> M f" |
279 defines "L \<equiv> lambda_system \<Omega> M f" |
280 shows "measure_space \<Omega> L f" |
280 shows "measure_space \<Omega> L f" |
281 proof%unimportant - |
281 proof - |
282 have pos: "positive M f" |
282 have pos: "positive M f" |
283 by (metis oms outer_measure_space_def) |
283 by (metis oms outer_measure_space_def) |
284 have alg: "algebra \<Omega> L" |
284 have alg: "algebra \<Omega> L" |
285 using lambda_system_algebra [of f, OF pos] |
285 using lambda_system_algebra [of f, OF pos] |
286 by (simp add: algebra_iff_Un L_def) |
286 by (simp add: algebra_iff_Un L_def) |
299 |
299 |
300 definition%important outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where |
300 definition%important outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where |
301 "outer_measure M f X = |
301 "outer_measure M f X = |
302 (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))" |
302 (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))" |
303 |
303 |
304 lemma%unimportant (in ring_of_sets) outer_measure_agrees: |
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" |
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" |
306 shows "outer_measure M f s = f s" |
307 unfolding outer_measure_def |
307 unfolding outer_measure_def |
308 proof (safe intro!: antisym INF_greatest) |
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)" |
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)" |
324 with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> \<Union>(A ` UNIV)}. \<Sum>i. f (A i)) \<le> f s" |
324 with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> \<Union>(A ` UNIV)}. \<Sum>i. f (A i)) \<le> f s" |
325 by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"]) |
325 by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"]) |
326 (auto simp: disjoint_family_on_def) |
326 (auto simp: disjoint_family_on_def) |
327 qed |
327 qed |
328 |
328 |
329 lemma%unimportant outer_measure_empty: |
329 lemma outer_measure_empty: |
330 "positive M f \<Longrightarrow> {} \<in> M \<Longrightarrow> outer_measure M f {} = 0" |
330 "positive M f \<Longrightarrow> {} \<in> M \<Longrightarrow> outer_measure M f {} = 0" |
331 unfolding outer_measure_def |
331 unfolding outer_measure_def |
332 by (intro antisym INF_lower2[of "\<lambda>_. {}"]) (auto simp: disjoint_family_on_def positive_def) |
332 by (intro antisym INF_lower2[of "\<lambda>_. {}"]) (auto simp: disjoint_family_on_def positive_def) |
333 |
333 |
334 lemma%unimportant (in ring_of_sets) positive_outer_measure: |
334 lemma (in ring_of_sets) positive_outer_measure: |
335 assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)" |
335 assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)" |
336 unfolding positive_def by (auto simp: assms outer_measure_empty) |
336 unfolding positive_def by (auto simp: assms outer_measure_empty) |
337 |
337 |
338 lemma%unimportant (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)" |
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) |
339 by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) |
340 |
340 |
341 lemma%unimportant (in ring_of_sets) outer_measure_le: |
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)" |
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))" |
343 shows "outer_measure M f X \<le> (\<Sum>i. f (A i))" |
344 unfolding outer_measure_def |
344 unfolding outer_measure_def |
345 proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) |
345 proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) |
346 show dA: "range (disjointed A) \<subseteq> M" |
346 show dA: "range (disjointed A) \<subseteq> M" |
349 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) |
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))" |
350 then show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))" |
351 by (blast intro!: suminf_le) |
351 by (blast intro!: suminf_le) |
352 qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) |
352 qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) |
353 |
353 |
354 lemma%unimportant (in ring_of_sets) outer_measure_close: |
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" |
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 |
356 unfolding outer_measure_def INF_less_iff by auto |
357 |
357 |
358 lemma%unimportant (in ring_of_sets) countably_subadditive_outer_measure: |
358 lemma (in ring_of_sets) countably_subadditive_outer_measure: |
359 assumes posf: "positive M f" and inc: "increasing M f" |
359 assumes posf: "positive M f" and inc: "increasing M f" |
360 shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)" |
360 shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)" |
361 proof (simp add: countably_subadditive_def, safe) |
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>" |
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" |
363 let ?O = "outer_measure M f" |
396 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
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" . |
397 finally show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . |
398 qed |
398 qed |
399 qed |
399 qed |
400 |
400 |
401 lemma%unimportant (in ring_of_sets) outer_measure_space_outer_measure: |
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)" |
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 |
403 by (simp add: outer_measure_space_def |
404 positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) |
404 positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) |
405 |
405 |
406 lemma%unimportant (in ring_of_sets) algebra_subset_lambda_system: |
406 lemma (in ring_of_sets) algebra_subset_lambda_system: |
407 assumes posf: "positive M f" and inc: "increasing M f" |
407 assumes posf: "positive M f" and inc: "increasing M f" |
408 and add: "additive M f" |
408 and add: "additive M f" |
409 shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)" |
409 shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)" |
410 proof (auto dest: sets_into_space |
410 proof (auto dest: sets_into_space |
411 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
411 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
455 ultimately |
455 ultimately |
456 show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s" |
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) |
457 by (rule order_antisym) |
458 qed |
458 qed |
459 |
459 |
460 lemma%unimportant measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
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) |
461 by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) |
462 |
462 |
463 subsection%important \<open>Caratheodory's theorem\<close> |
463 subsection%important \<open>Caratheodory's theorem\<close> |
464 |
464 |
465 theorem%important (in ring_of_sets) caratheodory': |
465 theorem (in ring_of_sets) caratheodory': |
466 assumes posf: "positive M f" and ca: "countably_additive M f" |
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>" |
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%unimportant - |
468 proof - |
469 have inc: "increasing M f" |
469 have inc: "increasing M f" |
470 by (metis additive_increasing ca countably_additive_additive posf) |
470 by (metis additive_increasing ca countably_additive_additive posf) |
471 let ?O = "outer_measure M f" |
471 let ?O = "outer_measure M f" |
472 define ls where "ls = lambda_system \<Omega> (Pow \<Omega>) ?O" |
472 define ls where "ls = lambda_system \<Omega> (Pow \<Omega>) ?O" |
473 have mls: "measure_space \<Omega> ls ?O" |
473 have mls: "measure_space \<Omega> ls ?O" |
487 (simp_all add: sgs_sb space_closed) |
487 (simp_all add: sgs_sb space_closed) |
488 thus ?thesis using outer_measure_agrees [OF posf ca] |
488 thus ?thesis using outer_measure_agrees [OF posf ca] |
489 by (intro exI[of _ ?O]) auto |
489 by (intro exI[of _ ?O]) auto |
490 qed |
490 qed |
491 |
491 |
492 lemma%important (in ring_of_sets) caratheodory_empty_continuous: |
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>" |
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" |
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>" |
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%unimportant (intro caratheodory' empty_continuous_imp_countably_additive f) |
496 proof (intro caratheodory' empty_continuous_imp_countably_additive f) |
497 show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto |
497 show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto |
498 qed (rule cont) |
498 qed (rule cont) |
499 |
499 |
500 subsection%important \<open>Volumes\<close> |
500 subsection%important \<open>Volumes\<close> |
501 |
501 |
502 definition%important volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
502 definition%important volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where |
503 "volume M f \<longleftrightarrow> |
503 "volume M f \<longleftrightarrow> |
504 (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and> |
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))" |
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 |
506 |
507 lemma%unimportant volumeI: |
507 lemma volumeI: |
508 assumes "f {} = 0" |
508 assumes "f {} = 0" |
509 assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a" |
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)" |
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" |
511 shows "volume M f" |
512 using assms by (auto simp: volume_def) |
512 using assms by (auto simp: volume_def) |
513 |
513 |
514 lemma%unimportant volume_positive: |
514 lemma volume_positive: |
515 "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a" |
515 "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a" |
516 by (auto simp: volume_def) |
516 by (auto simp: volume_def) |
517 |
517 |
518 lemma%unimportant volume_empty: |
518 lemma volume_empty: |
519 "volume M f \<Longrightarrow> f {} = 0" |
519 "volume M f \<Longrightarrow> f {} = 0" |
520 by (auto simp: volume_def) |
520 by (auto simp: volume_def) |
521 |
521 |
522 lemma%unimportant volume_finite_additive: |
522 proposition volume_finite_additive: |
523 assumes "volume M f" |
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>(A ` I) \<in> M" |
524 assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "\<Union>(A ` I) \<in> M" |
525 shows "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))" |
525 shows "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))" |
526 proof - |
526 proof - |
527 have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M" |
527 have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M" |
538 qed (auto intro: \<open>finite I\<close>) |
538 qed (auto intro: \<open>finite I\<close>) |
539 finally show "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))" |
539 finally show "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))" |
540 by simp |
540 by simp |
541 qed |
541 qed |
542 |
542 |
543 lemma%unimportant (in ring_of_sets) volume_additiveI: |
543 lemma (in ring_of_sets) volume_additiveI: |
544 assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" |
544 assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" |
545 assumes [simp]: "\<mu> {} = 0" |
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" |
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>" |
547 shows "volume M \<mu>" |
548 proof (unfold volume_def, safe) |
548 proof (unfold volume_def, safe) |
555 with insert show ?case |
555 with insert show ?case |
556 by (simp add: disjoint_def) |
556 by (simp add: disjoint_def) |
557 qed simp |
557 qed simp |
558 qed fact+ |
558 qed fact+ |
559 |
559 |
560 lemma%important (in semiring_of_sets) extend_volume: |
560 proposition (in semiring_of_sets) extend_volume: |
561 assumes "volume M \<mu>" |
561 assumes "volume M \<mu>" |
562 shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)" |
562 shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)" |
563 proof%unimportant - |
563 proof - |
564 let ?R = generated_ring |
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)" |
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) |
566 by (auto simp: generated_ring_def) |
567 from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this |
567 from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this |
568 |
568 |
635 qed |
635 qed |
636 qed |
636 qed |
637 |
637 |
638 subsubsection%important \<open>Caratheodory on semirings\<close> |
638 subsubsection%important \<open>Caratheodory on semirings\<close> |
639 |
639 |
640 theorem%important (in semiring_of_sets) caratheodory: |
640 theorem (in semiring_of_sets) caratheodory: |
641 assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>" |
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>'" |
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%unimportant - |
643 proof - |
644 have "volume M \<mu>" |
644 have "volume M \<mu>" |
645 proof (rule volumeI) |
645 proof (rule volumeI) |
646 { fix a assume "a \<in> M" then show "0 \<le> \<mu> a" |
646 { fix a assume "a \<in> M" then show "0 \<le> \<mu> a" |
647 using pos unfolding positive_def by auto } |
647 using pos unfolding positive_def by auto } |
648 note p = this |
648 note p = this |
814 with V show ?thesis |
814 with V show ?thesis |
815 unfolding sigma_sets_generated_ring_eq |
815 unfolding sigma_sets_generated_ring_eq |
816 by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic) |
816 by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic) |
817 qed |
817 qed |
818 |
818 |
819 lemma%important extend_measure_caratheodory: |
819 lemma extend_measure_caratheodory: |
820 fixes G :: "'i \<Rightarrow> 'a set" |
820 fixes G :: "'i \<Rightarrow> 'a set" |
821 assumes M: "M = extend_measure \<Omega> I G \<mu>" |
821 assumes M: "M = extend_measure \<Omega> I G \<mu>" |
822 assumes "i \<in> I" |
822 assumes "i \<in> I" |
823 assumes "semiring_of_sets \<Omega> (G ` I)" |
823 assumes "semiring_of_sets \<Omega> (G ` I)" |
824 assumes empty: "\<And>i. i \<in> I \<Longrightarrow> G i = {} \<Longrightarrow> \<mu> i = 0" |
824 assumes empty: "\<And>i. i \<in> I \<Longrightarrow> G i = {} \<Longrightarrow> \<mu> i = 0" |
826 assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> \<mu> i" |
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> |
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" |
828 (\<Union>i. G (A i)) = G j \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> j" |
829 shows "emeasure M (G i) = \<mu> i" |
829 shows "emeasure M (G i) = \<mu> i" |
830 |
830 |
831 proof%unimportant - |
831 proof - |
832 interpret semiring_of_sets \<Omega> "G ` I" |
832 interpret semiring_of_sets \<Omega> "G ` I" |
833 by fact |
833 by fact |
834 have "\<forall>g\<in>G`I. \<exists>i\<in>I. g = G i" |
834 have "\<forall>g\<in>G`I. \<exists>i\<in>I. g = G i" |
835 by auto |
835 by auto |
836 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 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" |
859 then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'" |
859 then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'" |
860 using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def) |
860 using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def) |
861 qed fact |
861 qed fact |
862 qed |
862 qed |
863 |
863 |
864 lemma%important extend_measure_caratheodory_pair: |
864 proposition extend_measure_caratheodory_pair: |
865 fixes G :: "'i \<Rightarrow> 'j \<Rightarrow> 'a set" |
865 fixes G :: "'i \<Rightarrow> 'j \<Rightarrow> 'a set" |
866 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 M: "M = extend_measure \<Omega> {(a, b). P a b} (\<lambda>(a, b). G a b) (\<lambda>(a, b). \<mu> a b)" |
867 assumes "P i j" |
867 assumes "P i j" |
868 assumes semiring: "semiring_of_sets \<Omega> {G a b | a b. P a b}" |
868 assumes semiring: "semiring_of_sets \<Omega> {G a b | a b. P a b}" |
869 assumes empty: "\<And>i j. P i j \<Longrightarrow> G i j = {} \<Longrightarrow> \<mu> i j = 0" |
869 assumes empty: "\<And>i j. P i j \<Longrightarrow> G i j = {} \<Longrightarrow> \<mu> i j = 0" |
871 assumes nonneg: "\<And>i j. P i j \<Longrightarrow> 0 \<le> \<mu> i j" |
871 assumes nonneg: "\<And>i j. P i j \<Longrightarrow> 0 \<le> \<mu> i j" |
872 assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>B::nat \<Rightarrow> 'j. \<And>j k. |
872 assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>B::nat \<Rightarrow> 'j. \<And>j k. |
873 (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow> |
873 (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow> |
874 (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k" |
874 (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k" |
875 shows "emeasure M (G i j) = \<mu> i j" |
875 shows "emeasure M (G i j) = \<mu> i j" |
876 proof%unimportant - |
876 proof - |
877 have "emeasure M ((\<lambda>(a, b). G a b) (i, j)) = (\<lambda>(a, b). \<mu> a b) (i, j)" |
877 have "emeasure M ((\<lambda>(a, b). G a b) (i, j)) = (\<lambda>(a, b). \<mu> a b) (i, j)" |
878 proof (rule extend_measure_caratheodory[OF M]) |
878 proof (rule extend_measure_caratheodory[OF M]) |
879 show "semiring_of_sets \<Omega> ((\<lambda>(a, b). G a b) ` {(a, b). P a b})" |
879 show "semiring_of_sets \<Omega> ((\<lambda>(a, b). G a b) ` {(a, b). P a b})" |
880 using semiring by (simp add: image_def conj_commute) |
880 using semiring by (simp add: image_def conj_commute) |
881 next |
881 next |