--- a/src/HOL/Probability/Caratheodory.thy Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Wed Apr 25 19:26:27 2012 +0200
@@ -655,7 +655,7 @@
by (simp add: measure_space_def positive_def countably_additive_def)
blast
-theorem (in ring_of_sets) caratheodory:
+theorem (in ring_of_sets) caratheodory':
assumes posf: "positive M f" and ca: "countably_additive M f"
shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
proof -
@@ -828,8 +828,327 @@
assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
-proof (intro caratheodory empty_continuous_imp_countably_additive f)
+proof (intro caratheodory' empty_continuous_imp_countably_additive f)
show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
qed (rule cont)
+section {* Volumes *}
+
+definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
+ "volume M f \<longleftrightarrow>
+ (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and>
+ (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))"
+
+lemma volumeI:
+ assumes "f {} = 0"
+ assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a"
+ 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)"
+ shows "volume M f"
+ using assms by (auto simp: volume_def)
+
+lemma volume_positive:
+ "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a"
+ by (auto simp: volume_def)
+
+lemma volume_empty:
+ "volume M f \<Longrightarrow> f {} = 0"
+ by (auto simp: volume_def)
+
+lemma volume_finite_additive:
+ assumes "volume M f"
+ assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
+ shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+proof -
+ have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"
+ using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
+ with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"
+ unfolding volume_def by blast
+ also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
+ proof (subst setsum_reindex_nonzero)
+ fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"
+ with `disjoint_family_on A I` have "A i = {}"
+ by (auto simp: disjoint_family_on_def)
+ then show "f (A i) = 0"
+ using volume_empty[OF `volume M f`] by simp
+ qed (auto intro: `finite I`)
+ finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+ by simp
+qed
+
+lemma (in ring_of_sets) volume_additiveI:
+ assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a"
+ assumes [simp]: "\<mu> {} = 0"
+ 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"
+ shows "volume M \<mu>"
+proof (unfold volume_def, safe)
+ fix C assume "finite C" "C \<subseteq> M" "disjoint C"
+ then show "\<mu> (\<Union>C) = setsum \<mu> C"
+ proof (induct C)
+ case (insert c C)
+ from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)"
+ by (auto intro!: add simp: disjoint_def)
+ with insert show ?case
+ by (simp add: disjoint_def)
+ qed simp
+qed fact+
+
+lemma (in semiring_of_sets) extend_volume:
+ assumes "volume M \<mu>"
+ shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)"
+proof -
+ let ?R = generated_ring
+ 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)"
+ by (auto simp: generated_ring_def)
+ from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this
+
+ { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+ fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
+ assume "\<Union>C = \<Union>D"
+ have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))"
+ proof (intro setsum_cong refl)
+ fix d assume "d \<in> D"
+ have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d"
+ using `d \<in> D` `\<Union>C = \<Union>D` by auto
+ moreover have "\<mu> (\<Union>c\<in>C. c \<inter> d) = (\<Sum>c\<in>C. \<mu> (c \<inter> d))"
+ proof (rule volume_finite_additive)
+ { fix c assume "c \<in> C" then show "c \<inter> d \<in> M"
+ using C D `d \<in> D` by auto }
+ show "(\<Union>a\<in>C. a \<inter> d) \<in> M"
+ unfolding Un_eq_d using `d \<in> D` D by auto
+ show "disjoint_family_on (\<lambda>a. a \<inter> d) C"
+ using `disjoint C` by (auto simp: disjoint_family_on_def disjoint_def)
+ qed fact+
+ ultimately show "\<mu> d = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" by simp
+ qed }
+ note split_sum = this
+
+ { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+ fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
+ assume "\<Union>C = \<Union>D"
+ with split_sum[OF C D] split_sum[OF D C]
+ have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
+ by (simp, subst setsum_commute, simp add: ac_simps) }
+ note sum_eq = this
+
+ { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+ then have "\<Union>C \<in> ?R" by (auto simp: generated_ring_def)
+ with \<mu>'_spec[THEN bspec, of "\<Union>C"]
+ obtain D where
+ D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)"
+ by blast
+ with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp }
+ note \<mu>' = this
+
+ show ?thesis
+ proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI)
+ fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a"
+ by (simp add: disjoint_def)
+ next
+ fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+ with \<mu>'[of Ca] `volume M \<mu>`[THEN volume_positive]
+ show "0 \<le> \<mu>' a"
+ by (auto intro!: setsum_nonneg)
+ next
+ show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto
+ next
+ fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+ fix b assume "b \<in> ?R" then guess Cb .. note Cb = this
+ assume "a \<inter> b = {}"
+ with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
+ then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
+
+ from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
+ using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
+ also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
+ using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
+ also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)"
+ using Ca Cb by (simp add: setsum_Un_Int)
+ also have "\<dots> = \<mu>' a + \<mu>' b"
+ using Ca Cb by (simp add: \<mu>')
+ finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b"
+ using Ca Cb by simp
+ qed
+qed
+
+section {* Caratheodory on semirings *}
+
+theorem (in semiring_of_sets) caratheodory:
+ assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
+ shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'"
+proof -
+ have "volume M \<mu>"
+ proof (rule volumeI)
+ { fix a assume "a \<in> M" then show "0 \<le> \<mu> a"
+ using pos unfolding positive_def by auto }
+ note p = this
+
+ fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C"
+ have "\<exists>F'. bij_betw F' {..<card C} C"
+ by (rule finite_same_card_bij[OF _ `finite C`]) auto
+ then guess F' .. note F' = this
+ then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
+ by (auto simp: bij_betw_def)
+ { fix i j assume *: "i < card C" "j < card C" "i \<noteq> j"
+ with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j"
+ unfolding inj_on_def by auto
+ with `disjoint C`[THEN disjointD]
+ have "F' i \<inter> F' j = {}"
+ by auto }
+ note F'_disj = this
+ def F \<equiv> "\<lambda>i. if i < card C then F' i else {}"
+ then have "disjoint_family F"
+ using F'_disj by (auto simp: disjoint_family_on_def)
+ moreover from F' have "(\<Union>i. F i) = \<Union>C"
+ by (auto simp: F_def set_eq_iff split: split_if_asm)
+ moreover have sets_F: "\<And>i. F i \<in> M"
+ using F' sets_C by (auto simp: F_def)
+ moreover note sets_C
+ ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))"
+ using ca[unfolded countably_additive_def, THEN spec, of F] by auto
+ also have "\<dots> = (\<Sum>i<card C. \<mu> (F' i))"
+ proof -
+ have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) sums (\<Sum>i<card C. \<mu> (F' i))"
+ by (rule sums_If_finite_set) auto
+ also have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) = (\<lambda>i. \<mu> (F i))"
+ using pos by (auto simp: positive_def F_def)
+ finally show "(\<Sum>i. \<mu> (F i)) = (\<Sum>i<card C. \<mu> (F' i))"
+ by (simp add: sums_iff)
+ qed
+ also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)"
+ using F'(2) by (subst (2) F') (simp add: setsum_reindex)
+ finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" .
+ next
+ show "\<mu> {} = 0"
+ using `positive M \<mu>` by (rule positiveD1)
+ qed
+ from extend_volume[OF this] obtain \<mu>_r where
+ V: "volume generated_ring \<mu>_r" "\<And>a. a \<in> M \<Longrightarrow> \<mu> a = \<mu>_r a"
+ by auto
+
+ interpret G: ring_of_sets \<Omega> generated_ring
+ by (rule generating_ring)
+
+ have pos: "positive generated_ring \<mu>_r"
+ using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty)
+
+ have "countably_additive generated_ring \<mu>_r"
+ proof (rule countably_additiveI)
+ fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
+ and Un_A: "(\<Union>i. A' i) \<in> generated_ring"
+
+ from generated_ringE[OF Un_A] guess C' . note C' = this
+
+ { fix c assume "c \<in> C'"
+ moreover def A \<equiv> "\<lambda>i. A' i \<inter> c"
+ ultimately have A: "range A \<subseteq> generated_ring" "disjoint_family A"
+ and Un_A: "(\<Union>i. A i) \<in> generated_ring"
+ using A' C'
+ by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def)
+ from A C' `c \<in> C'` have UN_eq: "(\<Union>i. A i) = c"
+ by (auto simp: A_def)
+
+ have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)"
+ (is "\<forall>i. ?P i")
+ proof
+ fix i
+ from A have Ai: "A i \<in> generated_ring" by auto
+ from generated_ringE[OF this] guess C . note C = this
+
+ have "\<exists>F'. bij_betw F' {..<card C} C"
+ by (rule finite_same_card_bij[OF _ `finite C`]) auto
+ then guess F .. note F = this
+ def f \<equiv> "\<lambda>i. if i < card C then F i else {}"
+ then have f: "bij_betw f {..< card C} C"
+ by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
+ with C have "\<forall>j. f j \<in> M"
+ by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset)
+ moreover
+ from f C have d_f: "disjoint_family_on f {..<card C}"
+ by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def)
+ then have "disjoint_family f"
+ by (auto simp: disjoint_family_on_def f_def)
+ moreover
+ have Ai_eq: "A i = (\<Union> x<card C. f x)"
+ using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
+ then have "\<Union>range f = A i"
+ using f C Ai unfolding bij_betw_def by (auto simp: f_def)
+ moreover
+ { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
+ using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
+ also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))"
+ by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp
+ also have "\<dots> = \<mu>_r (A i)"
+ using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq
+ by (intro volume_finite_additive[OF V(1) _ d_f, symmetric])
+ (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic)
+ finally have "\<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j))" .. }
+ ultimately show "?P i"
+ by blast
+ qed
+ from choice[OF this] guess f .. note f = this
+ then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)"
+ unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
+
+ have d: "disjoint_family (\<lambda>i. split f (prod_decode i))"
+ unfolding disjoint_family_on_def
+ proof (intro ballI impI)
+ fix m n :: nat assume "m \<noteq> n"
+ then have neq: "prod_decode m \<noteq> prod_decode n"
+ using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
+ show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}"
+ proof cases
+ assume "fst (prod_decode m) = fst (prod_decode n)"
+ then show ?thesis
+ using neq f by (fastforce simp: disjoint_family_on_def)
+ next
+ assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
+ have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
+ "split f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
+ using f[THEN spec, of "fst (prod_decode m)"]
+ using f[THEN spec, of "fst (prod_decode n)"]
+ by (auto simp: set_eq_iff)
+ with f A neq show ?thesis
+ by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
+ qed
+ qed
+ from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))"
+ by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
+ (auto split: prod.split)
+ also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))"
+ using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
+ also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))"
+ using f `c \<in> C'` C'
+ by (intro ca[unfolded countably_additive_def, rule_format])
+ (auto split: prod.split simp: UN_f_eq d UN_eq)
+ finally have "(\<Sum>n. \<mu>_r (A' n \<inter> c)) = \<mu> c"
+ using UN_f_eq UN_eq by (simp add: A_def) }
+ note eq = this
+
+ have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
+ using C' A' find_theorems "\<Union> _ ` _"
+ by (subst volume_finite_additive[symmetric, OF V(1)])
+ (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq
+ intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
+ intro: generated_ringI_Basic)
+ also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
+ using C' A'
+ by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union)
+ (auto intro: generated_ringI_Basic)
+ also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)"
+ using eq V C' by (auto intro!: setsum_cong)
+ also have "\<dots> = \<mu>_r (\<Union>C')"
+ using C' Un_A
+ by (subst volume_finite_additive[symmetric, OF V(1)])
+ (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq
+ intro: generated_ringI_Basic)
+ finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
+ using C' by simp
+ qed
+ from G.caratheodory'[OF `positive generated_ring \<mu>_r` `countably_additive generated_ring \<mu>_r`]
+ guess \<mu>' ..
+ with V show ?thesis
+ unfolding sigma_sets_generated_ring_eq
+ by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
+qed
+
end
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Apr 25 19:26:27 2012 +0200
@@ -8,21 +8,6 @@
imports Probability_Measure Caratheodory
begin
-lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
-proof
- fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
- by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
-qed
-
-lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
-proof
- fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
- by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
-qed
-
-lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
- by (auto intro: sigma_sets.Basic)
-
lemma (in product_sigma_finite)
assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
shows emeasure_fold_integral:
@@ -187,7 +172,8 @@
lemma (in product_prob_space) algebra_generator:
assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
-proof
+ unfolding algebra_def algebra_axioms_def ring_of_sets_iff
+proof (intro conjI ballI)
let ?G = generator
show "?G \<subseteq> Pow ?\<Omega>"
by (auto simp: generator_def prod_emb_def)
--- a/src/HOL/Probability/Measure_Space.thy Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Wed Apr 25 19:26:27 2012 +0200
@@ -636,7 +636,7 @@
unfolding null_sets_def by simp
interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
-proof
+proof (rule ring_of_setsI)
show "null_sets M \<subseteq> Pow (space M)"
using sets_into_space by auto
show "{} \<in> null_sets M"
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 25 19:26:27 2012 +0200
@@ -24,7 +24,7 @@
subsets of the universe. A sigma algebra is such a set that has
three very natural and desirable properties. *}
-subsection {* Algebras *}
+subsection {* Families of sets *}
locale subset_class =
fixes \<Omega> :: "'a set" and M :: "'a set set"
@@ -33,20 +33,85 @@
lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>"
by (metis PowD contra_subsetD space_closed)
-locale ring_of_sets = subset_class +
- assumes empty_sets [iff]: "{} \<in> M"
- and Diff [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M"
- and Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+subsection {* Semiring of sets *}
+
+subsubsection {* Disjoint sets *}
+
+definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+
+lemma disjointI:
+ "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
+ unfolding disjoint_def by auto
+
+lemma disjointD:
+ "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
+ unfolding disjoint_def by auto
+
+lemma disjoint_empty[iff]: "disjoint {}"
+ by (auto simp: disjoint_def)
-lemma (in ring_of_sets) Int [intro]:
- assumes a: "a \<in> M" and b: "b \<in> M" shows "a \<inter> b \<in> M"
+lemma disjoint_union:
+ assumes C: "disjoint C" and B: "disjoint B" and disj: "\<Union>C \<inter> \<Union>B = {}"
+ shows "disjoint (C \<union> B)"
+proof (rule disjointI)
+ fix c d assume sets: "c \<in> C \<union> B" "d \<in> C \<union> B" and "c \<noteq> d"
+ show "c \<inter> d = {}"
+ proof cases
+ assume "(c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B)"
+ then show ?thesis
+ proof
+ assume "c \<in> C \<and> d \<in> C" with `c \<noteq> d` C show "c \<inter> d = {}"
+ by (auto simp: disjoint_def)
+ next
+ assume "c \<in> B \<and> d \<in> B" with `c \<noteq> d` B show "c \<inter> d = {}"
+ by (auto simp: disjoint_def)
+ qed
+ next
+ assume "\<not> ((c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B))"
+ with sets have "(c \<subseteq> \<Union>C \<and> d \<subseteq> \<Union>B) \<or> (c \<subseteq> \<Union>B \<and> d \<subseteq> \<Union>C)"
+ by auto
+ with disj show "c \<inter> d = {}" by auto
+ qed
+qed
+
+locale semiring_of_sets = subset_class +
+ assumes empty_sets[iff]: "{} \<in> M"
+ assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
+ assumes Diff_cover:
+ "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
+
+lemma (in semiring_of_sets) finite_INT[intro]:
+ assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M"
+ shows "(\<Inter>i\<in>I. A i) \<in> M"
+ using assms by (induct rule: finite_ne_induct) auto
+
+lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x"
+ by (metis Int_absorb1 sets_into_space)
+
+lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x"
+ by (metis Int_absorb2 sets_into_space)
+
+lemma (in semiring_of_sets) sets_Collect_conj:
+ assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
+ shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M"
proof -
- have "a \<inter> b = a - (a - b)"
+ have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}"
by auto
- then show "a \<inter> b \<in> M"
- using a b by auto
+ with assms show ?thesis by auto
qed
+lemma (in semiring_of_sets) sets_Collect_finite_All:
+ assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
+ shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+ have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
+ using `S \<noteq> {}` by auto
+ with assms show ?thesis by auto
+qed
+
+locale ring_of_sets = semiring_of_sets +
+ assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+
lemma (in ring_of_sets) finite_Union [intro]:
"finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M"
by (induct set: finite) (auto simp add: Un)
@@ -56,10 +121,32 @@
shows "(\<Union>i\<in>I. A i) \<in> M"
using assms by induct auto
-lemma (in ring_of_sets) finite_INT[intro]:
- assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M"
- shows "(\<Inter>i\<in>I. A i) \<in> M"
- using assms by (induct rule: finite_ne_induct) auto
+lemma (in ring_of_sets) Diff [intro]:
+ assumes "a \<in> M" "b \<in> M" shows "a - b \<in> M"
+ using Diff_cover[OF assms] by auto
+
+lemma ring_of_setsI:
+ assumes space_closed: "M \<subseteq> Pow \<Omega>"
+ assumes empty_sets[iff]: "{} \<in> M"
+ assumes Un[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+ assumes Diff[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M"
+ shows "ring_of_sets \<Omega> M"
+proof
+ fix a b assume ab: "a \<in> M" "b \<in> M"
+ from ab show "\<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
+ by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def)
+ have "a \<inter> b = a - (a - b)" by auto
+ also have "\<dots> \<in> M" using ab by auto
+ finally show "a \<inter> b \<in> M" .
+qed fact+
+
+lemma ring_of_sets_iff: "ring_of_sets \<Omega> M \<longleftrightarrow> M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)"
+proof
+ assume "ring_of_sets \<Omega> M"
+ then interpret ring_of_sets \<Omega> M .
+ show "M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)"
+ using space_closed by auto
+qed (auto intro!: ring_of_setsI)
lemma (in ring_of_sets) insert_in_sets:
assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M"
@@ -68,21 +155,6 @@
thus ?thesis by auto
qed
-lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x"
- by (metis Int_absorb1 sets_into_space)
-
-lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x"
- by (metis Int_absorb2 sets_into_space)
-
-lemma (in ring_of_sets) sets_Collect_conj:
- assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
- shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M"
-proof -
- have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}"
- by auto
- with assms show ?thesis by auto
-qed
-
lemma (in ring_of_sets) sets_Collect_disj:
assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M"
@@ -92,15 +164,6 @@
with assms show ?thesis by auto
qed
-lemma (in ring_of_sets) sets_Collect_finite_All:
- assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
- shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
-proof -
- have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
- using `S \<noteq> {}` by auto
- with assms show ?thesis by auto
-qed
-
lemma (in ring_of_sets) sets_Collect_finite_Ex:
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
shows "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} \<in> M"
@@ -129,9 +192,10 @@
show ?Un using sets_into_space by auto
next
assume ?Un
- show "algebra \<Omega> M"
- proof
- show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" "\<Omega> \<in> M"
+ then have "\<Omega> \<in> M" by auto
+ interpret ring_of_sets \<Omega> M
+ proof (rule ring_of_setsI)
+ show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
using `?Un` by auto
fix a b assume a: "a \<in> M" and b: "b \<in> M"
then show "a \<union> b \<in> M" using `?Un` by auto
@@ -140,6 +204,7 @@
then show "a - b \<in> M"
using a b `?Un` by auto
qed
+ show "algebra \<Omega> M" proof qed fact
qed
lemma algebra_iff_Int:
@@ -184,9 +249,8 @@
by (cases P) auto
lemma algebra_single_set:
- assumes "X \<subseteq> S"
- shows "algebra S { {}, X, S - X, S }"
- by default (insert `X \<subseteq> S`, auto)
+ "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
+ by (auto simp: algebra_iff_Int)
section {* Restricted algebras *}
@@ -195,7 +259,7 @@
lemma (in algebra) restricted_algebra:
assumes "A \<in> M" shows "algebra A (restricted_space A)"
- using assms by unfold_locales auto
+ using assms by (auto simp: algebra_iff_Int)
subsection {* Sigma Algebras *}
@@ -261,19 +325,19 @@
qed
lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
- by default auto
+ by (auto simp: ring_of_sets_iff)
lemma algebra_Pow: "algebra sp (Pow sp)"
- by default auto
-
-lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
- by default auto
+ by (auto simp: algebra_iff_Un)
lemma sigma_algebra_iff:
"sigma_algebra \<Omega> M \<longleftrightarrow>
algebra \<Omega> M \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
+lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
+ by (auto simp: sigma_algebra_iff algebra_iff_Int)
+
lemma (in sigma_algebra) sets_Collect_countable_All:
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M"
shows "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} \<in> M"
@@ -452,6 +516,21 @@
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros(2-))
qed
+lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
+proof
+ fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
+ by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros(2-))
+qed
+
+lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
+proof
+ fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
+ by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros(2-))
+qed
+
+lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
+ by (auto intro: sigma_sets.Basic)
+
lemma (in sigma_algebra) restriction_in_sets:
fixes A :: "nat \<Rightarrow> 'a set"
assumes "S \<in> M"
@@ -762,6 +841,150 @@
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
qed
+lemma disjoint_family_on_disjoint_image:
+ "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
+ unfolding disjoint_family_on_def disjoint_def by force
+
+lemma disjoint_image_disjoint_family_on:
+ assumes d: "disjoint (A ` I)" and i: "inj_on A I"
+ shows "disjoint_family_on A I"
+ unfolding disjoint_family_on_def
+proof (intro ballI impI)
+ fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
+ with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
+ by (intro disjointD[OF d]) auto
+qed
+
+section {* Ring generated by a semiring *}
+
+definition (in semiring_of_sets)
+ "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
+
+lemma (in semiring_of_sets) generated_ringE[elim?]:
+ assumes "a \<in> generated_ring"
+ obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C"
+ using assms unfolding generated_ring_def by auto
+
+lemma (in semiring_of_sets) generated_ringI[intro?]:
+ assumes "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C"
+ shows "a \<in> generated_ring"
+ using assms unfolding generated_ring_def by auto
+
+lemma (in semiring_of_sets) generated_ringI_Basic:
+ "A \<in> M \<Longrightarrow> A \<in> generated_ring"
+ by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]:
+ assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
+ and "a \<inter> b = {}"
+ shows "a \<union> b \<in> generated_ring"
+proof -
+ from a guess Ca .. note Ca = this
+ from b guess Cb .. note Cb = this
+ show ?thesis
+ proof
+ show "disjoint (Ca \<union> Cb)"
+ using `a \<inter> b = {}` Ca Cb by (auto intro!: disjoint_union)
+ qed (insert Ca Cb, auto)
+qed
+
+lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring"
+ by (auto simp: generated_ring_def disjoint_def)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_Union:
+ assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring"
+ using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
+ "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring"
+ unfolding SUP_def by (intro generated_ring_disjoint_Union) auto
+
+lemma (in semiring_of_sets) generated_ring_Int:
+ assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
+ shows "a \<inter> b \<in> generated_ring"
+proof -
+ from a guess Ca .. note Ca = this
+ from b guess Cb .. note Cb = this
+ def C \<equiv> "(\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
+ show ?thesis
+ proof
+ show "disjoint C"
+ proof (simp add: disjoint_def C_def, intro ballI impI)
+ fix a1 b1 a2 b2 assume sets: "a1 \<in> Ca" "b1 \<in> Cb" "a2 \<in> Ca" "b2 \<in> Cb"
+ assume "a1 \<inter> b1 \<noteq> a2 \<inter> b2"
+ then have "a1 \<noteq> a2 \<or> b1 \<noteq> b2" by auto
+ then show "(a1 \<inter> b1) \<inter> (a2 \<inter> b2) = {}"
+ proof
+ assume "a1 \<noteq> a2"
+ with sets Ca have "a1 \<inter> a2 = {}"
+ by (auto simp: disjoint_def)
+ then show ?thesis by auto
+ next
+ assume "b1 \<noteq> b2"
+ with sets Cb have "b1 \<inter> b2 = {}"
+ by (auto simp: disjoint_def)
+ then show ?thesis by auto
+ qed
+ qed
+ qed (insert Ca Cb, auto simp: C_def)
+qed
+
+lemma (in semiring_of_sets) generated_ring_Inter:
+ assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring"
+ using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)
+
+lemma (in semiring_of_sets) generated_ring_INTER:
+ "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
+ unfolding INF_def by (intro generated_ring_Inter) auto
+
+lemma (in semiring_of_sets) generating_ring:
+ "ring_of_sets \<Omega> generated_ring"
+proof (rule ring_of_setsI)
+ let ?R = generated_ring
+ show "?R \<subseteq> Pow \<Omega>"
+ using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
+ show "{} \<in> ?R" by (rule generated_ring_empty)
+
+ { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this
+ fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this
+
+ show "a - b \<in> ?R"
+ proof cases
+ assume "Cb = {}" with Cb `a \<in> ?R` show ?thesis
+ by simp
+ next
+ assume "Cb \<noteq> {}"
+ with Ca Cb have "a - b = (\<Union>a'\<in>Ca. \<Inter>b'\<in>Cb. a' - b')" by auto
+ also have "\<dots> \<in> ?R"
+ proof (intro generated_ring_INTER generated_ring_disjoint_UNION)
+ fix a b assume "a \<in> Ca" "b \<in> Cb"
+ with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R"
+ by (auto simp add: generated_ring_def)
+ next
+ show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)"
+ using Ca by (auto simp add: disjoint_def `Cb \<noteq> {}`)
+ next
+ show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+
+ qed
+ finally show "a - b \<in> ?R" .
+ qed }
+ note Diff = this
+
+ fix a b assume sets: "a \<in> ?R" "b \<in> ?R"
+ have "a \<union> b = (a - b) \<union> (a \<inter> b) \<union> (b - a)" by auto
+ also have "\<dots> \<in> ?R"
+ by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto
+ finally show "a \<union> b \<in> ?R" .
+qed
+
+lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \<Omega> generated_ring = sigma_sets \<Omega> M"
+proof
+ interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M"
+ using space_closed by (rule sigma_algebra_sigma_sets)
+ show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M"
+ by (blast intro!: sigma_sets_mono elim: generated_ringE)
+qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
+
section {* Measure type *}
definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
@@ -777,7 +1000,7 @@
typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
proof
have "sigma_algebra UNIV {{}, UNIV}"
- proof qed auto
+ by (auto simp: sigma_algebra_iff2)
then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
by (auto simp: measure_space_def positive_def countably_additive_def)
qed