author  wenzelm 
Fri, 16 Aug 2013 21:33:36 +0200  
changeset 53043  8cbfbeb566a4 
parent 50530  6266e44b3396 
child 56021  e0c9d76c2a6d 
permissions  rwrr 
50530  1 
(* Title: HOL/Probability/Measurable.thy 
50387  2 
Author: Johannes Hölzl <hoelzl@in.tum.de> 
3 
*) 

4 
theory Measurable 

5 
imports Sigma_Algebra 

6 
begin 

7 

8 
subsection {* Measurability prover *} 

9 

10 
lemma (in algebra) sets_Collect_finite_All: 

11 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" 

12 
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" 

13 
proof  

14 
have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" 

15 
by auto 

16 
with assms show ?thesis by (auto intro!: sets_Collect_finite_All') 

17 
qed 

18 

19 
abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))" 

20 

21 
lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M" 

22 
proof 

23 
assume "pred M P" 

24 
then have "P ` {True} \<inter> space M \<in> sets M" 

25 
by (auto simp: measurable_count_space_eq2) 

26 
also have "P ` {True} \<inter> space M = {x\<in>space M. P x}" by auto 

27 
finally show "{x\<in>space M. P x} \<in> sets M" . 

28 
next 

29 
assume P: "{x\<in>space M. P x} \<in> sets M" 

30 
moreover 

31 
{ fix X 

32 
have "X \<in> Pow (UNIV :: bool set)" by simp 

33 
then have "P ` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}" 

34 
unfolding UNIV_bool Pow_insert Pow_empty by auto 

35 
then have "P ` X \<inter> space M \<in> sets M" 

36 
by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } 

37 
then show "pred M P" 

38 
by (auto simp: measurable_def) 

39 
qed 

40 

41 
lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))" 

42 
by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) 

43 

44 
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)" 

45 
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) 

46 

47 
ML_file "measurable.ML" 

48 

53043
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

49 
attribute_setup measurable = {* 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

50 
Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false  
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

51 
Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

52 
(false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm)) 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

53 
*} "declaration of measurability theorems" 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

54 

8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

55 
attribute_setup measurable_dest = {* 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

56 
Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest)) 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

57 
*} "add dest rule for measurability prover" 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

58 

8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

59 
attribute_setup measurable_app = {* 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

60 
Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app)) 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

61 
*} "add application rule for measurability prover" 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

62 

8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

63 
method_setup measurable = {* 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

64 
Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts))) 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

65 
*} "measurability prover" 
8cbfbeb566a4
more standard attribute_setup / method_setup  export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset

66 

50387  67 
simproc_setup measurable ("A \<in> sets M"  "f \<in> measurable M N") = {* K Measurable.simproc *} 
68 

69 
declare 

70 
measurable_compose_rev[measurable_dest] 

71 
pred_sets1[measurable_dest] 

72 
pred_sets2[measurable_dest] 

73 
sets.sets_into_space[measurable_dest] 

74 

75 
declare 

76 
sets.top[measurable] 

77 
sets.empty_sets[measurable (raw)] 

78 
sets.Un[measurable (raw)] 

79 
sets.Diff[measurable (raw)] 

80 

81 
declare 

82 
measurable_count_space[measurable (raw)] 

83 
measurable_ident[measurable (raw)] 

84 
measurable_ident_sets[measurable (raw)] 

85 
measurable_const[measurable (raw)] 

86 
measurable_If[measurable (raw)] 

87 
measurable_comp[measurable (raw)] 

88 
measurable_sets[measurable (raw)] 

89 

90 
lemma predE[measurable (raw)]: 

91 
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" 

92 
unfolding pred_def . 

93 

94 
lemma pred_intros_imp'[measurable (raw)]: 

95 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)" 

96 
by (cases K) auto 

97 

98 
lemma pred_intros_conj1'[measurable (raw)]: 

99 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)" 

100 
by (cases K) auto 

101 

102 
lemma pred_intros_conj2'[measurable (raw)]: 

103 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)" 

104 
by (cases K) auto 

105 

106 
lemma pred_intros_disj1'[measurable (raw)]: 

107 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)" 

108 
by (cases K) auto 

109 

110 
lemma pred_intros_disj2'[measurable (raw)]: 

111 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)" 

112 
by (cases K) auto 

113 

114 
lemma pred_intros_logic[measurable (raw)]: 

115 
"pred M (\<lambda>x. x \<in> space M)" 

116 
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)" 

117 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)" 

118 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)" 

119 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)" 

120 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)" 

