40859
|
1 |
(* Title: Complete_Measure.thy
|
|
2 |
Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen
|
|
3 |
*)
|
|
4 |
theory Complete_Measure
|
|
5 |
imports Product_Measure
|
|
6 |
begin
|
|
7 |
|
|
8 |
locale completeable_measure_space = measure_space
|
|
9 |
|
|
10 |
definition (in completeable_measure_space) completion :: "'a algebra" where
|
|
11 |
"completion = \<lparr> space = space M,
|
|
12 |
sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"
|
|
13 |
|
|
14 |
lemma (in completeable_measure_space) space_completion[simp]:
|
|
15 |
"space completion = space M" unfolding completion_def by simp
|
|
16 |
|
|
17 |
lemma (in completeable_measure_space) sets_completionE:
|
|
18 |
assumes "A \<in> sets completion"
|
|
19 |
obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
|
|
20 |
using assms unfolding completion_def by auto
|
|
21 |
|
|
22 |
lemma (in completeable_measure_space) sets_completionI:
|
|
23 |
assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
|
|
24 |
shows "A \<in> sets completion"
|
|
25 |
using assms unfolding completion_def by auto
|
|
26 |
|
|
27 |
lemma (in completeable_measure_space) sets_completionI_sets[intro]:
|
|
28 |
"A \<in> sets M \<Longrightarrow> A \<in> sets completion"
|
|
29 |
unfolding completion_def by force
|
|
30 |
|
|
31 |
lemma (in completeable_measure_space) null_sets_completion:
|
|
32 |
assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
|
|
33 |
apply(rule sets_completionI[of N "{}" N N'])
|
|
34 |
using assms by auto
|
|
35 |
|
|
36 |
sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
|
|
37 |
proof (unfold sigma_algebra_iff2, safe)
|
|
38 |
fix A x assume "A \<in> sets completion" "x \<in> A"
|
|
39 |
with sets_into_space show "x \<in> space completion"
|
|
40 |
by (auto elim!: sets_completionE)
|
|
41 |
next
|
|
42 |
fix A assume "A \<in> sets completion"
|
|
43 |
from this[THEN sets_completionE] guess S N N' . note A = this
|
|
44 |
let ?C = "space completion"
|
|
45 |
show "?C - A \<in> sets completion" using A
|
|
46 |
by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
|
|
47 |
auto
|
|
48 |
next
|
|
49 |
fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
|
|
50 |
then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N'"
|
|
51 |
unfolding completion_def by (auto simp: image_subset_iff)
|
|
52 |
from choice[OF this] guess S ..
|
|
53 |
from choice[OF this] guess N ..
|
|
54 |
from choice[OF this] guess N' ..
|
|
55 |
then show "UNION UNIV A \<in> sets completion"
|
|
56 |
using null_sets_UN[of N']
|
|
57 |
by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
|
|
58 |
auto
|
|
59 |
qed auto
|
|
60 |
|
|
61 |
definition (in completeable_measure_space)
|
|
62 |
"split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
|
|
63 |
fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
|
|
64 |
|
|
65 |
definition (in completeable_measure_space)
|
|
66 |
"main_part A = fst (Eps (split_completion A))"
|
|
67 |
|
|
68 |
definition (in completeable_measure_space)
|
|
69 |
"null_part A = snd (Eps (split_completion A))"
|
|
70 |
|
|
71 |
lemma (in completeable_measure_space) split_completion:
|
|
72 |
assumes "A \<in> sets completion"
|
|
73 |
shows "split_completion A (main_part A, null_part A)"
|
|
74 |
unfolding main_part_def null_part_def
|
|
75 |
proof (rule someI2_ex)
|
|
76 |
from assms[THEN sets_completionE] guess S N N' . note A = this
|
|
77 |
let ?P = "(S, N - S)"
|
|
78 |
show "\<exists>p. split_completion A p"
|
|
79 |
unfolding split_completion_def using A
|
|
80 |
proof (intro exI conjI)
|
|
81 |
show "A = fst ?P \<union> snd ?P" using A by auto
|
|
82 |
show "snd ?P \<subseteq> N'" using A by auto
|
|
83 |
qed auto
|
|
84 |
qed auto
|
|
85 |
|
|
86 |
lemma (in completeable_measure_space)
|
|
87 |
assumes "S \<in> sets completion"
|
|
88 |
shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
|
|
89 |
and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
|
|
90 |
and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
|
|
91 |
using split_completion[OF assms] by (auto simp: split_completion_def)
|
|
92 |
|
|
93 |
lemma (in completeable_measure_space) null_part:
|
|
94 |
assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
|
|
95 |
using split_completion[OF assms] by (auto simp: split_completion_def)
|
|
96 |
|
|
97 |
lemma (in completeable_measure_space) null_part_sets[intro, simp]:
|
|
98 |
assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
|
|
99 |
proof -
|
|
100 |
have S: "S \<in> sets completion" using assms by auto
|
|
101 |
have "S - main_part S \<in> sets M" using assms by auto
|
|
102 |
moreover
|
|
103 |
from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
|
|
104 |
have "S - main_part S = null_part S" by auto
|
|
105 |
ultimately show sets: "null_part S \<in> sets M" by auto
|
|
106 |
from null_part[OF S] guess N ..
|
|
107 |
with measure_eq_0[of N "null_part S"] sets
|
|
108 |
show "\<mu> (null_part S) = 0" by auto
|
|
109 |
qed
|
|
110 |
|
|
111 |
definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"
|
|
112 |
|
|
113 |
lemma (in completeable_measure_space) \<mu>'_set[simp]:
|
|
114 |
assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
|
|
115 |
proof -
|
|
116 |
have S: "S \<in> sets completion" using assms by auto
|
|
117 |
then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
|
|
118 |
also have "\<dots> = \<mu> (main_part S)"
|
|
119 |
using S assms measure_additive[of "main_part S" "null_part S"]
|
|
120 |
by (auto simp: measure_additive)
|
|
121 |
finally show ?thesis unfolding \<mu>'_def by simp
|
|
122 |
qed
|
|
123 |
|
|
124 |
lemma (in completeable_measure_space) sets_completionI_sub:
|
|
125 |
assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
|
|
126 |
shows "N \<in> sets completion"
|
|
127 |
using assms by (intro sets_completionI[of _ "{}" N N']) auto
|
|
128 |
|
|
129 |
lemma (in completeable_measure_space) \<mu>_main_part_UN:
|
|
130 |
fixes S :: "nat \<Rightarrow> 'a set"
|
|
131 |
assumes "range S \<subseteq> sets completion"
|
|
132 |
shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
|
|
133 |
proof -
|
|
134 |
have S: "\<And>i. S i \<in> sets completion" using assms by auto
|
|
135 |
then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
|
|
136 |
have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
|
|
137 |
using null_part[OF S] by auto
|
|
138 |
from choice[OF this] guess N .. note N = this
|
|
139 |
then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
|
|
140 |
have "(\<Union>i. S i) \<in> sets completion" using S by auto
|
|
141 |
from null_part[OF this] guess N' .. note N' = this
|
|
142 |
let ?N = "(\<Union>i. N i) \<union> N'"
|
|
143 |
have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
|
|
144 |
have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
|
|
145 |
using N' by auto
|
|
146 |
also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
|
|
147 |
unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
|
|
148 |
also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
|
|
149 |
using N by auto
|
|
150 |
finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
|
|
151 |
have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
|
|
152 |
using null_set UN by (intro measure_Un_null_set[symmetric]) auto
|
|
153 |
also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
|
|
154 |
unfolding * ..
|
|
155 |
also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
|
|
156 |
using null_set S by (intro measure_Un_null_set) auto
|
|
157 |
finally show ?thesis unfolding \<mu>'_def .
|
|
158 |
qed
|
|
159 |
|
|
160 |
lemma (in completeable_measure_space) \<mu>_main_part_Un:
|
|
161 |
assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
|
|
162 |
shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
|
|
163 |
proof -
|
|
164 |
have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
|
|
165 |
unfolding binary_def by (auto split: split_if_asm)
|
|
166 |
show ?thesis
|
|
167 |
using \<mu>_main_part_UN[of "binary S T"] assms
|
|
168 |
unfolding range_binary_eq Un_range_binary UN by auto
|
|
169 |
qed
|
|
170 |
|
|
171 |
sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
|
|
172 |
proof
|
|
173 |
show "\<mu>' {} = 0" by auto
|
|
174 |
next
|
|
175 |
show "countably_additive completion \<mu>'"
|
|
176 |
proof (unfold countably_additive_def, intro allI conjI impI)
|
|
177 |
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
|
|
178 |
have "disjoint_family (\<lambda>i. main_part (A i))"
|
|
179 |
proof (intro disjoint_family_on_bisimulation[OF A(2)])
|
|
180 |
fix n m assume "A n \<inter> A m = {}"
|
|
181 |
then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
|
|
182 |
using A by (subst (1 2) main_part_null_part_Un) auto
|
|
183 |
then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
|
|
184 |
qed
|
|
185 |
then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
|
|
186 |
unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
|
|
187 |
then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
|
|
188 |
unfolding \<mu>_main_part_UN[OF A(1)] .
|
|
189 |
qed
|
|
190 |
qed
|
|
191 |
|
|
192 |
lemma (in completeable_measure_space) completion_ex_simple_function:
|
|
193 |
assumes f: "completion.simple_function f"
|
|
194 |
shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
|
|
195 |
proof -
|
|
196 |
let "?F x" = "f -` {x} \<inter> space M"
|
|
197 |
have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
|
40871
|
198 |
using completion.simple_functionD[OF f]
|
40859
|
199 |
completion.simple_functionD[OF f] by simp_all
|
|
200 |
have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
|
|
201 |
using F null_part by auto
|
|
202 |
from choice[OF this] obtain N where
|
|
203 |
N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
|
|
204 |
let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
|
|
205 |
have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
|
|
206 |
show ?thesis unfolding simple_function_def
|
|
207 |
proof (safe intro!: exI[of _ ?f'])
|
|
208 |
have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
|
|
209 |
from finite_subset[OF this] completion.simple_functionD(1)[OF f]
|
|
210 |
show "finite (?f' ` space M)" by auto
|
|
211 |
next
|
|
212 |
fix x assume "x \<in> space M"
|
|
213 |
have "?f' -` {?f' x} \<inter> space M =
|
|
214 |
(if x \<in> ?N then ?F undefined \<union> ?N
|
|
215 |
else if f x = undefined then ?F (f x) \<union> ?N
|
|
216 |
else ?F (f x) - ?N)"
|
|
217 |
using N(2) sets_into_space by (auto split: split_if_asm)
|
|
218 |
moreover { fix y have "?F y \<union> ?N \<in> sets M"
|
|
219 |
proof cases
|
|
220 |
assume y: "y \<in> f`space M"
|
|
221 |
have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
|
|
222 |
using main_part_null_part_Un[OF F] by auto
|
|
223 |
also have "\<dots> = main_part (?F y) \<union> ?N"
|
|
224 |
using y N by auto
|
|
225 |
finally show ?thesis
|
|
226 |
using F sets by auto
|
|
227 |
next
|
|
228 |
assume "y \<notin> f`space M" then have "?F y = {}" by auto
|
|
229 |
then show ?thesis using sets by auto
|
|
230 |
qed }
|
|
231 |
moreover {
|
|
232 |
have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
|
|
233 |
using main_part_null_part_Un[OF F] by auto
|
|
234 |
also have "\<dots> = main_part (?F (f x)) - ?N"
|
|
235 |
using N `x \<in> space M` by auto
|
|
236 |
finally have "?F (f x) - ?N \<in> sets M"
|
|
237 |
using F sets by auto }
|
|
238 |
ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
|
|
239 |
next
|
|
240 |
show "AE x. f x = ?f' x"
|
|
241 |
by (rule AE_I', rule sets) auto
|
|
242 |
qed
|
|
243 |
qed
|
|
244 |
|
|
245 |
lemma (in completeable_measure_space) completion_ex_borel_measurable:
|
|
246 |
fixes g :: "'a \<Rightarrow> pinfreal"
|
|
247 |
assumes g: "g \<in> borel_measurable completion"
|
|
248 |
shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
|
|
249 |
proof -
|
|
250 |
from g[THEN completion.borel_measurable_implies_simple_function_sequence]
|
|
251 |
obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
|
|
252 |
then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
|
|
253 |
using completion_ex_simple_function by auto
|
|
254 |
from this[THEN choice] obtain f' where
|
|
255 |
sf: "\<And>i. simple_function (f' i)" and
|
|
256 |
AE: "\<forall>i. AE x. f i x = f' i x" by auto
|
|
257 |
show ?thesis
|
|
258 |
proof (intro bexI)
|
|
259 |
from AE[unfolded all_AE_countable]
|
|
260 |
show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
|
|
261 |
proof (rule AE_mp, safe intro!: AE_cong)
|
|
262 |
fix x assume eq: "\<forall>i. f i x = f' i x"
|
|
263 |
have "g x = (SUP i. f i x)"
|
|
264 |
using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
|
|
265 |
then show "g x = ?f x"
|
|
266 |
using eq unfolding SUPR_fun_expand by auto
|
|
267 |
qed
|
|
268 |
show "?f \<in> borel_measurable M"
|
|
269 |
using sf by (auto intro!: borel_measurable_SUP
|
|
270 |
intro: borel_measurable_simple_function)
|
|
271 |
qed
|
|
272 |
qed
|
|
273 |
|
|
274 |
end
|