author  hoelzl 
Wed, 01 Dec 2010 19:20:30 +0100  
changeset 40859  de0b30e6c2d2 
parent 40702  cf26dd7395e4 
child 40869  251df82c0088 
permissions  rwrr 
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 
38656  3 
Plus material from the Hurd/Coble measure theory development, 
33271
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 

39092  9 
theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin 
33271
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 

38656  21 
record 'a algebra = 
22 
space :: "'a set" 

33271
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 = 
40859  26 
fixes M :: "'a algebra" 
33271
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 

38656  38 
lemma (in algebra) Int [intro]: 
33271
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  
38656  41 
have "((space M  a) \<union> (space M  b)) \<in> sets M" 
33271
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 
38656  44 
have "a \<inter> b = space M  ((space M  a) \<union> (space M  b))" 
33271
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 

38656  51 
lemma (in algebra) Diff [intro]: 
33271
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 

38656  63 
lemma (in algebra) finite_union [intro]: 
33271
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" 
38656  65 
by (induct set: finite) (auto simp add: Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

66 

38656  67 
lemma algebra_iff_Int: 
68 
"algebra M \<longleftrightarrow> 

69 
sets M \<subseteq> Pow (space M) & {} \<in> sets M & 

70 
(\<forall>a \<in> sets M. space M  a \<in> sets M) & 

71 
(\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" 

72 
proof (auto simp add: algebra.Int, auto simp add: algebra_def) 

73 
fix a b 

74 
assume ab: "sets M \<subseteq> Pow (space M)" 

75 
"\<forall>a\<in>sets M. space M  a \<in> sets M" 

76 
"\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M" 

77 
"a \<in> sets M" "b \<in> sets M" 

78 
hence "a \<union> b = space M  ((space M  a) \<inter> (space M  b))" 

79 
by blast 

80 
also have "... \<in> sets M" 

81 
by (metis ab) 

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

83 
qed 

84 

85 
lemma (in algebra) insert_in_sets: 

86 
assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M" 

87 
proof  

88 
have "{x} \<union> A \<in> sets M" using assms by (rule Un) 

89 
thus ?thesis by auto 

90 
qed 

91 

92 
lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x" 

93 
by (metis Int_absorb1 sets_into_space) 

94 

95 
lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x" 

96 
by (metis Int_absorb2 sets_into_space) 

97 

39092  98 
section {* Restricted algebras *} 
99 

100 
abbreviation (in algebra) 

101 
"restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M \<rparr>" 

102 

38656  103 
lemma (in algebra) restricted_algebra: 
39092  104 
assumes "A \<in> sets M" shows "algebra (restricted_space A)" 
38656  105 
using assms by unfold_locales auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

106 

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

107 
subsection {* Sigma Algebras *} 
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 
locale sigma_algebra = algebra + 
38656  110 
assumes countable_nat_UN [intro]: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

111 
"!!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 

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

115 
shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow> 

116 
(range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)" 

117 
proof  

118 
let ?A' = "A \<circ> from_nat" 

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

120 
proof safe 

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

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

123 
next 

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

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

126 
qed 

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

40702  128 
using surj_from_nat 
38656  129 
by (auto simp: image_compose intro!: imageI) 
130 
show ?thesis unfolding * ** .. 

131 
qed 

132 

133 
lemma (in sigma_algebra) countable_UN[intro]: 

134 
fixes A :: "'i::countable \<Rightarrow> 'a set" 

135 
assumes "A`X \<subseteq> sets M" 

136 
shows "(\<Union>x\<in>X. A x) \<in> sets M" 

137 
proof  

138 
let "?A i" = "if i \<in> X then A i else {}" 

139 
from assms have "range ?A \<subseteq> sets M" by auto 

140 
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M] 

141 
have "(\<Union>x. ?A x) \<in> sets M" by auto 

142 
moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm) 

143 
ultimately show ?thesis by simp 

144 
qed 

145 

146 
lemma (in sigma_algebra) finite_UN: 

147 
assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M" 

148 
shows "(\<Union>i\<in>I. A i) \<in> sets M" 

149 
using assms by induct auto 

150 

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

151 
lemma (in sigma_algebra) countable_INT [intro]: 
38656  152 
fixes A :: "'i::countable \<Rightarrow> 'a set" 
153 
assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}" 

154 
shows "(\<Inter>i\<in>X. A i) \<in> sets M" 

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

155 
proof  
38656  156 
from A have "\<forall>i\<in>X. A i \<in> sets M" by fast 
157 
hence "space M  (\<Union>i\<in>X. space M  A i) \<in> sets M" by blast 

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

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

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

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

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

163 

38656  164 
lemma (in sigma_algebra) finite_INT: 
165 
assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M" 

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

167 
using assms by (induct rule: finite_ne_induct) auto 

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

168 

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

169 
lemma algebra_Pow: 
38656  170 
"algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>" 
171 
by (auto simp add: algebra_def) 

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

172 

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

173 
lemma sigma_algebra_Pow: 
38656  174 
"sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>" 
175 
by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) 

176 

177 
lemma sigma_algebra_iff: 

178 
"sigma_algebra M \<longleftrightarrow> 

179 
algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 

180 
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

181 

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

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

183 

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

184 
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

185 
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

186 

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

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

189 

38656  190 
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
191 
by (simp add: UNION_eq_Union_image range_binary_eq) 

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

192 

38656  193 
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
194 
by (simp add: INTER_eq_Inter_image range_binary_eq) 

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

195 

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

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

197 
"sigma_algebra M \<longleftrightarrow> 
38656  198 
sets M \<subseteq> Pow (space M) \<and> 
199 
{} \<in> sets M \<and> (\<forall>s \<in> sets M. space M  s \<in> sets M) \<and> 

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

