author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51683  baefa3b461c2 
child 53374  a14d2a854c02 
permissions  rwrr 
41983  1 
(* Title: HOL/Probability/Sigma_Algebra.thy 
42067  2 
Author: Stefan Richter, Markus Wenzel, TU München 
3 
Author: Johannes Hölzl, TU München 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

4 
Plus material from the Hurd/Coble measure theory development, 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

5 
translated by Lawrence Paulson. 
33271
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 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

8 
header {* Sigma Algebras *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

9 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

10 
theory Sigma_Algebra 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

11 
imports 
42145  12 
Complex_Main 
50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

13 
"~~/src/HOL/Library/Countable_Set" 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

14 
"~~/src/HOL/Library/FuncSet" 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

15 
"~~/src/HOL/Library/Indicator_Function" 
47694  16 
"~~/src/HOL/Library/Extended_Real" 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

17 
begin 
33271
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 
text {* Sigma algebras are an elementary concept in measure 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

20 
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

21 
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

22 
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

23 
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

24 
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

25 
three very natural and desirable properties. *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

26 

47762  27 
subsection {* Families of sets *} 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

28 

47694  29 
locale subset_class = 
30 
fixes \<Omega> :: "'a set" and M :: "'a set set" 

31 
assumes space_closed: "M \<subseteq> Pow \<Omega>" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

32 

47694  33 
lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

34 
by (metis PowD contra_subsetD space_closed) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

35 

47762  36 
subsection {* Semiring of sets *} 
37 

38 
subsubsection {* Disjoint sets *} 

39 

40 
definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})" 

41 

42 
lemma disjointI: 

43 
"(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A" 

44 
unfolding disjoint_def by auto 

45 

46 
lemma disjointD: 

47 
"disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}" 

48 
unfolding disjoint_def by auto 

49 

50 
lemma disjoint_empty[iff]: "disjoint {}" 

51 
by (auto simp: disjoint_def) 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

52 

47762  53 
lemma disjoint_union: 
54 
assumes C: "disjoint C" and B: "disjoint B" and disj: "\<Union>C \<inter> \<Union>B = {}" 

55 
shows "disjoint (C \<union> B)" 

56 
proof (rule disjointI) 

57 
fix c d assume sets: "c \<in> C \<union> B" "d \<in> C \<union> B" and "c \<noteq> d" 

58 
show "c \<inter> d = {}" 

59 
proof cases 

60 
assume "(c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B)" 

61 
then show ?thesis 

62 
proof 

63 
assume "c \<in> C \<and> d \<in> C" with `c \<noteq> d` C show "c \<inter> d = {}" 

64 
by (auto simp: disjoint_def) 

65 
next 

66 
assume "c \<in> B \<and> d \<in> B" with `c \<noteq> d` B show "c \<inter> d = {}" 

67 
by (auto simp: disjoint_def) 

68 
qed 

69 
next 

70 
assume "\<not> ((c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B))" 

71 
with sets have "(c \<subseteq> \<Union>C \<and> d \<subseteq> \<Union>B) \<or> (c \<subseteq> \<Union>B \<and> d \<subseteq> \<Union>C)" 

72 
by auto 

73 
with disj show "c \<inter> d = {}" by auto 

74 
qed 

75 
qed 

76 

77 
locale semiring_of_sets = subset_class + 

78 
assumes empty_sets[iff]: "{} \<in> M" 

79 
assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M" 

80 
assumes Diff_cover: 

81 
"\<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" 

82 

83 
lemma (in semiring_of_sets) finite_INT[intro]: 

84 
assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" 

85 
shows "(\<Inter>i\<in>I. A i) \<in> M" 

86 
using assms by (induct rule: finite_ne_induct) auto 

87 

88 
lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x" 

89 
by (metis Int_absorb1 sets_into_space) 

90 

91 
lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x" 

92 
by (metis Int_absorb2 sets_into_space) 

93 

94 
lemma (in semiring_of_sets) sets_Collect_conj: 

95 
assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" 

96 
shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

97 
proof  
47762  98 
have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

99 
by auto 
47762  100 
with assms show ?thesis by auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

101 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

102 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
49834
diff
changeset

103 
lemma (in semiring_of_sets) sets_Collect_finite_All': 
47762  104 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}" 
105 
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" 

106 
proof  

107 
have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" 

108 
using `S \<noteq> {}` by auto 

109 
with assms show ?thesis by auto 

110 
qed 

111 

112 
locale ring_of_sets = semiring_of_sets + 

113 
assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" 

114 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

