35582
|
1 |
header {*Lebesgue Integration*}
|
|
2 |
|
|
3 |
theory Lebesgue
|
|
4 |
imports Measure Borel
|
|
5 |
begin
|
|
6 |
|
|
7 |
text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}
|
|
8 |
|
|
9 |
definition
|
|
10 |
"pos_part f = (\<lambda>x. max 0 (f x))"
|
|
11 |
|
|
12 |
definition
|
|
13 |
"neg_part f = (\<lambda>x. - min 0 (f x))"
|
|
14 |
|
|
15 |
definition
|
|
16 |
"nonneg f = (\<forall>x. 0 \<le> f x)"
|
|
17 |
|
|
18 |
lemma nonneg_pos_part[intro!]:
|
|
19 |
fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"
|
|
20 |
shows "nonneg (pos_part f)"
|
|
21 |
unfolding nonneg_def pos_part_def by auto
|
|
22 |
|
|
23 |
lemma nonneg_neg_part[intro!]:
|
|
24 |
fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"
|
|
25 |
shows "nonneg (neg_part f)"
|
|
26 |
unfolding nonneg_def neg_part_def min_def by auto
|
|
27 |
|
|
28 |
context measure_space
|
|
29 |
begin
|
|
30 |
|
|
31 |
definition
|
|
32 |
"pos_simple f =
|
|
33 |
{ (s :: nat set, a, x).
|
|
34 |
finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>
|
|
35 |
(\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"
|
|
36 |
|
|
37 |
definition
|
|
38 |
"pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"
|
|
39 |
|
|
40 |
definition
|
|
41 |
"psfis f = pos_simple_integral ` (pos_simple f)"
|
|
42 |
|
|
43 |
definition
|
|
44 |
"nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
|
|
45 |
(\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
|
|
46 |
|
|
47 |
definition
|
|
48 |
"integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
|
|
49 |
|
|
50 |
definition
|
|
51 |
"integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
|
|
52 |
|
|
53 |
definition
|
|
54 |
"enumerate s \<equiv> SOME f. bij_betw f UNIV s"
|
|
55 |
|
|
56 |
definition
|
|
57 |
"countable_space_integral f \<equiv>
|
|
58 |
let e = enumerate (f ` space M) in
|
|
59 |
suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
|
|
60 |
|
|
61 |
definition
|
|
62 |
"RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
|
|
63 |
f \<in> borel_measurable M \<and>
|
|
64 |
(\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
|
|
65 |
|
|
66 |
lemma pos_simpleE[consumes 1]:
|
|
67 |
assumes ps: "(s, a, x) \<in> pos_simple f"
|
|
68 |
obtains "finite s" and "nonneg f" and "nonneg x"
|
|
69 |
and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"
|
|
70 |
and "disjoint_family_on a s"
|
|
71 |
and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
|
|
72 |
and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
|
|
73 |
proof
|
|
74 |
show "finite s" and "nonneg f" and "nonneg x"
|
|
75 |
and as_in_M: "a ` s \<subseteq> sets M"
|
|
76 |
and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
|
|
77 |
and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
|
|
78 |
using ps unfolding pos_simple_def by auto
|
|
79 |
|
|
80 |
thus t: "(\<Union>i\<in>s. a i) = space M"
|
|
81 |
proof safe
|
|
82 |
fix x assume "x \<in> space M"
|
|
83 |
from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto
|
|
84 |
next
|
|
85 |
fix t i assume "i \<in> s"
|
|
86 |
hence "a i \<in> sets M" using as_in_M by auto
|
|
87 |
moreover assume "t \<in> a i"
|
|
88 |
ultimately show "t \<in> space M" using sets_into_space by blast
|
|
89 |
qed
|
|
90 |
|
|
91 |
show "disjoint_family_on a s" unfolding disjoint_family_on_def
|
|
92 |
proof safe
|
|
93 |
fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"
|
|
94 |
with t * show "t \<in> {}" by auto
|
|
95 |
qed
|
|
96 |
qed
|
|
97 |
|
|
98 |
lemma pos_simple_cong:
|
|
99 |
assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
|
|
100 |
shows "pos_simple f = pos_simple g"
|
|
101 |
unfolding pos_simple_def using assms by auto
|
|
102 |
|
|
103 |
lemma psfis_cong:
|
|
104 |
assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
|
|
105 |
shows "psfis f = psfis g"
|
|
106 |
unfolding psfis_def using pos_simple_cong[OF assms] by simp
|
|
107 |
|
|
108 |
lemma pos_simple_setsum_indicator_fn:
|
|
109 |
assumes ps: "(s, a, x) \<in> pos_simple f"
|
|
110 |
and "t \<in> space M"
|
|
111 |
shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"
|
|
112 |
proof -
|
|
113 |
from assms obtain i where *: "i \<in> s" "t \<in> a i"
|
|
114 |
and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)
|
|
115 |
|
|
116 |
have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =
|
|
117 |
(\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"
|
|
118 |
unfolding indicator_fn_def using assms *
|
|
119 |
by (auto intro!: setsum_cong elim!: pos_simpleE)
|
|
120 |
show ?thesis unfolding ** setsum_cases[OF `finite s`] xi
|
|
121 |
using `i \<in> s` by simp
|
|
122 |
qed
|
|
123 |
|
|
124 |
lemma (in measure_space) measure_setsum_split:
|
|
125 |
assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
|
|
126 |
assumes "(\<Union>i \<in> r. b i) = space M"
|
|
127 |
assumes "disjoint_family_on b r"
|
|
128 |
shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
|
|
129 |
proof -
|
|
130 |
have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
|
|
131 |
using assms by auto
|
|
132 |
show ?thesis unfolding *
|
|
133 |
proof (rule measure_finitely_additive''[symmetric])
|
|
134 |
show "finite r" using `finite r` by auto
|
|
135 |
{ fix i assume "i \<in> r"
|
|
136 |
hence "b i \<in> sets M" using br_in_M by auto
|
|
137 |
thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
|
|
138 |
}
|
|
139 |
show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
|
|
140 |
using `disjoint_family_on b r`
|
|
141 |
unfolding disjoint_family_on_def by auto
|
|
142 |
qed
|
|
143 |
qed
|
|
144 |
|
|
145 |
lemma (in measure_space) pos_simple_common_partition:
|
|
146 |
assumes psf: "(s, a, x) \<in> pos_simple f"
|
|
147 |
assumes psg: "(s', b, y) \<in> pos_simple g"
|
|
148 |
obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
|
|
149 |
proof -
|
|
150 |
(* definitions *)
|
|
151 |
|
|
152 |
def k == "{0 ..< card (s \<times> s')}"
|
|
153 |
have fs: "finite s" "finite s'" "finite k" unfolding k_def
|
|
154 |
using psf psg unfolding pos_simple_def by auto
|
|
155 |
hence "finite (s \<times> s')" by simp
|
|
156 |
then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"
|
|
157 |
using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast
|
|
158 |
def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"
|
|
159 |
def z == "\<lambda> i. x (fst (p i))"
|
|
160 |
def z' == "\<lambda> i. y (snd (p i))"
|
|
161 |
|
|
162 |
have "finite k" unfolding k_def by simp
|
|
163 |
|
|
164 |
have "nonneg z" and "nonneg z'"
|
|
165 |
using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto
|
|
166 |
|
|
167 |
have ck_subset_M: "c ` k \<subseteq> sets M"
|
|
168 |
proof
|
|
169 |
fix x assume "x \<in> c ` k"
|
|
170 |
then obtain j where "j \<in> k" and "x = c j" by auto
|
|
171 |
hence "p j \<in> s \<times> s'" using p(1) by auto
|
|
172 |
hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")
|
|
173 |
and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")
|
|
174 |
using psf psg unfolding pos_simple_def by auto
|
|
175 |
thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp
|
|
176 |
qed
|
|
177 |
|
|
178 |
{ fix t assume "t \<in> space M"
|
|
179 |
hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"
|
|
180 |
using psf psg unfolding pos_simple_def by auto
|
|
181 |
then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"
|
|
182 |
by auto
|
|
183 |
then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto
|
|
184 |
have "\<exists>!i\<in>k. t \<in> c i"
|
|
185 |
proof (rule ex1I[of _ i])
|
|
186 |
show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"
|
|
187 |
proof -
|
|
188 |
fix l assume "l \<in> k" "t \<in> c l"
|
|
189 |
hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"
|
|
190 |
using p unfolding c_def by auto
|
|
191 |
hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto
|
|
192 |
with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)
|
|
193 |
thus "l = i"
|
|
194 |
using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto
|
|
195 |
qed
|
|
196 |
|
|
197 |
show "i \<in> k \<and> t \<in> c i"
|
|
198 |
using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto
|
|
199 |
qed auto
|
|
200 |
} note ex1 = this
|
|
201 |
|
|
202 |
show thesis
|
|
203 |
proof (rule that)
|
|
204 |
{ fix t i assume "t \<in> space M" and "i \<in> k"
|
|
205 |
hence "p i \<in> s \<times> s'" using p(1) by auto
|
|
206 |
hence "fst (p i) \<in> s" by auto
|
|
207 |
moreover
|
|
208 |
assume "t \<in> c i"
|
|
209 |
hence "t \<in> a (fst (p i))" unfolding c_def by auto
|
|
210 |
ultimately have "f t = z i" using psf `t \<in> space M`
|
|
211 |
unfolding z_def pos_simple_def by auto
|
|
212 |
}
|
|
213 |
thus "(k, c, z) \<in> pos_simple f"
|
|
214 |
using psf `finite k` `nonneg z` ck_subset_M ex1
|
|
215 |
unfolding pos_simple_def by auto
|
|
216 |
|
|
217 |
{ fix t i assume "t \<in> space M" and "i \<in> k"
|
|
218 |
hence "p i \<in> s \<times> s'" using p(1) by auto
|
|
219 |
hence "snd (p i) \<in> s'" by auto
|
|
220 |
moreover
|
|
221 |
assume "t \<in> c i"
|
|
222 |
hence "t \<in> b (snd (p i))" unfolding c_def by auto
|
|
223 |
ultimately have "g t = z' i" using psg `t \<in> space M`
|
|
224 |
unfolding z'_def pos_simple_def by auto
|
|
225 |
}
|
|
226 |
thus "(k, c, z') \<in> pos_simple g"
|
|
227 |
using psg `finite k` `nonneg z'` ck_subset_M ex1
|
|
228 |
unfolding pos_simple_def by auto
|
|
229 |
qed
|
|
230 |
qed
|
|
231 |
|
|
232 |
lemma (in measure_space) pos_simple_integral_equal:
|
|
233 |
assumes psx: "(s, a, x) \<in> pos_simple f"
|
|
234 |
assumes psy: "(s', b, y) \<in> pos_simple f"
|
|
235 |
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
|
|
236 |
unfolding pos_simple_integral_def
|
|
237 |
proof simp
|
|
238 |
have "(\<Sum>i\<in>s. x i * measure M (a i)) =
|
|
239 |
(\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")
|
|
240 |
using psy psx unfolding setsum_right_distrib[symmetric]
|
|
241 |
by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)
|
|
242 |
also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"
|
|
243 |
proof (rule setsum_cong, simp, rule setsum_cong, simp_all)
|
|
244 |
fix i j assume i: "i \<in> s" and j: "j \<in> s'"
|
|
245 |
hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)
|
|
246 |
|
|
247 |
show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"
|
|
248 |
proof (cases "a i \<inter> b j = {}")
|
|
249 |
case True thus ?thesis using empty_measure by simp
|
|
250 |
next
|
|
251 |
case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto
|
|
252 |
hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto
|
|
253 |
with psx psy t i j have "x i = f t" and "y j = f t"
|
|
254 |
unfolding pos_simple_def by auto
|
|
255 |
thus ?thesis by simp
|
|
256 |
qed
|
|
257 |
qed
|
|
258 |
also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"
|
|
259 |
by (subst setsum_commute) simp
|
|
260 |
also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")
|
|
261 |
proof (rule setsum_cong)
|
|
262 |
fix j assume "j \<in> s'"
|
|
263 |
have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"
|
|
264 |
using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]
|
|
265 |
by (auto intro!: measure_setsum_split elim!: pos_simpleE)
|
|
266 |
thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"
|
|
267 |
by (auto intro!: setsum_cong arg_cong[where f="measure M"])
|
|
268 |
qed simp
|
|
269 |
finally show "?left = ?right" .
|
|
270 |
qed
|
|
271 |
|
|
272 |
lemma (in measure_space)psfis_present:
|
|
273 |
assumes "A \<in> psfis f"
|
|
274 |
assumes "B \<in> psfis g"
|
|
275 |
obtains z z' c k where
|
|
276 |
"A = pos_simple_integral (k, c, z)"
|
|
277 |
"B = pos_simple_integral (k, c, z')"
|
|
278 |
"(k, c, z) \<in> pos_simple f"
|
|
279 |
"(k, c, z') \<in> pos_simple g"
|
|
280 |
using assms
|
|
281 |
proof -
|
|
282 |
from assms obtain s a x s' b y where
|
|
283 |
ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and
|
|
284 |
A: "A = pos_simple_integral (s, a, x)" and
|
|
285 |
B: "B = pos_simple_integral (s', b, y)"
|
|
286 |
unfolding psfis_def pos_simple_integral_def by auto
|
|
287 |
|
|
288 |
guess z z' c k using pos_simple_common_partition[OF ps] . note part = this
|
|
289 |
show thesis
|
|
290 |
proof (rule that[of k c z z', OF _ _ part])
|
|
291 |
show "A = pos_simple_integral (k, c, z)"
|
|
292 |
unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])
|
|
293 |
show "B = pos_simple_integral (k, c, z')"
|
|
294 |
unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])
|
|
295 |
qed
|
|
296 |
qed
|
|
297 |
|
|
298 |
lemma (in measure_space) pos_simple_integral_add:
|
|
299 |
assumes "(s, a, x) \<in> pos_simple f"
|
|
300 |
assumes "(s', b, y) \<in> pos_simple g"
|
|
301 |
obtains s'' c z where
|
|
302 |
"(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"
|
|
303 |
"(pos_simple_integral (s, a, x) +
|
|
304 |
pos_simple_integral (s', b, y) =
|
|
305 |
pos_simple_integral (s'', c, z))"
|
|
306 |
using assms
|
|
307 |
proof -
|
|
308 |
guess z z' c k
|
|
309 |
by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])
|
|
310 |
note kczz' = this
|
|
311 |
have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
|
|
312 |
by (rule pos_simple_integral_equal) (fact, fact)
|
|
313 |
have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"
|
|
314 |
by (rule pos_simple_integral_equal) (fact, fact)
|
|
315 |
|
|
316 |
have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
|
|
317 |
= (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
|
|
318 |
unfolding pos_simple_integral_def by auto
|
|
319 |
also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
|
|
320 |
also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
|
|
321 |
also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
|
|
322 |
finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
|
|
323 |
pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto
|
|
324 |
show ?thesis
|
|
325 |
apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])
|
|
326 |
using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)
|
|
327 |
qed
|
|
328 |
|
|
329 |
lemma psfis_add:
|
|
330 |
assumes "a \<in> psfis f" "b \<in> psfis g"
|
|
331 |
shows "a + b \<in> psfis (\<lambda>x. f x + g x)"
|
|
332 |
using assms pos_simple_integral_add
|
|
333 |
unfolding psfis_def by auto blast
|
|
334 |
|
|
335 |
lemma pos_simple_integral_mono_on_mspace:
|
|
336 |
assumes f: "(s, a, x) \<in> pos_simple f"
|
|
337 |
assumes g: "(s', b, y) \<in> pos_simple g"
|
|
338 |
assumes mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
|
|
339 |
shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
|
|
340 |
using assms
|
|
341 |
proof -
|
|
342 |
guess z z' c k by (rule pos_simple_common_partition[OF f g])
|
|
343 |
note kczz' = this
|
|
344 |
(* w = z and w' = z' except where c _ = {} or undef *)
|
|
345 |
def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"
|
|
346 |
def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"
|
|
347 |
{ fix i
|
|
348 |
have "w i \<le> w' i"
|
|
349 |
proof (cases "i \<notin> k \<or> c i = {}")
|
|
350 |
case False hence "i \<in> k" "c i \<noteq> {}" by auto
|
|
351 |
then obtain v where v: "v \<in> c i" and "c i \<in> sets M"
|
|
352 |
using kczz'(1) unfolding pos_simple_def by blast
|
|
353 |
hence "v \<in> space M" using sets_into_space by blast
|
|
354 |
with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`
|
|
355 |
have "z i \<le> z' i" unfolding pos_simple_def by simp
|
|
356 |
thus ?thesis unfolding w_def w'_def using False by auto
|
|
357 |
next
|
|
358 |
case True thus ?thesis unfolding w_def w'_def by auto
|
|
359 |
qed
|
|
360 |
} note w_mn = this
|
|
361 |
|
|
362 |
(* some technical stuff for the calculation*)
|
|
363 |
have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto
|
|
364 |
hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto
|
|
365 |
hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"
|
|
366 |
using mult_right_mono w_mn by blast
|
|
367 |
|
|
368 |
{ fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"
|
|
369 |
unfolding w_def by (cases "c i = {}") auto }
|
|
370 |
hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto
|
|
371 |
|
|
372 |
{ fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"
|
|
373 |
unfolding w_def by (cases "c i = {}") simp_all }
|
|
374 |
note zw = this
|
|
375 |
|
|
376 |
{ fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"
|
|
377 |
unfolding w'_def by (cases "c i = {}") simp_all }
|
|
378 |
note z'w' = this
|
|
379 |
|
|
380 |
(* the calculation *)
|
|
381 |
have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
|
|
382 |
using f kczz'(1) by (rule pos_simple_integral_equal)
|
|
383 |
also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"
|
|
384 |
unfolding pos_simple_integral_def by auto
|
|
385 |
also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"
|
|
386 |
using setsum_cong2[of k, OF zw] by auto
|
|
387 |
also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"
|
|
388 |
using setsum_mono[OF w_mono, of k] by auto
|
|
389 |
also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"
|
|
390 |
using setsum_cong2[of k, OF z'w'] by auto
|
|
391 |
also have "\<dots> = pos_simple_integral (k, c, z')"
|
|
392 |
unfolding pos_simple_integral_def by auto
|
|
393 |
also have "\<dots> = pos_simple_integral (s', b, y)"
|
|
394 |
using kczz'(2) g by (rule pos_simple_integral_equal)
|
|
395 |
finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
|
|
396 |
by simp
|
|
397 |
qed
|
|
398 |
|
|
399 |
lemma pos_simple_integral_mono:
|
|
400 |
assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"
|
|
401 |
assumes "\<And> z. f z \<le> g z"
|
|
402 |
shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
|
|
403 |
using assms pos_simple_integral_mono_on_mspace by auto
|
|
404 |
|
|
405 |
lemma psfis_mono:
|
|
406 |
assumes "a \<in> psfis f" "b \<in> psfis g"
|
|
407 |
assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
|
|
408 |
shows "a \<le> b"
|
|
409 |
using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto
|
|
410 |
|
|
411 |
lemma pos_simple_fn_integral_unique:
|
|
412 |
assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
|
|
413 |
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
|
|
414 |
using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
|
|
415 |
|
|
416 |
lemma psfis_unique:
|
|
417 |
assumes "a \<in> psfis f" "b \<in> psfis f"
|
|
418 |
shows "a = b"
|
|
419 |
using assms real_le_antisym real_le_refl psfis_mono by metis
|
|
420 |
|
|
421 |
lemma pos_simple_integral_indicator:
|
|
422 |
assumes "A \<in> sets M"
|
|
423 |
obtains s a x where
|
|
424 |
"(s, a, x) \<in> pos_simple (indicator_fn A)"
|
|
425 |
"measure M A = pos_simple_integral (s, a, x)"
|
|
426 |
using assms
|
|
427 |
proof -
|
|
428 |
def s == "{0, 1} :: nat set"
|
|
429 |
def a == "\<lambda> i :: nat. if i = 0 then A else space M - A"
|
|
430 |
def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"
|
|
431 |
have eq: "pos_simple_integral (s, a, x) = measure M A"
|
|
432 |
unfolding s_def a_def x_def pos_simple_integral_def by auto
|
|
433 |
have "(s, a, x) \<in> pos_simple (indicator_fn A)"
|
|
434 |
unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def
|
|
435 |
using assms sets_into_space by auto
|
|
436 |
from that[OF this] eq show thesis by auto
|
|
437 |
qed
|
|
438 |
|
|
439 |
lemma psfis_indicator:
|
|
440 |
assumes "A \<in> sets M"
|
|
441 |
shows "measure M A \<in> psfis (indicator_fn A)"
|
|
442 |
using pos_simple_integral_indicator[OF assms]
|
|
443 |
unfolding psfis_def image_def by auto
|
|
444 |
|
|
445 |
lemma pos_simple_integral_mult:
|
|
446 |
assumes f: "(s, a, x) \<in> pos_simple f"
|
|
447 |
assumes "0 \<le> z"
|
|
448 |
obtains s' b y where
|
|
449 |
"(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
|
|
450 |
"pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"
|
|
451 |
using assms that[of s a "\<lambda>i. z * x i"]
|
|
452 |
by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)
|
|
453 |
|
|
454 |
lemma psfis_mult:
|
|
455 |
assumes "r \<in> psfis f"
|
|
456 |
assumes "0 \<le> z"
|
|
457 |
shows "z * r \<in> psfis (\<lambda>x. z * f x)"
|
|
458 |
using assms
|
|
459 |
proof -
|
|
460 |
from assms obtain s a x
|
|
461 |
where sax: "(s, a, x) \<in> pos_simple f"
|
|
462 |
and r: "r = pos_simple_integral (s, a, x)"
|
|
463 |
unfolding psfis_def image_def by auto
|
|
464 |
obtain s' b y where
|
|
465 |
"(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
|
|
466 |
"z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
|
|
467 |
using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto
|
|
468 |
thus ?thesis using r unfolding psfis_def image_def by auto
|
|
469 |
qed
|
|
470 |
|
|
471 |
lemma pos_simple_integral_setsum_image:
|
|
472 |
assumes "finite P"
|
|
473 |
assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
|
|
474 |
obtains s' a' x' where
|
|
475 |
"(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
|
|
476 |
"pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
|
|
477 |
using assms that
|
|
478 |
proof (induct P arbitrary:thesis rule:finite.induct)
|
|
479 |
case emptyI note asms = this
|
|
480 |
def s' == "{0 :: nat}"
|
|
481 |
def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
|
|
482 |
def x' == "\<lambda> x :: nat. (0 :: real)"
|
|
483 |
have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
|
|
484 |
unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
|
|
485 |
moreover have "pos_simple_integral (s', a', x') = 0"
|
|
486 |
unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
|
|
487 |
ultimately show ?case using asms by auto
|
|
488 |
next
|
|
489 |
|
|
490 |
case (insertI P c) note asms = this
|
|
491 |
then obtain s' a' x' where
|
|
492 |
sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
|
|
493 |
"pos_simple_integral (s', a', x') =
|
|
494 |
(\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
|
|
495 |
by auto
|
|
496 |
|
|
497 |
{ assume "c \<in> P"
|
|
498 |
hence "P = insert c P" by auto
|
|
499 |
hence thesis using asms sax by auto
|
|
500 |
}
|
|
501 |
moreover
|
|
502 |
{ assume "c \<notin> P"
|
|
503 |
from asms obtain s'' a'' x'' where
|
|
504 |
sax': "s'' = s c" "a'' = a c" "x'' = x c"
|
|
505 |
"(s'', a'', x'') \<in> pos_simple (f c)" by auto
|
|
506 |
from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
|
|
507 |
tybbie:
|
|
508 |
"(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
|
|
509 |
"(pos_simple_integral (s', a', x') +
|
|
510 |
pos_simple_integral (s'', a'', x'') =
|
|
511 |
pos_simple_integral (k, b, z))"
|
|
512 |
using pos_simple_integral_add by blast
|
|
513 |
|
|
514 |
from tybbie have
|
|
515 |
"pos_simple_integral (k, b, z) =
|
|
516 |
pos_simple_integral (s', a', x') +
|
|
517 |
pos_simple_integral (s'', a'', x'')" by simp
|
|
518 |
also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
|
|
519 |
+ pos_simple_integral (s c, a c, x c)"
|
|
520 |
using sax sax' by auto
|
|
521 |
also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
|
|
522 |
using asms `c \<notin> P` by auto
|
|
523 |
finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
|
|
524 |
by simp
|
|
525 |
|
|
526 |
have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
|
|
527 |
using `c \<notin> P` `finite P` by auto
|
|
528 |
hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
|
|
529 |
using tybbie by simp
|
|
530 |
|
|
531 |
from A B have thesis using asms by auto
|
|
532 |
} ultimately show thesis by blast
|
|
533 |
qed
|
|
534 |
|
|
535 |
lemma psfis_setsum_image:
|
|
536 |
assumes "finite P"
|
|
537 |
assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
|
|
538 |
shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"
|
|
539 |
using assms
|
|
540 |
proof (induct P)
|
|
541 |
case empty
|
|
542 |
let ?s = "{0 :: nat}"
|
|
543 |
let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"
|
|
544 |
let ?x = "\<lambda> (i :: nat). (0 :: real)"
|
|
545 |
have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"
|
|
546 |
unfolding pos_simple_def image_def nonneg_def by auto
|
|
547 |
moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto
|
|
548 |
ultimately have "0 \<in> psfis (\<lambda> t. 0)"
|
|
549 |
unfolding psfis_def image_def pos_simple_integral_def nonneg_def
|
|
550 |
by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])
|
|
551 |
thus ?case by auto
|
|
552 |
next
|
|
553 |
case (insert x P) note asms = this
|
|
554 |
have "finite P" by fact
|
|
555 |
have "x \<notin> P" by fact
|
|
556 |
have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>
|
|
557 |
setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact
|
|
558 |
have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto
|
|
559 |
also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"
|
|
560 |
using asms psfis_add by auto
|
|
561 |
also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"
|
|
562 |
using `x \<notin> P` `finite P` by auto
|
|
563 |
finally show ?case by simp
|
|
564 |
qed
|
|
565 |
|
|
566 |
lemma psfis_intro:
|
|
567 |
assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"
|
|
568 |
shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"
|
|
569 |
using assms psfis_mult psfis_indicator
|
|
570 |
unfolding image_def nonneg_def
|
|
571 |
by (auto intro!:psfis_setsum_image)
|
|
572 |
|
|
573 |
lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"
|
|
574 |
unfolding psfis_def pos_simple_def by auto
|
|
575 |
|
|
576 |
lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"
|
|
577 |
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
|
|
578 |
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
|
|
579 |
|
|
580 |
lemma pos_part_neg_part_borel_measurable:
|
|
581 |
assumes "f \<in> borel_measurable M"
|
|
582 |
shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
|
|
583 |
using assms
|
|
584 |
proof -
|
|
585 |
{ fix a :: real
|
|
586 |
{ assume asm: "0 \<le> a"
|
|
587 |
from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
|
|
588 |
have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
|
|
589 |
unfolding pos_part_def using assms borel_measurable_le_iff by auto
|
|
590 |
hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
|
|
591 |
moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
|
|
592 |
unfolding pos_part_def using empty_sets by auto
|
|
593 |
ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
|
|
594 |
using le_less_linear by auto
|
|
595 |
} hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
|
|
596 |
{ fix a :: real
|
|
597 |
{ assume asm: "0 \<le> a"
|
|
598 |
from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
|
|
599 |
have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
|
|
600 |
unfolding neg_part_def using assms borel_measurable_ge_iff by auto
|
|
601 |
hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
|
|
602 |
moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
|
|
603 |
moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
|
|
604 |
ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
|
|
605 |
using le_less_linear by auto
|
|
606 |
} hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
|
|
607 |
from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
|
|
608 |
qed
|
|
609 |
|
|
610 |
lemma pos_part_neg_part_borel_measurable_iff:
|
|
611 |
"f \<in> borel_measurable M \<longleftrightarrow>
|
|
612 |
pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
|
|
613 |
proof -
|
|
614 |
{ fix x
|
|
615 |
have "f x = pos_part f x - neg_part f x"
|
|
616 |
unfolding pos_part_def neg_part_def unfolding max_def min_def
|
|
617 |
by auto }
|
|
618 |
hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
|
|
619 |
hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
|
|
620 |
from pos_part_neg_part_borel_measurable[of f]
|
|
621 |
borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
|
|
622 |
this
|
|
623 |
show ?thesis by auto
|
|
624 |
qed
|
|
625 |
|
|
626 |
lemma borel_measurable_cong:
|
|
627 |
assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
|
|
628 |
shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
|
|
629 |
using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
|
|
630 |
|
|
631 |
lemma psfis_borel_measurable:
|
|
632 |
assumes "a \<in> psfis f"
|
|
633 |
shows "f \<in> borel_measurable M"
|
|
634 |
using assms
|
|
635 |
proof -
|
|
636 |
from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"
|
|
637 |
and fs: "finite s"
|
|
638 |
unfolding psfis_def pos_simple_integral_def image_def
|
|
639 |
by (auto elim:pos_simpleE)
|
|
640 |
{ fix w assume "w \<in> space M"
|
|
641 |
hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
|
|
642 |
using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp
|
|
643 |
} hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
|
|
644 |
by auto
|
|
645 |
{ fix i assume "i \<in> s"
|
|
646 |
hence "indicator_fn (a' i) \<in> borel_measurable M"
|
|
647 |
using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
|
|
648 |
hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
|
|
649 |
using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
|
|
650 |
real_mult_commute by auto }
|
|
651 |
from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
|
|
652 |
have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
|
|
653 |
from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
|
|
654 |
show ?thesis by simp
|
|
655 |
qed
|
|
656 |
|
|
657 |
lemma mono_conv_outgrow:
|
|
658 |
assumes "incseq x" "x ----> y" "z < y"
|
|
659 |
shows "\<exists>b. \<forall> a \<ge> b. z < x a"
|
|
660 |
using assms
|
|
661 |
proof -
|
|
662 |
from assms have "y - z > 0" by simp
|
|
663 |
hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
|
|
664 |
unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
|
|
665 |
by simp
|
|
666 |
have "\<forall>m. x m \<le> y" using incseq_le assms by auto
|
|
667 |
hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
|
|
668 |
by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
|
|
669 |
from A B show ?thesis by auto
|
|
670 |
qed
|
|
671 |
|
|
672 |
lemma psfis_mono_conv_mono:
|
|
673 |
assumes mono: "mono_convergent u f (space M)"
|
|
674 |
and ps_u: "\<And>n. x n \<in> psfis (u n)"
|
|
675 |
and "x ----> y"
|
|
676 |
and "r \<in> psfis s"
|
|
677 |
and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"
|
|
678 |
shows "r <= y"
|
|
679 |
proof (rule field_le_mult_one_interval)
|
|
680 |
fix z :: real assume "0 < z" and "z < 1"
|
|
681 |
hence "0 \<le> z" by auto
|
|
682 |
(* def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
|
|
683 |
let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
|
|
684 |
|
|
685 |
have "incseq x" unfolding incseq_def
|
|
686 |
proof safe
|
|
687 |
fix m n :: nat assume "m \<le> n"
|
|
688 |
show "x m \<le> x n"
|
|
689 |
proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])
|
|
690 |
fix t assume "t \<in> space M"
|
|
691 |
with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"
|
|
692 |
unfolding incseq_def by auto
|
|
693 |
qed
|
|
694 |
qed
|
|
695 |
|
|
696 |
from `r \<in> psfis s`
|
|
697 |
obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"
|
|
698 |
and ps_s: "(s', a, x') \<in> pos_simple s"
|
|
699 |
unfolding psfis_def by auto
|
|
700 |
|
|
701 |
{ fix t i assume "i \<in> s'" "t \<in> a i"
|
|
702 |
hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }
|
|
703 |
note t_in_space = this
|
|
704 |
|
|
705 |
{ fix n
|
|
706 |
from psfis_borel_measurable[OF `r \<in> psfis s`]
|
|
707 |
psfis_borel_measurable[OF ps_u]
|
|
708 |
have "?B' n \<in> sets M"
|
|
709 |
by (auto intro!:
|
|
710 |
borel_measurable_leq_borel_measurable
|
|
711 |
borel_measurable_times_borel_measurable
|
|
712 |
borel_measurable_const) }
|
|
713 |
note B'_in_M = this
|
|
714 |
|
|
715 |
{ fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s
|
|
716 |
by (auto intro!: Int elim!: pos_simpleE) }
|
|
717 |
note B'_inter_a_in_M = this
|
|
718 |
|
|
719 |
let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"
|
|
720 |
{ fix n
|
|
721 |
have "z * ?sum n \<le> x n"
|
|
722 |
proof (rule psfis_mono[OF _ ps_u])
|
|
723 |
have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =
|
|
724 |
x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto
|
|
725 |
have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"
|
|
726 |
unfolding setsum_right_distrib * using B'_in_M ps_s
|
|
727 |
by (auto intro!: psfis_intro Int elim!: pos_simpleE)
|
|
728 |
also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")
|
|
729 |
proof (rule psfis_cong)
|
|
730 |
show "nonneg ?l" using psfis_nonneg[OF ps'] .
|
|
731 |
show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto
|
|
732 |
fix t assume "t \<in> space M"
|
|
733 |
show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..
|
|
734 |
qed
|
|
735 |
finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp
|
|
736 |
next
|
|
737 |
fix t assume "t \<in> space M"
|
|
738 |
show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"
|
|
739 |
using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto
|
|
740 |
qed }
|
|
741 |
hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])
|
|
742 |
|
|
743 |
show "z * r \<le> y" unfolding r pos_simple_integral_def
|
|
744 |
proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *],
|
|
745 |
simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)
|
|
746 |
fix i assume "i \<in> s'"
|
|
747 |
from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]
|
|
748 |
have "\<And>t. 0 \<le> s t" by simp
|
|
749 |
|
|
750 |
have *: "(\<Union>j. a i \<inter> ?B' j) = a i"
|
|
751 |
proof (safe, simp, safe)
|
|
752 |
fix t assume "t \<in> a i"
|
|
753 |
thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto
|
|
754 |
show "\<exists>j. z * s t \<le> u j t"
|
|
755 |
proof (cases "s t = 0")
|
|
756 |
case True thus ?thesis
|
|
757 |
using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto
|
|
758 |
next
|
|
759 |
case False with `0 \<le> s t`
|
|
760 |
have "0 < s t" by auto
|
|
761 |
hence "z * s t < 1 * s t" using `0 < z` `z < 1`
|
|
762 |
by (auto intro!: mult_strict_right_mono simp del: mult_1_left)
|
|
763 |
also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto
|
|
764 |
finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`
|
|
765 |
using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]
|
|
766 |
using mono_convergentD[OF mono] by auto
|
|
767 |
from this[of b] show ?thesis by (auto intro!: exI[of _ b])
|
|
768 |
qed
|
|
769 |
qed
|
|
770 |
|
|
771 |
show "(\<lambda>n. measure M (a i \<inter> ?B' n)) ----> measure M (a i)"
|
|
772 |
proof (safe intro!:
|
|
773 |
monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])
|
|
774 |
fix n show "a i \<inter> ?B' n \<in> sets M"
|
|
775 |
using B'_inter_a_in_M[of n] `i \<in> s'` by auto
|
|
776 |
next
|
|
777 |
fix j t assume "t \<in> space M" and "z * s t \<le> u j t"
|
|
778 |
thus "z * s t \<le> u (Suc j) t"
|
|
779 |
using mono_convergentD(1)[OF mono, unfolded incseq_def,
|
|
780 |
rule_format, of t j "Suc j"]
|
|
781 |
by auto
|
|
782 |
qed
|
|
783 |
qed
|
|
784 |
qed
|
|
785 |
|
|
786 |
lemma psfis_nnfis:
|
|
787 |
"a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
|
|
788 |
unfolding nnfis_def mono_convergent_def incseq_def
|
|
789 |
by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
|
|
790 |
|
|
791 |
lemma nnfis_times:
|
|
792 |
assumes "a \<in> nnfis f" and "0 \<le> z"
|
|
793 |
shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
|
|
794 |
proof -
|
|
795 |
obtain u x where "mono_convergent u f (space M)" and
|
|
796 |
"\<And>n. x n \<in> psfis (u n)" "x ----> a"
|
|
797 |
using `a \<in> nnfis f` unfolding nnfis_def by auto
|
|
798 |
with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
|
|
799 |
by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
|
|
800 |
LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
|
|
801 |
qed
|
|
802 |
|
|
803 |
lemma nnfis_add:
|
|
804 |
assumes "a \<in> nnfis f" and "b \<in> nnfis g"
|
|
805 |
shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"
|
|
806 |
proof -
|
|
807 |
obtain u x w y
|
|
808 |
where "mono_convergent u f (space M)" and
|
|
809 |
"\<And>n. x n \<in> psfis (u n)" "x ----> a" and
|
|
810 |
"mono_convergent w g (space M)" and
|
|
811 |
"\<And>n. y n \<in> psfis (w n)" "y ----> b"
|
|
812 |
using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto
|
|
813 |
thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def
|
|
814 |
by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]
|
|
815 |
LIMSEQ_add LIMSEQ_const psfis_add add_mono)
|
|
816 |
qed
|
|
817 |
|
|
818 |
lemma nnfis_mono:
|
|
819 |
assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"
|
|
820 |
and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
|
|
821 |
shows "a \<le> b"
|
|
822 |
proof -
|
|
823 |
obtain u x w y where
|
|
824 |
mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and
|
|
825 |
psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and
|
|
826 |
limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto
|
|
827 |
show ?thesis
|
|
828 |
proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)
|
|
829 |
fix n
|
|
830 |
show "x n \<le> b"
|
|
831 |
proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])
|
|
832 |
fix t assume "t \<in> space M"
|
|
833 |
from mono_convergent_le[OF mc(1) this] mono[OF this]
|
|
834 |
show "u n t \<le> g t" by (rule order_trans)
|
|
835 |
qed
|
|
836 |
qed
|
|
837 |
qed
|
|
838 |
|
|
839 |
lemma nnfis_unique:
|
|
840 |
assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
|
|
841 |
shows "a = b"
|
|
842 |
using nnfis_mono[OF a b] nnfis_mono[OF b a]
|
|
843 |
by (auto intro!: real_le_antisym[of a b])
|
|
844 |
|
|
845 |
lemma psfis_equiv:
|
|
846 |
assumes "a \<in> psfis f" and "nonneg g"
|
|
847 |
and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
|
|
848 |
shows "a \<in> psfis g"
|
|
849 |
using assms unfolding psfis_def pos_simple_def by auto
|
|
850 |
|
|
851 |
lemma psfis_mon_upclose:
|
|
852 |
assumes "\<And>m. a m \<in> psfis (u m)"
|
|
853 |
shows "\<exists>c. c \<in> psfis (mon_upclose n u)"
|
|
854 |
proof (induct n)
|
|
855 |
case 0 thus ?case unfolding mon_upclose.simps using assms ..
|
|
856 |
next
|
|
857 |
case (Suc n)
|
|
858 |
then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"
|
|
859 |
unfolding psfis_def by auto
|
|
860 |
obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"
|
|
861 |
using assms[of "Suc n"] unfolding psfis_def by auto
|
|
862 |
from pos_simple_common_partition[OF ps ps'] guess x x' a s .
|
|
863 |
hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"
|
|
864 |
by (simp add: upclose_def pos_simple_def nonneg_def max_def)
|
|
865 |
thus ?case unfolding psfis_def by auto
|
|
866 |
qed
|
|
867 |
|
|
868 |
text {* Beppo-Levi monotone convergence theorem *}
|
|
869 |
lemma nnfis_mon_conv:
|
|
870 |
assumes mc: "mono_convergent f h (space M)"
|
|
871 |
and nnfis: "\<And>n. x n \<in> nnfis (f n)"
|
|
872 |
and "x ----> z"
|
|
873 |
shows "z \<in> nnfis h"
|
|
874 |
proof -
|
|
875 |
have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>
|
|
876 |
y ----> x n"
|
|
877 |
using nnfis unfolding nnfis_def by auto
|
|
878 |
from choice[OF this] guess u ..
|
|
879 |
from choice[OF this] guess y ..
|
|
880 |
hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"
|
|
881 |
and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n ----> x n"
|
|
882 |
by auto
|
|
883 |
|
|
884 |
let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"
|
|
885 |
|
|
886 |
have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"
|
|
887 |
by (safe intro!: choice psfis_mon_upclose) (rule psfis)
|
|
888 |
then guess c .. note c = this[rule_format]
|
|
889 |
|
|
890 |
show ?thesis unfolding nnfis_def
|
|
891 |
proof (safe intro!: exI)
|
|
892 |
show mc_upclose: "mono_convergent ?upclose h (space M)"
|
|
893 |
by (rule mon_upclose_mono_convergent[OF mc_u mc])
|
|
894 |
show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"
|
|
895 |
using c .
|
|
896 |
|
|
897 |
{ fix n m :: nat assume "n \<le> m"
|
|
898 |
hence "c n \<le> c m"
|
|
899 |
using psfis_mono[OF c c]
|
|
900 |
using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]
|
|
901 |
by auto }
|
|
902 |
hence "incseq c" unfolding incseq_def by auto
|
|
903 |
|
|
904 |
{ fix n
|
|
905 |
have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)
|
|
906 |
from nnfis_mono[OF c_nnfis nnfis]
|
|
907 |
mon_upclose_le_mono_convergent[OF mc_u]
|
|
908 |
mono_convergentD(1)[OF mc]
|
|
909 |
have "c n \<le> x n" by fast }
|
|
910 |
note c_less_x = this
|
|
911 |
|
|
912 |
{ fix n
|
|
913 |
note c_less_x[of n]
|
|
914 |
also have "x n \<le> z"
|
|
915 |
proof (rule incseq_le)
|
|
916 |
show "x ----> z" by fact
|
|
917 |
from mono_convergentD(1)[OF mc]
|
|
918 |
show "incseq x" unfolding incseq_def
|
|
919 |
by (auto intro!: nnfis_mono[OF nnfis nnfis])
|
|
920 |
qed
|
|
921 |
finally have "c n \<le> z" . }
|
|
922 |
note c_less_z = this
|
|
923 |
|
|
924 |
have "convergent c"
|
|
925 |
proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])
|
|
926 |
show "Bseq c"
|
|
927 |
using pos_psfis[OF c] c_less_z
|
|
928 |
by (auto intro!: BseqI'[of _ z])
|
|
929 |
show "incseq c" by fact
|
|
930 |
qed
|
|
931 |
then obtain l where l: "c ----> l" unfolding convergent_def by auto
|
|
932 |
|
|
933 |
have "l \<le> z" using c_less_x l
|
|
934 |
by (auto intro!: LIMSEQ_le[OF _ `x ----> z`])
|
|
935 |
moreover have "z \<le> l"
|
|
936 |
proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0])
|
|
937 |
fix n
|
|
938 |
have "l \<in> nnfis h"
|
|
939 |
unfolding nnfis_def using l mc_upclose psfis_upclose by auto
|
|
940 |
from nnfis this mono_convergent_le[OF mc]
|
|
941 |
show "x n \<le> l" by (rule nnfis_mono)
|
|
942 |
qed
|
|
943 |
ultimately have "l = z" by (rule real_le_antisym)
|
|
944 |
thus "c ----> z" using `c ----> l` by simp
|
|
945 |
qed
|
|
946 |
qed
|
|
947 |
|
|
948 |
lemma nnfis_pos_on_mspace:
|
|
949 |
assumes "a \<in> nnfis f" and "x \<in>space M"
|
|
950 |
shows "0 \<le> f x"
|
|
951 |
using assms
|
|
952 |
proof -
|
|
953 |
from assms[unfolded nnfis_def] guess u y by auto note uy = this
|
|
954 |
hence "\<And> n. 0 \<le> u n x"
|
|
955 |
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
|
|
956 |
by auto
|
|
957 |
thus "0 \<le> f x" using uy[rule_format]
|
|
958 |
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
|
|
959 |
using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
|
|
960 |
by fast
|
|
961 |
qed
|
|
962 |
|
|
963 |
lemma nnfis_borel_measurable:
|
|
964 |
assumes "a \<in> nnfis f"
|
|
965 |
shows "f \<in> borel_measurable M"
|
|
966 |
using assms unfolding nnfis_def
|
|
967 |
apply auto
|
|
968 |
apply (rule mono_convergent_borel_measurable)
|
|
969 |
using psfis_borel_measurable
|
|
970 |
by auto
|
|
971 |
|
|
972 |
lemma borel_measurable_mon_conv_psfis:
|
|
973 |
assumes f_borel: "f \<in> borel_measurable M"
|
|
974 |
and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
|
|
975 |
shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"
|
|
976 |
proof (safe intro!: exI)
|
|
977 |
let "?I n" = "{0<..<n * 2^n}"
|
|
978 |
let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"
|
|
979 |
let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"
|
|
980 |
let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"
|
|
981 |
|
|
982 |
let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"
|
|
983 |
|
|
984 |
{ fix t n assume t: "t \<in> space M"
|
|
985 |
have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")
|
|
986 |
proof (cases "f t < real n")
|
|
987 |
case True
|
|
988 |
with nonneg t
|
|
989 |
have i: "?i < n * 2^n"
|
|
990 |
by (auto simp: real_of_nat_power[symmetric]
|
|
991 |
intro!: less_natfloor mult_nonneg_nonneg)
|
|
992 |
|
|
993 |
hence t_in_A: "t \<in> ?A n ?i"
|
|
994 |
unfolding divide_le_eq less_divide_eq
|
|
995 |
using nonneg t True
|
|
996 |
by (auto intro!: real_natfloor_le
|
|
997 |
real_natfloor_gt_diff_one[unfolded diff_less_eq]
|
|
998 |
simp: real_of_nat_Suc zero_le_mult_iff)
|
|
999 |
|
|
1000 |
hence *: "real ?i / 2^n \<le> f t"
|
|
1001 |
"f t < real (?i + 1) / 2^n" by auto
|
|
1002 |
{ fix j assume "t \<in> ?A n j"
|
|
1003 |
hence "real j / 2^n \<le> f t"
|
|
1004 |
and "f t < real (j + 1) / 2^n" by auto
|
|
1005 |
with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq
|
|
1006 |
by auto }
|
|
1007 |
hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto
|
|
1008 |
|
|
1009 |
have "?u n t = real ?i / 2^n"
|
|
1010 |
unfolding indicator_fn_def if_distrib *
|
|
1011 |
setsum_cases[OF finite_greaterThanLessThan]
|
|
1012 |
using i by (cases "?i = 0") simp_all
|
|
1013 |
thus ?thesis using True by auto
|
|
1014 |
next
|
|
1015 |
case False
|
|
1016 |
have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"
|
|
1017 |
proof (rule setsum_cong)
|
|
1018 |
fix i assume "i \<in> {0 <..< n*2^n}"
|
|
1019 |
hence "i + 1 \<le> n * 2^n" by simp
|
|
1020 |
hence "real (i + 1) \<le> real n * 2^n"
|
|
1021 |
unfolding real_of_nat_le_iff[symmetric]
|
|
1022 |
by (auto simp: real_of_nat_power[symmetric])
|
|
1023 |
also have "... \<le> f t * 2^n"
|
|
1024 |
using False by (auto intro!: mult_nonneg_nonneg)
|
|
1025 |
finally have "t \<notin> ?A n i"
|
|
1026 |
by (auto simp: divide_le_eq less_divide_eq)
|
|
1027 |
thus "real i / 2^n * indicator_fn (?A n i) t = 0"
|
|
1028 |
unfolding indicator_fn_def by auto
|
|
1029 |
qed simp
|
|
1030 |
thus ?thesis using False by auto
|
|
1031 |
qed }
|
|
1032 |
note u_at_t = this
|
|
1033 |
|
|
1034 |
show "mono_convergent ?u f (space M)" unfolding mono_convergent_def
|
|
1035 |
proof safe
|
|
1036 |
fix t assume t: "t \<in> space M"
|
|
1037 |
{ fix m n :: nat assume "m \<le> n"
|
|
1038 |
hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
|
|
1039 |
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
|
|
1040 |
apply (subst *)
|
|
1041 |
apply (subst class_semiring.mul_a)
|
|
1042 |
apply (subst real_of_nat_le_iff)
|
|
1043 |
apply (rule le_mult_natfloor)
|
|
1044 |
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
|
|
1045 |
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
|
|
1046 |
apply (subst *)
|
|
1047 |
apply (subst (3) class_semiring.mul_c)
|
|
1048 |
apply (subst class_semiring.mul_a)
|
|
1049 |
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
|
|
1050 |
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
|
|
1051 |
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
|
|
1052 |
|
|
1053 |
show "(\<lambda>i. ?u i t) ----> f t" unfolding u_at_t[OF t]
|
|
1054 |
proof (rule LIMSEQ_I, safe intro!: exI)
|
|
1055 |
fix r :: real and n :: nat
|
|
1056 |
let ?N = "natfloor (1/r) + 1"
|
|
1057 |
assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"
|
|
1058 |
hence "?N \<le> n" by auto
|
|
1059 |
|
|
1060 |
have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt
|
|
1061 |
by (simp add: real_of_nat_Suc)
|
|
1062 |
also have "... < 2^?N" by (rule two_realpow_gt)
|
|
1063 |
finally have less_r: "1 / 2^?N < r" using `0 < r`
|
|
1064 |
by (auto simp: less_divide_eq divide_less_eq algebra_simps)
|
|
1065 |
|
|
1066 |
have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto
|
|
1067 |
also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto
|
|
1068 |
finally have "f t < real n" .
|
|
1069 |
|
|
1070 |
have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"
|
|
1071 |
using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)
|
|
1072 |
hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto
|
|
1073 |
|
|
1074 |
have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .
|
|
1075 |
hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"
|
|
1076 |
by (auto simp: less_divide_eq divide_less_eq algebra_simps)
|
|
1077 |
also have "... \<le> 1 / 2^?N" using `?N \<le> n`
|
|
1078 |
by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)
|
|
1079 |
also have "... < r" using less_r .
|
|
1080 |
finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto
|
|
1081 |
qed
|
|
1082 |
qed
|
|
1083 |
|
|
1084 |
fix n
|
|
1085 |
show "?x n \<in> psfis (?u n)"
|
|
1086 |
proof (rule psfis_intro)
|
|
1087 |
show "?A n ` ?I n \<subseteq> sets M"
|
|
1088 |
proof safe
|
|
1089 |
fix i :: nat
|
|
1090 |
from Int[OF
|
|
1091 |
f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]
|
|
1092 |
f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]
|
|
1093 |
show "?A n i \<in> sets M"
|
|
1094 |
by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)
|
|
1095 |
qed
|
|
1096 |
show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"
|
|
1097 |
unfolding nonneg_def by (auto intro!: divide_nonneg_pos)
|
|
1098 |
qed auto
|
|
1099 |
qed
|
|
1100 |
|
|
1101 |
lemma nnfis_dom_conv:
|
|
1102 |
assumes borel: "f \<in> borel_measurable M"
|
|
1103 |
and nnfis: "b \<in> nnfis g"
|
|
1104 |
and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
|
|
1105 |
and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
|
|
1106 |
shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"
|
|
1107 |
proof -
|
|
1108 |
obtain u x where mc_f: "mono_convergent u f (space M)" and
|
|
1109 |
psfis: "\<And>n. x n \<in> psfis (u n)"
|
|
1110 |
using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto
|
|
1111 |
|
|
1112 |
{ fix n
|
|
1113 |
{ fix t assume t: "t \<in> space M"
|
|
1114 |
note mono_convergent_le[OF mc_f this, of n]
|
|
1115 |
also note ord[OF t]
|
|
1116 |
finally have "u n t \<le> g t" . }
|
|
1117 |
from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]
|
|
1118 |
have "x n \<le> b" by simp }
|
|
1119 |
note x_less_b = this
|
|
1120 |
|
|
1121 |
have "convergent x"
|
|
1122 |
proof (safe intro!: Bseq_mono_convergent)
|
|
1123 |
from x_less_b pos_psfis[OF psfis]
|
|
1124 |
show "Bseq x" by (auto intro!: BseqI'[of _ b])
|
|
1125 |
|
|
1126 |
fix n m :: nat assume *: "n \<le> m"
|
|
1127 |
show "x n \<le> x m"
|
|
1128 |
proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])
|
|
1129 |
fix t assume "t \<in> space M"
|
|
1130 |
from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]
|
|
1131 |
show "u n t \<le> u m t" using * by auto
|
|
1132 |
qed
|
|
1133 |
qed
|
|
1134 |
then obtain a where "x ----> a" unfolding convergent_def by auto
|
|
1135 |
with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis
|
|
1136 |
show ?thesis unfolding nnfis_def by auto
|
|
1137 |
qed
|
|
1138 |
|
|
1139 |
lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
|
|
1140 |
unfolding psfis_def pos_simple_def pos_simple_integral_def
|
|
1141 |
by (auto simp: nonneg_def
|
|
1142 |
intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
|
|
1143 |
|
|
1144 |
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
|
|
1145 |
by (auto intro: the_equality nnfis_unique)
|
|
1146 |
|
|
1147 |
lemma nnfis_cong:
|
|
1148 |
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
|
|
1149 |
shows "nnfis f = nnfis g"
|
|
1150 |
proof -
|
|
1151 |
{ fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
|
|
1152 |
fix x assume "x \<in> nnfis f"
|
|
1153 |
then guess u y unfolding nnfis_def by safe note x = this
|
|
1154 |
hence "mono_convergent u g (space M)"
|
|
1155 |
unfolding mono_convergent_def using cong by auto
|
|
1156 |
with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }
|
|
1157 |
from this[OF cong] this[OF cong[symmetric]]
|
|
1158 |
show ?thesis by safe
|
|
1159 |
qed
|
|
1160 |
|
|
1161 |
lemma integral_cong:
|
|
1162 |
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
|
|
1163 |
shows "integral f = integral g"
|
|
1164 |
proof -
|
|
1165 |
have "nnfis (pos_part f) = nnfis (pos_part g)"
|
|
1166 |
using cong by (auto simp: pos_part_def intro!: nnfis_cong)
|
|
1167 |
moreover
|
|
1168 |
have "nnfis (neg_part f) = nnfis (neg_part g)"
|
|
1169 |
using cong by (auto simp: neg_part_def intro!: nnfis_cong)
|
|
1170 |
ultimately show ?thesis
|
|
1171 |
unfolding integral_def by auto
|
|
1172 |
qed
|
|
1173 |
|
|
1174 |
lemma nnfis_integral:
|
|
1175 |
assumes "a \<in> nnfis f"
|
|
1176 |
shows "integrable f" and "integral f = a"
|
|
1177 |
proof -
|
|
1178 |
have a: "a \<in> nnfis (pos_part f)"
|
|
1179 |
using assms nnfis_pos_on_mspace[OF assms]
|
|
1180 |
by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]
|
|
1181 |
LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)
|
|
1182 |
|
|
1183 |
have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"
|
|
1184 |
unfolding neg_part_def min_def
|
|
1185 |
using nnfis_pos_on_mspace[OF assms] by auto
|
|
1186 |
hence 0: "0 \<in> nnfis (neg_part f)"
|
|
1187 |
by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def
|
|
1188 |
intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])
|
|
1189 |
|
|
1190 |
from 0 a show "integrable f" "integral f = a"
|
|
1191 |
unfolding integrable_def integral_def by auto
|
|
1192 |
qed
|
|
1193 |
|
|
1194 |
lemma nnfis_minus_nnfis_integral:
|
|
1195 |
assumes "a \<in> nnfis f" and "b \<in> nnfis g"
|
|
1196 |
shows "integrable (\<lambda>t. f t - g t)" and "integral (\<lambda>t. f t - g t) = a - b"
|
|
1197 |
proof -
|
|
1198 |
have borel: "(\<lambda>t. f t - g t) \<in> borel_measurable M" using assms
|
|
1199 |
by (blast intro:
|
|
1200 |
borel_measurable_diff_borel_measurable nnfis_borel_measurable)
|
|
1201 |
|
|
1202 |
have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
|
|
1203 |
(is "\<exists>x. x \<in> nnfis ?pp \<and> _")
|
|
1204 |
proof (rule nnfis_dom_conv)
|
|
1205 |
show "?pp \<in> borel_measurable M"
|
|
1206 |
using borel by (rule pos_part_neg_part_borel_measurable)
|
|
1207 |
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
|
|
1208 |
fix t assume "t \<in> space M"
|
|
1209 |
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
|
|
1210 |
show "?pp t \<le> f t + g t" unfolding pos_part_def by auto
|
|
1211 |
show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t - g t"]
|
|
1212 |
unfolding nonneg_def by auto
|
|
1213 |
qed
|
|
1214 |
then obtain x where x: "x \<in> nnfis ?pp" by auto
|
|
1215 |
moreover
|
|
1216 |
have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
|
|
1217 |
(is "\<exists>x. x \<in> nnfis ?np \<and> _")
|
|
1218 |
proof (rule nnfis_dom_conv)
|
|
1219 |
show "?np \<in> borel_measurable M"
|
|
1220 |
using borel by (rule pos_part_neg_part_borel_measurable)
|
|
1221 |
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
|
|
1222 |
fix t assume "t \<in> space M"
|
|
1223 |
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
|
|
1224 |
show "?np t \<le> f t + g t" unfolding neg_part_def by auto
|
|
1225 |
show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t - g t"]
|
|
1226 |
unfolding nonneg_def by auto
|
|
1227 |
qed
|
|
1228 |
then obtain y where y: "y \<in> nnfis ?np" by auto
|
|
1229 |
ultimately show "integrable (\<lambda>t. f t - g t)"
|
|
1230 |
unfolding integrable_def by auto
|
|
1231 |
|
|
1232 |
from x and y
|
|
1233 |
have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"
|
|
1234 |
and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)
|
|
1235 |
moreover
|
|
1236 |
have "\<And>t. f t + ?np t = g t + ?pp t"
|
|
1237 |
unfolding pos_part_def neg_part_def by auto
|
|
1238 |
ultimately have "a - b = x - y"
|
|
1239 |
using nnfis_unique by (auto simp: algebra_simps)
|
|
1240 |
thus "integral (\<lambda>t. f t - g t) = a - b"
|
|
1241 |
unfolding integral_def
|
|
1242 |
using the_nnfis[OF x] the_nnfis[OF y] by simp
|
|
1243 |
qed
|
|
1244 |
|
|
1245 |
lemma integral_borel_measurable:
|
|
1246 |
"integrable f \<Longrightarrow> f \<in> borel_measurable M"
|
|
1247 |
unfolding integrable_def
|
|
1248 |
by (subst pos_part_neg_part_borel_measurable_iff)
|
|
1249 |
(auto intro: nnfis_borel_measurable)
|
|
1250 |
|
|
1251 |
lemma integral_indicator_fn:
|
|
1252 |
assumes "a \<in> sets M"
|
|
1253 |
shows "integral (indicator_fn a) = measure M a"
|
|
1254 |
and "integrable (indicator_fn a)"
|
|
1255 |
using psfis_indicator[OF assms, THEN psfis_nnfis]
|
|
1256 |
by (auto intro!: nnfis_integral)
|
|
1257 |
|
|
1258 |
lemma integral_add:
|
|
1259 |
assumes "integrable f" and "integrable g"
|
|
1260 |
shows "integrable (\<lambda>t. f t + g t)"
|
|
1261 |
and "integral (\<lambda>t. f t + g t) = integral f + integral g"
|
|
1262 |
proof -
|
|
1263 |
{ fix t
|
|
1264 |
have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) =
|
|
1265 |
f t + g t"
|
|
1266 |
unfolding pos_part_def neg_part_def by auto }
|
|
1267 |
note part_sum = this
|
|
1268 |
|
|
1269 |
from assms obtain a b c d where
|
|
1270 |
a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
|
|
1271 |
c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
|
|
1272 |
unfolding integrable_def by auto
|
|
1273 |
note sums = nnfis_add[OF a c] nnfis_add[OF b d]
|
|
1274 |
note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]
|
|
1275 |
|
|
1276 |
show "integrable (\<lambda>t. f t + g t)" using int(1) .
|
|
1277 |
|
|
1278 |
show "integral (\<lambda>t. f t + g t) = integral f + integral g"
|
|
1279 |
using int(2) sums a b c d by (simp add: the_nnfis integral_def)
|
|
1280 |
qed
|
|
1281 |
|
|
1282 |
lemma integral_mono:
|
|
1283 |
assumes "integrable f" and "integrable g"
|
|
1284 |
and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
|
|
1285 |
shows "integral f \<le> integral g"
|
|
1286 |
proof -
|
|
1287 |
from assms obtain a b c d where
|
|
1288 |
a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
|
|
1289 |
c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
|
|
1290 |
unfolding integrable_def by auto
|
|
1291 |
|
|
1292 |
have "a \<le> c"
|
|
1293 |
proof (rule nnfis_mono[OF a c])
|
|
1294 |
fix t assume "t \<in> space M"
|
|
1295 |
from mono[OF this] show "pos_part f t \<le> pos_part g t"
|
|
1296 |
unfolding pos_part_def by auto
|
|
1297 |
qed
|
|
1298 |
moreover have "d \<le> b"
|
|
1299 |
proof (rule nnfis_mono[OF d b])
|
|
1300 |
fix t assume "t \<in> space M"
|
|
1301 |
from mono[OF this] show "neg_part g t \<le> neg_part f t"
|
|
1302 |
unfolding neg_part_def by auto
|
|
1303 |
qed
|
|
1304 |
ultimately have "a - b \<le> c - d" by auto
|
|
1305 |
thus ?thesis unfolding integral_def
|
|
1306 |
using a b c d by (simp add: the_nnfis)
|
|
1307 |
qed
|
|
1308 |
|
|
1309 |
lemma integral_uminus:
|
|
1310 |
assumes "integrable f"
|
|
1311 |
shows "integrable (\<lambda>t. - f t)"
|
|
1312 |
and "integral (\<lambda>t. - f t) = - integral f"
|
|
1313 |
proof -
|
|
1314 |
have "pos_part f = neg_part (\<lambda>t.-f t)" and "neg_part f = pos_part (\<lambda>t.-f t)"
|
|
1315 |
unfolding pos_part_def neg_part_def by (auto intro!: ext)
|
|
1316 |
with assms show "integrable (\<lambda>t.-f t)" and "integral (\<lambda>t.-f t) = -integral f"
|
|
1317 |
unfolding integrable_def integral_def by simp_all
|
|
1318 |
qed
|
|
1319 |
|
|
1320 |
lemma integral_times_const:
|
|
1321 |
assumes "integrable f"
|
|
1322 |
shows "integrable (\<lambda>t. a * f t)" (is "?P a")
|
|
1323 |
and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")
|
|
1324 |
proof -
|
|
1325 |
{ fix a :: real assume "0 \<le> a"
|
|
1326 |
hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"
|
|
1327 |
and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"
|
|
1328 |
unfolding pos_part_def neg_part_def max_def min_def
|
|
1329 |
by (auto intro!: ext simp: zero_le_mult_iff)
|
|
1330 |
moreover
|
|
1331 |
obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"
|
|
1332 |
using assms unfolding integrable_def by auto
|
|
1333 |
ultimately
|
|
1334 |
have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and
|
|
1335 |
"a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"
|
|
1336 |
using nnfis_times[OF _ `0 \<le> a`] by auto
|
|
1337 |
with x y have "?P a \<and> ?I a"
|
|
1338 |
unfolding integrable_def integral_def by (auto simp: algebra_simps) }
|
|
1339 |
note int = this
|
|
1340 |
|
|
1341 |
have "?P a \<and> ?I a"
|
|
1342 |
proof (cases "0 \<le> a")
|
|
1343 |
case True from int[OF this] show ?thesis .
|
|
1344 |
next
|
|
1345 |
case False with int[of "- a"] integral_uminus[of "\<lambda>t. - a * f t"]
|
|
1346 |
show ?thesis by auto
|
|
1347 |
qed
|
|
1348 |
thus "integrable (\<lambda>t. a * f t)"
|
|
1349 |
and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all
|
|
1350 |
qed
|
|
1351 |
|
|
1352 |
lemma integral_cmul_indicator:
|
|
1353 |
assumes "s \<in> sets M"
|
|
1354 |
shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"
|
|
1355 |
and "integrable (\<lambda>x. c * indicator_fn s x)"
|
|
1356 |
using assms integral_times_const integral_indicator_fn by auto
|
|
1357 |
|
|
1358 |
lemma integral_zero:
|
|
1359 |
shows "integral (\<lambda>x. 0) = 0"
|
|
1360 |
and "integrable (\<lambda>x. 0)"
|
|
1361 |
using integral_cmul_indicator[OF empty_sets, of 0]
|
|
1362 |
unfolding indicator_fn_def by auto
|
|
1363 |
|
|
1364 |
lemma integral_setsum:
|
|
1365 |
assumes "finite S"
|
|
1366 |
assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
|
|
1367 |
shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
|
|
1368 |
and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")
|
|
1369 |
proof -
|
|
1370 |
from assms have "?int S \<and> ?I S"
|
|
1371 |
proof (induct S)
|
|
1372 |
case empty thus ?case by (simp add: integral_zero)
|
|
1373 |
next
|
|
1374 |
case (insert i S)
|
|
1375 |
thus ?case
|
|
1376 |
apply simp
|
|
1377 |
apply (subst integral_add)
|
|
1378 |
using assms apply auto
|
|
1379 |
apply (subst integral_add)
|
|
1380 |
using assms by auto
|
|
1381 |
qed
|
|
1382 |
thus "?int S" and "?I S" by auto
|
|
1383 |
qed
|
|
1384 |
|
|
1385 |
lemma markov_ineq:
|
|
1386 |
assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
|
|
1387 |
shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
|
|
1388 |
using assms
|
|
1389 |
proof -
|
|
1390 |
from assms have "0 < a ^ n" using real_root_pow_pos by auto
|
|
1391 |
from assms have "f \<in> borel_measurable M"
|
|
1392 |
using integral_borel_measurable[OF `integrable f`] by auto
|
|
1393 |
hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"
|
|
1394 |
using borel_measurable_ge_iff by auto
|
|
1395 |
have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"
|
|
1396 |
using integral_indicator_fn[OF w] by simp
|
|
1397 |
have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t
|
|
1398 |
\<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"
|
|
1399 |
unfolding indicator_fn_def
|
|
1400 |
using `0 < a` power_mono[of a] assms by auto
|
|
1401 |
have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"
|
|
1402 |
unfolding indicator_fn_def
|
|
1403 |
using power_mono[of a _ n] abs_ge_self `a > 0`
|
|
1404 |
by auto
|
|
1405 |
have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"
|
|
1406 |
using Collect_eq by auto
|
|
1407 |
from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this
|
|
1408 |
have "(a ^ n) * (measure M ((f -` {y . a \<le> y}) \<inter> space M)) =
|
|
1409 |
(a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"
|
|
1410 |
unfolding vimage_Collect_eq[of f] by simp
|
|
1411 |
also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"
|
|
1412 |
using integral_cmul_indicator[OF w] i by auto
|
|
1413 |
also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
|
|
1414 |
apply (rule integral_mono)
|
|
1415 |
using integral_cmul_indicator[OF w]
|
|
1416 |
`integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
|
|
1417 |
finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
|
|
1418 |
unfolding atLeast_def
|
|
1419 |
by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
|
|
1420 |
qed
|
|
1421 |
|
|
1422 |
lemma integral_finite_on_sets:
|
|
1423 |
assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
|
|
1424 |
shows "integral (\<lambda>x. f x * indicator_fn a x) =
|
|
1425 |
(\<Sum> r \<in> f`a. r * measure M (f -` {r} \<inter> a))" (is "integral ?f = _")
|
|
1426 |
proof -
|
|
1427 |
{ fix x assume "x \<in> a"
|
|
1428 |
with assms have "f -` {f x} \<inter> space M \<in> sets M"
|
|
1429 |
by (subst Int_commute)
|
|
1430 |
(auto simp: vimage_def Int_def
|
|
1431 |
intro!: borel_measurable_const
|
|
1432 |
borel_measurable_eq_borel_measurable)
|
|
1433 |
from Int[OF this assms(3)]
|
|
1434 |
sets_into_space[OF assms(3), THEN Int_absorb1]
|
|
1435 |
have "f -` {f x} \<inter> a \<in> sets M" by (simp add: Int_assoc) }
|
|
1436 |
note vimage_f = this
|
|
1437 |
|
|
1438 |
have "finite a"
|
|
1439 |
using assms(2,3) sets_into_space
|
|
1440 |
by (auto intro: finite_subset)
|
|
1441 |
|
|
1442 |
have "integral (\<lambda>x. f x * indicator_fn a x) =
|
|
1443 |
integral (\<lambda>x. \<Sum>i\<in>f ` a. i * indicator_fn (f -` {i} \<inter> a) x)"
|
|
1444 |
(is "_ = integral (\<lambda>x. setsum (?f x) _)")
|
|
1445 |
unfolding indicator_fn_def if_distrib
|
|
1446 |
using `finite a` by (auto simp: setsum_cases intro!: integral_cong)
|
|
1447 |
also have "\<dots> = (\<Sum>i\<in>f`a. integral (\<lambda>x. ?f x i))"
|
|
1448 |
proof (rule integral_setsum, safe)
|
|
1449 |
fix n x assume "x \<in> a"
|
|
1450 |
thus "integrable (\<lambda>y. ?f y (f x))"
|
|
1451 |
using integral_indicator_fn(2)[OF vimage_f]
|
|
1452 |
by (auto intro!: integral_times_const)
|
|
1453 |
qed (simp add: `finite a`)
|
|
1454 |
also have "\<dots> = (\<Sum>i\<in>f`a. i * measure M (f -` {i} \<inter> a))"
|
|
1455 |
using integral_cmul_indicator[OF vimage_f]
|
|
1456 |
by (auto intro!: setsum_cong)
|
|
1457 |
finally show ?thesis .
|
|
1458 |
qed
|
|
1459 |
|
|
1460 |
lemma integral_finite:
|
|
1461 |
assumes "f \<in> borel_measurable M" and "finite (space M)"
|
|
1462 |
shows "integral f = (\<Sum> r \<in> f ` space M. r * measure M (f -` {r} \<inter> space M))"
|
|
1463 |
using integral_finite_on_sets[OF assms top]
|
|
1464 |
integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
|
|
1465 |
by (auto simp add: indicator_fn_def)
|
|
1466 |
|
|
1467 |
lemma integral_finite_singleton:
|
|
1468 |
assumes fin: "finite (space M)" and "Pow (space M) = sets M"
|
|
1469 |
shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
|
|
1470 |
proof -
|
|
1471 |
have "f \<in> borel_measurable M"
|
|
1472 |
unfolding borel_measurable_le_iff
|
|
1473 |
using assms by auto
|
|
1474 |
{ fix r let ?x = "f -` {r} \<inter> space M"
|
|
1475 |
have "?x \<subseteq> space M" by auto
|
|
1476 |
with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
|
|
1477 |
by (auto intro!: measure_real_sum_image) }
|
|
1478 |
note measure_eq_setsum = this
|
|
1479 |
show ?thesis
|
|
1480 |
unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
|
|
1481 |
measure_eq_setsum setsum_right_distrib
|
|
1482 |
apply (subst setsum_Sigma)
|
|
1483 |
apply (simp add: assms)
|
|
1484 |
apply (simp add: assms)
|
|
1485 |
proof (rule setsum_reindex_cong[symmetric])
|
|
1486 |
fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
|
|
1487 |
thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
|
|
1488 |
by auto
|
|
1489 |
qed (auto intro!: image_eqI inj_onI)
|
|
1490 |
qed
|
|
1491 |
|
|
1492 |
lemma borel_measurable_inverse:
|
|
1493 |
assumes "f \<in> borel_measurable M"
|
|
1494 |
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
|
|
1495 |
unfolding borel_measurable_ge_iff
|
|
1496 |
proof (safe, rule linorder_cases)
|
|
1497 |
fix a :: real assume "0 < a"
|
|
1498 |
{ fix w
|
|
1499 |
from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
|
|
1500 |
by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
|
|
1501 |
linorder_not_le real_le_refl real_le_trans real_less_def
|
|
1502 |
xt1(7) zero_less_divide_1_iff) }
|
|
1503 |
hence "{w \<in> space M. a \<le> inverse (f w)} =
|
|
1504 |
{w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
|
|
1505 |
with Int assms[unfolded borel_measurable_gr_iff]
|
|
1506 |
assms[unfolded borel_measurable_le_iff]
|
|
1507 |
show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
|
|
1508 |
next
|
|
1509 |
fix a :: real assume "0 = a"
|
|
1510 |
{ fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
|
|
1511 |
unfolding `0 = a`[symmetric] by auto }
|
|
1512 |
thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
|
|
1513 |
using assms[unfolded borel_measurable_ge_iff] by simp
|
|
1514 |
next
|
|
1515 |
fix a :: real assume "a < 0"
|
|
1516 |
{ fix w
|
|
1517 |
from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
|
|
1518 |
apply (cases "0 \<le> f w")
|
|
1519 |
apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
|
|
1520 |
zero_le_divide_1_iff)
|
|
1521 |
apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
|
|
1522 |
linorder_not_le real_le_refl real_le_trans)
|
|
1523 |
done }
|
|
1524 |
hence "{w \<in> space M. a \<le> inverse (f w)} =
|
|
1525 |
{w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
|
|
1526 |
with Un assms[unfolded borel_measurable_ge_iff]
|
|
1527 |
assms[unfolded borel_measurable_le_iff]
|
|
1528 |
show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
|
|
1529 |
qed
|
|
1530 |
|
|
1531 |
lemma borel_measurable_divide:
|
|
1532 |
assumes "f \<in> borel_measurable M"
|
|
1533 |
and "g \<in> borel_measurable M"
|
|
1534 |
shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
|
|
1535 |
unfolding field_divide_inverse
|
|
1536 |
by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
|
|
1537 |
|
|
1538 |
lemma RN_deriv_finite_singleton:
|
|
1539 |
fixes v :: "'a set \<Rightarrow> real"
|
|
1540 |
assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
|
|
1541 |
and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
|
|
1542 |
and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
|
|
1543 |
and "x \<in> space M" and "measure M {x} \<noteq> 0"
|
|
1544 |
shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
|
|
1545 |
unfolding RN_deriv_def
|
|
1546 |
proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
|
|
1547 |
show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
|
|
1548 |
unfolding borel_measurable_le_iff using Pow by auto
|
|
1549 |
next
|
|
1550 |
fix a assume "a \<in> sets M"
|
|
1551 |
hence "a \<subseteq> space M" and "finite a"
|
|
1552 |
using sets_into_space finite by (auto intro: finite_subset)
|
|
1553 |
have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
|
|
1554 |
v {x} * indicator_fn a x" using eq_0 by auto
|
|
1555 |
|
|
1556 |
from measure_space.measure_real_sum_image[OF ms_v, of a]
|
|
1557 |
Pow `a \<in> sets M` sets_into_space `finite a`
|
|
1558 |
have "v a = (\<Sum>x\<in>a. v {x})" by auto
|
|
1559 |
thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
|
|
1560 |
apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
|
|
1561 |
apply (unfold divide_1)
|
|
1562 |
by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
|
|
1563 |
next
|
|
1564 |
fix w assume "w \<in> borel_measurable M"
|
|
1565 |
assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
|
|
1566 |
have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
|
|
1567 |
|
|
1568 |
have "w x * measure M {x} =
|
|
1569 |
(\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
|
|
1570 |
apply (subst (3) mult_commute)
|
|
1571 |
unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
|
|
1572 |
using `x \<in> space M` by simp
|
|
1573 |
also have "... = v {x}"
|
|
1574 |
using int_eq_v[rule_format, OF `{x} \<in> sets M`]
|
|
1575 |
by (simp add: integral_finite_singleton[OF finite Pow])
|
|
1576 |
finally show "w x = v {x} / measure M {x}"
|
|
1577 |
using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
|
|
1578 |
qed fact
|
|
1579 |
|
|
1580 |
lemma countable_space_integral_reduce:
|
|
1581 |
assumes "positive M (measure M)" and "f \<in> borel_measurable M"
|
|
1582 |
and "countable (f ` space M)"
|
|
1583 |
and "\<not> finite (pos_part f ` space M)"
|
|
1584 |
and "\<not> finite (neg_part f ` space M)"
|
|
1585 |
and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
|
|
1586 |
and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
|
|
1587 |
shows "integral f = p - n"
|
|
1588 |
oops
|
|
1589 |
|
|
1590 |
(*
|
|
1591 |
val countable_space_integral_reduce = store_thm
|
|
1592 |
("countable_space_integral_reduce",
|
|
1593 |
"\<forall>m f p n. measure_space m \<and>
|
|
1594 |
positive m \<and>
|
|
1595 |
f \<in> borel_measurable (space m, sets m) \<and>
|
|
1596 |
countable (IMAGE f (space m)) \<and>
|
|
1597 |
~(FINITE (IMAGE (pos_part f) (space m))) \<and>
|
|
1598 |
~(FINITE (IMAGE (neg_part f) (space m))) \<and>
|
|
1599 |
(\<lambda>r. r *
|
|
1600 |
measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
|
|
1601 |
enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
|
|
1602 |
(\<lambda>r. r *
|
|
1603 |
measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
|
|
1604 |
enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
|
|
1605 |
(integral m f = p - n)",
|
|
1606 |
RW_TAC std_ss [integral_def]
|
|
1607 |
++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
|
|
1608 |
>> RW_TAC std_ss []
|
|
1609 |
++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
|
|
1610 |
>> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
|
|
1611 |
++ MATCH_MP_TAC nnfis_mon_conv
|
|
1612 |
++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
|
|
1613 |
by (`countable (IMAGE (pos_part f) (space m))`
|
|
1614 |
by (MATCH_MP_TAC COUNTABLE_SUBSET
|
|
1615 |
++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
|
|
1616 |
++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
|
|
1617 |
++ METIS_TAC [])
|
|
1618 |
++ METIS_TAC [COUNTABLE_ALT])
|
|
1619 |
++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
|
|
1620 |
++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
|
|
1621 |
(pred_set$count n) then pos_part f t else 0)`
|
|
1622 |
++ Q.EXISTS_TAC `(\<lambda>n.
|
|
1623 |
sum (0,n)
|
|
1624 |
((\<lambda>r.
|
|
1625 |
r *
|
|
1626 |
measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
|
|
1627 |
enumerate (IMAGE (pos_part f) (space m))))`
|
|
1628 |
++ ASM_SIMP_TAC std_ss []
|
|
1629 |
++ CONJ_TAC
|
|
1630 |
>> (RW_TAC std_ss [mono_convergent_def]
|
|
1631 |
>> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
|
|
1632 |
++ RW_TAC std_ss [SEQ]
|
|
1633 |
++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
|
|
1634 |
by METIS_TAC [IN_IMAGE]
|
|
1635 |
++ Q.EXISTS_TAC `SUC N`
|
|
1636 |
++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
|
|
1637 |
++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
|
|
1638 |
++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
|
|
1639 |
++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
|
|
1640 |
++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
|
|
1641 |
then pos_part f t else 0)) =
|
|
1642 |
(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
|
|
1643 |
indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
|
|
1644 |
\<inter> (space m)) i) t)
|
|
1645 |
(pred_set$count n'))`
|
|
1646 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
|
|
1647 |
>> (`pred_set$count n' = x INSERT (pred_set$count n')`
|
|
1648 |
by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
|
|
1649 |
++ POP_ORW
|
|
1650 |
++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
|
|
1651 |
++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
|
|
1652 |
REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
|
|
1653 |
++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
|
|
1654 |
++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
|
|
1655 |
enumerate (IMAGE (pos_part f) (space m)) x' *
|
|
1656 |
(if enumerate (IMAGE (pos_part f) (space m)) x =
|
|
1657 |
enumerate (IMAGE (pos_part f) (space m)) x'
|
|
1658 |
then 1 else 0) else 0)) = (\<lambda>x. 0)`
|
|
1659 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
|
|
1660 |
++ POP_ORW
|
|
1661 |
++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
|
|
1662 |
++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
|
|
1663 |
>> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
|
|
1664 |
++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
|
|
1665 |
REAL_SUM_IMAGE_IN_IF]
|
|
1666 |
++ `(\<lambda>x. (if x \<in> pred_set$count n' then
|
|
1667 |
(\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
|
|
1668 |
(if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
|
|
1669 |
t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
|
|
1670 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
|
|
1671 |
++ POP_ORW
|
|
1672 |
++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
|
|
1673 |
++ POP_ORW
|
|
1674 |
++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
|
|
1675 |
enumerate (IMAGE (pos_part f) (space m))) =
|
|
1676 |
(\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
|
|
1677 |
measure m ((\<lambda>i.
|
|
1678 |
PREIMAGE (pos_part f)
|
|
1679 |
{enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
|
|
1680 |
space m) i))`
|
|
1681 |
by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
|
|
1682 |
++ POP_ORW
|
|
1683 |
++ MATCH_MP_TAC psfis_intro
|
|
1684 |
++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
|
|
1685 |
++ REVERSE CONJ_TAC
|
|
1686 |
>> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
|
|
1687 |
++ METIS_TAC [REAL_LE_REFL])
|
|
1688 |
++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
|
|
1689 |
by METIS_TAC [pos_part_neg_part_borel_measurable]
|
|
1690 |
++ REPEAT STRIP_TAC
|
|
1691 |
++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
|
|
1692 |
{w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
|
|
1693 |
by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
|
|
1694 |
++ DECIDE_TAC)
|
|
1695 |
++ POP_ORW
|
|
1696 |
++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
|
|
1697 |
++ METIS_TAC [borel_measurable_const, measure_space_def])
|
|
1698 |
++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
|
|
1699 |
++ MATCH_MP_TAC nnfis_mon_conv
|
|
1700 |
++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
|
|
1701 |
by (`countable (IMAGE (neg_part f) (space m))`
|
|
1702 |
by (MATCH_MP_TAC COUNTABLE_SUBSET
|
|
1703 |
++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
|
|
1704 |
++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
|
|
1705 |
++ METIS_TAC [])
|
|
1706 |
++ METIS_TAC [COUNTABLE_ALT])
|
|
1707 |
++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
|
|
1708 |
++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
|
|
1709 |
(pred_set$count n) then neg_part f t else 0)`
|
|
1710 |
++ Q.EXISTS_TAC `(\<lambda>n.
|
|
1711 |
sum (0,n)
|
|
1712 |
((\<lambda>r.
|
|
1713 |
r *
|
|
1714 |
measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
|
|
1715 |
enumerate (IMAGE (neg_part f) (space m))))`
|
|
1716 |
++ ASM_SIMP_TAC std_ss []
|
|
1717 |
++ CONJ_TAC
|
|
1718 |
>> (RW_TAC std_ss [mono_convergent_def]
|
|
1719 |
>> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
|
|
1720 |
++ RW_TAC std_ss [SEQ]
|
|
1721 |
++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
|
|
1722 |
by METIS_TAC [IN_IMAGE]
|
|
1723 |
++ Q.EXISTS_TAC `SUC N`
|
|
1724 |
++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
|
|
1725 |
++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
|
|
1726 |
++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
|
|
1727 |
++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
|
|
1728 |
++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
|
|
1729 |
then neg_part f t else 0)) =
|
|
1730 |
(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
|
|
1731 |
indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
|
|
1732 |
\<inter> (space m)) i) t)
|
|
1733 |
(pred_set$count n'))`
|
|
1734 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
|
|
1735 |
>> (`pred_set$count n' = x INSERT (pred_set$count n')`
|
|
1736 |
by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
|
|
1737 |
++ POP_ORW
|
|
1738 |
++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
|
|
1739 |
++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
|
|
1740 |
REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
|
|
1741 |
++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
|
|
1742 |
++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
|
|
1743 |
enumerate (IMAGE (neg_part f) (space m)) x' *
|
|
1744 |
(if enumerate (IMAGE (neg_part f) (space m)) x =
|
|
1745 |
enumerate (IMAGE (neg_part f) (space m)) x'
|
|
1746 |
then 1 else 0) else 0)) = (\<lambda>x. 0)`
|
|
1747 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
|
|
1748 |
++ POP_ORW
|
|
1749 |
++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
|
|
1750 |
++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
|
|
1751 |
>> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
|
|
1752 |
++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
|
|
1753 |
REAL_SUM_IMAGE_IN_IF]
|
|
1754 |
++ `(\<lambda>x. (if x \<in> pred_set$count n' then
|
|
1755 |
(\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
|
|
1756 |
(if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
|
|
1757 |
t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
|
|
1758 |
by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
|
|
1759 |
++ POP_ORW
|
|
1760 |
++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
|
|
1761 |
++ POP_ORW
|
|
1762 |
++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
|
|
1763 |
enumerate (IMAGE (neg_part f) (space m))) =
|
|
1764 |
(\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
|
|
1765 |
measure m ((\<lambda>i.
|
|
1766 |
PREIMAGE (neg_part f)
|
|
1767 |
{enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
|
|
1768 |
space m) i))`
|
|
1769 |
by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
|
|
1770 |
++ POP_ORW
|
|
1771 |
++ MATCH_MP_TAC psfis_intro
|
|
1772 |
++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
|
|
1773 |
++ REVERSE CONJ_TAC
|
|
1774 |
>> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
|
|
1775 |
++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
|
|
1776 |
++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
|
|
1777 |
by METIS_TAC [pos_part_neg_part_borel_measurable]
|
|
1778 |
++ REPEAT STRIP_TAC
|
|
1779 |
++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
|
|
1780 |
{w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
|
|
1781 |
by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
|
|
1782 |
++ DECIDE_TAC)
|
|
1783 |
++ POP_ORW
|
|
1784 |
++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
|
|
1785 |
++ METIS_TAC [borel_measurable_const, measure_space_def]);
|
|
1786 |
*)
|
|
1787 |
|
|
1788 |
end
|
|
1789 |
|
|
1790 |
end |