200 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 
38656  201 
by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def 
202 
algebra_def Un_range_binary) 

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

203 

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

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

205 

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

206 
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

207 
sets with regard to the properties just postulated. *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

208 

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

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

210 
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

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

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

213 
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

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

215 
 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

216 
 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

217 

40859  218 
definition 
219 
"sigma M = ( space = space M, sets = sigma_sets (space M) (sets M) )" 

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

220 

40859  221 
lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)" 
38656  222 
unfolding sigma_def by simp 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

223 

40859  224 
lemma space_sigma [simp]: "space (sigma M) = space M" 
38656  225 
by (simp add: sigma_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

226 

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

227 
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

228 
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

229 

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

230 
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp" 
38656  231 
by (erule sigma_sets.induct, auto) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

232 

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

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

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

238 

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

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

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

241 
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

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

243 
assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A" 
38656  244 
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

245 
by (rule sigma_sets.Compl) 
38656  246 
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

247 
by (rule sigma_sets.Union) 
38656  248 
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

249 
by (rule sigma_sets.Compl) 
38656  250 
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

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

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

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

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

256 

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

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

259 
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

260 
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

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

262 
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

263 
by (simp add: sigma_sets.intros sigma_sets_top) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

264 
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

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

266 
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

267 
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

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

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

270 

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

271 
lemma (in sigma_algebra) sigma_sets_subset: 
38656  272 
assumes a: "a \<subseteq> sets M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

273 
shows "sigma_sets (space M) a \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

276 
assume "x \<in> sigma_sets (space M) a" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

277 
from this show "x \<in> sets M" 
38656  278 
by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

280 

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

281 
lemma (in sigma_algebra) sigma_sets_eq: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

282 
"sigma_sets (space M) (sets M) = sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

284 
show "sets M \<subseteq> sigma_sets (space M) (sets M)" 
37032  285 
by (metis Set.subsetI sigma_sets.Basic) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

287 
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

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

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

290 

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

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

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

293 
apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def 
38656  294 
algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

295 
apply (blast dest: sigma_sets_into_sp) 
37032  296 
apply (rule sigma_sets.Union, fast) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

298 

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

299 
lemma sigma_algebra_sigma: 
40859  300 
"sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)" 
38656  301 
apply (rule sigma_algebra_sigma_sets) 
302 
apply (auto simp add: sigma_def) 

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

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

304 

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

305 
lemma (in sigma_algebra) sigma_subset: 
40859  306 
"sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

307 
by (simp add: sigma_def sigma_sets_subset) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

308 

40859  309 
lemma sigma_sets_least_sigma_algebra: 
310 
assumes "A \<subseteq> Pow S" 

311 
shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}" 

312 
proof safe 

313 
fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>" 

314 
and X: "X \<in> sigma_sets S A" 

315 
from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X 

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

317 
next 

318 
fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}" 

319 
then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B" 

320 
by simp 

321 
have "A \<subseteq> sigma_sets S A" using assms 

322 
by (auto intro!: sigma_sets.Basic) 

323 
moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>" 

324 
using assms by (intro sigma_algebra_sigma_sets[of A]) auto 

325 
ultimately show "X \<in> sigma_sets S A" by auto 

326 
qed 

327 

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

330 
assumes "S \<in> sets M" 

331 
and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r") 

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

333 
proof  

334 
{ fix i have "A i \<in> ?r" using * by auto 

335 
hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto 

336 
hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto } 

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

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

339 
qed 

340 

341 
lemma (in sigma_algebra) restricted_sigma_algebra: 

342 
assumes "S \<in> sets M" 

39092  343 
shows "sigma_algebra (restricted_space S)" 
38656  344 
unfolding sigma_algebra_def sigma_algebra_axioms_def 
345 
proof safe 

39092  346 
show "algebra (restricted_space S)" using restricted_algebra[OF assms] . 
38656  347 
next 
39092  348 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (restricted_space S)" 
38656  349 
from restriction_in_sets[OF assms this[simplified]] 
39092  350 
show "(\<Union>i. A i) \<in> sets (restricted_space S)" by simp 
38656  351 
qed 
352 

40859  353 
lemma sigma_sets_Int: 
354 
assumes "A \<in> sigma_sets sp st" 

355 
shows "op \<inter> A ` sigma_sets sp st = sigma_sets (A \<inter> sp) (op \<inter> A ` st)" 

356 
proof (intro equalityI subsetI) 

357 
fix x assume "x \<in> op \<inter> A ` sigma_sets sp st" 

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

359 
then show "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)" 

360 
proof (induct arbitrary: x) 

361 
case (Compl a) 

362 
then show ?case 

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

364 
next 

365 
case (Union a) 

366 
then show ?case 

367 
by (auto intro!: sigma_sets.Union 

368 
simp add: UN_extend_simps simp del: UN_simps) 

369 
qed (auto intro!: sigma_sets.intros) 

370 
next 

371 
fix x assume "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)" 

372 
then show "x \<in> op \<inter> A ` sigma_sets sp st" 

373 
proof induct 

374 
case (Compl a) 

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

376 
then show ?case 

377 
by (force simp add: image_iff intro!: bexI[of _ "sp  x"] sigma_sets.Compl) 

378 
next 

379 
case (Union a) 

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

381 
by (auto simp: image_iff Bex_def) 

382 
from choice[OF this] guess f .. 

383 
then show ?case 

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

385 
simp add: image_iff) 

386 
qed (auto intro!: sigma_sets.intros) 

387 
qed 

388 

389 
lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}" 

390 
proof (intro set_eqI iffI) 

391 
fix x assume "x \<in> sigma_sets {X} {{X}}" 

392 
from sigma_sets_into_sp[OF _ this] 

393 
show "x \<in> {{}, {X}}" by auto 

394 
next 

395 
fix x assume "x \<in> {{}, {X}}" 

