author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 50244  de72bbe42190 
child 56949  d1a937cbf858 
permissions  rwrr 
41983  1 
(* Title: HOL/Probability/Complete_Measure.thy 
40859  2 
Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen 
3 
*) 

41983  4 

40859  5 
theory Complete_Measure 
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
41983
diff
changeset

6 
imports Lebesgue_Integration 
40859  7 
begin 
8 

47694  9 
definition 
10 
"split_completion M A p = (if A \<in> sets M then p = (A, {}) else 

11 
\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)" 

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

12 

47694  13 
definition 
14 
"main_part M A = fst (Eps (split_completion M A))" 

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

15 

47694  16 
definition 
17 
"null_part M A = snd (Eps (split_completion M A))" 

40859  18 

47694  19 
definition completion :: "'a measure \<Rightarrow> 'a measure" where 
20 
"completion M = measure_of (space M) { S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } 

21 
(emeasure M \<circ> main_part M)" 

40859  22 

47694  23 
lemma completion_into_space: 
24 
"{ S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)" 

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

25 
using sets.sets_into_space by auto 
40859  26 

47694  27 
lemma space_completion[simp]: "space (completion M) = space M" 
28 
unfolding completion_def using space_measure_of[OF completion_into_space] by simp 

40859  29 

47694  30 
lemma completionI: 
31 
assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" 

32 
shows "A \<in> { S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" 

40859  33 
using assms by auto 
34 

47694  35 
lemma completionE: 
36 
assumes "A \<in> { S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" 

37 
obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" 

38 
using assms by auto 

39 

40 
lemma sigma_algebra_completion: 

41 
"sigma_algebra (space M) { S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" 

42 
(is "sigma_algebra _ ?A") 

43 
unfolding sigma_algebra_iff2 

44 
proof (intro conjI ballI allI impI) 

45 
show "?A \<subseteq> Pow (space M)" 

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

46 
using sets.sets_into_space by auto 
40859  47 
next 
47694  48 
show "{} \<in> ?A" by auto 
40859  49 
next 
47694  50 
let ?C = "space M" 
51 
fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' . 

52 
then show "space M  A \<in> ?A" 

53 
by (intro completionI[of _ "(?C  S) \<inter> (?C  N')" "(?C  S) \<inter> N' \<inter> (?C  N)"]) auto 

54 
next 

55 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A" 

56 
then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'" 

57 
by (auto simp: image_subset_iff) 

40859  58 
from choice[OF this] guess S .. 
59 
from choice[OF this] guess N .. 

60 
from choice[OF this] guess N' .. 

47694  61 
then show "UNION UNIV A \<in> ?A" 
40859  62 
using null_sets_UN[of N'] 
47694  63 
by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto 
64 
qed 

65 

66 
lemma sets_completion: 

67 
"sets (completion M) = { S \<union> N S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" 

68 
using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def) 

69 

70 
lemma sets_completionE: 

71 
assumes "A \<in> sets (completion M)" 

72 
obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" 

73 
using assms unfolding sets_completion by auto 

74 

75 
lemma sets_completionI: 

76 
assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" 

77 
shows "A \<in> sets (completion M)" 

78 
using assms unfolding sets_completion by auto 

79 

80 
lemma sets_completionI_sets[intro, simp]: 

81 
"A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)" 

82 
unfolding sets_completion by force 

40859  83 

47694  84 
lemma null_sets_completion: 
85 
assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)" 