121 
"pred M (\<lambda>x. f x \<in> UNIV)" 

122 
"pred M (\<lambda>x. f x \<in> {})" 

123 
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})" 

124 
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in>  (B x))" 

125 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x)  (B x))" 

126 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))" 

127 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))" 

128 
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) ` (X x))" 

129 
by (auto simp: iff_conv_conj_imp pred_def) 

130 

131 
lemma pred_intros_countable[measurable (raw)]: 

132 
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool" 

133 
shows 

134 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)" 

135 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)" 

136 
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) 

137 

138 
lemma pred_intros_countable_bounded[measurable (raw)]: 

139 
fixes X :: "'i :: countable set" 

140 
shows 

141 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))" 

142 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))" 

143 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)" 

144 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)" 

145 
by (auto simp: Bex_def Ball_def) 

146 

147 
lemma pred_intros_finite[measurable (raw)]: 

148 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))" 

149 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))" 

150 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)" 

151 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)" 

152 
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) 

153 

154 
lemma countable_Un_Int[measurable (raw)]: 

155 
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M" 

156 
"I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M" 

157 
by auto 

158 

159 
declare 

160 
finite_UN[measurable (raw)] 

161 
finite_INT[measurable (raw)] 

162 

163 
lemma sets_Int_pred[measurable (raw)]: 

164 
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)" 

165 
shows "A \<inter> B \<in> sets M" 

166 
proof  

167 
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto 

168 
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B" 

169 
using space by auto 

170 
finally show ?thesis . 

171 
qed 

172 

173 
lemma [measurable (raw generic)]: 

174 
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N" 

175 
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)" 

176 
and pred_eq_const2: "pred M (\<lambda>x. c = f x)" 

177 
proof  

178 
show "pred M (\<lambda>x. f x = c)" 

179 
proof cases 

180 
assume "c \<in> space N" 

181 
with measurable_sets[OF f c] show ?thesis 

182 
by (auto simp: Int_def conj_commute pred_def) 

183 
next 

184 
assume "c \<notin> space N" 

185 
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto 

186 
then show ?thesis by (auto simp: pred_def cong: conj_cong) 

187 
qed 

188 
then show "pred M (\<lambda>x. c = f x)" 

189 
by (simp add: eq_commute) 

190 
qed 

191 

192 
lemma pred_le_const[measurable (raw generic)]: 

193 
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)" 

194 
using measurable_sets[OF f c] 

195 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

196 

197 
lemma pred_const_le[measurable (raw generic)]: 

198 
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)" 

199 
using measurable_sets[OF f c] 

200 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

201 

202 
lemma pred_less_const[measurable (raw generic)]: 

203 
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)" 

204 
using measurable_sets[OF f c] 

205 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

206 

207 
lemma pred_const_less[measurable (raw generic)]: 

208 
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)" 

209 
using measurable_sets[OF f c] 

210 
by (auto simp: Int_def conj_commute eq_commute pred_def) 

211 

212 
declare 

213 
sets.Int[measurable (raw)] 

214 

215 
lemma pred_in_If[measurable (raw)]: 

216 
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow> 

217 
pred M (\<lambda>x. x \<in> (if P then A x else B x))" 

218 
by auto 

219 

220 
lemma sets_range[measurable_dest]: 

221 
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M" 

222 
by auto 

223 

224 
lemma pred_sets_range[measurable_dest]: 

225 
"A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" 

226 
using pred_sets2[OF sets_range] by auto 

227 

228 
lemma sets_All[measurable_dest]: 

229 
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)" 

230 
by auto 

231 

232 
lemma pred_sets_All[measurable_dest]: 

233 
"\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" 

234 
using pred_sets2[OF sets_All, of A N f] by auto 

235 

236 
lemma sets_Ball[measurable_dest]: 

237 
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)" 

238 
by auto 

239 

240 
lemma pred_sets_Ball[measurable_dest]: 

241 
"\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" 

242 
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto 

243 

244 
lemma measurable_finite[measurable (raw)]: 

245 
fixes S :: "'a \<Rightarrow> nat set" 

246 
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" 

247 
shows "pred M (\<lambda>x. finite (S x))" 

248 
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) 

249 

250 
lemma measurable_Least[measurable]: 

251 
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q 

252 
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)" 

253 
unfolding measurable_def by (safe intro!: sets_Least) simp_all 

254 

255 
lemma measurable_count_space_insert[measurable (raw)]: 

256 
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)" 

257 
by simp 

258 

259 
hide_const (open) pred 

260 

261 
end 