396 
then show "x \<in> sigma_sets {X} {{X}}" 

397 
by (auto intro: sigma_sets.Empty sigma_sets_top) 

398 
qed 

399 

38656  400 
section {* Measurable functions *} 
401 

402 
definition 

403 
"measurable A B = {f \<in> space A > space B. \<forall>y \<in> sets B. f ` y \<inter> space A \<in> sets A}" 

404 

405 
lemma (in sigma_algebra) measurable_sigma: 

40859  406 
assumes B: "sets N \<subseteq> Pow (space N)" 
407 
and f: "f \<in> space M > space N" 

408 
and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f ` y) \<inter> space M \<in> sets M" 

409 
shows "f \<in> measurable M (sigma N)" 

38656  410 
proof  
40859  411 
have "sigma_sets (space N) (sets N) \<subseteq> {y . (f ` y) \<inter> space M \<in> sets M & y \<subseteq> space N}" 
38656  412 
proof clarify 
413 
fix x 

40859  414 
assume "x \<in> sigma_sets (space N) (sets N)" 
415 
thus "f ` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N" 

38656  416 
proof induct 
417 
case (Basic a) 

418 
thus ?case 

419 
by (auto simp add: ba) (metis B subsetD PowD) 

420 
next 

421 
case Empty 

422 
thus ?case 

423 
by auto 

424 
next 

425 
case (Compl a) 

40859  426 
have [simp]: "f ` space N \<inter> space M = space M" 
38656  427 
by (auto simp add: funcset_mem [OF f]) 
428 
thus ?case 

429 
by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl) 

430 
next 

431 
case (Union a) 

432 
thus ?case 

40859  433 
by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast 
38656  434 
qed 
435 
qed 

436 
thus ?thesis 

437 
by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 

438 
(auto simp add: sigma_def) 

439 
qed 

440 

441 
lemma measurable_cong: 

442 
assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w" 

443 
shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'" 

444 
unfolding measurable_def using assms 

445 
by (simp cong: vimage_inter_cong Pi_cong) 

446 

447 
lemma measurable_space: 

448 
"f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A" 

449 
unfolding measurable_def by auto 

450 

451 
lemma measurable_sets: 

452 
"f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f ` S \<inter> space M \<in> sets M" 

453 
unfolding measurable_def by auto 

454 

455 
lemma (in sigma_algebra) measurable_subset: 

40859  456 
"(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)" 
38656  457 
by (auto intro: measurable_sigma measurable_sets measurable_space) 
458 

459 
lemma measurable_eqI: 

460 
"\<lbrakk> space m1 = space m1' ; space m2 = space m2' ; 

461 
sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk> 

462 
\<Longrightarrow> measurable m1 m2 = measurable m1' m2'" 

463 
by (simp add: measurable_def sigma_algebra_iff2) 

464 

465 
lemma (in sigma_algebra) measurable_const[intro, simp]: 

466 
assumes "c \<in> space M'" 

467 
shows "(\<lambda>x. c) \<in> measurable M M'" 

468 
using assms by (auto simp add: measurable_def) 

469 

470 
lemma (in sigma_algebra) measurable_If: 

471 
assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'" 

472 
assumes P: "{x\<in>space M. P x} \<in> sets M" 

473 
shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'" 

474 
unfolding measurable_def 

475 
proof safe 

476 
fix x assume "x \<in> space M" 

477 
thus "(if P x then f x else g x) \<in> space M'" 

478 
using measure unfolding measurable_def by auto 

479 
next 

480 
fix A assume "A \<in> sets M'" 

481 
hence *: "(\<lambda>x. if P x then f x else g x) ` A \<inter> space M = 

482 
((f ` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union> 

483 
((g ` A \<inter> space M) \<inter> (space M  {x\<in>space M. P x}))" 

484 
using measure unfolding measurable_def by (auto split: split_if_asm) 

485 
show "(\<lambda>x. if P x then f x else g x) ` A \<inter> space M \<in> sets M" 

486 
using `A \<in> sets M'` measure P unfolding * measurable_def 

487 
by (auto intro!: Un) 

488 
qed 

489 

490 
lemma (in sigma_algebra) measurable_If_set: 

491 
assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'" 

492 
assumes P: "A \<in> sets M" 

493 
shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'" 

494 
proof (rule measurable_If[OF measure]) 

495 
have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto 

496 
thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto 

497 
qed 

498 

499 
lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M" 

500 
by (auto simp add: measurable_def) 

501 

502 
lemma measurable_comp[intro]: 

503 
fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 

504 
shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c" 

505 
apply (auto simp add: measurable_def vimage_compose) 

506 
apply (subgoal_tac "f ` g ` y \<inter> space a = f ` (g ` y \<inter> space b) \<inter> space a") 

507 
apply force+ 

508 
done 

509 

510 
lemma measurable_strong: 

511 
fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 

512 
assumes f: "f \<in> measurable a b" and g: "g \<in> (space b > space c)" 

513 
and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c" 

514 
and t: "f ` (space a) \<subseteq> t" 

515 
and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g ` s) \<inter> t \<in> sets b" 

516 
shows "(g o f) \<in> measurable a c" 

517 
proof  

518 
have fab: "f \<in> (space a > space b)" 

519 
and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f ` y) \<inter> (space a) \<in> sets a" using f 

520 
by (auto simp add: measurable_def) 

521 
have eq: "f ` g ` y \<inter> space a = f ` (g ` y \<inter> t) \<inter> space a" using t 

522 
by force 

523 
show ?thesis 

524 
apply (auto simp add: measurable_def vimage_compose a c) 

525 
apply (metis funcset_mem fab g) 

526 
apply (subst eq, metis ba cb) 

527 
done 

528 
qed 

529 

530 
lemma measurable_mono1: 

