author | paulson |
Wed, 28 Oct 2009 11:42:31 +0000 | |
changeset 33271 | 7be66dee1a5a |
child 33533 | 40b44cb20c8c |
permissions | -rw-r--r-- |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
1 |
(* Title: Sigma_Algebra.thy |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
2 |
Author: Stefan Richter, Markus Wenzel, TU Muenchen |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
3 |
Plus material from the Hurd/Coble measure theory development, |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
4 |
translated by Lawrence Paulson. |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
5 |
*) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
6 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
7 |
header {* Sigma Algebras *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
8 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
9 |
theory Sigma_Algebra imports Complex_Main begin |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
10 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
11 |
text {* Sigma algebras are an elementary concept in measure |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
12 |
theory. To measure --- that is to integrate --- functions, we first have |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
13 |
to measure sets. Unfortunately, when dealing with a large universe, |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
14 |
it is often not possible to consistently assign a measure to every |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
15 |
subset. Therefore it is necessary to define the set of measurable |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
16 |
subsets of the universe. A sigma algebra is such a set that has |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
17 |
three very natural and desirable properties. *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
18 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
19 |
subsection {* Algebras *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
20 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
21 |
record 'a algebra = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
22 |
space :: "'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
23 |
sets :: "'a set set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
24 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
25 |
locale algebra = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
26 |
fixes M |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
27 |
assumes space_closed: "sets M \<subseteq> Pow (space M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
28 |
and empty_sets [iff]: "{} \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
29 |
and compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
30 |
and Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
31 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
32 |
lemma (in algebra) top [iff]: "space M \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
33 |
by (metis Diff_empty compl_sets empty_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
34 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
35 |
lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
36 |
by (metis PowD contra_subsetD space_closed) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
37 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
38 |
lemma (in algebra) Int [intro]: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
39 |
assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
40 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
41 |
have "((space M - a) \<union> (space M - b)) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
42 |
by (metis a b compl_sets Un) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
43 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
44 |
have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
45 |
using space_closed a b |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
46 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
47 |
ultimately show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
48 |
by (metis compl_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
49 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
50 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
51 |
lemma (in algebra) Diff [intro]: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
52 |
assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
53 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
54 |
have "(a \<inter> (space M - b)) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
55 |
by (metis a b compl_sets Int) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
56 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
57 |
have "a - b = (a \<inter> (space M - b))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
58 |
by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
59 |
ultimately show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
60 |
by metis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
61 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
62 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
63 |
lemma (in algebra) finite_union [intro]: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
64 |
"finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
65 |
by (induct set: finite) (auto simp add: Un) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
66 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
67 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
68 |
subsection {* Sigma Algebras *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
69 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
70 |
locale sigma_algebra = algebra + |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
71 |
assumes countable_UN [intro]: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
72 |
"!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
73 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
74 |
lemma (in sigma_algebra) countable_INT: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
75 |
assumes a: "range a \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
76 |
shows "(\<Inter>i::nat. a i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
77 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
78 |
have "space M - (\<Union>i. space M - a i) \<in> sets M" using a |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
79 |
by (blast intro: countable_UN compl_sets a) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
80 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
81 |
have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
82 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
83 |
ultimately show ?thesis by metis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
84 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
85 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
86 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
87 |
lemma algebra_Pow: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
88 |
"algebra (| space = sp, sets = Pow sp |)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
89 |
by (auto simp add: algebra_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
90 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
91 |
lemma sigma_algebra_Pow: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
92 |
"sigma_algebra (| space = sp, sets = Pow sp |)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
93 |
by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
94 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
95 |
subsection {* Binary Unions *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
96 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
97 |
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
98 |
where "binary a b = (\<lambda>\<^isup>x. b)(0 := a)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
99 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
100 |
lemma range_binary_eq: "range(binary a b) = {a,b}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
101 |
by (auto simp add: binary_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
102 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
103 |
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
104 |
by (simp add: UNION_eq_Union_image range_binary_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
105 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
106 |
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
107 |
by (simp add: INTER_eq_Inter_image range_binary_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
108 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
109 |
lemma sigma_algebra_iff: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
110 |
"sigma_algebra M \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
111 |
algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
112 |
by (simp add: sigma_algebra_def sigma_algebra_axioms_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
113 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
114 |
lemma sigma_algebra_iff2: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
115 |
"sigma_algebra M \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
116 |
sets M \<subseteq> Pow (space M) & |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
117 |
{} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) & |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
118 |
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
119 |
by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
120 |
algebra_def Un_range_binary) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
121 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
122 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
123 |
subsection {* Initial Sigma Algebra *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
124 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
125 |
text {*Sigma algebras can naturally be created as the closure of any set of |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
126 |
sets with regard to the properties just postulated. *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
127 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
128 |
inductive_set |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
129 |
sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
130 |
for sp :: "'a set" and A :: "'a set set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
131 |
where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
132 |
Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
133 |
| Empty: "{} \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
134 |
| Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
135 |
| Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
136 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
137 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
138 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
139 |
sigma where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
140 |
"sigma sp A = (| space = sp, sets = sigma_sets sp A |)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
141 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
142 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
143 |
lemma space_sigma [simp]: "space (sigma X B) = X" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
144 |
by (simp add: sigma_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
145 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
146 |
lemma sigma_sets_top: "sp \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
147 |
by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
148 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
149 |
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
150 |
by (erule sigma_sets.induct, auto) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
151 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
152 |
lemma sigma_sets_Un: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
153 |
"a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
154 |
apply (simp add: Un_range_binary range_binary_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
155 |
apply (metis Union COMBK_def binary_def fun_upd_apply) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
156 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
157 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
158 |
lemma sigma_sets_Inter: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
159 |
assumes Asb: "A \<subseteq> Pow sp" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
160 |
shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
161 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
162 |
assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
163 |
hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
164 |
by (rule sigma_sets.Compl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
165 |
hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
166 |
by (rule sigma_sets.Union) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
167 |
hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
168 |
by (rule sigma_sets.Compl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
169 |
also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
170 |
by auto |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
171 |
also have "... = (\<Inter>i. a i)" using ai |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
172 |
by (blast dest: sigma_sets_into_sp [OF Asb]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
173 |
finally show ?thesis . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
174 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
175 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
176 |
lemma sigma_sets_INTER: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
177 |
assumes Asb: "A \<subseteq> Pow sp" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
178 |
and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
179 |
shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
180 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
181 |
from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
182 |
by (simp add: sigma_sets.intros sigma_sets_top) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
183 |
hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
184 |
by (rule sigma_sets_Inter [OF Asb]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
185 |
also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
186 |
by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
187 |
finally show ?thesis . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
188 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
189 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
190 |
lemma (in sigma_algebra) sigma_sets_subset: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
191 |
assumes a: "a \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
192 |
shows "sigma_sets (space M) a \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
193 |
proof |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
194 |
fix x |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
195 |
assume "x \<in> sigma_sets (space M) a" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
196 |
from this show "x \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
197 |
by (induct rule: sigma_sets.induct, auto) (metis a subsetD) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
198 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
199 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
200 |
lemma (in sigma_algebra) sigma_sets_eq: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
201 |
"sigma_sets (space M) (sets M) = sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
202 |
proof |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
203 |
show "sets M \<subseteq> sigma_sets (space M) (sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
204 |
by (metis Set.subsetI sigma_sets.Basic space_closed) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
205 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
206 |
show "sigma_sets (space M) (sets M) \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
207 |
by (metis sigma_sets_subset subset_refl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
208 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
209 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
210 |
lemma sigma_algebra_sigma_sets: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
211 |
"a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
212 |
apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
213 |
algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
214 |
apply (blast dest: sigma_sets_into_sp) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
215 |
apply (blast intro: sigma_sets.intros) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
216 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
217 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
218 |
lemma sigma_algebra_sigma: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
219 |
"a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
220 |
apply (rule sigma_algebra_sigma_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
221 |
apply (auto simp add: sigma_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
222 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
223 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
224 |
lemma (in sigma_algebra) sigma_subset: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
225 |
"a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
226 |
by (simp add: sigma_def sigma_sets_subset) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
227 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
228 |
end |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
229 |