115 
lemma (in ring_of_sets) finite_Union [intro]: 
47694  116 
"finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M" 
38656  117 
by (induct set: finite) (auto simp add: Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

118 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

119 
lemma (in ring_of_sets) finite_UN[intro]: 
47694  120 
assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" 
121 
shows "(\<Union>i\<in>I. A i) \<in> M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

122 
using assms by induct auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

123 

47762  124 
lemma (in ring_of_sets) Diff [intro]: 
125 
assumes "a \<in> M" "b \<in> M" shows "a  b \<in> M" 

126 
using Diff_cover[OF assms] by auto 

127 

128 
lemma ring_of_setsI: 

129 
assumes space_closed: "M \<subseteq> Pow \<Omega>" 

130 
assumes empty_sets[iff]: "{} \<in> M" 

131 
assumes Un[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" 

132 
assumes Diff[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a  b \<in> M" 

133 
shows "ring_of_sets \<Omega> M" 

134 
proof 

135 
fix a b assume ab: "a \<in> M" "b \<in> M" 

136 
from ab show "\<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a  b = \<Union>C" 

137 
by (intro exI[of _ "{a  b}"]) (auto simp: disjoint_def) 

138 
have "a \<inter> b = a  (a  b)" by auto 

139 
also have "\<dots> \<in> M" using ab by auto 

140 
finally show "a \<inter> b \<in> M" . 

141 
qed fact+ 

142 

143 
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)" 

144 
proof 

145 
assume "ring_of_sets \<Omega> M" 

146 
then interpret ring_of_sets \<Omega> M . 

147 
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)" 

148 
using space_closed by auto 

149 
qed (auto intro!: ring_of_setsI) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

150 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

151 
lemma (in ring_of_sets) insert_in_sets: 
47694  152 
assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M" 
38656  153 
proof  
47694  154 
have "{x} \<union> A \<in> M" using assms by (rule Un) 
38656  155 
thus ?thesis by auto 
156 
qed 

157 

42867  158 
lemma (in ring_of_sets) sets_Collect_disj: 
47694  159 
assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" 
160 
shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M" 

42867  161 
proof  
47694  162 
have "{x\<in>\<Omega>. Q x \<or> P x} = {x\<in>\<Omega>. Q x} \<union> {x\<in>\<Omega>. P x}" 
42867  163 
by auto 
164 
with assms show ?thesis by auto 

165 
qed 

166 

167 
lemma (in ring_of_sets) sets_Collect_finite_Ex: 

47694  168 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" 
169 
shows "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} \<in> M" 

42867  170 
proof  
47694  171 
have "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>\<Omega>. P i x})" 
42867  172 
by auto 
173 
with assms show ?thesis by auto 

174 
qed 

175 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

176 
locale algebra = ring_of_sets + 
47694  177 
assumes top [iff]: "\<Omega> \<in> M" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

178 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

179 
lemma (in algebra) compl_sets [intro]: 
47694  180 
"a \<in> M \<Longrightarrow> \<Omega>  a \<in> M" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

181 
by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

182 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

183 
lemma algebra_iff_Un: 
47694  184 
"algebra \<Omega> M \<longleftrightarrow> 
185 
M \<subseteq> Pow \<Omega> \<and> 

186 
{} \<in> M \<and> 

187 
(\<forall>a \<in> M. \<Omega>  a \<in> M) \<and> 

188 
(\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un") 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

189 
proof 
47694  190 
assume "algebra \<Omega> M" 
191 
then interpret algebra \<Omega> M . 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

192 
show ?Un using sets_into_space by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

193 
next 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

194 
assume ?Un 
47762  195 
then have "\<Omega> \<in> M" by auto 
196 
interpret ring_of_sets \<Omega> M 

197 
proof (rule ring_of_setsI) 

198 
show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

199 
using `?Un` by auto 
47694  200 
fix a b assume a: "a \<in> M" and b: "b \<in> M" 
201 
then show "a \<union> b \<in> M" using `?Un` by auto 

202 
have "a  b = \<Omega>  ((\<Omega>  a) \<union> b)" 

203 
using \<Omega> a b by auto 

204 
then show "a  b \<in> M" 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

205 
using a b `?Un` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

206 
qed 
47762  207 
show "algebra \<Omega> M" proof qed fact 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

208 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

209 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

210 
lemma algebra_iff_Int: 
47694  211 
"algebra \<Omega> M \<longleftrightarrow> 
212 
M \<subseteq> Pow \<Omega> & {} \<in> M & 

213 
(\<forall>a \<in> M. \<Omega>  a \<in> M) & 

214 
(\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int") 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

215 
proof 
47694  216 
assume "algebra \<Omega> M" 
217 
then interpret algebra \<Omega> M . 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

218 
show ?Int using sets_into_space by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

219 
next 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

220 
assume ?Int 
47694  221 
show "algebra \<Omega> M" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

222 
proof (unfold algebra_iff_Un, intro conjI ballI) 
47694  223 
show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

224 
using `?Int` by auto 
47694  225 
from `?Int` show "\<And>a. a \<in> M \<Longrightarrow> \<Omega>  a \<in> M" by auto 
226 
fix a b assume M: "a \<in> M" "b \<in> M" 

227 
hence "a \<union> b = \<Omega>  ((\<Omega>  a) \<inter> (\<Omega>  b))" 

228 
using \<Omega> by blast 

229 
also have "... \<in> M" 

230 
using M `?Int` by auto 

231 
finally show "a \<union> b \<in> M" . 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

232 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

233 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

234 

42867  235 
lemma (in algebra) sets_Collect_neg: 
47694  236 
assumes "{x\<in>\<Omega>. P x} \<in> M" 
237 
shows "{x\<in>\<Omega>. \<not> P x} \<in> M" 

42867  238 
proof  
47694  239 
have "{x\<in>\<Omega>. \<not> P x} = \<Omega>  {x\<in>\<Omega>. P x}" by auto 
42867  240 
with assms show ?thesis by auto 
241 
qed 

242 

243 
lemma (in algebra) sets_Collect_imp: 

47694  244 
"{x\<in>\<Omega>. P x} \<in> M \<Longrightarrow> {x\<in>\<Omega>. Q x} \<in> M \<Longrightarrow> {x\<in>\<Omega>. Q x \<longrightarrow> P x} \<in> M" 
42867  245 
unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg) 
246 

247 
lemma (in algebra) sets_Collect_const: 

47694  248 
"{x\<in>\<Omega>. P} \<in> M" 
42867  249 
by (cases P) auto 
250 

42984  251 
lemma algebra_single_set: 
47762  252 
"X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S  X, S }" 
253 
by (auto simp: algebra_iff_Int) 

42984  254 

50387  255 
subsection {* Restricted algebras *} 
39092  256 

257 
abbreviation (in algebra) 

47694  258 
"restricted_space A \<equiv> (op \<inter> A) ` M" 
39092  259 

38656  260 
lemma (in algebra) restricted_algebra: 
47694  261 
assumes "A \<in> M" shows "algebra A (restricted_space A)" 
47762  262 
using assms by (auto simp: algebra_iff_Int) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

263 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

264 
subsection {* Sigma Algebras *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

265 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

266 
locale sigma_algebra = algebra + 
47694  267 
assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

268 

42984  269 
lemma (in algebra) is_sigma_algebra: 
47694  270 
assumes "finite M" 
271 
shows "sigma_algebra \<Omega> M" 

42984  272 
proof 
47694  273 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> M" 
274 
then have "(\<Union>i. A i) = (\<Union>s\<in>M \<inter> range A. s)" 

42984  275 
by auto 
47694  276 
also have "(\<Union>s\<in>M \<inter> range A. s) \<in> M" 
277 
using `finite M` by auto 

278 
finally show "(\<Union>i. A i) \<in> M" . 

42984  279 
qed 
280 

38656  281 
lemma countable_UN_eq: 
282 
fixes A :: "'i::countable \<Rightarrow> 'a set" 

47694  283 
shows "(range A \<subseteq> M \<longrightarrow> (\<Union>i. A i) \<in> M) \<longleftrightarrow> 
284 
(range (A \<circ> from_nat) \<subseteq> M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> M)" 

38656  285 
proof  
286 
let ?A' = "A \<circ> from_nat" 

287 
have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r") 

288 
proof safe 

289 
fix x i assume "x \<in> A i" thus "x \<in> ?l" 

290 
by (auto intro!: exI[of _ "to_nat i"]) 

291 
next 

292 
fix x i assume "x \<in> ?A' i" thus "x \<in> ?r" 

293 
by (auto intro!: exI[of _ "from_nat i"]) 

294 
qed 

295 
have **: "range ?A' = range A" 

40702  296 
using surj_from_nat 
38656  297 
by (auto simp: image_compose intro!: imageI) 
298 
show ?thesis unfolding * ** .. 

299 
qed 

300 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

301 
lemma (in sigma_algebra) countable_Union [intro]: 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

302 
assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

303 
proof cases 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

304 
assume "X \<noteq> {}" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

305 
hence "\<Union>X = (\<Union>n. from_nat_into X n)" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

306 
using assms by (auto intro: from_nat_into) (metis from_nat_into_surj) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

307 
also have "\<dots> \<in> M" using assms 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

308 
by (auto intro!: countable_nat_UN) (metis `X \<noteq> {}` from_nat_into set_mp) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

309 
finally show ?thesis . 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

310 
qed simp 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

311 

38656  312 
lemma (in sigma_algebra) countable_UN[intro]: 
313 
fixes A :: "'i::countable \<Rightarrow> 'a set" 

47694  314 
assumes "A`X \<subseteq> M" 
315 
shows "(\<Union>x\<in>X. A x) \<in> M" 

38656  316 
proof  
46731  317 
let ?A = "\<lambda>i. if i \<in> X then A i else {}" 
47694  318 
from assms have "range ?A \<subseteq> M" by auto 
38656  319 
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M] 
47694  320 
have "(\<Union>x. ?A x) \<in> M" by auto 
38656  321 
moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm) 
322 
ultimately show ?thesis by simp 

323 
qed 

324 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

325 
lemma (in sigma_algebra) countable_UN': 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

326 
fixes A :: "'i \<Rightarrow> 'a set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

327 
assumes X: "countable X" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

328 
assumes A: "A`X \<subseteq> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

329 
shows "(\<Union>x\<in>X. A x) \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

330 
proof  
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

331 
have "(\<Union>x\<in>X. A x) = (\<Union>i\<in>to_nat_on X ` X. A (from_nat_into X i))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

332 
using X by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

333 
also have "\<dots> \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

334 
using A X 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

335 
by (intro countable_UN) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

336 
finally show ?thesis . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

337 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

338 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
33271
diff
changeset

339 
lemma (in sigma_algebra) countable_INT [intro]: 
38656  340 
fixes A :: "'i::countable \<Rightarrow> 'a set" 
47694  341 
assumes A: "A`X \<subseteq> M" "X \<noteq> {}" 
342 
shows "(\<Inter>i\<in>X. A i) \<in> M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

343 
proof  
47694  344 
from A have "\<forall>i\<in>X. A i \<in> M" by fast 
345 
hence "\<Omega>  (\<Union>i\<in>X. \<Omega>  A i) \<in> M" by blast 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

346 
moreover 
47694  347 
have "(\<Inter>i\<in>X. A i) = \<Omega>  (\<Union>i\<in>X. \<Omega>  A i)" using space_closed A 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

348 
by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

349 
ultimately show ?thesis by metis 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

350 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

351 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

352 
lemma (in sigma_algebra) countable_INT': 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

353 
fixes A :: "'i \<Rightarrow> 'a set" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

354 
assumes X: "countable X" "X \<noteq> {}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

355 
assumes A: "A`X \<subseteq> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

356 
shows "(\<Inter>x\<in>X. A x) \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

357 
proof  
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

358 
have "(\<Inter>x\<in>X. A x) = (\<Inter>i\<in>to_nat_on X ` X. A (from_nat_into X i))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

359 
using X by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

360 
also have "\<dots> \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

361 
using A X 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

362 
by (intro countable_INT) auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

363 
finally show ?thesis . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

364 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

365 

47694  366 
lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)" 
47762  367 
by (auto simp: ring_of_sets_iff) 
42145  368 