531 
"a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr> 

532 
\<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c" 

533 
by (auto simp add: measurable_def) 

534 

535 
lemma measurable_up_sigma: 

40859  536 
"measurable A M \<subseteq> measurable (sigma A) M" 
38656  537 
unfolding measurable_def 
538 
by (auto simp: sigma_def intro: sigma_sets.Basic) 

539 

540 
lemma (in sigma_algebra) measurable_range_reduce: 

541 
"\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk> 

542 
\<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>" 

543 
by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast 

544 

545 
lemma (in sigma_algebra) measurable_Pow_to_Pow: 

546 
"(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>" 

547 
by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def) 

548 

549 
lemma (in sigma_algebra) measurable_Pow_to_Pow_image: 

550 
"sets M = Pow (space M) 

551 
\<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>" 

552 
by (simp add: measurable_def sigma_algebra_Pow) intro_locales 

553 

40859  554 
lemma (in sigma_algebra) measurable_iff_sigma: 
555 
assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E" 

556 
shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f ` A \<inter> space M \<in> sets M)" 

557 
using measurable_sigma[OF assms] 

558 
by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros) 

38656  559 

560 
section "Disjoint families" 

561 

562 
definition 

563 
disjoint_family_on where 

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

565 

566 
abbreviation 

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

568 

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

570 
by blast 

571 

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

573 
by blast 

574 

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

576 
by blast 

577 

578 
lemma disjoint_family_subset: 

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

580 
by (force simp add: disjoint_family_on_def) 

581 

40859  582 
lemma disjoint_family_on_bisimulation: 
583 
assumes "disjoint_family_on f S" 

584 
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 = {}" 

585 
shows "disjoint_family_on g S" 

586 
using assms unfolding disjoint_family_on_def by auto 

587 

38656  588 
lemma disjoint_family_on_mono: 
589 
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A" 

590 
unfolding disjoint_family_on_def by auto 

591 

592 
lemma disjoint_family_Suc: 

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

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

595 
proof  

596 
{ 

597 
fix m 

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

599 
proof (induct m) 

600 
case 0 show ?case by simp 

601 
next 

602 
case (Suc m) thus ?case 

603 
by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans) 

604 
qed 

605 
} 

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

607 
by (metis add_commute le_add_diff_inverse nat_less_le) 

608 
thus ?thesis 

609 
by (auto simp add: disjoint_family_on_def) 

610 
(metis insert_absorb insert_subset le_SucE le_antisym not_leE) 

611 
qed 

612 

39092  613 
lemma setsum_indicator_disjoint_family: 
614 
fixes f :: "'d \<Rightarrow> 'e::semiring_1" 

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

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

617 
proof  

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

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

620 
by auto 

621 
thus ?thesis 

622 
unfolding indicator_def 

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

624 
qed 

625 

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

628 

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

630 
proof (induct n) 

631 
case 0 show ?case by simp 

632 
next 

633 
case (Suc n) 

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

635 
qed 

636 

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

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

639 
apply (simp add: finite_UN_disjointed_eq) 

640 
done 

641 

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

643 
by (auto simp add: disjointed_def) 

644 

645 
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" 

646 
by (simp add: disjoint_family_on_def) 

647 
(metis neq_iff Int_commute less_disjoint_disjointed) 

648 

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

650 
by (auto simp add: disjointed_def) 

651 

652 
lemma (in algebra) UNION_in_sets: 

653 
fixes A:: "nat \<Rightarrow> 'a set" 

654 
assumes A: "range A \<subseteq> sets M " 

655 
shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" 

656 
proof (induct n) 

657 
case 0 show ?case by simp 

658 
next 

659 
case (Suc n) 

660 
thus ?case 

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

662 
qed 

663 

664 
lemma (in algebra) range_disjointed_sets: 

665 
assumes A: "range A \<subseteq> sets M " 

666 
shows "range (disjointed A) \<subseteq> sets M" 

667 
proof (auto simp add: disjointed_def) 

668 
fix n 

669 
show "A n  (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets 

670 
by (metis A Diff UNIV_I image_subset_iff) 

671 
qed 

672 

673 
lemma sigma_algebra_disjoint_iff: 

674 
"sigma_algebra M \<longleftrightarrow> 

675 
algebra M & 

676 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> 

677 
(\<Union>i::nat. A i) \<in> sets M)" 

678 
proof (auto simp add: sigma_algebra_iff) 

679 
fix A :: "nat \<Rightarrow> 'a set" 

680 
assume M: "algebra M" 

681 
and A: "range A \<subseteq> sets M" 

682 
and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> 

683 
disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

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

685 
disjoint_family (disjointed A) \<longrightarrow> 

686 
(\<Union>i. disjointed A i) \<in> sets M" by blast 

687 
hence "(\<Union>i. disjointed A i) \<in> sets M" 

688 
by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) 

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

690 
qed 

691 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

692 
subsection {* Sigma algebra generated by function preimages *} 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

693 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

694 
definition (in sigma_algebra) 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

695 
"vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f ` A \<inter> S) ` sets M \<rparr>" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

696 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

697 
lemma (in sigma_algebra) in_vimage_algebra[simp]: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

698 
"A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f ` B \<inter> S)" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

699 
by (simp add: vimage_algebra_def image_iff) 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

700 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

701 
lemma (in sigma_algebra) space_vimage_algebra[simp]: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

702 
"space (vimage_algebra S f) = S" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

703 
by (simp add: vimage_algebra_def) 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

704 

40859  705 
lemma (in sigma_algebra) sigma_algebra_preimages: 
706 
fixes f :: "'x \<Rightarrow> 'a" 

707 
assumes "f \<in> A \<rightarrow> space M" 

708 
shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f ` M \<inter> A) ` sets M \<rparr>" 

