211 moreover |
178 moreover |
212 have "u - x \<inter> y - y = u - y" by blast |
179 have "u - x \<inter> y - y = u - y" by blast |
213 ultimately |
180 ultimately |
214 have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy |
181 have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy |
215 by force |
182 by force |
216 have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) |
183 have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) |
217 = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)" |
184 = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)" |
218 by (simp add: ey) |
185 by (simp add: ey ac_simps) |
219 also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)" |
186 also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)" |
220 by (simp add: Int_ac) |
187 by (simp add: Int_ac) |
221 also have "... = f (u \<inter> y) + f (u - y)" |
188 also have "... = f (u \<inter> y) + f (u - y)" |
222 using fx [THEN bspec, of "u \<inter> y"] Int y u |
189 using fx [THEN bspec, of "u \<inter> y"] Int y u |
223 by force |
190 by force |
224 also have "... = f u" |
191 also have "... = f u" |
225 by (metis fy u) |
192 by (metis fy u) |
226 finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" . |
193 finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" . |
227 qed |
194 qed |
228 qed |
195 qed |
229 |
196 |
230 |
197 |
231 lemma (in algebra) lambda_system_Un: |
198 lemma (in algebra) lambda_system_Un: |
232 fixes f:: "'a set \<Rightarrow> real" |
199 fixes f:: "'a set \<Rightarrow> pinfreal" |
233 assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
200 assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
234 shows "x \<union> y \<in> lambda_system M f" |
201 shows "x \<union> y \<in> lambda_system M f" |
235 proof - |
202 proof - |
236 have "(space M - x) \<inter> (space M - y) \<in> sets M" |
203 have "(space M - x) \<inter> (space M - y) \<in> sets M" |
237 by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) |
204 by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) |
238 moreover |
205 moreover |
239 have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))" |
206 have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))" |
240 by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ |
207 by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ |
241 ultimately show ?thesis |
208 ultimately show ?thesis |
242 by (metis lambda_system_Compl lambda_system_Int xl yl) |
209 by (metis lambda_system_Compl lambda_system_Int xl yl) |
243 qed |
210 qed |
244 |
211 |
245 lemma (in algebra) lambda_system_algebra: |
212 lemma (in algebra) lambda_system_algebra: |
246 "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))" |
213 "positive f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))" |
247 apply (auto simp add: algebra_def) |
214 apply (auto simp add: algebra_def) |
248 apply (metis lambda_system_sets set_mp sets_into_space) |
215 apply (metis lambda_system_sets set_mp sets_into_space) |
249 apply (metis lambda_system_empty) |
216 apply (metis lambda_system_empty) |
250 apply (metis lambda_system_Compl) |
217 apply (metis lambda_system_Compl) |
251 apply (metis lambda_system_Un) |
218 apply (metis lambda_system_Un) |
252 done |
219 done |
253 |
220 |
254 lemma (in algebra) lambda_system_strong_additive: |
221 lemma (in algebra) lambda_system_strong_additive: |
255 assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}" |
222 assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}" |
256 and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
223 and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
257 shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" |
224 shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" |
258 proof - |
225 proof - |
259 have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
226 have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
260 moreover |
227 moreover |
261 have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast |
228 have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast |
262 moreover |
229 moreover |
263 have "(z \<inter> (x \<union> y)) \<in> sets M" |
230 have "(z \<inter> (x \<union> y)) \<in> sets M" |
264 by (metis Int Un lambda_system_sets xl yl z) |
231 by (metis Int Un lambda_system_sets xl yl z) |
265 ultimately show ?thesis using xl yl |
232 ultimately show ?thesis using xl yl |
266 by (simp add: lambda_system_eq) |
233 by (simp add: lambda_system_eq) |
267 qed |
234 qed |
268 |
|
269 lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x" |
|
270 by (metis Int_absorb1 sets_into_space) |
|
271 |
|
272 lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x" |
|
273 by (metis Int_absorb2 sets_into_space) |
|
274 |
235 |
275 lemma (in algebra) lambda_system_additive: |
236 lemma (in algebra) lambda_system_additive: |
276 "additive (M (|sets := lambda_system M f|)) f" |
237 "additive (M (|sets := lambda_system M f|)) f" |
277 proof (auto simp add: additive_def) |
238 proof (auto simp add: additive_def) |
278 fix x and y |
239 fix x and y |
279 assume disj: "x \<inter> y = {}" |
240 assume disj: "x \<inter> y = {}" |
280 and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
241 and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" |
281 hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+ |
242 hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+ |
282 thus "f (x \<union> y) = f x + f y" |
243 thus "f (x \<union> y) = f x + f y" |
283 using lambda_system_strong_additive [OF top disj xl yl] |
244 using lambda_system_strong_additive [OF top disj xl yl] |
284 by (simp add: Un) |
245 by (simp add: Un) |
285 qed |
246 qed |
286 |
247 |
287 |
248 |
288 lemma (in algebra) countably_subadditive_subadditive: |
249 lemma (in algebra) countably_subadditive_subadditive: |
289 assumes f: "positive M f" and cs: "countably_subadditive M f" |
250 assumes f: "positive f" and cs: "countably_subadditive M f" |
290 shows "subadditive M f" |
251 shows "subadditive M f" |
291 proof (auto simp add: subadditive_def) |
252 proof (auto simp add: subadditive_def) |
292 fix x y |
253 fix x y |
293 assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" |
254 assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" |
294 hence "disjoint_family (binaryset x y)" |
255 hence "disjoint_family (binaryset x y)" |
295 by (auto simp add: disjoint_family_on_def binaryset_def) |
256 by (auto simp add: disjoint_family_on_def binaryset_def) |
296 hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
257 hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
297 (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
258 (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
298 summable (f o (binaryset x y)) \<longrightarrow> |
259 f (\<Union>i. binaryset x y i) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" |
299 f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))" |
|
300 using cs by (simp add: countably_subadditive_def) |
260 using cs by (simp add: countably_subadditive_def) |
301 hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
261 hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
302 summable (f o (binaryset x y)) \<longrightarrow> |
262 f (x \<union> y) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" |
303 f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))" |
|
304 by (simp add: range_binaryset_eq UN_binaryset_eq) |
263 by (simp add: range_binaryset_eq UN_binaryset_eq) |
305 thus "f (x \<union> y) \<le> f x + f y" using f x y binaryset_sums |
264 thus "f (x \<union> y) \<le> f x + f y" using f x y |
306 by (auto simp add: Un sums_iff positive_def o_def) |
265 by (auto simp add: Un o_def binaryset_psuminf positive_def) |
307 qed |
266 qed |
308 |
267 |
309 |
268 lemma (in algebra) additive_sum: |
310 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set " |
269 fixes A:: "nat \<Rightarrow> 'a set" |
311 where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)" |
270 assumes f: "positive f" and ad: "additive M f" |
312 |
271 and A: "range A \<subseteq> sets M" |
313 lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" |
272 and disj: "disjoint_family A" |
|
273 shows "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" |
314 proof (induct n) |
274 proof (induct n) |
315 case 0 show ?case by simp |
275 case 0 show ?case using f by (simp add: positive_def) |
316 next |
276 next |
317 case (Suc n) |
277 case (Suc n) |
318 thus ?case by (simp add: atLeastLessThanSuc disjointed_def) |
278 have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj |
319 qed |
|
320 |
|
321 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" |
|
322 apply (rule UN_finite2_eq [where k=0]) |
|
323 apply (simp add: finite_UN_disjointed_eq) |
|
324 done |
|
325 |
|
326 lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" |
|
327 by (auto simp add: disjointed_def) |
|
328 |
|
329 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" |
|
330 by (simp add: disjoint_family_on_def) |
|
331 (metis neq_iff Int_commute less_disjoint_disjointed) |
|
332 |
|
333 lemma disjointed_subset: "disjointed A n \<subseteq> A n" |
|
334 by (auto simp add: disjointed_def) |
|
335 |
|
336 |
|
337 lemma (in algebra) UNION_in_sets: |
|
338 fixes A:: "nat \<Rightarrow> 'a set" |
|
339 assumes A: "range A \<subseteq> sets M " |
|
340 shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
|
341 proof (induct n) |
|
342 case 0 show ?case by simp |
|
343 next |
|
344 case (Suc n) |
|
345 thus ?case |
|
346 by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) |
|
347 qed |
|
348 |
|
349 lemma (in algebra) range_disjointed_sets: |
|
350 assumes A: "range A \<subseteq> sets M " |
|
351 shows "range (disjointed A) \<subseteq> sets M" |
|
352 proof (auto simp add: disjointed_def) |
|
353 fix n |
|
354 show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets |
|
355 by (metis A Diff UNIV_I image_subset_iff) |
|
356 qed |
|
357 |
|
358 lemma sigma_algebra_disjoint_iff: |
|
359 "sigma_algebra M \<longleftrightarrow> |
|
360 algebra M & |
|
361 (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> |
|
362 (\<Union>i::nat. A i) \<in> sets M)" |
|
363 proof (auto simp add: sigma_algebra_iff) |
|
364 fix A :: "nat \<Rightarrow> 'a set" |
|
365 assume M: "algebra M" |
|
366 and A: "range A \<subseteq> sets M" |
|
367 and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> |
|
368 disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M" |
|
369 hence "range (disjointed A) \<subseteq> sets M \<longrightarrow> |
|
370 disjoint_family (disjointed A) \<longrightarrow> |
|
371 (\<Union>i. disjointed A i) \<in> sets M" by blast |
|
372 hence "(\<Union>i. disjointed A i) \<in> sets M" |
|
373 by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) |
|
374 thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq) |
|
375 qed |
|
376 |
|
377 |
|
378 lemma (in algebra) additive_sum: |
|
379 fixes A:: "nat \<Rightarrow> 'a set" |
|
380 assumes f: "positive M f" and ad: "additive M f" |
|
381 and A: "range A \<subseteq> sets M" |
|
382 and disj: "disjoint_family A" |
|
383 shows "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" |
|
384 proof (induct n) |
|
385 case 0 show ?case using f by (simp add: positive_def) |
|
386 next |
|
387 case (Suc n) |
|
388 have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj |
|
389 by (auto simp add: disjoint_family_on_def neq_iff) blast |
279 by (auto simp add: disjoint_family_on_def neq_iff) blast |
390 moreover |
280 moreover |
391 have "A n \<in> sets M" using A by blast |
281 have "A n \<in> sets M" using A by blast |
392 moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
282 moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
393 by (metis A UNION_in_sets atLeast0LessThan) |
283 by (metis A UNION_in_sets atLeast0LessThan) |
394 moreover |
284 moreover |
395 ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)" |
285 ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)" |
396 using ad UNION_in_sets A by (auto simp add: additive_def) |
286 using ad UNION_in_sets A by (auto simp add: additive_def) |
397 with Suc.hyps show ?case using ad |
287 with Suc.hyps show ?case using ad |
398 by (auto simp add: atLeastLessThanSuc additive_def) |
288 by (auto simp add: atLeastLessThanSuc additive_def) |
399 qed |
289 qed |
400 |
290 |
401 |
291 |
402 lemma countably_subadditiveD: |
292 lemma countably_subadditiveD: |
403 "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> |
293 "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> |
404 (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)" |
294 (\<Union>i. A i) \<in> sets M \<Longrightarrow> f (\<Union>i. A i) \<le> psuminf (f o A)" |
405 by (auto simp add: countably_subadditive_def o_def) |
295 by (auto simp add: countably_subadditive_def o_def) |
406 |
296 |
407 lemma (in algebra) increasing_additive_summable: |
297 lemma (in algebra) increasing_additive_bound: |
408 fixes A:: "nat \<Rightarrow> 'a set" |
298 fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal" |
409 assumes f: "positive M f" and ad: "additive M f" |
299 assumes f: "positive f" and ad: "additive M f" |
410 and inc: "increasing M f" |
300 and inc: "increasing M f" |
411 and A: "range A \<subseteq> sets M" |
301 and A: "range A \<subseteq> sets M" |
412 and disj: "disjoint_family A" |
302 and disj: "disjoint_family A" |
413 shows "summable (f o A)" |
303 shows "psuminf (f \<circ> A) \<le> f (space M)" |
414 proof (rule pos_summable) |
304 proof (safe intro!: psuminf_bound) |
415 fix n |
305 fix N |
416 show "0 \<le> (f \<circ> A) n" using f A |
306 have "setsum (f \<circ> A) {0..<N} = f (\<Union>i\<in>{0..<N}. A i)" |
417 by (force simp add: positive_def) |
307 by (rule additive_sum [OF f ad A disj]) |
418 next |
|
419 fix n |
|
420 have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" |
|
421 by (rule additive_sum [OF f ad A disj]) |
|
422 also have "... \<le> f (space M)" using space_closed A |
308 also have "... \<le> f (space M)" using space_closed A |
423 by (blast intro: increasingD [OF inc] UNION_in_sets top) |
309 by (blast intro: increasingD [OF inc] UNION_in_sets top) |
424 finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" . |
310 finally show "setsum (f \<circ> A) {..<N} \<le> f (space M)" by (simp add: atLeast0LessThan) |
425 qed |
311 qed |
426 |
|
427 lemma lambda_system_positive: |
|
428 "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f" |
|
429 by (simp add: positive_def lambda_system_def) |
|
430 |
312 |
431 lemma lambda_system_increasing: |
313 lemma lambda_system_increasing: |
432 "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f" |
314 "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f" |
433 by (simp add: increasing_def lambda_system_def) |
315 by (simp add: increasing_def lambda_system_def) |
434 |
316 |
435 lemma (in algebra) lambda_system_strong_sum: |
317 lemma (in algebra) lambda_system_strong_sum: |
436 fixes A:: "nat \<Rightarrow> 'a set" |
318 fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal" |
437 assumes f: "positive M f" and a: "a \<in> sets M" |
319 assumes f: "positive f" and a: "a \<in> sets M" |
438 and A: "range A \<subseteq> lambda_system M f" |
320 and A: "range A \<subseteq> lambda_system M f" |
439 and disj: "disjoint_family A" |
321 and disj: "disjoint_family A" |
440 shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))" |
322 shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))" |
441 proof (induct n) |
323 proof (induct n) |
442 case 0 show ?case using f by (simp add: positive_def) |
324 case 0 show ?case using f by (simp add: positive_def) |
443 next |
325 next |
444 case (Suc n) |
326 case (Suc n) |
445 have 2: "A n \<inter> UNION {0..<n} A = {}" using disj |
327 have 2: "A n \<inter> UNION {0..<n} A = {}" using disj |
446 by (force simp add: disjoint_family_on_def neq_iff) |
328 by (force simp add: disjoint_family_on_def neq_iff) |
447 have 3: "A n \<in> lambda_system M f" using A |
329 have 3: "A n \<in> lambda_system M f" using A |
448 by blast |
330 by blast |
449 have 4: "UNION {0..<n} A \<in> lambda_system M f" |
331 have 4: "UNION {0..<n} A \<in> lambda_system M f" |
450 using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] |
332 using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f] |
451 by simp |
333 by simp |
452 from Suc.hyps show ?case |
334 from Suc.hyps show ?case |
453 by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) |
335 by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) |
454 qed |
336 qed |
455 |
337 |
456 |
338 |
457 lemma (in sigma_algebra) lambda_system_caratheodory: |
339 lemma (in sigma_algebra) lambda_system_caratheodory: |
458 assumes oms: "outer_measure_space M f" |
340 assumes oms: "outer_measure_space M f" |
459 and A: "range A \<subseteq> lambda_system M f" |
341 and A: "range A \<subseteq> lambda_system M f" |
460 and disj: "disjoint_family A" |
342 and disj: "disjoint_family A" |
461 shows "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A) sums f (\<Union>i. A i)" |
343 shows "(\<Union>i. A i) \<in> lambda_system M f \<and> psuminf (f \<circ> A) = f (\<Union>i. A i)" |
462 proof - |
344 proof - |
463 have pos: "positive M f" and inc: "increasing M f" |
345 have pos: "positive f" and inc: "increasing M f" |
464 and csa: "countably_subadditive M f" |
346 and csa: "countably_subadditive M f" |
465 by (metis oms outer_measure_space_def)+ |
347 by (metis oms outer_measure_space_def)+ |
466 have sa: "subadditive M f" |
348 have sa: "subadditive M f" |
467 by (metis countably_subadditive_subadditive csa pos) |
349 by (metis countably_subadditive_subadditive csa pos) |
468 have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A |
350 have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A |
469 by simp |
351 by simp |
470 have alg_ls: "algebra (M(|sets := lambda_system M f|))" |
352 have alg_ls: "algebra (M(|sets := lambda_system M f|))" |
471 by (rule lambda_system_algebra [OF pos]) |
353 by (rule lambda_system_algebra) (rule pos) |
472 have A'': "range A \<subseteq> sets M" |
354 have A'': "range A \<subseteq> sets M" |
473 by (metis A image_subset_iff lambda_system_sets) |
355 by (metis A image_subset_iff lambda_system_sets) |
474 have sumfA: "summable (f \<circ> A)" |
356 |
475 by (metis algebra.increasing_additive_summable [OF alg_ls] |
|
476 lambda_system_positive lambda_system_additive lambda_system_increasing |
|
477 A' oms outer_measure_space_def disj) |
|
478 have U_in: "(\<Union>i. A i) \<in> sets M" |
357 have U_in: "(\<Union>i. A i) \<in> sets M" |
479 by (metis A'' countable_UN) |
358 by (metis A'' countable_UN) |
480 have U_eq: "f (\<Union>i. A i) = suminf (f o A)" |
359 have U_eq: "f (\<Union>i. A i) = psuminf (f o A)" |
481 proof (rule antisym) |
360 proof (rule antisym) |
482 show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)" |
361 show "f (\<Union>i. A i) \<le> psuminf (f \<circ> A)" |
483 by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) |
362 by (rule countably_subadditiveD [OF csa A'' disj U_in]) |
484 show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)" |
363 show "psuminf (f \<circ> A) \<le> f (\<Union>i. A i)" |
485 by (rule suminf_le [OF sumfA]) |
364 by (rule psuminf_bound, unfold atLeast0LessThan[symmetric]) |
486 (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right |
365 (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right |
487 lambda_system_positive lambda_system_additive |
366 lambda_system_additive subset_Un_eq increasingD [OF inc] |
488 subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) |
367 A' A'' UNION_in_sets U_in) |
489 qed |
368 qed |
490 { |
369 { |
491 fix a |
370 fix a |
492 assume a [iff]: "a \<in> sets M" |
371 assume a [iff]: "a \<in> sets M" |
493 have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a" |
372 have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a" |
494 proof - |
373 proof - |
495 have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' |
|
496 apply - |
|
497 apply (rule summable_comparison_test [OF _ sumfA]) |
|
498 apply (rule_tac x="0" in exI) |
|
499 apply (simp add: positive_def) |
|
500 apply (auto simp add: ) |
|
501 apply (subst abs_of_nonneg) |
|
502 apply (metis A'' Int UNIV_I a image_subset_iff) |
|
503 apply (blast intro: increasingD [OF inc]) |
|
504 done |
|
505 show ?thesis |
374 show ?thesis |
506 proof (rule antisym) |
375 proof (rule antisym) |
507 have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A'' |
376 have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A'' |
508 by blast |
377 by blast |
509 moreover |
378 moreover |
510 have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
379 have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
511 by (auto simp add: disjoint_family_on_def) |
380 by (auto simp add: disjoint_family_on_def) |
512 moreover |
381 moreover |
513 have "a \<inter> (\<Union>i. A i) \<in> sets M" |
382 have "a \<inter> (\<Union>i. A i) \<in> sets M" |
514 by (metis Int U_in a) |
383 by (metis Int U_in a) |
515 ultimately |
384 ultimately |
516 have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" |
385 have "f (a \<inter> (\<Union>i. A i)) \<le> psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" |
517 using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ |
386 using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] |
518 by (simp add: o_def) |
387 by (simp add: o_def) |
519 moreover |
388 hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> |
520 have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) \<le> f a - f (a - (\<Union>i. A i))" |
389 psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i))" |
521 proof (rule suminf_le [OF summ]) |
390 by (rule add_right_mono) |
|
391 moreover |
|
392 have "psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i)) \<le> f a" |
|
393 proof (safe intro!: psuminf_bound_add) |
522 fix n |
394 fix n |
523 have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
395 have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
524 by (metis A'' UNION_in_sets) |
396 by (metis A'' UNION_in_sets) |
525 have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
397 have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
526 by (blast intro: increasingD [OF inc] A'' UNION_in_sets) |
398 by (blast intro: increasingD [OF inc] A'' UNION_in_sets) |
527 have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f" |
399 have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f" |
528 using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]] |
400 using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]] |
529 by (simp add: A) |
401 by (simp add: A) |
530 hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a" |
402 hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))" |
531 by (simp add: lambda_system_eq UNION_in) |
403 by (simp add: lambda_system_eq UNION_in) |
532 have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
404 have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
533 by (blast intro: increasingD [OF inc] UNION_eq_Union_image |
405 by (blast intro: increasingD [OF inc] UNION_eq_Union_image |
534 UNION_in U_in) |
406 UNION_in U_in) |
535 thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))" |
407 thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {..<n} + f (a - (\<Union>i. A i)) \<le> f a" |
536 using eq_fa |
408 by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) |
537 by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos |
|
538 a A disj) |
|
539 qed |
409 qed |
540 ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
410 ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
541 by arith |
411 by (rule order_trans) |
542 next |
412 next |
543 have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
413 have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
544 by (blast intro: increasingD [OF inc] U_in) |
414 by (blast intro: increasingD [OF inc] U_in) |
545 also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
415 also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
546 by (blast intro: subadditiveD [OF sa] U_in) |
416 by (blast intro: subadditiveD [OF sa] U_in) |
547 finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" . |
417 finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" . |
548 qed |
418 qed |
549 qed |
419 qed |
550 } |
420 } |
551 thus ?thesis |
421 thus ?thesis |
552 by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA) |
422 by (simp add: lambda_system_eq sums_iff U_eq U_in) |
553 qed |
423 qed |
554 |
424 |
555 lemma (in sigma_algebra) caratheodory_lemma: |
425 lemma (in sigma_algebra) caratheodory_lemma: |
556 assumes oms: "outer_measure_space M f" |
426 assumes oms: "outer_measure_space M f" |
557 shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)" |
427 shows "measure_space (|space = space M, sets = lambda_system M f|) f" |
558 proof - |
428 proof - |
559 have pos: "positive M f" |
429 have pos: "positive f" |
560 by (metis oms outer_measure_space_def) |
430 by (metis oms outer_measure_space_def) |
561 have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)" |
431 have alg: "algebra (|space = space M, sets = lambda_system M f|)" |
562 using lambda_system_algebra [OF pos] |
432 using lambda_system_algebra [of f, OF pos] |
563 by (simp add: algebra_def) |
433 by (simp add: algebra_def) |
564 then moreover |
434 then moreover |
565 have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)" |
435 have "sigma_algebra (|space = space M, sets = lambda_system M f|)" |
566 using lambda_system_caratheodory [OF oms] |
436 using lambda_system_caratheodory [OF oms] |
567 by (simp add: sigma_algebra_disjoint_iff) |
437 by (simp add: sigma_algebra_disjoint_iff) |
568 moreover |
438 moreover |
569 have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" |
439 have "measure_space_axioms (|space = space M, sets = lambda_system M f|) f" |
570 using pos lambda_system_caratheodory [OF oms] |
440 using pos lambda_system_caratheodory [OF oms] |
571 by (simp add: measure_space_axioms_def positive_def lambda_system_sets |
441 by (simp add: measure_space_axioms_def positive_def lambda_system_sets |
572 countably_additive_def o_def) |
442 countably_additive_def o_def) |
573 ultimately |
443 ultimately |
574 show ?thesis |
444 show ?thesis |
575 by intro_locales (auto simp add: sigma_algebra_def) |
445 by intro_locales (auto simp add: sigma_algebra_def) |
576 qed |
446 qed |
577 |
447 |
578 |
448 |
579 lemma (in algebra) inf_measure_nonempty: |
449 lemma (in algebra) inf_measure_nonempty: |
580 assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b" |
450 assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b" |
581 shows "f b \<in> measure_set M f a" |
451 shows "f b \<in> measure_set M f a" |
582 proof - |
452 proof - |
583 have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}" |
453 have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}" |
584 by (rule series_zero) (simp add: positive_imp_0 [OF f]) |
454 by (rule psuminf_finite) (simp add: f[unfolded positive_def]) |
585 also have "... = f b" |
455 also have "... = f b" |
586 by simp |
456 by simp |
587 finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" . |
457 finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" . |
588 thus ?thesis using a |
458 thus ?thesis using a b |
589 by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] |
459 by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] |
590 simp add: measure_set_def disjoint_family_on_def b split_if_mem2) |
460 simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) |
591 qed |
461 qed |
592 |
|
593 lemma (in algebra) inf_measure_pos0: |
|
594 "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x" |
|
595 apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero) |
|
596 apply blast |
|
597 done |
|
598 |
|
599 lemma (in algebra) inf_measure_pos: |
|
600 shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)" |
|
601 apply (rule Inf_greatest) |
|
602 apply (metis emptyE inf_measure_nonempty top) |
|
603 apply (metis inf_measure_pos0) |
|
604 done |
|
605 |
462 |
606 lemma (in algebra) additive_increasing: |
463 lemma (in algebra) additive_increasing: |
607 assumes posf: "positive M f" and addf: "additive M f" |
464 assumes posf: "positive f" and addf: "additive M f" |
608 shows "increasing M f" |
465 shows "increasing M f" |
609 proof (auto simp add: increasing_def) |
466 proof (auto simp add: increasing_def) |
610 fix x y |
467 fix x y |
611 assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y" |
468 assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y" |
612 have "f x \<le> f x + f (y-x)" using posf |
469 have "f x \<le> f x + f (y-x)" .. |
613 by (simp add: positive_def) (metis Diff xy(1,2)) |
|
614 also have "... = f (x \<union> (y-x))" using addf |
470 also have "... = f (x \<union> (y-x))" using addf |
615 by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) |
471 by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) |
616 also have "... = f y" |
472 also have "... = f y" |
617 by (metis Un_Diff_cancel Un_absorb1 xy(3)) |
473 by (metis Un_Diff_cancel Un_absorb1 xy(3)) |
618 finally show "f x \<le> f y" . |
474 finally show "f x \<le> f y" . |
619 qed |
475 qed |
620 |
476 |
621 lemma (in algebra) countably_additive_additive: |
477 lemma (in algebra) countably_additive_additive: |
622 assumes posf: "positive M f" and ca: "countably_additive M f" |
478 assumes posf: "positive f" and ca: "countably_additive M f" |
623 shows "additive M f" |
479 shows "additive M f" |
624 proof (auto simp add: additive_def) |
480 proof (auto simp add: additive_def) |
625 fix x y |
481 fix x y |
626 assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" |
482 assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" |
627 hence "disjoint_family (binaryset x y)" |
483 hence "disjoint_family (binaryset x y)" |
628 by (auto simp add: disjoint_family_on_def binaryset_def) |
484 by (auto simp add: disjoint_family_on_def binaryset_def) |
629 hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
485 hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
630 (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
486 (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
631 f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))" |
487 f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" |
632 using ca |
488 using ca |
633 by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) |
489 by (simp add: countably_additive_def) |
634 hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
490 hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
635 f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))" |
491 f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" |
636 by (simp add: range_binaryset_eq UN_binaryset_eq) |
492 by (simp add: range_binaryset_eq UN_binaryset_eq) |
637 thus "f (x \<union> y) = f x + f y" using posf x y |
493 thus "f (x \<union> y) = f x + f y" using posf x y |
638 by (simp add: Un suminf_binaryset_eq positive_def) |
494 by (auto simp add: Un binaryset_psuminf positive_def) |
639 qed |
495 qed |
640 |
496 |
641 lemma (in algebra) inf_measure_agrees: |
497 lemma (in algebra) inf_measure_agrees: |
642 assumes posf: "positive M f" and ca: "countably_additive M f" |
498 assumes posf: "positive f" and ca: "countably_additive M f" |
643 and s: "s \<in> sets M" |
499 and s: "s \<in> sets M" |
644 shows "Inf (measure_set M f s) = f s" |
500 shows "Inf (measure_set M f s) = f s" |
645 proof (rule Inf_eq) |
501 unfolding Inf_pinfreal_def |
|
502 proof (safe intro!: Greatest_equality) |
646 fix z |
503 fix z |
647 assume z: "z \<in> measure_set M f s" |
504 assume z: "z \<in> measure_set M f s" |
648 from this obtain A where |
505 from this obtain A where |
649 A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
506 A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
650 and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)" |
507 and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z" |
651 and si: "suminf (f \<circ> A) = z" |
508 by (auto simp add: measure_set_def comp_def) |
652 by (auto simp add: measure_set_def sums_iff) |
|
653 hence seq: "s = (\<Union>i. A i \<inter> s)" by blast |
509 hence seq: "s = (\<Union>i. A i \<inter> s)" by blast |
654 have inc: "increasing M f" |
510 have inc: "increasing M f" |
655 by (metis additive_increasing ca countably_additive_additive posf) |
511 by (metis additive_increasing ca countably_additive_additive posf) |
656 have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)" |
512 have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)" |
657 proof (rule countably_additiveD [OF ca]) |
513 proof (rule countably_additiveD [OF ca]) |
658 show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s |
514 show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s |
659 by blast |
515 by blast |
660 show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj |
516 show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj |
661 by (auto simp add: disjoint_family_on_def) |
517 by (auto simp add: disjoint_family_on_def) |
662 show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s |
518 show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s |
663 by (metis UN_extend_simps(4) s seq) |
519 by (metis UN_extend_simps(4) s seq) |
664 qed |
520 qed |
665 hence "f s = suminf (\<lambda>i. f (A i \<inter> s))" |
521 hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))" |
666 using seq [symmetric] by (simp add: sums_iff) |
522 using seq [symmetric] by (simp add: sums_iff) |
667 also have "... \<le> suminf (f \<circ> A)" |
523 also have "... \<le> psuminf (f \<circ> A)" |
668 proof (rule summable_le [OF _ _ sm]) |
524 proof (rule psuminf_le) |
669 show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s |
525 fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s |
670 by (force intro: increasingD [OF inc]) |
526 by (force intro: increasingD [OF inc]) |
671 show "summable (\<lambda>i. f (A i \<inter> s))" using sums |
|
672 by (simp add: sums_iff) |
|
673 qed |
527 qed |
674 also have "... = z" by (rule si) |
528 also have "... = z" by (rule si) |
675 finally show "f s \<le> z" . |
529 finally show "f s \<le> z" . |
676 next |
530 next |
677 fix y |
531 fix y |
678 assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u" |
532 assume y: "\<forall>u \<in> measure_set M f s. y \<le> u" |
679 thus "y \<le> f s" |
533 thus "y \<le> f s" |
680 by (blast intro: inf_measure_nonempty [OF posf s subset_refl]) |
534 by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl]) |
681 qed |
535 qed |
682 |
536 |
683 lemma (in algebra) inf_measure_empty: |
537 lemma (in algebra) inf_measure_empty: |
684 assumes posf: "positive M f" |
538 assumes posf: "positive f" |
685 shows "Inf (measure_set M f {}) = 0" |
539 shows "Inf (measure_set M f {}) = 0" |
686 proof (rule antisym) |
540 proof (rule antisym) |
687 show "0 \<le> Inf (measure_set M f {})" |
|
688 by (metis empty_subsetI inf_measure_pos posf) |
|
689 show "Inf (measure_set M f {}) \<le> 0" |
541 show "Inf (measure_set M f {}) \<le> 0" |
690 by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf |
542 by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) |
691 positive_imp_0 subset_refl) |
543 qed simp |
692 qed |
|
693 |
544 |
694 lemma (in algebra) inf_measure_positive: |
545 lemma (in algebra) inf_measure_positive: |
695 "positive M f \<Longrightarrow> |
546 "positive f \<Longrightarrow> |
696 positive (| space = space M, sets = Pow (space M) |) |
547 positive (\<lambda>x. Inf (measure_set M f x))" |
697 (\<lambda>x. Inf (measure_set M f x))" |
548 by (simp add: positive_def inf_measure_empty) |
698 by (simp add: positive_def inf_measure_empty inf_measure_pos) |
|
699 |
549 |
700 lemma (in algebra) inf_measure_increasing: |
550 lemma (in algebra) inf_measure_increasing: |
701 assumes posf: "positive M f" |
551 assumes posf: "positive f" |
702 shows "increasing (| space = space M, sets = Pow (space M) |) |
552 shows "increasing (| space = space M, sets = Pow (space M) |) |
703 (\<lambda>x. Inf (measure_set M f x))" |
553 (\<lambda>x. Inf (measure_set M f x))" |
704 apply (auto simp add: increasing_def) |
554 apply (auto simp add: increasing_def) |
705 apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf) |
555 apply (rule complete_lattice_class.Inf_greatest) |
706 apply (rule Inf_lower) |
556 apply (rule complete_lattice_class.Inf_lower) |
707 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) |
557 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) |
708 apply (blast intro: inf_measure_pos0 posf) |
|
709 done |
558 done |
710 |
559 |
711 |
560 |
712 lemma (in algebra) inf_measure_le: |
561 lemma (in algebra) inf_measure_le: |
713 assumes posf: "positive M f" and inc: "increasing M f" |
562 assumes posf: "positive f" and inc: "increasing M f" |
714 and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}" |
563 and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> psuminf (f \<circ> A) = r}" |
715 shows "Inf (measure_set M f s) \<le> x" |
564 shows "Inf (measure_set M f s) \<le> x" |
716 proof - |
565 proof - |
717 from x |
566 from x |
718 obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" |
567 obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" |
719 and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x" |
568 and xeq: "psuminf (f \<circ> A) = x" |
720 by (auto simp add: sums_iff) |
569 by auto |
721 have dA: "range (disjointed A) \<subseteq> sets M" |
570 have dA: "range (disjointed A) \<subseteq> sets M" |
722 by (metis A range_disjointed_sets) |
571 by (metis A range_disjointed_sets) |
723 have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n" |
572 have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def |
724 proof (auto) |
573 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) |
725 fix n |
574 hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)" |
726 have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA |
575 by (blast intro: psuminf_le) |
727 by (auto simp add: positive_def image_subset_iff) |
576 hence ley: "psuminf (f o disjointed A) \<le> x" |
728 also have "... \<le> f (A n)" |
577 by (metis xeq) |
729 by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) |
578 hence y: "psuminf (f o disjointed A) \<in> measure_set M f s" |
730 finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" . |
|
731 qed |
|
732 from Series.summable_le2 [OF this sm] |
|
733 have sda: "summable (f o disjointed A)" |
|
734 "suminf (f o disjointed A) \<le> suminf (f \<circ> A)" |
|
735 by blast+ |
|
736 hence ley: "suminf (f o disjointed A) \<le> x" |
|
737 by (metis xeq) |
|
738 from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)" |
|
739 by (simp add: sums_iff) |
|
740 hence y: "suminf (f o disjointed A) \<in> measure_set M f s" |
|
741 apply (auto simp add: measure_set_def) |
579 apply (auto simp add: measure_set_def) |
742 apply (rule_tac x="disjointed A" in exI) |
580 apply (rule_tac x="disjointed A" in exI) |
743 apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA) |
581 apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def) |
744 done |
582 done |
745 show ?thesis |
583 show ?thesis |
746 by (blast intro: y order_trans [OF _ ley] inf_measure_pos0 posf) |
584 by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower) |
747 qed |
585 qed |
748 |
586 |
749 lemma (in algebra) inf_measure_close: |
587 lemma (in algebra) inf_measure_close: |
750 assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" |
588 assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)" |
751 shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) & |
589 shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and> |
752 (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e" |
590 psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e" |
753 proof - |
591 proof (cases "Inf (measure_set M f s) = \<omega>") |
754 have " measure_set M f s \<noteq> {}" |
592 case False |
755 by (metis emptyE ss inf_measure_nonempty [OF posf top]) |
593 obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e" |
756 hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e" |
594 using Inf_close[OF False e] by auto |
757 by (rule Inf_close [OF _ e]) |
595 thus ?thesis |
758 thus ?thesis |
596 by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) |
759 by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto) |
597 next |
|
598 case True |
|
599 have "measure_set M f s \<noteq> {}" |
|
600 by (metis emptyE ss inf_measure_nonempty [of f, OF posf top]) |
|
601 then obtain l where "l \<in> measure_set M f s" by auto |
|
602 moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp |
|
603 ultimately show ?thesis |
|
604 by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) |
760 qed |
605 qed |
761 |
606 |
762 lemma (in algebra) inf_measure_countably_subadditive: |
607 lemma (in algebra) inf_measure_countably_subadditive: |
763 assumes posf: "positive M f" and inc: "increasing M f" |
608 assumes posf: "positive f" and inc: "increasing M f" |
764 shows "countably_subadditive (| space = space M, sets = Pow (space M) |) |
609 shows "countably_subadditive (| space = space M, sets = Pow (space M) |) |
765 (\<lambda>x. Inf (measure_set M f x))" |
610 (\<lambda>x. Inf (measure_set M f x))" |
766 proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon) |
611 unfolding countably_subadditive_def o_def |
767 fix A :: "nat \<Rightarrow> 'a set" and e :: real |
612 proof (safe, simp, rule pinfreal_le_epsilon) |
768 assume A: "range A \<subseteq> Pow (space M)" |
613 fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal |
769 and disj: "disjoint_family A" |
614 |
770 and sb: "(\<Union>i. A i) \<subseteq> space M" |
615 let "?outer n" = "Inf (measure_set M f (A n))" |
771 and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))" |
616 assume A: "range A \<subseteq> Pow (space M)" |
772 and e: "0 < e" |
617 and disj: "disjoint_family A" |
773 have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and> |
618 and sb: "(\<Union>i. A i) \<subseteq> space M" |
774 (f o B) sums l \<and> |
619 and e: "0 < e" |
775 l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
620 hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and> |
776 apply (rule inf_measure_close [OF posf]) |
621 A n \<subseteq> (\<Union>i. BB n i) \<and> |
777 apply (metis e half mult_pos_pos zero_less_power) |
622 psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)" |
778 apply (metis UNIV_I UN_subset_iff sb) |
623 apply (safe intro!: choice inf_measure_close [of f, OF posf _]) |
779 done |
624 using e sb by (cases e, auto simp add: not_le mult_pos_pos) |
780 hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and> |
625 then obtain BB |
781 A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and> |
626 where BB: "\<And>n. (range (BB n) \<subseteq> sets M)" |
782 ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
627 and disjBB: "\<And>n. disjoint_family (BB n)" |
783 by (rule choice2) |
628 and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)" |
784 then obtain BB ll |
629 and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)" |
785 where BB: "!!n. (range (BB n) \<subseteq> sets M)" |
630 by auto blast |
786 and disjBB: "!!n. disjoint_family (BB n)" |
631 have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e" |
787 and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)" |
632 proof - |
788 and BBsums: "!!n. (f o BB n) sums ll n" |
633 have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)" |
789 and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
634 by (rule psuminf_le[OF BBle]) |
790 by auto blast |
635 also have "... = psuminf ?outer + e" |
791 have llpos: "!!n. 0 \<le> ll n" |
636 using psuminf_half_series by simp |
792 by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero |
637 finally show ?thesis . |
793 range_subsetD BB) |
638 qed |
794 have sll: "summable ll & |
639 def C \<equiv> "(split BB) o prod_decode" |
795 suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e" |
640 have C: "!!n. C n \<in> sets M" |
796 proof - |
641 apply (rule_tac p="prod_decode n" in PairE) |
797 have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)" |
642 apply (simp add: C_def) |
798 by (rule sums_mult [OF power_half_series]) |
643 apply (metis BB subsetD rangeI) |
799 hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)" |
644 done |
800 and eqe: "(\<Sum>n. e * (1 / 2) ^ n / 2) = e" |
645 have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
801 by (auto simp add: sums_iff) |
646 proof (auto simp add: C_def) |
802 have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) + |
647 fix x i |
803 suminf (\<lambda>n. e * (1/2)^(Suc n)) = |
648 assume x: "x \<in> A i" |
804 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))" |
649 with sbBB [of i] obtain j where "x \<in> BB i j" |
805 by (rule suminf_add [OF sum1 sum0]) |
650 by blast |
806 have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n" |
651 thus "\<exists>i. x \<in> split BB (prod_decode i)" |
807 by (metis ll llpos abs_of_nonneg) |
652 by (metis prod_encode_inverse prod.cases) |
808 have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))" |
653 qed |
809 by (rule summable_add [OF sum1 sum0]) |
654 have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" |
810 have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)" |
655 by (rule ext) (auto simp add: C_def) |
811 using Series.summable_le2 [OF 1 2] by auto |
656 moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle |
812 also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + |
657 by (force intro!: psuminf_2dimen simp: o_def) |
813 (\<Sum>n. e * (1 / 2) ^ Suc n)" |
658 ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp |
814 by (metis 0) |
659 have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" |
815 also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e" |
660 apply (rule inf_measure_le [OF posf(1) inc], auto) |
816 by (simp add: eqe) |
661 apply (rule_tac x="C" in exI) |
817 finally show ?thesis using Series.summable_le2 [OF 1 2] by auto |
662 apply (auto simp add: C sbC Csums) |
818 qed |
663 done |
819 def C \<equiv> "(split BB) o prod_decode" |
664 also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll |
820 have C: "!!n. C n \<in> sets M" |
665 by blast |
821 apply (rule_tac p="prod_decode n" in PairE) |
666 finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" . |
822 apply (simp add: C_def) |
|
823 apply (metis BB subsetD rangeI) |
|
824 done |
|
825 have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
|
826 proof (auto simp add: C_def) |
|
827 fix x i |
|
828 assume x: "x \<in> A i" |
|
829 with sbBB [of i] obtain j where "x \<in> BB i j" |
|
830 by blast |
|
831 thus "\<exists>i. x \<in> split BB (prod_decode i)" |
|
832 by (metis prod_encode_inverse prod.cases) |
|
833 qed |
|
834 have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" |
|
835 by (rule ext) (auto simp add: C_def) |
|
836 also have "... sums suminf ll" |
|
837 proof (rule suminf_2dimen) |
|
838 show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB |
|
839 by (force simp add: positive_def) |
|
840 show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB |
|
841 by (force simp add: o_def) |
|
842 show "summable ll" using sll |
|
843 by auto |
|
844 qed |
|
845 finally have Csums: "(f \<circ> C) sums suminf ll" . |
|
846 have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll" |
|
847 apply (rule inf_measure_le [OF posf inc], auto) |
|
848 apply (rule_tac x="C" in exI) |
|
849 apply (auto simp add: C sbC Csums) |
|
850 done |
|
851 also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll |
|
852 by blast |
|
853 finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> |
|
854 (\<Sum>n. Inf (measure_set M f (A n))) + e" . |
|
855 qed |
667 qed |
856 |
668 |
857 lemma (in algebra) inf_measure_outer: |
669 lemma (in algebra) inf_measure_outer: |
858 "positive M f \<Longrightarrow> increasing M f |
670 "\<lbrakk> positive f ; increasing M f \<rbrakk> |
859 \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |) |
671 \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |) |
860 (\<lambda>x. Inf (measure_set M f x))" |
672 (\<lambda>x. Inf (measure_set M f x))" |
861 by (simp add: outer_measure_space_def inf_measure_positive |
673 by (simp add: outer_measure_space_def inf_measure_empty |
862 inf_measure_increasing inf_measure_countably_subadditive) |
674 inf_measure_increasing inf_measure_countably_subadditive positive_def) |
863 |
675 |
864 (*MOVE UP*) |
676 (*MOVE UP*) |
865 |
677 |
866 lemma (in algebra) algebra_subset_lambda_system: |
678 lemma (in algebra) algebra_subset_lambda_system: |
867 assumes posf: "positive M f" and inc: "increasing M f" |
679 assumes posf: "positive f" and inc: "increasing M f" |
868 and add: "additive M f" |
680 and add: "additive M f" |
869 shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |) |
681 shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |) |
870 (\<lambda>x. Inf (measure_set M f x))" |
682 (\<lambda>x. Inf (measure_set M f x))" |
871 proof (auto dest: sets_into_space |
683 proof (auto dest: sets_into_space |
872 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
684 simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
873 fix x s |
685 fix x s |
874 assume x: "x \<in> sets M" |
686 assume x: "x \<in> sets M" |
875 and s: "s \<subseteq> space M" |
687 and s: "s \<subseteq> space M" |
876 have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s |
688 have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s |
877 by blast |
689 by blast |
878 have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
690 have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
879 \<le> Inf (measure_set M f s)" |
691 \<le> Inf (measure_set M f s)" |
880 proof (rule field_le_epsilon) |
692 proof (rule pinfreal_le_epsilon) |
881 fix e :: real |
693 fix e :: pinfreal |
882 assume e: "0 < e" |
694 assume e: "0 < e" |
883 from inf_measure_close [OF posf e s] |
695 from inf_measure_close [of f, OF posf e s] |
884 obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
696 obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
885 and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l" |
697 and sUN: "s \<subseteq> (\<Union>i. A i)" |
886 and l: "l \<le> Inf (measure_set M f s) + e" |
698 and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e" |
887 by auto |
699 by auto |
888 have [simp]: "!!x. x \<in> sets M \<Longrightarrow> |
700 have [simp]: "!!x. x \<in> sets M \<Longrightarrow> |
889 (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)" |
701 (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)" |
890 by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) |
702 by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) |
891 have [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)" |
703 have [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)" |
892 by (subst additiveD [OF add, symmetric]) |
704 by (subst additiveD [OF add, symmetric]) |
893 (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) |
705 (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) |
894 have fsumb: "summable (f \<circ> A)" |
|
895 by (metis fsums sums_iff) |
|
896 { fix u |
706 { fix u |
897 assume u: "u \<in> sets M" |
707 assume u: "u \<in> sets M" |
898 have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)" |
708 have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)" |
899 by (simp add: positive_imp_pos [OF posf] increasingD [OF inc] |
709 by (simp add: increasingD [OF inc] u Int range_subsetD [OF A]) |
900 u Int range_subsetD [OF A]) |
710 have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)" |
901 have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" |
711 proof (rule complete_lattice_class.Inf_lower) |
902 by (rule summable_comparison_test [OF _ fsumb]) simp |
712 show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)" |
903 have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)" |
713 apply (simp add: measure_set_def) |
904 proof (rule Inf_lower) |
714 apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) |
905 show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)" |
715 apply (auto simp add: disjoint_family_subset [OF disj] o_def) |
906 apply (simp add: measure_set_def) |
716 apply (blast intro: u range_subsetD [OF A]) |
907 apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) |
|
908 apply (auto simp add: disjoint_family_subset [OF disj]) |
|
909 apply (blast intro: u range_subsetD [OF A]) |
|
910 apply (blast dest: subsetD [OF sUN]) |
717 apply (blast dest: subsetD [OF sUN]) |
911 apply (metis 1 o_assoc sums_iff) |
|
912 done |
718 done |
913 next |
719 qed |
914 show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x" |
|
915 by (blast intro: inf_measure_pos0 [OF posf]) |
|
916 qed |
|
917 note 1 2 |
|
918 } note lesum = this |
720 } note lesum = this |
919 have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)" |
721 have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)" |
920 and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)" |
722 and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) |
921 and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)" |
723 \<le> psuminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)" |
922 and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) |
|
923 \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)" |
|
924 by (metis Diff lesum top x)+ |
724 by (metis Diff lesum top x)+ |
925 hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
725 hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
926 \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)" |
726 \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)" |
927 by (simp add: x) |
727 by (simp add: x add_mono) |
928 also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] |
728 also have "... \<le> psuminf (f o A)" |
929 by (simp add: x) (simp add: o_def) |
729 by (simp add: x psuminf_add[symmetric] o_def) |
930 also have "... \<le> Inf (measure_set M f s) + e" |
730 also have "... \<le> Inf (measure_set M f s) + e" |
931 by (metis fsums l sums_unique) |
731 by (rule l) |
932 finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
732 finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
933 \<le> Inf (measure_set M f s) + e" . |
733 \<le> Inf (measure_set M f s) + e" . |
934 qed |
734 qed |
935 moreover |
735 moreover |
936 have "Inf (measure_set M f s) |
736 have "Inf (measure_set M f s) |
937 \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
737 \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
938 proof - |
738 proof - |
939 have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))" |
739 have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))" |
940 by (metis Un_Diff_Int Un_commute) |
740 by (metis Un_Diff_Int Un_commute) |
941 also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
741 also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
942 apply (rule subadditiveD) |
742 apply (rule subadditiveD) |
943 apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow |
743 apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow |
944 inf_measure_positive inf_measure_countably_subadditive posf inc) |
744 inf_measure_positive inf_measure_countably_subadditive posf inc) |
945 apply (auto simp add: subsetD [OF s]) |
745 apply (auto simp add: subsetD [OF s]) |
946 done |
746 done |
947 finally show ?thesis . |
747 finally show ?thesis . |
948 qed |
748 qed |
949 ultimately |
749 ultimately |
950 show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
750 show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
951 = Inf (measure_set M f s)" |
751 = Inf (measure_set M f s)" |
952 by (rule order_antisym) |
752 by (rule order_antisym) |
953 qed |
753 qed |
954 |
754 |
955 lemma measure_down: |
755 lemma measure_down: |
956 "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow> |
756 "measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow> |
957 (measure M = measure N) \<Longrightarrow> measure_space M" |
757 (\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>" |
958 by (simp add: measure_space_def measure_space_axioms_def positive_def |
758 by (simp add: measure_space_def measure_space_axioms_def positive_def |
959 countably_additive_def) |
759 countably_additive_def) |
960 blast |
760 blast |
961 |
761 |
962 theorem (in algebra) caratheodory: |
762 theorem (in algebra) caratheodory: |
963 assumes posf: "positive M f" and ca: "countably_additive M f" |
763 assumes posf: "positive f" and ca: "countably_additive M f" |
964 shows "\<exists>MS :: 'a measure_space. |
764 shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma (space M) (sets M)) \<mu>" |
965 (\<forall>s \<in> sets M. measure MS s = f s) \<and> |
|
966 ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and> |
|
967 measure_space MS" |
|
968 proof - |
765 proof - |
969 have inc: "increasing M f" |
766 have inc: "increasing M f" |
970 by (metis additive_increasing ca countably_additive_additive posf) |
767 by (metis additive_increasing ca countably_additive_additive posf) |
971 let ?infm = "(\<lambda>x. Inf (measure_set M f x))" |
768 let ?infm = "(\<lambda>x. Inf (measure_set M f x))" |
972 def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" |
769 def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" |
973 have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)" |
770 have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm" |
974 using sigma_algebra.caratheodory_lemma |
771 using sigma_algebra.caratheodory_lemma |
975 [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] |
772 [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] |
976 by (simp add: ls_def) |
773 by (simp add: ls_def) |
977 hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)" |
774 hence sls: "sigma_algebra (|space = space M, sets = ls|)" |
978 by (simp add: measure_space_def) |
775 by (simp add: measure_space_def) |
979 have "sets M \<subseteq> ls" |
776 have "sets M \<subseteq> ls" |
980 by (simp add: ls_def) |
777 by (simp add: ls_def) |
981 (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
778 (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
982 hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" |
779 hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" |
983 using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] |
780 using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] |
984 by simp |
781 by simp |
985 have "measure_space (|space = space M, |
782 have "measure_space (sigma (space M) (sets M)) ?infm" |
986 sets = sigma_sets (space M) (sets M), |
783 unfolding sigma_def |
987 measure = ?infm|)" |
784 by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
988 by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
|
989 (simp_all add: sgs_sb space_closed) |
785 (simp_all add: sgs_sb space_closed) |
990 thus ?thesis |
786 thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm]) |
991 by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) |
787 qed |
992 qed |
|
993 |
788 |
994 end |
789 end |