47694  369 
lemma algebra_Pow: "algebra sp (Pow sp)" 
47762  370 
by (auto simp: algebra_iff_Un) 
38656  371 

372 
lemma sigma_algebra_iff: 

47694  373 
"sigma_algebra \<Omega> M \<longleftrightarrow> 
374 
algebra \<Omega> M \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" 

38656  375 
by (simp add: sigma_algebra_def sigma_algebra_axioms_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

376 

47762  377 
lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)" 
378 
by (auto simp: sigma_algebra_iff algebra_iff_Int) 

379 

42867  380 
lemma (in sigma_algebra) sets_Collect_countable_All: 
47694  381 
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" 
382 
shows "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} \<in> M" 

42867  383 
proof  
47694  384 
have "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>\<Omega>. P i x})" by auto 
42867  385 
with assms show ?thesis by auto 
386 
qed 

387 

388 
lemma (in sigma_algebra) sets_Collect_countable_Ex: 

47694  389 
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" 
390 
shows "{x\<in>\<Omega>. \<exists>i::'i::countable. P i x} \<in> M" 

42867  391 
proof  
47694  392 
have "{x\<in>\<Omega>. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>\<Omega>. P i x})" by auto 
42867  393 
with assms show ?thesis by auto 
394 
qed 

395 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

396 
lemma (in sigma_algebra) sets_Collect_countable_Ex': 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

397 
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

398 
assumes "countable I" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

399 
shows "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} \<in> M" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

400 
proof  
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

401 
have "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} = (\<Union>i\<in>I. {x\<in>\<Omega>. P i x})" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

402 
with assms show ?thesis 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