709 
(is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>") 

710 
proof (simp add: sigma_algebra_iff2, safe) 

711 
show "{} \<in> ?F ` sets M" by blast 

712 
next 

713 
fix S assume "S \<in> sets M" 

714 
moreover have "A  ?F S = ?F (space M  S)" 

715 
using assms by auto 

716 
ultimately show "A  ?F S \<in> ?F ` sets M" 

717 
by blast 

718 
next 

719 
fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M" 

720 
have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b" 

721 
proof safe 

722 
fix i 

723 
have "S i \<in> ?F ` sets M" using * by auto 

724 
then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto 

725 
qed 

726 
from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)" 

727 
by auto 

728 
then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto 

729 
then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast 

730 
qed 

731 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

732 
lemma (in sigma_algebra) sigma_algebra_vimage: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

733 
fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

734 
shows "sigma_algebra (vimage_algebra S f)" 
40859  735 
proof  
736 
from sigma_algebra_preimages[OF assms] 

737 
show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2) 

738 
qed 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

739 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

740 
lemma (in sigma_algebra) measurable_vimage_algebra: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

741 
fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

742 
shows "f \<in> measurable (vimage_algebra S f) M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

743 
unfolding measurable_def using assms by force 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

744 

40859  745 
lemma (in sigma_algebra) measurable_vimage: 
746 
fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a" 

747 
assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M" 

748 
shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2" 

749 
proof  

750 
note measurable_vimage_algebra[OF assms(2)] 

751 
from measurable_comp[OF this assms(1)] 

752 
show ?thesis by (simp add: comp_def) 

753 
qed 

754 

755 
lemma (in sigma_algebra) vimage_vimage_inv: 

756 
assumes f: "bij_betw f S (space M)" 

757 
assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f (g x) = x" and g: "g \<in> space M \<rightarrow> S" 

758 
shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M" 

759 
proof  

760 
interpret T: sigma_algebra "vimage_algebra S f" 

761 
using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset) 

762 

763 
have inj: "inj_on f S" and [simp]: "f`S = space M" 

764 
using f unfolding bij_betw_def by auto 

765 

766 
{ fix A assume A: "A \<in> sets M" 

767 
have "g ` f ` A \<inter> g ` S \<inter> space M = (f \<circ> g) ` A \<inter> space M" 

768 
using g by auto 

769 
also have "\<dots> = A" 

770 
using `A \<in> sets M`[THEN sets_into_space] by auto 

771 
finally have "g ` f ` A \<inter> g ` S \<inter> space M = A" . } 

772 
note X = this 

773 
show ?thesis 

774 
unfolding T.vimage_algebra_def unfolding vimage_algebra_def 

775 
by (simp add: image_compose[symmetric] comp_def X cong: image_cong) 

776 
qed 

777 

778 
lemma (in sigma_algebra) measurable_vimage_iff: 

779 
fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)" 

780 
shows "g \<in> measurable M M' \<longleftrightarrow> (g \<circ> f) \<in> measurable (vimage_algebra S f) M'" 

781 
proof 

782 
assume "g \<in> measurable M M'" 

783 
from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]] 

784 
show "(g \<circ> f) \<in> measurable (vimage_algebra S f) M'" unfolding comp_def . 

785 
next 

786 
interpret v: sigma_algebra "vimage_algebra S f" 

787 
using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage) 

788 
note f' = f[THEN bij_betw_the_inv_into] 

789 
assume "g \<circ> f \<in> measurable (vimage_algebra S f) M'" 

790 
from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]] 

791 
show "g \<in> measurable M M'" 

792 
using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def] 

793 
by (subst (asm) vimage_vimage_inv) 

794 
(simp_all add: f_the_inv_into_f cong: measurable_cong) 

795 
qed 

796 

797 
lemma (in sigma_algebra) measurable_vimage_iff_inv: 

798 
fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)" 

799 
shows "g \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (g \<circ> the_inv_into S f) \<in> measurable M M'" 

800 
unfolding measurable_vimage_iff[OF f] 

801 
using f[unfolded bij_betw_def] 

802 
by (auto intro!: measurable_cong simp add: the_inv_into_f_f) 

803 

804 
lemma sigma_sets_vimage: 

805 
assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S" 

806 
shows "sigma_sets S' ((\<lambda>X. f ` X \<inter> S') ` A) = (\<lambda>X. f ` X \<inter> S') ` sigma_sets S A" 

807 
proof (intro set_eqI iffI) 

808 
let ?F = "\<lambda>X. f ` X \<inter> S'" 

809 
fix X assume "X \<in> sigma_sets S' (?F ` A)" 

810 
then show "X \<in> ?F ` sigma_sets S A" 

811 
proof induct 

812 
case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A" 

813 
by auto 

814 
then show ?case by (auto intro!: sigma_sets.Basic) 

815 
next 

816 
case Empty then show ?case 

817 
by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty) 

818 
next 

819 
case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A" 

820 
by auto 

821 
then have "S  X' \<in> sigma_sets S A" 

822 
by (auto intro!: sigma_sets.Compl) 

823 
then show ?case 

824 
using X assms by (auto intro!: image_eqI[where x="S  X'"]) 

825 
next 

826 
case (Union F) 

827 
then have "\<forall>i. \<exists>F'. F' \<in> sigma_sets S A \<and> F i = f ` F' \<inter> S'" 

828 
by (auto simp: image_iff Bex_def) 

829 
from choice[OF this] obtain F' where 

830 
"\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f ` F' i \<inter> S'" 

831 
by auto 

832 
then show ?case 

833 
by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"]) 

834 
qed 

835 
next 

836 
let ?F = "\<lambda>X. f ` X \<inter> S'" 

837 
fix X assume "X \<in> ?F ` sigma_sets S A" 

838 
then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto 