86 
using assms by (intro sets_completionI[of N "{}" N N']) auto 

87 

88 
lemma split_completion: 

89 
assumes "A \<in> sets (completion M)" 

90 
shows "split_completion M A (main_part M A, null_part M A)" 

91 
proof cases 

92 
assume "A \<in> sets M" then show ?thesis 

93 
by (simp add: split_completion_def[abs_def] main_part_def null_part_def) 

94 
next 

95 
assume nA: "A \<notin> sets M" 

96 
show ?thesis 

97 
unfolding main_part_def null_part_def if_not_P[OF nA] 

98 
proof (rule someI2_ex) 

99 
from assms[THEN sets_completionE] guess S N N' . note A = this 

100 
let ?P = "(S, N  S)" 

101 
show "\<exists>p. split_completion M A p" 

102 
unfolding split_completion_def if_not_P[OF nA] using A 

103 
proof (intro exI conjI) 

104 
show "A = fst ?P \<union> snd ?P" using A by auto 

105 
show "snd ?P \<subseteq> N'" using A by auto 

106 
qed auto 

40859  107 
qed auto 
47694  108 
qed 
40859  109 

47694  110 
lemma 
111 
assumes "S \<in> sets (completion M)" 

112 
shows main_part_sets[intro, simp]: "main_part M S \<in> sets M" 

113 
and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S" 

114 
and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}" 

115 
using split_completion[OF assms] 

116 
by (auto simp: split_completion_def split: split_if_asm) 

40859  117 

47694  118 
lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S" 
119 
using split_completion[of S M] 

120 
by (auto simp: split_completion_def split: split_if_asm) 

40859  121 

47694  122 
lemma null_part: 
123 
assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N" 

124 
using split_completion[OF assms] by (auto simp: split_completion_def split: split_if_asm) 

125 

126 
lemma null_part_sets[intro, simp]: 

127 
assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0" 

40859  128 
proof  
47694  129 
have S: "S \<in> sets (completion M)" using assms by auto 
130 
have "S  main_part M S \<in> sets M" using assms by auto 

40859  131 
moreover 
132 
from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S] 

47694  133 
have "S  main_part M S = null_part M S" by auto 
134 
ultimately show sets: "null_part M S \<in> sets M" by auto 

40859  135 
from null_part[OF S] guess N .. 
47694  136 
with emeasure_eq_0[of N _ "null_part M S"] sets 
137 
show "emeasure M (null_part M S) = 0" by auto 

40859  138 
qed 
139 

47694  140 
lemma emeasure_main_part_UN: 
40859  141 
fixes S :: "nat \<Rightarrow> 'a set" 
47694  142 
assumes "range S \<subseteq> sets (completion M)" 
143 
shows "emeasure M (main_part M (\<Union>i. (S i))) = emeasure M (\<Union>i. main_part M (S i))" 

40859  144 
proof  
47694  145 
have S: "\<And>i. S i \<in> sets (completion M)" using assms by auto 
146 
then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto 

147 
have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N" 

40859  148 
using null_part[OF S] by auto 
149 
from choice[OF this] guess N .. note N = this 

47694  150 
then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto 
151 
have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto 

40859  152 
from null_part[OF this] guess N' .. note N' = this 
153 
let ?N = "(\<Union>i. N i) \<union> N'" 

47694  154 
have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto 
155 
have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N" 

40859  156 
using N' by auto 
47694  157 
also have "\<dots> = (\<Union>i. main_part M (S i) \<union> null_part M (S i)) \<union> ?N" 
40859  158 
unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto 
47694  159 
also have "\<dots> = (\<Union>i. main_part M (S i)) \<union> ?N" 
40859  160 
using N by auto 
47694  161 
finally have *: "main_part M (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part M (S i)) \<union> ?N" . 
162 
have "emeasure M (main_part M (\<Union>i. S i)) = emeasure M (main_part M (\<Union>i. S i) \<union> ?N)" 

163 
using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto 

164 
also have "\<dots> = emeasure M ((\<Union>i. main_part M (S i)) \<union> ?N)" 

40859  165 
unfolding * .. 
47694  166 
also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))" 
167 
using null_set S by (intro emeasure_Un_null_set) auto 

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

168 
finally show ?thesis . 
40859  169 
qed 
170 

47694  171 
lemma emeasure_completion[simp]: 
172 
assumes S: "S \<in> sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)" 

173 
proof (subst emeasure_measure_of[OF completion_def completion_into_space]) 