403 
by (auto intro!: countable_UN') 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

404 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50387
diff
changeset

405 

42867  406 
lemmas (in sigma_algebra) sets_Collect = 
407 
sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const 

408 
sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All 

409 

47694  410 
lemma (in sigma_algebra) sets_Collect_countable_Ball: 
411 
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" 

412 
shows "{x\<in>\<Omega>. \<forall>i::'i::countable\<in>X. P i x} \<in> M" 

413 
unfolding Ball_def by (intro sets_Collect assms) 

414 

415 
lemma (in sigma_algebra) sets_Collect_countable_Bex: 

416 
assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M" 

417 
shows "{x\<in>\<Omega>. \<exists>i::'i::countable\<in>X. P i x} \<in> M" 

418 
unfolding Bex_def by (intro sets_Collect assms) 

419 

42984  420 
lemma sigma_algebra_single_set: 
421 
assumes "X \<subseteq> S" 

47694  422 
shows "sigma_algebra S { {}, X, S  X, S }" 
42984  423 
using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp 
424 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

425 
subsection {* Binary Unions *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

426 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

427 
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" 
50252  428 
where "binary a b = (\<lambda>x. b)(0 := a)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

429 

38656  430 
lemma range_binary_eq: "range(binary a b) = {a,b}" 
431 
by (auto simp add: binary_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

432 

38656  433 
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
44106  434 
by (simp add: SUP_def range_binary_eq) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

435 

38656  436 
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
44106  437 
by (simp add: INF_def range_binary_eq) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

438 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

439 
lemma sigma_algebra_iff2: 
47694  440 
"sigma_algebra \<Omega> M \<longleftrightarrow> 
441 
M \<subseteq> Pow \<Omega> \<and> 

442 
{} \<in> M \<and> (\<forall>s \<in> M. \<Omega>  s \<in> M) \<and> 

443 
(\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" 

38656  444 
by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

445 
algebra_iff_Un Un_range_binary) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

446 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

447 
subsection {* Initial Sigma Algebra *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

448 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

449 
text {*Sigma algebras can naturally be created as the closure of any set of 
47694  450 
M with regard to the properties just postulated. *} 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

451 

51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

452 
inductive_set sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

453 
for sp :: "'a set" and A :: "'a set set" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

454 
where 
47694  455 
Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

456 
 Empty: "{} \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

457 
 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

458 
 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

459 

41543  460 
lemma (in sigma_algebra) sigma_sets_subset: 
47694  461 
assumes a: "a \<subseteq> M" 
462 
shows "sigma_sets \<Omega> a \<subseteq> M" 

41543  463 
proof 
464 
fix x 

47694  465 
assume "x \<in> sigma_sets \<Omega> a" 
466 
from this show "x \<in> M" 

41543  467 
by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 
468 
qed 

469 

470 
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp" 

471 
by (erule sigma_sets.induct, auto) 

472 

473 
lemma sigma_algebra_sigma_sets: 

47694  474 
"a \<subseteq> Pow \<Omega> \<Longrightarrow> sigma_algebra \<Omega> (sigma_sets \<Omega> a)" 
41543  475 
by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp 
476 
intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl) 

477 

478 
lemma sigma_sets_least_sigma_algebra: 

479 
assumes "A \<subseteq> Pow S" 

47694  480 
shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra S B}" 
41543  481 
proof safe 
47694  482 
fix B X assume "A \<subseteq> B" and sa: "sigma_algebra S B" 
41543  483 
and X: "X \<in> sigma_sets S A" 
484 
from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X 

485 
show "X \<in> B" by auto 

486 
next 

47694  487 
fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra S B}" 
488 
then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra S B \<Longrightarrow> X \<in> B" 

41543  489 
by simp 
47694  490 
have "A \<subseteq> sigma_sets S A" using assms by auto 
491 
moreover have "sigma_algebra S (sigma_sets S A)" 

41543  492 
using assms by (intro sigma_algebra_sigma_sets[of A]) auto 
493 
ultimately show "X \<in> sigma_sets S A" by auto 

494 
qed 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

495 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

496 
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

497 
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

498 

38656  499 
lemma sigma_sets_Un: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

500 
"a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A" 
38656  501 
apply (simp add: Un_range_binary range_binary_eq) 
40859  502 
apply (rule Union, simp add: binary_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

503 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

504 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

505 
lemma sigma_sets_Inter: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

506 
assumes Asb: "A \<subseteq> Pow sp" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

507 
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

508 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

509 
assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A" 
38656  510 
hence "\<And>i::nat. sp(a i) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

511 
by (rule sigma_sets.Compl) 
38656  512 
hence "(\<Union>i. sp(a i)) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

513 
by (rule sigma_sets.Union) 
38656  514 
hence "sp(\<Union>i. sp(a i)) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

515 
by (rule sigma_sets.Compl) 
38656  516 
also have "sp(\<Union>i. sp(a i)) = sp Int (\<Inter>i. a i)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

517 
by auto 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

518 
also have "... = (\<Inter>i. a i)" using ai 
38656  519 
by (blast dest: sigma_sets_into_sp [OF Asb]) 
520 
finally show ?thesis . 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

521 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

522 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

523 
lemma sigma_sets_INTER: 
38656  524 
assumes Asb: "A \<subseteq> Pow sp" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

525 
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

526 
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

527 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

528 
from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A" 
47694  529 
by (simp add: sigma_sets.intros(2) sigma_sets_top) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

530 
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

531 
by (rule sigma_sets_Inter [OF Asb]) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

532 
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

533 
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

534 
finally show ?thesis . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

535 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

536 

51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

537 
lemma sigma_sets_UNION: "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A" 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

538 
using from_nat_into[of B] range_from_nat_into[of B] sigma_sets.Union[of "from_nat_into B" X A] 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

539 
apply (cases "B = {}") 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

540 
apply (simp add: sigma_sets.Empty) 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

541 
apply (simp del: Union_image_eq add: Union_image_eq[symmetric]) 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

542 
done 
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
50526
diff
changeset

543 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

544 
lemma (in sigma_algebra) sigma_sets_eq: 
47694  545 
"sigma_sets \<Omega> M = M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

546 
proof 
47694  547 
show "M \<subseteq> sigma_sets \<Omega> M" 
37032  548 
by (metis Set.subsetI sigma_sets.Basic) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

549 
next 
47694  550 
show "sigma_sets \<Omega> M \<subseteq> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

551 
by (metis sigma_sets_subset subset_refl) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

552 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

553 

42981  554 
lemma sigma_sets_eqI: 
555 
assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B" 

556 
assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A" 

557 
shows "sigma_sets M A = sigma_sets M B" 

558 
proof (intro set_eqI iffI) 

559 
fix a assume "a \<in> sigma_sets M A" 

560 
from this A show "a \<in> sigma_sets M B" 

47694  561 
by induct (auto intro!: sigma_sets.intros(2) del: sigma_sets.Basic) 
42981  562 
next 
563 
fix b assume "b \<in> sigma_sets M B" 

564 
from this B show "b \<in> sigma_sets M A" 

47694  565 
by induct (auto intro!: sigma_sets.intros(2) del: sigma_sets.Basic) 
42981  566 
qed 
567 

42984  568 
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" 
569 
proof 

570 
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" 

47694  571 
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros(2)) 
42984  572 
qed 
573 

47762  574 
lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B" 
575 
proof 

576 
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" 

577 
by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros(2)) 

578 
qed 

579 

580 
lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" 

581 
proof 

582 
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" 

583 
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros(2)) 

584 
qed 

585 

586 
lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A" 

587 
by (auto intro: sigma_sets.Basic) 

588 

38656  589 
lemma (in sigma_algebra) restriction_in_sets: 
590 
fixes A :: "nat \<Rightarrow> 'a set" 

47694  591 
assumes "S \<in> M" 
592 
and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` M" (is "_ \<subseteq> ?r") 

593 
shows "range A \<subseteq> M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` M" 

38656  594 
proof  
595 
{ fix i have "A i \<in> ?r" using * by auto 

47694  596 
hence "\<exists>B. A i = B \<inter> S \<and> B \<in> M" by auto 
597 
hence "A i \<subseteq> S" "A i \<in> M" using `S \<in> M` by auto } 

598 
thus "range A \<subseteq> M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` M" 

38656  599 
by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"]) 
600 
qed 

601 

602 
lemma (in sigma_algebra) restricted_sigma_algebra: 

47694  603 
assumes "S \<in> M" 
604 
shows "sigma_algebra S (restricted_space S)" 

38656  605 
unfolding sigma_algebra_def sigma_algebra_axioms_def 
606 
proof safe 

47694  607 
show "algebra S (restricted_space S)" using restricted_algebra[OF assms] . 
38656  608 
next 
47694  609 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> restricted_space S" 
38656  610 
from restriction_in_sets[OF assms this[simplified]] 
47694  611 
show "(\<Union>i. A i) \<in> restricted_space S" by simp 
38656  612 
qed 
613 