839 
then show "X \<in> sigma_sets S' (?F ` A)" 

840 
proof (induct arbitrary: X) 

841 
case (Basic X') then show ?case by (auto intro: sigma_sets.Basic) 

842 
next 

843 
case Empty then show ?case by (auto intro: sigma_sets.Empty) 

844 
next 

845 
case (Compl X') 

846 
have "S'  (S'  X) \<in> sigma_sets S' (?F ` A)" 

847 
apply (rule sigma_sets.Compl) 

848 
using assms by (auto intro!: Compl.hyps simp: Compl.prems) 

849 
also have "S'  (S'  X) = X" 

850 
using assms Compl by auto 

851 
finally show ?case . 

852 
next 

853 
case (Union F) 

854 
have "(\<Union>i. f ` F i \<inter> S') \<in> sigma_sets S' (?F ` A)" 

855 
by (intro sigma_sets.Union Union.hyps) simp 

856 
also have "(\<Union>i. f ` F i \<inter> S') = X" 

857 
using assms Union by auto 

858 
finally show ?case . 

859 
qed 

860 
qed 

861 

39092  862 
section {* Conditional space *} 
863 

864 
definition (in algebra) 

865 
"image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M \<rparr>" 

866 

867 
definition (in algebra) 

868 
"conditional_space X A = algebra.image_space (restricted_space A) X" 

869 

870 
lemma (in algebra) space_conditional_space: 

871 
assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A" 

872 
proof  

873 
interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra) 

874 
show ?thesis unfolding conditional_space_def r.image_space_def 

875 
by simp 

876 
qed 

877 

38656  878 
subsection {* A TwoElement Series *} 
879 

880 
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set " 

881 
where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)" 

882 

883 
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" 

884 
apply (simp add: binaryset_def) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39092
diff
changeset

885 
apply (rule set_eqI) 
38656  886 
apply (auto simp add: image_iff) 
887 
done 

888 

889 
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" 

890 
by (simp add: UNION_eq_Union_image range_binaryset_eq) 

891 

892 
section {* Closed CDI *} 

893 

894 
definition 

895 
closed_cdi where 

896 
"closed_cdi M \<longleftrightarrow> 

897 
sets M \<subseteq> Pow (space M) & 

898 
(\<forall>s \<in> sets M. space M  s \<in> sets M) & 

899 
(\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow> 

900 
(\<Union>i. A i) \<in> sets M) & 

901 
(\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 

902 

903 

904 
inductive_set 

905 
smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set" 

906 
for M 

907 
where 

908 
Basic [intro]: 

909 
"a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M" 

910 
 Compl [intro]: 

911 
"a \<in> smallest_ccdi_sets M \<Longrightarrow> space M  a \<in> smallest_ccdi_sets M" 

912 
 Inc: 

913 
"range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n)) 

914 
\<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M" 

915 
 Disj: 

916 
"range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A 

917 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M" 

918 
monos Pow_mono 

919 

920 

921 
definition 

922 
smallest_closed_cdi where 

923 
"smallest_closed_cdi M = (space = space M, sets = smallest_ccdi_sets M)" 

924 

925 
lemma space_smallest_closed_cdi [simp]: 

926 
"space (smallest_closed_cdi M) = space M" 

927 
by (simp add: smallest_closed_cdi_def) 

928 

929 
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)" 

930 
by (auto simp add: smallest_closed_cdi_def) 

931 

932 
lemma (in algebra) smallest_ccdi_sets: 

933 
"smallest_ccdi_sets M \<subseteq> Pow (space M)" 

934 
apply (rule subsetI) 

935 
apply (erule smallest_ccdi_sets.induct) 

936 
apply (auto intro: range_subsetD dest: sets_into_space) 

937 
done 

938 

939 
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)" 

940 
apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets) 

941 
apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) + 

942 
done 

943 

944 
lemma (in algebra) smallest_closed_cdi3: 

945 
"sets (smallest_closed_cdi M) \<subseteq> Pow (space M)" 

946 
by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 

947 

948 
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)" 

949 
by (simp add: closed_cdi_def) 

950 

951 
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M  s \<in> sets M" 

952 
by (simp add: closed_cdi_def) 

953 

954 
lemma closed_cdi_Inc: 

955 
"closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow> 

956 
(\<Union>i. A i) \<in> sets M" 

957 
by (simp add: closed_cdi_def) 

958 

959 
lemma closed_cdi_Disj: 

960 
"closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

961 
by (simp add: closed_cdi_def) 

962 

963 
lemma closed_cdi_Un: 

964 
assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M" 

965 
and A: "A \<in> sets M" and B: "B \<in> sets M" 

966 
and disj: "A \<inter> B = {}" 

967 
shows "A \<union> B \<in> sets M" 

968 
proof  

969 
have ra: "range (binaryset A B) \<subseteq> sets M" 

970 
by (simp add: range_binaryset_eq empty A B) 

971 
have di: "disjoint_family (binaryset A B)" using disj 

972 
by (simp add: disjoint_family_on_def binaryset_def Int_commute) 

973 
from closed_cdi_Disj [OF cdi ra di] 

974 
show ?thesis 

975 
by (simp add: UN_binaryset_eq) 

976 
qed 

977 

978 
lemma (in algebra) smallest_ccdi_sets_Un: 

979 
assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M" 

980 
and disj: "A \<inter> B = {}" 

981 
shows "A \<union> B \<in> smallest_ccdi_sets M" 

982 
proof  

983 
have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)" 

984 
by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic) 

985 
have di: "disjoint_family (binaryset A B)" using disj 

986 
by (simp add: disjoint_family_on_def binaryset_def Int_commute) 

987 
from Disj [OF ra di] 

988 
show ?thesis 

989 
by (simp add: UN_binaryset_eq) 

990 
qed 

991 