174 
let ?\<mu> = "emeasure M \<circ> main_part M" 

175 
show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all 

176 
show "positive (sets (completion M)) ?\<mu>" 

177 
by (simp add: positive_def emeasure_nonneg) 

178 
show "countably_additive (sets (completion M)) ?\<mu>" 

179 
proof (intro countably_additiveI) 

180 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (completion M)" "disjoint_family A" 

181 
have "disjoint_family (\<lambda>i. main_part M (A i))" 

182 
proof (intro disjoint_family_on_bisimulation[OF A(2)]) 

183 
fix n m assume "A n \<inter> A m = {}" 

184 
then have "(main_part M (A n) \<union> null_part M (A n)) \<inter> (main_part M (A m) \<union> null_part M (A m)) = {}" 

185 
using A by (subst (1 2) main_part_null_part_Un) auto 

186 
then show "main_part M (A n) \<inter> main_part M (A m) = {}" by auto 

187 
qed 

188 
then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))" 

189 
using A by (auto intro!: suminf_emeasure) 

190 
then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)" 

191 
by (simp add: completion_def emeasure_main_part_UN[OF A(1)]) 

192 
qed 

40859  193 
qed 
194 

47694  195 
lemma emeasure_completion_UN: 
196 
"range S \<subseteq> sets (completion M) \<Longrightarrow> 

197 
emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))" 

198 
by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN) 

40859  199 

47694  200 
lemma emeasure_completion_Un: 
201 
assumes S: "S \<in> sets (completion M)" and T: "T \<in> sets (completion M)" 

202 
shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)" 

203 
proof (subst emeasure_completion) 

204 
have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))" 

205 
unfolding binary_def by (auto split: split_if_asm) 

206 
show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)" 

207 
using emeasure_main_part_UN[of "binary S T" M] assms 

208 
unfolding range_binary_eq Un_range_binary UN by auto 

209 
qed (auto intro: S T) 

210 

211 
lemma sets_completionI_sub: 

212 
assumes N: "N' \<in> null_sets M" "N \<subseteq> N'" 

213 
shows "N \<in> sets (completion M)" 