40859  614 
lemma sigma_sets_Int: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

615 
assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

616 
shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)" 
40859  617 
proof (intro equalityI subsetI) 
618 
fix x assume "x \<in> op \<inter> A ` sigma_sets sp st" 

619 
then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

620 
then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)" 
40859  621 
proof (induct arbitrary: x) 
622 
case (Compl a) 

623 
then show ?case 

624 
by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps) 

625 
next 

626 
case (Union a) 

627 
then show ?case 

628 
by (auto intro!: sigma_sets.Union 

629 
simp add: UN_extend_simps simp del: UN_simps) 

47694  630 
qed (auto intro!: sigma_sets.intros(2)) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

631 
then show "x \<in> sigma_sets A (op \<inter> A ` st)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

632 
using `A \<subseteq> sp` by (simp add: Int_absorb2) 
40859  633 
next 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

634 
fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)" 
40859  635 
then show "x \<in> op \<inter> A ` sigma_sets sp st" 
636 
proof induct 

637 
case (Compl a) 

638 
then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

639 
then show ?case using `A \<subseteq> sp` 
40859  640 
by (force simp add: image_iff intro!: bexI[of _ "sp  x"] sigma_sets.Compl) 
641 
next 

642 
case (Union a) 

643 
then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x" 

644 
by (auto simp: image_iff Bex_def) 

645 
from choice[OF this] guess f .. 

646 
then show ?case 

647 
by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union 

648 
simp add: image_iff) 

47694  649 
qed (auto intro!: sigma_sets.intros(2)) 
40859  650 
qed 
651 

47694  652 
lemma sigma_sets_empty_eq: "sigma_sets A {} = {{}, A}" 
40859  653 
proof (intro set_eqI iffI) 
47694  654 
fix a assume "a \<in> sigma_sets A {}" then show "a \<in> {{}, A}" 
655 
by induct blast+ 

656 
qed (auto intro: sigma_sets.Empty sigma_sets_top) 

657 

658 
lemma sigma_sets_single[simp]: "sigma_sets A {A} = {{}, A}" 

659 
proof (intro set_eqI iffI) 

660 
fix x assume "x \<in> sigma_sets A {A}" 

661 
then show "x \<in> {{}, A}" 

662 
by induct blast+ 

40859  663 
next 
47694  664 
fix x assume "x \<in> {{}, A}" 
665 
then show "x \<in> sigma_sets A {A}" 

40859  666 
by (auto intro: sigma_sets.Empty sigma_sets_top) 
667 
qed 

668 

42987  669 
lemma sigma_sets_sigma_sets_eq: 
670 
"M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M" 

47694  671 
by (rule sigma_algebra.sigma_sets_eq[OF sigma_algebra_sigma_sets, of M S]) auto 
42987  672 

42984  673 
lemma sigma_sets_singleton: 
674 
assumes "X \<subseteq> S" 

675 
shows "sigma_sets S { X } = { {}, X, S  X, S }" 

676 
proof  

47694  677 
interpret sigma_algebra S "{ {}, X, S  X, S }" 
42984  678 
by (rule sigma_algebra_single_set) fact 
679 
have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S  X, S }" 

680 
by (rule sigma_sets_subseteq) simp 

681 
moreover have "\<dots> = { {}, X, S  X, S }" 

47694  682 
using sigma_sets_eq by simp 
42984  683 
moreover 
684 
{ fix A assume "A \<in> { {}, X, S  X, S }" 

685 
then have "A \<in> sigma_sets S { X }" 

47694  686 
by (auto intro: sigma_sets.intros(2) sigma_sets_top) } 
42984  687 
ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S  X, S }" 
688 
by (intro antisym) auto 

47694  689 
with sigma_sets_eq show ?thesis by simp 
42984  690 
qed 
691 

42863  692 
lemma restricted_sigma: 
47694  693 
assumes S: "S \<in> sigma_sets \<Omega> M" and M: "M \<subseteq> Pow \<Omega>" 
694 
shows "algebra.restricted_space (sigma_sets \<Omega> M) S = 

695 
sigma_sets S (algebra.restricted_space M S)" 

42863  696 
proof  
697 
from S sigma_sets_into_sp[OF M] 

47694  698 
have "S \<in> sigma_sets \<Omega> M" "S \<subseteq> \<Omega>" by auto 
42863  699 
from sigma_sets_Int[OF this] 
47694  700 
show ?thesis by simp 
42863  701 
qed 
702 

42987  703 
lemma sigma_sets_vimage_commute: 
47694  704 
assumes X: "X \<in> \<Omega> \<rightarrow> \<Omega>'" 
705 
shows "{X ` A \<inter> \<Omega> A. A \<in> sigma_sets \<Omega>' M'} 

706 
= sigma_sets \<Omega> {X ` A \<inter> \<Omega> A. A \<in> M'}" (is "?L = ?R") 

42987  707 
proof 
708 
show "?L \<subseteq> ?R" 

709 
proof clarify 

47694  710 
fix A assume "A \<in> sigma_sets \<Omega>' M'" 
711 
then show "X ` A \<inter> \<Omega> \<in> ?R" 

42987  712 
proof induct 
713 
case Empty then show ?case 

714 
by (auto intro!: sigma_sets.Empty) 

715 
next 

716 
case (Compl B) 

47694  717 
have [simp]: "X ` (\<Omega>'  B) \<inter> \<Omega> = \<Omega>  (X ` B \<inter> \<Omega>)" 
42987  718 
by (auto simp add: funcset_mem [OF X]) 
719 
with Compl show ?case 

720 
by (auto intro!: sigma_sets.Compl) 

721 
next 

722 
case (Union F) 

723 
then show ?case 

724 
by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps 

725 
intro!: sigma_sets.Union) 

47694  726 
qed auto 
42987  727 
qed 
728 
show "?R \<subseteq> ?L" 

729 
proof clarify 

730 
fix A assume "A \<in> ?R" 

47694  731 
then show "\<exists>B. A = X ` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" 
42987  732 
proof induct 
733 
case (Basic B) then show ?case by auto 

734 
next 

735 
case Empty then show ?case 

47694  736 
by (auto intro!: sigma_sets.Empty exI[of _ "{}"]) 
42987  737 
next 
738 
case (Compl B) 

47694  739 
then obtain A where A: "B = X ` A \<inter> \<Omega>" "A \<in> sigma_sets \<Omega>' M'" by auto 
740 
then have [simp]: "\<Omega>  B = X ` (\<Omega>'  A) \<inter> \<Omega>" 

42987  741 
by (auto simp add: funcset_mem [OF X]) 
742 
with A(2) show ?case 

47694  743 
by (auto intro: sigma_sets.Compl) 
42987  744 
next 
745 
case (Union F) 

47694  746 
then have "\<forall>i. \<exists>B. F i = X ` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" by auto 
42987  747 
from choice[OF this] guess A .. note A = this 
748 
with A show ?case 