992 
lemma (in algebra) smallest_ccdi_sets_Int1: 

993 
assumes a: "a \<in> sets M" 

994 
shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M" 

995 
proof (induct rule: smallest_ccdi_sets.induct) 

996 
case (Basic x) 

997 
thus ?case 

998 
by (metis a Int smallest_ccdi_sets.Basic) 

999 
next 

1000 
case (Compl x) 

1001 
have "a \<inter> (space M  x) = space M  ((space M  a) \<union> (a \<inter> x))" 

1002 
by blast 

1003 
also have "... \<in> smallest_ccdi_sets M" 

1004 
by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2 

1005 
Diff_disjoint Int_Diff Int_empty_right Un_commute 

1006 
smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl 

1007 
smallest_ccdi_sets_Un) 

1008 
finally show ?case . 

1009 
next 

1010 
case (Inc A) 

1011 
have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" 

1012 
by blast 

1013 
have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc 

1014 
by blast 

1015 
moreover have "(\<lambda>i. a \<inter> A i) 0 = {}" 

1016 
by (simp add: Inc) 

1017 
moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc 

1018 
by blast 

1019 
ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M" 

1020 
by (rule smallest_ccdi_sets.Inc) 

1021 
show ?case 

1022 
by (metis 1 2) 

1023 
next 

1024 
case (Disj A) 

1025 
have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" 

1026 
by blast 

1027 
have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj 

1028 
by blast 

1029 
moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj 

1030 
by (auto simp add: disjoint_family_on_def) 

1031 
ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M" 

1032 
by (rule smallest_ccdi_sets.Disj) 

1033 
show ?case 

1034 
by (metis 1 2) 

1035 
qed 

1036 

1037 

1038 
lemma (in algebra) smallest_ccdi_sets_Int: 

1039 
assumes b: "b \<in> smallest_ccdi_sets M" 

1040 
shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M" 

1041 
proof (induct rule: smallest_ccdi_sets.induct) 

1042 
case (Basic x) 

1043 
thus ?case 

1044 
by (metis b smallest_ccdi_sets_Int1) 

1045 
next 

1046 
case (Compl x) 

1047 
have "(space M  x) \<inter> b = space M  (x \<inter> b \<union> (space M  b))" 

1048 
by blast 

1049 
also have "... \<in> smallest_ccdi_sets M" 

1050 
by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b 

1051 
smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) 

1052 
finally show ?case . 

1053 
next 

1054 
case (Inc A) 

1055 
have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b" 

1056 
by blast 

1057 
have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc 

1058 
by blast 

1059 
moreover have "(\<lambda>i. A i \<inter> b) 0 = {}" 

1060 
by (simp add: Inc) 

1061 
moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc 

1062 
by blast 

1063 
ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M" 

1064 
by (rule smallest_ccdi_sets.Inc) 

1065 
show ?case 

1066 
by (metis 1 2) 

1067 
next 

1068 
case (Disj A) 

1069 
have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b" 

1070 
by blast 

1071 
have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj 

1072 
by blast 

1073 
moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj 

1074 
by (auto simp add: disjoint_family_on_def) 

1075 
ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M" 

1076 
by (rule smallest_ccdi_sets.Disj) 

1077 
show ?case 

1078 
by (metis 1 2) 

1079 
qed 

1080 

1081 
lemma (in algebra) sets_smallest_closed_cdi_Int: 

1082 
"a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M) 

1083 
\<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)" 

1084 
by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) 

1085 

1086 
lemma (in algebra) sigma_property_disjoint_lemma: 

1087 
assumes sbC: "sets M \<subseteq> C" 

1088 
and ccdi: "closed_cdi (space = space M, sets = C)" 

1089 
shows "sigma_sets (space M) (sets M) \<subseteq> C" 

1090 
proof  

1091 
have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (space = space M, sets = B)}" 

1092 
apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int 

1093 
smallest_ccdi_sets_Int) 

1094 
apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) 

1095 
apply (blast intro: smallest_ccdi_sets.Disj) 

1096 
done 

1097 
hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M" 

1098 
by clarsimp 

1099 
(drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto) 

1100 
also have "... \<subseteq> C" 

1101 
proof 

1102 
fix x 

1103 
assume x: "x \<in> smallest_ccdi_sets M" 

1104 
thus "x \<in> C" 

1105 
proof (induct rule: smallest_ccdi_sets.induct) 

1106 
case (Basic x) 

1107 
thus ?case 

1108 
by (metis Basic subsetD sbC) 

1109 
next 

1110 
case (Compl x) 

1111 
thus ?case 

1112 
by (blast intro: closed_cdi_Compl [OF ccdi, simplified]) 

1113 
next 

1114 
case (Inc A) 

1115 
thus ?case 

1116 
by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 

1117 
next 

1118 
case (Disj A) 

1119 
thus ?case 

1120 
by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 

1121 
qed 

1122 
qed 

1123 
finally show ?thesis . 

1124 
qed 

1125 

1126 
lemma (in algebra) sigma_property_disjoint: 

1127 
assumes sbC: "sets M \<subseteq> C" 

1128 
and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M  s \<in> C" 

1129 
and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 

1130 
\<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) 

1131 
\<Longrightarrow> (\<Union>i. A i) \<in> C" 

1132 
and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 

1133 
\<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C" 

1134 
shows "sigma_sets (space M) (sets M) \<subseteq> C" 

1135 
proof  

1136 
have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 

1137 
proof (rule sigma_property_disjoint_lemma) 

1138 
show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 

1139 
by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic) 

1140 
next 

1141 
show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>" 

1142 
by (simp add: closed_cdi_def compl inc disj) 

1143 
(metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed 

1144 
IntE sigma_sets.Compl range_subsetD sigma_sets.Union) 

1145 
qed 