214 
using assms by (intro sets_completionI[of _ "{}" N N']) auto 

215 

216 
lemma completion_ex_simple_function: 

217 
assumes f: "simple_function (completion M) f" 

218 
shows "\<exists>f'. simple_function M f' \<and> (AE x in M. f x = f' x)" 

40859  219 
proof  
46731  220 
let ?F = "\<lambda>x. f ` {x} \<inter> space M" 
47694  221 
have F: "\<And>x. ?F x \<in> sets (completion M)" and fin: "finite (f`space M)" 
222 
using simple_functionD[OF f] simple_functionD[OF f] by simp_all 

223 
have "\<forall>x. \<exists>N. N \<in> null_sets M \<and> null_part M (?F x) \<subseteq> N" 

40859  224 
using F null_part by auto 
225 
from choice[OF this] obtain N where 

47694  226 
N: "\<And>x. null_part M (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets M" by auto 
46731  227 
let ?N = "\<Union>x\<in>f`space M. N x" 
228 
let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x" 

47694  229 
have sets: "?N \<in> null_sets M" using N fin by (intro null_sets.finite_UN) auto 
40859  230 
show ?thesis unfolding simple_function_def 
231 
proof (safe intro!: exI[of _ ?f']) 

232 
have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto 

47694  233 
from finite_subset[OF this] simple_functionD(1)[OF f] 
40859  234 
show "finite (?f' ` space M)" by auto 
235 
next 

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

237 
have "?f' ` {?f' x} \<inter> space M = 

238 
(if x \<in> ?N then ?F undefined \<union> ?N 

239 
else if f x = undefined then ?F (f x) \<union> ?N 

240 
else ?F (f x)  ?N)" 

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

241 
using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def) 
40859  242 
moreover { fix y have "?F y \<union> ?N \<in> sets M" 
243 
proof cases 

244 
assume y: "y \<in> f`space M" 

47694  245 
have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N" 
40859  246 
using main_part_null_part_Un[OF F] by auto 
47694  247 
also have "\<dots> = main_part M (?F y) \<union> ?N" 
40859  248 
using y N by auto 
249 
finally show ?thesis 

250 
using F sets by auto 

251 
next 

252 
assume "y \<notin> f`space M" then have "?F y = {}" by auto 

253 
then show ?thesis using sets by auto 

254 
qed } 

255 
moreover { 

47694  256 
have "?F (f x)  ?N = main_part M (?F (f x)) \<union> null_part M (?F (f x))  ?N" 
40859  257 
using main_part_null_part_Un[OF F] by auto 
47694  258 
also have "\<dots> = main_part M (?F (f x))  ?N" 
40859  259 
using N `x \<in> space M` by auto 
260 
finally have "?F (f x)  ?N \<in> sets M" 

261 
using F sets by auto } 

262 
ultimately show "?f' ` {?f' x} \<inter> space M \<in> sets M" by auto 

263 
next 

47694  264 
show "AE x in M. f x = ?f' x" 
40859  265 
by (rule AE_I', rule sets) auto 
266 
qed 

267 
qed 

268 

47694  269 
lemma completion_ex_borel_measurable_pos: 
43920  270 
fixes g :: "'a \<Rightarrow> ereal" 
47694  271 
assumes g: "g \<in> borel_measurable (completion M)" and "\<And>x. 0 \<le> g x" 
272 
shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)" 

40859  273 
proof  
47694  274 
from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

275 
from this(1)[THEN completion_ex_simple_function] 
47694  276 
have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" .. 
40859  277 
from this[THEN choice] obtain f' where 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41097
diff
changeset

278 
sf: "\<And>i. simple_function M (f' i)" and 
47694  279 
AE: "\<forall>i. AE x in M. f i x = f' i x" by auto 
40859  280 
show ?thesis 
281 
proof (intro bexI) 

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

282 
from AE[unfolded AE_all_countable[symmetric]] 
47694  283 
show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x") 
41705  284 
proof (elim AE_mp, safe intro!: AE_I2) 
40859  285 
fix x assume eq: "\<forall>i. f i x = f' i x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

286 
moreover have "g x = (SUP i. f i x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

287 
unfolding f using `0 \<le> g x` by (auto split: split_max) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

288 
ultimately show "g x = ?f x" by auto 
40859  289 
qed 
290 
show "?f \<in> borel_measurable M" 

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41023
diff
changeset

291 
using sf by (auto intro: borel_measurable_simple_function) 
40859  292 
qed 
293 
qed 

294 

47694  295 
lemma completion_ex_borel_measurable: 
43920  296 
fixes g :: "'a \<Rightarrow> ereal" 
47694  297 
assumes g: "g \<in> borel_measurable (completion M)" 
298 
shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)" 

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

299 
proof  
47694  300 
have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable (completion M)" "\<And>x. 0 \<le> max 0 (g x)" using g by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

301 
from completion_ex_borel_measurable_pos[OF this] guess g_pos .. 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

302 
moreover 
47694  303 
have "(\<lambda>x. max 0 ( g x)) \<in> borel_measurable (completion M)" "\<And>x. 0 \<le> max 0 ( g x)" using g by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

304 
from completion_ex_borel_measurable_pos[OF this] guess g_neg .. 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

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

306 
show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

307 
proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x  g_neg x"]) 
47694  308 
show "AE x in M. max 0 ( g x) = g_neg x \<longrightarrow> max 0 (g x) = g_pos x \<longrightarrow> g x = g_pos x  g_neg x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

309 
proof (intro AE_I2 impI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

310 
fix x assume g: "max 0 ( g x) = g_neg x" "max 0 (g x) = g_pos x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

311 
show "g x = g_pos x  g_neg x" unfolding g[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

312 
by (cases "g x") (auto split: split_max) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

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

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

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

316 

40859  317 
end 