47694  749 
by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union) 
42987  750 
qed 
751 
qed 

752 
qed 

753 

50387  754 
subsection "Disjoint families" 
38656  755 

756 
definition 

757 
disjoint_family_on where 

758 
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" 

759 

760 
abbreviation 

761 
"disjoint_family A \<equiv> disjoint_family_on A UNIV" 

762 

763 
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B" 

764 
by blast 

765 

766 
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A  B) = {}" 

767 
by blast 

768 

769 
lemma Int_Diff_Un: "A \<inter> B \<union> (A  B) = A" 

770 
by blast 

771 

772 
lemma disjoint_family_subset: 

773 
"disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B" 

774 
by (force simp add: disjoint_family_on_def) 

775 

40859  776 
lemma disjoint_family_on_bisimulation: 
777 
assumes "disjoint_family_on f S" 

778 
and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}" 

779 
shows "disjoint_family_on g S" 

780 
using assms unfolding disjoint_family_on_def by auto 

781 

38656  782 
lemma disjoint_family_on_mono: 
783 
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A" 

784 
unfolding disjoint_family_on_def by auto 

785 

786 
lemma disjoint_family_Suc: 

787 
assumes Suc: "!!n. A n \<subseteq> A (Suc n)" 

788 
shows "disjoint_family (\<lambda>i. A (Suc i)  A i)" 

789 
proof  

790 
{ 

791 
fix m 

792 
have "!!n. A n \<subseteq> A (m+n)" 

793 
proof (induct m) 

794 
case 0 show ?case by simp 

795 
next 

796 
case (Suc m) thus ?case 

797 
by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans) 

798 
qed 

799 
} 

800 
hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n" 

801 
by (metis add_commute le_add_diff_inverse nat_less_le) 

802 
thus ?thesis 

803 
by (auto simp add: disjoint_family_on_def) 

804 
(metis insert_absorb insert_subset le_SucE le_antisym not_leE) 

805 
qed 

806 

39092  807 
lemma setsum_indicator_disjoint_family: 
808 
fixes f :: "'d \<Rightarrow> 'e::semiring_1" 

809 
assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P" 

810 
shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j" 

811 
proof  

812 
have "P \<inter> {i. x \<in> A i} = {j}" 

813 
using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def 

814 
by auto 

815 
thus ?thesis 

816 
unfolding indicator_def 

817 
by (simp add: if_distrib setsum_cases[OF `finite P`]) 

818 
qed 

819 

38656  820 
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set " 
821 
where "disjointed A n = A n  (\<Union>i\<in>{0..<n}. A i)" 

822 

823 
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" 

824 
proof (induct n) 

825 
case 0 show ?case by simp 

826 
next 

827 
case (Suc n) 

828 
thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 

829 
qed 

830 

831 
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" 

832 
apply (rule UN_finite2_eq [where k=0]) 

833 
apply (simp add: finite_UN_disjointed_eq) 

834 
done 

835 

836 
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" 

837 
by (auto simp add: disjointed_def) 

838 

839 
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" 

840 
by (simp add: disjoint_family_on_def) 

841 
(metis neq_iff Int_commute less_disjoint_disjointed) 

842 

843 
lemma disjointed_subset: "disjointed A n \<subseteq> A n" 

844 
by (auto simp add: disjointed_def) 

845 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

846 
lemma (in ring_of_sets) UNION_in_sets: 
38656  847 
fixes A:: "nat \<Rightarrow> 'a set" 
47694  848 
assumes A: "range A \<subseteq> M" 
849 
shows "(\<Union>i\<in>{0..<n}. A i) \<in> M" 

38656  850 
proof (induct n) 
851 
case 0 show ?case by simp 

852 
next 

853 
case (Suc n) 

854 
thus ?case 

855 
by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) 

856 
qed 

857 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

858 
lemma (in ring_of_sets) range_disjointed_sets: 
47694  859 
assumes A: "range A \<subseteq> M" 
860 
shows "range (disjointed A) \<subseteq> M" 

38656  861 
proof (auto simp add: disjointed_def) 
862 
fix n 

47694  863 
show "A n  (\<Union>i\<in>{0..<n}. A i) \<in> M" using UNION_in_sets 
38656  864 
by (metis A Diff UNIV_I image_subset_iff) 
865 
qed 

866 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

867 
lemma (in algebra) range_disjointed_sets': 
47694  868 
"range A \<subseteq> M \<Longrightarrow> range (disjointed A) \<subseteq> M" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

869 
using range_disjointed_sets . 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

870 

42145  871 
lemma disjointed_0[simp]: "disjointed A 0 = A 0" 
872 
by (simp add: disjointed_def) 

873 

874 
lemma incseq_Un: 

875 
"incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n" 

876 
unfolding incseq_def by auto 

877 

878 
lemma disjointed_incseq: 

879 
"incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n)  A n" 

880 
using incseq_Un[of A] 

881 
by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) 

882 

38656  883 
lemma sigma_algebra_disjoint_iff: 
47694  884 
"sigma_algebra \<Omega> M \<longleftrightarrow> algebra \<Omega> M \<and> 
885 
(\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" 

38656  886 
proof (auto simp add: sigma_algebra_iff) 
887 
fix A :: "nat \<Rightarrow> 'a set" 

47694  888 
assume M: "algebra \<Omega> M" 
889 
and A: "range A \<subseteq> M" 

890 
and UnA: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M" 

891 
hence "range (disjointed A) \<subseteq> M \<longrightarrow> 

38656  892 
disjoint_family (disjointed A) \<longrightarrow> 
47694  893 
(\<Union>i. disjointed A i) \<in> M" by blast 
894 
hence "(\<Union>i. disjointed A i) \<in> M" 

895 
by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed) 

896 
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq) 

897 
qed 

898 

47762  899 
lemma disjoint_family_on_disjoint_image: 
900 
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)" 

901 
unfolding disjoint_family_on_def disjoint_def by force 

902 

903 
lemma disjoint_image_disjoint_family_on: 

904 
assumes d: "disjoint (A ` I)" and i: "inj_on A I" 

905 
shows "disjoint_family_on A I" 

906 
unfolding disjoint_family_on_def 

907 
proof (intro ballI impI) 

908 
fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m" 

909 
with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}" 

910 
by (intro disjointD[OF d]) auto 

911 
qed 

912 

50387  913 
subsection {* Ring generated by a semiring *} 
47762  914 

915 
definition (in semiring_of_sets) 

916 
"generated_ring = { \<Union>C  C. C \<subseteq> M \<and> finite C \<and> disjoint C }" 

917 

918 
lemma (in semiring_of_sets) generated_ringE[elim?]: 

919 
assumes "a \<in> generated_ring" 

920 
obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" 

921 
using assms unfolding generated_ring_def by auto 

922 