1146 
thus ?thesis 

1147 
by blast 

1148 
qed 

1149 

40859  1150 
section {* Dynkin systems *} 
1151 

1152 

1153 
locale dynkin_system = 

1154 
fixes M :: "'a algebra" 

1155 
assumes space_closed: "sets M \<subseteq> Pow (space M)" 

1156 
and space: "space M \<in> sets M" 

1157 
and compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M  A \<in> sets M" 

1158 
and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M 

1159 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

1160 

1161 
lemma (in dynkin_system) sets_into_space: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" 

1162 
using space_closed by auto 

1163 

1164 
lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M" 

1165 
using space compl[of "space M"] by simp 

1166 

1167 
lemma (in dynkin_system) diff: 

1168 
assumes sets: "D \<in> sets M" "E \<in> sets M" and "D \<subseteq> E" 

1169 
shows "E  D \<in> sets M" 

1170 
proof  

1171 
let ?f = "\<lambda>x. if x = 0 then D else if x = Suc 0 then space M  E else {}" 

1172 
have "range ?f = {D, space M  E, {}}" 

1173 
by (auto simp: image_iff) 

1174 
moreover have "D \<union> (space M  E) = (\<Union>i. ?f i)" 

1175 
by (auto simp: image_iff split: split_if_asm) 

1176 
moreover 

1177 
then have "disjoint_family ?f" unfolding disjoint_family_on_def 

1178 
using `D \<in> sets M`[THEN sets_into_space] `D \<subseteq> E` by auto 

1179 
ultimately have "space M  (D \<union> (space M  E)) \<in> sets M" 

1180 
using sets by auto 

1181 
also have "space M  (D \<union> (space M  E)) = E  D" 

1182 
using assms sets_into_space by auto 

1183 
finally show ?thesis . 

1184 
qed 

1185 

1186 
lemma dynkin_systemI: 

1187 
assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" "space M \<in> sets M" 

1188 
assumes "\<And> A. A \<in> sets M \<Longrightarrow> space M  A \<in> sets M" 

1189 
assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M 

1190 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

1191 
shows "dynkin_system M" 

1192 
using assms by (auto simp: dynkin_system_def) 

1193 

1194 
lemma dynkin_system_trivial: 

1195 
shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>" 

1196 
by (rule dynkin_systemI) auto 

1197 

1198 
lemma sigma_algebra_imp_dynkin_system: 

1199 
assumes "sigma_algebra M" shows "dynkin_system M" 

1200 
proof  

1201 
interpret sigma_algebra M by fact 

1202 
show ?thesis using sets_into_space by (fastsimp intro!: dynkin_systemI) 

1203 
qed 

1204 

1205 
subsection "Intersection stable algebras" 

1206 

1207 
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" 

1208 

1209 
lemma (in algebra) Int_stable: "Int_stable M" 

1210 
unfolding Int_stable_def by auto 

1211 

1212 
lemma (in dynkin_system) sigma_algebra_eq_Int_stable: 

1213 
"sigma_algebra M \<longleftrightarrow> Int_stable M" 

1214 
proof 

1215 
assume "sigma_algebra M" then show "Int_stable M" 

1216 
unfolding sigma_algebra_def using algebra.Int_stable by auto 

1217 
next 

1218 
assume "Int_stable M" 

1219 
show "sigma_algebra M" 

1220 
unfolding sigma_algebra_disjoint_iff algebra_def 

1221 
proof (intro conjI ballI allI impI) 

1222 
show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto 

1223 
next 

1224 
fix A B assume "A \<in> sets M" "B \<in> sets M" 

1225 
then have "A \<union> B = space M  ((space M  A) \<inter> (space M  B))" 

1226 
"space M  A \<in> sets M" "space M  B \<in> sets M" 

1227 
using sets_into_space by auto 

1228 
then show "A \<union> B \<in> sets M" 

1229 
using `Int_stable M` unfolding Int_stable_def by auto 

1230 
qed auto 

1231 
qed 

1232 

1233 
subsection "Smallest Dynkin systems" 

1234 

1235 
definition dynkin :: "'a algebra \<Rightarrow> 'a algebra" where 

1236 
"dynkin M = \<lparr> space = space M, 

1237 
sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D}\<rparr>" 

1238 

1239 
lemma dynkin_system_dynkin: 

1240 
fixes M :: "'a algebra" 

1241 
assumes "sets M \<subseteq> Pow (space M)" 

1242 
shows "dynkin_system (dynkin M)" 

1243 
proof (rule dynkin_systemI) 

1244 
fix A assume "A \<in> sets (dynkin M)" 

1245 
moreover 

1246 
{ fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>" 

1247 
from dynkin_system.sets_into_space[OF d] `A \<in> D` 

1248 
have "A \<subseteq> space M" by auto } 

1249 
moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}" 

1250 
using assms dynkin_system_trivial by fastsimp 

1251 
ultimately show "A \<subseteq> space (dynkin M)" 

1252 
unfolding dynkin_def using assms 

1253 
by simp (metis dynkin_system.sets_into_space in_mono mem_def) 

1254 
next 

1255 
show "space (dynkin M) \<in> sets (dynkin M)" 

1256 
unfolding dynkin_def using dynkin_system.space by fastsimp 

1257 
next 

1258 
fix A assume "A \<in> sets (dynkin M)" 

1259 
then show "space (dynkin M)  A \<in> sets (dynkin M)" 

1260 
unfolding dynkin_def using dynkin_system.compl by force 

1261 
next 

1262 
fix A :: "nat \<Rightarrow> 'a set" 

1263 
assume A: "disjoint_family A" "range A \<subseteq> sets (dynkin M)" 

1264 
show "(\<Union>i. A i) \<in> sets (dynkin M)" unfolding dynkin_def 

1265 
proof (simp, safe) 