equal
deleted
inserted
replaced
47 by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"]) |
47 by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"]) |
48 finally show ?thesis unfolding g_def |
48 finally show ?thesis unfolding g_def |
49 by (simp add: suminf_eq_SUP) |
49 by (simp add: suminf_eq_SUP) |
50 qed |
50 qed |
51 |
51 |
52 subsection%important \<open>Characterizations of Measures\<close> |
52 subsection \<open>Characterizations of Measures\<close> |
53 |
53 |
54 definition%important outer_measure_space where |
54 definition%important outer_measure_space where |
55 "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f" |
55 "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f" |
56 |
56 |
57 subsubsection%important \<open>Lambda Systems\<close> |
57 subsubsection \<open>Lambda Systems\<close> |
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 |
458 qed |
458 qed |
459 |
459 |
460 lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
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 \<open>Caratheodory's theorem\<close> |
464 |
464 |
465 theorem (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 - |
468 proof - |
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 (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 \<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))" |
633 finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b" |
633 finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b" |
634 using Ca Cb by simp |
634 using Ca Cb by simp |
635 qed |
635 qed |
636 qed |
636 qed |
637 |
637 |
638 subsubsection%important \<open>Caratheodory on semirings\<close> |
638 subsubsection \<open>Caratheodory on semirings\<close> |
639 |
639 |
640 theorem (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 - |
643 proof - |