923 
lemma (in semiring_of_sets) generated_ringI[intro?]: 

924 
assumes "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" 

925 
shows "a \<in> generated_ring" 

926 
using assms unfolding generated_ring_def by auto 

927 

928 
lemma (in semiring_of_sets) generated_ringI_Basic: 

929 
"A \<in> M \<Longrightarrow> A \<in> generated_ring" 

930 
by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def) 

931 

932 
lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]: 

933 
assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" 

934 
and "a \<inter> b = {}" 

935 
shows "a \<union> b \<in> generated_ring" 

936 
proof  

937 
from a guess Ca .. note Ca = this 

938 
from b guess Cb .. note Cb = this 

939 
show ?thesis 

940 
proof 

941 
show "disjoint (Ca \<union> Cb)" 

942 
using `a \<inter> b = {}` Ca Cb by (auto intro!: disjoint_union) 

943 
qed (insert Ca Cb, auto) 

944 
qed 

945 

946 
lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring" 

947 
by (auto simp: generated_ring_def disjoint_def) 

948 

949 
lemma (in semiring_of_sets) generated_ring_disjoint_Union: 

950 
assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring" 

951 
using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty) 

952 

953 
lemma (in semiring_of_sets) generated_ring_disjoint_UNION: 

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

955 
unfolding SUP_def by (intro generated_ring_disjoint_Union) auto 

956 

957 
lemma (in semiring_of_sets) generated_ring_Int: 

958 
assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" 

959 
shows "a \<inter> b \<in> generated_ring" 

960 
proof  

961 
from a guess Ca .. note Ca = this 

962 
from b guess Cb .. note Cb = this 

963 
def C \<equiv> "(\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)" 

964 
show ?thesis 

965 
proof 

966 
show "disjoint C" 

967 
proof (simp add: disjoint_def C_def, intro ballI impI) 

968 
fix a1 b1 a2 b2 assume sets: "a1 \<in> Ca" "b1 \<in> Cb" "a2 \<in> Ca" "b2 \<in> Cb" 

969 
assume "a1 \<inter> b1 \<noteq> a2 \<inter> b2" 

970 
then have "a1 \<noteq> a2 \<or> b1 \<noteq> b2" by auto 

971 
then show "(a1 \<inter> b1) \<inter> (a2 \<inter> b2) = {}" 

972 
proof 

973 
assume "a1 \<noteq> a2" 

974 
with sets Ca have "a1 \<inter> a2 = {}" 

975 
by (auto simp: disjoint_def) 

976 
then show ?thesis by auto 

977 
next 

978 
assume "b1 \<noteq> b2" 

979 
with sets Cb have "b1 \<inter> b2 = {}" 

980 
by (auto simp: disjoint_def) 

981 
then show ?thesis by auto 

982 
qed 

983 
qed 

984 
qed (insert Ca Cb, auto simp: C_def) 

985 
qed 

986 

987 
lemma (in semiring_of_sets) generated_ring_Inter: 

988 
assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring" 

989 
using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int) 

990 

991 
lemma (in semiring_of_sets) generated_ring_INTER: 

992 
"finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring" 

993 
unfolding INF_def by (intro generated_ring_Inter) auto 

994 

995 
lemma (in semiring_of_sets) generating_ring: 

996 
"ring_of_sets \<Omega> generated_ring" 

997 
proof (rule ring_of_setsI) 

998 
let ?R = generated_ring 

999 
show "?R \<subseteq> Pow \<Omega>" 

1000 
using sets_into_space by (auto simp: generated_ring_def generated_ring_empty) 

1001 
show "{} \<in> ?R" by (rule generated_ring_empty) 

1002 

