--- 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