1003 
{ fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this 

1004 
fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this 

1005 

1006 
show "a  b \<in> ?R" 

1007 
proof cases 

1008 
assume "Cb = {}" with Cb `a \<in> ?R` show ?thesis 

1009 
by simp 

1010 
next 

1011 
assume "Cb \<noteq> {}" 

1012 
with Ca Cb have "a  b = (\<Union>a'\<in>Ca. \<Inter>b'\<in>Cb. a'  b')" by auto 

1013 
also have "\<dots> \<in> ?R" 

1014 
proof (intro generated_ring_INTER generated_ring_disjoint_UNION) 

1015 
fix a b assume "a \<in> Ca" "b \<in> Cb" 

1016 
with Ca Cb Diff_cover[of a b] show "a  b \<in> ?R" 

1017 
by (auto simp add: generated_ring_def) 

1018 
next 

1019 
show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a'  b')`Ca)" 

1020 
using Ca by (auto simp add: disjoint_def `Cb \<noteq> {}`) 

1021 
next 

1022 
show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+ 

1023 
qed 

1024 
finally show "a  b \<in> ?R" . 

1025 
qed } 

1026 
note Diff = this 

1027 

1028 
fix a b assume sets: "a \<in> ?R" "b \<in> ?R" 

1029 
have "a \<union> b = (a  b) \<union> (a \<inter> b) \<union> (b  a)" by auto 

1030 
also have "\<dots> \<in> ?R" 

1031 
by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto 

1032 
finally show "a \<union> b \<in> ?R" . 

1033 
qed 

1034 

1035 
lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \<Omega> generated_ring = sigma_sets \<Omega> M" 

1036 
proof 

1037 
interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M" 

1038 
using space_closed by (rule sigma_algebra_sigma_sets) 

1039 
show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M" 

1040 
by (blast intro!: sigma_sets_mono elim: generated_ringE) 

1041 
qed (auto intro!: generated_ringI_Basic sigma_sets_mono) 

1042 

50387  1043 
subsection {* Measure type *} 
47694  1044 

1045 
definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where 

1046 
"positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)" 

1047 

1048 
definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where 

1049 
"countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> 

1050 
(\<Sum>i. f (A i)) = f (\<Union>i. A i))" 

1051 

1052 
definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where 

1053 
"measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>" 

1054 

49834  1055 
typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }" 
47694  1056 
proof 
1057 
have "sigma_algebra UNIV {{}, UNIV}" 

47762  1058 
by (auto simp: sigma_algebra_iff2) 
47694  1059 
then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} " 
1060 
by (auto simp: measure_space_def positive_def countably_additive_def) 

1061 
qed 

1062 

1063 
definition space :: "'a measure \<Rightarrow> 'a set" where 

1064 
"space M = fst (Rep_measure M)" 

1065 

1066 
definition sets :: "'a measure \<Rightarrow> 'a set set" where 

1067 
"sets M = fst (snd (Rep_measure M))" 

1068 

1069 
definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ereal" where 

1070 
"emeasure M = snd (snd (Rep_measure M))" 

1071 

1072 
definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where 

1073 
"measure M A = real (emeasure M A)" 

1074 

1075 
declare [[coercion sets]] 

1076 

1077 
declare [[coercion measure]] 

1078 

1079 
declare [[coercion emeasure]] 

1080 

1081 
lemma measure_space: "measure_space (space M) (sets M) (emeasure M)" 

1082 
by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse) 

1083 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50096
diff
changeset

1084 
interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure" 
47694  1085 
using measure_space[of M] by (auto simp: measure_space_def) 
1086 

1087 
definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where 

1088 
"measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, sigma_sets \<Omega> A, 

1089 
\<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)" 

1090 

1091 
abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)" 

1092 

1093 
lemma measure_space_0: "A \<subseteq> Pow \<Omega> \<Longrightarrow> measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>x. 0)" 

1094 
unfolding measure_space_def 

1095 
by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def) 

1096 

1097 
lemma (in ring_of_sets) positive_cong_eq: 

1098 
"(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> positive M \<mu>' = positive M \<mu>" 

1099 
by (auto simp add: positive_def) 

1100 

1101 
lemma (in sigma_algebra) countably_additive_eq: 

1102 
"(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> countably_additive M \<mu>' = countably_additive M \<mu>" 

1103 
unfolding countably_additive_def 

1104 
by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq) 

1105 

1106 
lemma measure_space_eq: 

1107 
assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a" 

1108 
shows "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'" 

1109 
proof  

1110 
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets) 

1111 
from positive_cong_eq[OF eq, of "\<lambda>i. i"] countably_additive_eq[OF eq, of "\<lambda>i. i"] show ?thesis 

1112 
by (auto simp: measure_space_def) 

1113 
qed 

1114 

1115 
lemma measure_of_eq: 

1116 
assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "(\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a)" 

1117 
shows "measure_of \<Omega> A \<mu> = measure_of \<Omega> A \<mu>'" 

1118 
proof  

1119 
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'" 

1120 
using assms by (rule measure_space_eq) 

1121 
with eq show ?thesis 

1122 
by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure]) 

1123 
qed 

1124 

1125 
lemma 

1126 
assumes A: "A \<subseteq> Pow \<Omega>" 

1127 
shows sets_measure_of[simp]: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A" (is ?sets) 

1128 
and space_measure_of[simp]: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space) 

1129 
proof  

1130 
have "?sets \<and> ?space" 

1131 
proof cases 

1132 
assume "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>" 

1133 
moreover have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) 

1134 
(\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)" 

1135 
using A by (rule measure_space_eq) auto 

1136 
ultimately show "?sets \<and> ?space" 

1137 
by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def) 

1138 
next 

1139 
assume "\<not> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>" 

1140 
with A show "?sets \<and> ?space" 

1141 
by (auto simp: Abs_measure_inverse measure_of_def sets_def space_def measure_space_0) 

1142 
qed 

1143 
then show ?sets ?space by auto 

1144 
qed 

1145 

1146 
lemma (in sigma_algebra) sets_measure_of_eq[simp]: 

1147 
"sets (measure_of \<Omega> M \<mu>) = M" 

1148 
using space_closed by (auto intro!: sigma_sets_eq) 

1149 

1150 
lemma (in sigma_algebra) space_measure_of_eq[simp]: 

1151 
"space (measure_of \<Omega> M \<mu>) = \<Omega>" 

1152 
using space_closed by (auto intro!: sigma_sets_eq) 

1153 

1154 
lemma measure_of_subset: 

1155 
"M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')" 

1156 
by (auto intro!: sigma_sets_subseteq) 

1157 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1158 
lemma sigma_sets_mono'': 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1159 
assumes "A \<in> sigma_sets C D" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1160 
assumes "B \<subseteq> D" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1161 
assumes "D \<subseteq> Pow C" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1162 
shows "sigma_sets A B \<subseteq> sigma_sets C D" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1163 
proof 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1164 
fix x assume "x \<in> sigma_sets A B" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1165 
thus "x \<in> sigma_sets C D" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1166 
proof induct 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1167 
case (Basic a) with assms have "a \<in> D" by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1168 
thus ?case .. 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1169 
next 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1170 
case Empty show ?case by (rule sigma_sets.Empty) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1171 
next 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1172 
from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`]) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1173 
moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`]) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1174 
ultimately have "A  a \<in> sets (sigma C D)" .. 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1175 
thus ?case by (subst (asm) sets_measure_of[OF `D \<subseteq> Pow C`]) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1176 
next 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1177 
case (Union a) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1178 
thus ?case by (intro sigma_sets.Union) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1179 
qed 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1180 
qed 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50244
diff
changeset

1181 

47756  1182 
lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)" 
47694  1183 
by auto 
1184 

50387  1185 
subsection {* Constructing simple @{typ "'a measure"} *} 
47694  1186 

1187 
lemma emeasure_measure_of: 

1188 
assumes M: "M = measure_of \<Omega> A \<mu>" 

1189 
assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>" 

1190 
assumes X: "X \<in> sets M" 

1191 
shows "emeasure M X = \<mu> X" 

1192 
proof  

1193 
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact 

1194 
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>" 

1195 
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets) 

1196 
moreover have "measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0) 

1197 
= measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>" 

1198 
using ms(1) by (rule measure_space_eq) auto 

1199 
moreover have "X \<in> sigma_sets \<Omega> A" 

1200 
using X M ms by simp 

1201 
ultimately show ?thesis 

1202 
unfolding emeasure_def measure_of_def M 

1203 
by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) 

1204 
qed 

1205 

1206 
lemma emeasure_measure_of_sigma: 

1207 
assumes ms: "sigma_algebra \<Omega> M" "positive M \<mu>" "countably_additive M \<mu>" 

1208 
assumes A: "A \<in> M" 

1209 
shows "emeasure (measure_of \<Omega> M \<mu>) A = \<mu> A" 

1210 
proof  

1211 
interpret sigma_algebra \<Omega> M by fact 

1212 
have "measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" 

1213 
using ms sigma_sets_eq by (simp add: measure_space_def) 

1214 
moreover have "measure_space \<Omega> (sigma_sets \<Omega> M) (\<lambda>a. if a \<in> sigma_sets \<Omega> M then \<mu> a else 0) 

1215 
= measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" 

1216 
using space_closed by (rule measure_space_eq) auto 

1217 
ultimately show ?thesis using A 

1218 
unfolding emeasure_def measure_of_def 

1219 
by (subst Abs_measure_inverse) (simp_all add: sigma_sets_eq) 

1220 
qed 

1221 

1222 
lemma measure_cases[cases type: measure]: 

1223 
obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>A. \<mu> a = 0" "measure_space \<Omega> A \<mu>" 

1224 
by atomize_elim (cases x, auto) 

1225 

1226 
lemma sets_eq_imp_space_eq: 

1227 
"sets M = sets M' \<Longrightarrow> space M = space M'" 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50096
diff
changeset

1228 
using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M'] 
47694  1229 
by blast 
1230 

1231 
lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0" 

1232 
by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def) 