|
1 (* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) |
|
2 |
|
3 header {*Lebesgue Integration*} |
|
4 |
|
5 theory Lebesgue_Integration |
|
6 imports Measure Borel |
|
7 begin |
|
8 |
|
9 section "@{text \<mu>}-null sets" |
|
10 |
|
11 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}" |
|
12 |
|
13 lemma sums_If_finite: |
|
14 assumes finite: "finite {r. P r}" |
|
15 shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _") |
|
16 proof cases |
|
17 assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto |
|
18 thus ?thesis by (simp add: sums_zero) |
|
19 next |
|
20 assume not_empty: "{r. P r} \<noteq> {}" |
|
21 have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)" |
|
22 by (rule series_zero) |
|
23 (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric]) |
|
24 also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)" |
|
25 by (subst setsum_cases) |
|
26 (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le) |
|
27 finally show ?thesis . |
|
28 qed |
|
29 |
|
30 lemma sums_single: |
|
31 "(\<lambda>r. if r = i then f r else 0) sums f i" |
|
32 using sums_If_finite[of "\<lambda>r. r = i" f] by simp |
|
33 |
|
34 section "Simple function" |
|
35 |
|
36 text {* |
|
37 |
|
38 Our simple functions are not restricted to positive real numbers. Instead |
|
39 they are just functions with a finite range and are measurable when singleton |
|
40 sets are measurable. |
|
41 |
|
42 *} |
|
43 |
|
44 definition (in sigma_algebra) "simple_function g \<longleftrightarrow> |
|
45 finite (g ` space M) \<and> |
|
46 (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)" |
|
47 |
|
48 lemma (in sigma_algebra) simple_functionD: |
|
49 assumes "simple_function g" |
|
50 shows "finite (g ` space M)" |
|
51 "x \<in> g ` space M \<Longrightarrow> g -` {x} \<inter> space M \<in> sets M" |
|
52 using assms unfolding simple_function_def by auto |
|
53 |
|
54 lemma (in sigma_algebra) simple_function_indicator_representation: |
|
55 fixes f ::"'a \<Rightarrow> pinfreal" |
|
56 assumes f: "simple_function f" and x: "x \<in> space M" |
|
57 shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)" |
|
58 (is "?l = ?r") |
|
59 proof - |
|
60 have "?r = (\<Sum>y \<in> f ` space M. |
|
61 (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))" |
|
62 by (auto intro!: setsum_cong2) |
|
63 also have "... = f x * indicator (f -` {f x} \<inter> space M) x" |
|
64 using assms by (auto dest: simple_functionD simp: setsum_delta) |
|
65 also have "... = f x" using x by (auto simp: indicator_def) |
|
66 finally show ?thesis by auto |
|
67 qed |
|
68 |
|
69 lemma (in measure_space) simple_function_notspace: |
|
70 "simple_function (\<lambda>x. h x * indicator (- space M) x::pinfreal)" (is "simple_function ?h") |
|
71 proof - |
|
72 have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto |
|
73 hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) |
|
74 have "?h -` {0} \<inter> space M = space M" by auto |
|
75 thus ?thesis unfolding simple_function_def by auto |
|
76 qed |
|
77 |
|
78 lemma (in sigma_algebra) simple_function_cong: |
|
79 assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
80 shows "simple_function f \<longleftrightarrow> simple_function g" |
|
81 proof - |
|
82 have "f ` space M = g ` space M" |
|
83 "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
84 using assms by (auto intro!: image_eqI) |
|
85 thus ?thesis unfolding simple_function_def using assms by simp |
|
86 qed |
|
87 |
|
88 lemma (in sigma_algebra) borel_measurable_simple_function: |
|
89 assumes "simple_function f" |
|
90 shows "f \<in> borel_measurable M" |
|
91 proof (rule borel_measurableI) |
|
92 fix S |
|
93 let ?I = "f ` (f -` S \<inter> space M)" |
|
94 have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto |
|
95 have "finite ?I" |
|
96 using assms unfolding simple_function_def by (auto intro: finite_subset) |
|
97 hence "?U \<in> sets M" |
|
98 apply (rule finite_UN) |
|
99 using assms unfolding simple_function_def by auto |
|
100 thus "f -` S \<inter> space M \<in> sets M" unfolding * . |
|
101 qed |
|
102 |
|
103 lemma (in sigma_algebra) simple_function_borel_measurable: |
|
104 fixes f :: "'a \<Rightarrow> 'x::t2_space" |
|
105 assumes "f \<in> borel_measurable M" and "finite (f ` space M)" |
|
106 shows "simple_function f" |
|
107 using assms unfolding simple_function_def |
|
108 by (auto intro: borel_measurable_vimage) |
|
109 |
|
110 lemma (in sigma_algebra) simple_function_const[intro, simp]: |
|
111 "simple_function (\<lambda>x. c)" |
|
112 by (auto intro: finite_subset simp: simple_function_def) |
|
113 |
|
114 lemma (in sigma_algebra) simple_function_compose[intro, simp]: |
|
115 assumes "simple_function f" |
|
116 shows "simple_function (g \<circ> f)" |
|
117 unfolding simple_function_def |
|
118 proof safe |
|
119 show "finite ((g \<circ> f) ` space M)" |
|
120 using assms unfolding simple_function_def by (auto simp: image_compose) |
|
121 next |
|
122 fix x assume "x \<in> space M" |
|
123 let ?G = "g -` {g (f x)} \<inter> (f`space M)" |
|
124 have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M = |
|
125 (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto |
|
126 show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M" |
|
127 using assms unfolding simple_function_def * |
|
128 by (rule_tac finite_UN) (auto intro!: finite_UN) |
|
129 qed |
|
130 |
|
131 lemma (in sigma_algebra) simple_function_indicator[intro, simp]: |
|
132 assumes "A \<in> sets M" |
|
133 shows "simple_function (indicator A)" |
|
134 proof - |
|
135 have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _") |
|
136 by (auto simp: indicator_def) |
|
137 hence "finite ?S" by (rule finite_subset) simp |
|
138 moreover have "- A \<inter> space M = space M - A" by auto |
|
139 ultimately show ?thesis unfolding simple_function_def |
|
140 using assms by (auto simp: indicator_def_raw) |
|
141 qed |
|
142 |
|
143 lemma (in sigma_algebra) simple_function_Pair[intro, simp]: |
|
144 assumes "simple_function f" |
|
145 assumes "simple_function g" |
|
146 shows "simple_function (\<lambda>x. (f x, g x))" (is "simple_function ?p") |
|
147 unfolding simple_function_def |
|
148 proof safe |
|
149 show "finite (?p ` space M)" |
|
150 using assms unfolding simple_function_def |
|
151 by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto |
|
152 next |
|
153 fix x assume "x \<in> space M" |
|
154 have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = |
|
155 (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" |
|
156 by auto |
|
157 with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M" |
|
158 using assms unfolding simple_function_def by auto |
|
159 qed |
|
160 |
|
161 lemma (in sigma_algebra) simple_function_compose1: |
|
162 assumes "simple_function f" |
|
163 shows "simple_function (\<lambda>x. g (f x))" |
|
164 using simple_function_compose[OF assms, of g] |
|
165 by (simp add: comp_def) |
|
166 |
|
167 lemma (in sigma_algebra) simple_function_compose2: |
|
168 assumes "simple_function f" and "simple_function g" |
|
169 shows "simple_function (\<lambda>x. h (f x) (g x))" |
|
170 proof - |
|
171 have "simple_function ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))" |
|
172 using assms by auto |
|
173 thus ?thesis by (simp_all add: comp_def) |
|
174 qed |
|
175 |
|
176 lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] |
|
177 and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] |
|
178 and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] |
|
179 and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] |
|
180 and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] |
|
181 and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] |
|
182 |
|
183 lemma (in sigma_algebra) simple_function_setsum[intro, simp]: |
|
184 assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)" |
|
185 shows "simple_function (\<lambda>x. \<Sum>i\<in>P. f i x)" |
|
186 proof cases |
|
187 assume "finite P" from this assms show ?thesis by induct auto |
|
188 qed auto |
|
189 |
|
190 lemma (in sigma_algebra) simple_function_le_measurable: |
|
191 assumes "simple_function f" "simple_function g" |
|
192 shows "{x \<in> space M. f x \<le> g x} \<in> sets M" |
|
193 proof - |
|
194 have *: "{x \<in> space M. f x \<le> g x} = |
|
195 (\<Union>(F, G)\<in>f`space M \<times> g`space M. |
|
196 if F \<le> G then (f -` {F} \<inter> space M) \<inter> (g -` {G} \<inter> space M) else {})" |
|
197 apply (auto split: split_if_asm) |
|
198 apply (rule_tac x=x in bexI) |
|
199 apply (rule_tac x=x in bexI) |
|
200 by simp_all |
|
201 have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> |
|
202 (f -` {f x} \<inter> space M) \<inter> (g -` {g y} \<inter> space M) \<in> sets M" |
|
203 using assms unfolding simple_function_def by auto |
|
204 have "finite (f`space M \<times> g`space M)" |
|
205 using assms unfolding simple_function_def by auto |
|
206 thus ?thesis unfolding * |
|
207 apply (rule finite_UN) |
|
208 using assms unfolding simple_function_def |
|
209 by (auto intro!: **) |
|
210 qed |
|
211 |
|
212 lemma setsum_indicator_disjoint_family: |
|
213 fixes f :: "'d \<Rightarrow> 'e::semiring_1" |
|
214 assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P" |
|
215 shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j" |
|
216 proof - |
|
217 have "P \<inter> {i. x \<in> A i} = {j}" |
|
218 using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def |
|
219 by auto |
|
220 thus ?thesis |
|
221 unfolding indicator_def |
|
222 by (simp add: if_distrib setsum_cases[OF `finite P`]) |
|
223 qed |
|
224 |
|
225 lemma LeastI2_wellorder: |
|
226 fixes a :: "_ :: wellorder" |
|
227 assumes "P a" |
|
228 and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a" |
|
229 shows "Q (Least P)" |
|
230 proof (rule LeastI2_order) |
|
231 show "P (Least P)" using `P a` by (rule LeastI) |
|
232 next |
|
233 fix y assume "P y" thus "Least P \<le> y" by (rule Least_le) |
|
234 next |
|
235 fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2)) |
|
236 qed |
|
237 |
|
238 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: |
|
239 fixes u :: "'a \<Rightarrow> pinfreal" |
|
240 assumes u: "u \<in> borel_measurable M" |
|
241 shows "\<exists>f. (\<forall>i. simple_function (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u" |
|
242 proof - |
|
243 have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and> |
|
244 (u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))" |
|
245 (is "\<exists>f. \<forall>x j. ?P x j (f x j)") |
|
246 proof(rule choice, rule, rule choice, rule) |
|
247 fix x j show "\<exists>n. ?P x j n" |
|
248 proof cases |
|
249 assume *: "u x < of_nat j" |
|
250 then obtain r where r: "u x = Real r" "0 \<le> r" by (cases "u x") auto |
|
251 from reals_Archimedean6a[of "r * 2^j"] |
|
252 obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)" |
|
253 using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff) |
|
254 thus ?thesis using r * by (auto intro!: exI[of _ n]) |
|
255 qed auto |
|
256 qed |
|
257 then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and |
|
258 upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and |
|
259 lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast |
|
260 |
|
261 { fix j x P |
|
262 assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)" |
|
263 assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k" |
|
264 have "P (f x j)" |
|
265 proof cases |
|
266 assume "of_nat j \<le> u x" thus "P (f x j)" |
|
267 using top[of j x] 1 by auto |
|
268 next |
|
269 assume "\<not> of_nat j \<le> u x" |
|
270 hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))" |
|
271 using upper lower by auto |
|
272 from 2[OF this] show "P (f x j)" . |
|
273 qed } |
|
274 note fI = this |
|
275 |
|
276 { fix j x |
|
277 have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x" |
|
278 by (rule fI, simp, cases "u x") (auto split: split_if_asm) } |
|
279 note f_eq = this |
|
280 |
|
281 { fix j x |
|
282 have "f x j \<le> j * 2 ^ j" |
|
283 proof (rule fI) |
|
284 fix k assume *: "u x < of_nat j" |
|
285 assume "of_nat k \<le> u x * 2 ^ j" |
|
286 also have "\<dots> \<le> of_nat (j * 2^j)" |
|
287 using * by (cases "u x") (auto simp: zero_le_mult_iff) |
|
288 finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult) |
|
289 qed simp } |
|
290 note f_upper = this |
|
291 |
|
292 let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal" |
|
293 show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def |
|
294 proof (safe intro!: exI[of _ ?g]) |
|
295 fix j |
|
296 have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}" |
|
297 using f_upper by auto |
|
298 thus "finite (?g j ` space M)" by (rule finite_subset) auto |
|
299 next |
|
300 fix j t assume "t \<in> space M" |
|
301 have **: "?g j -` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}" |
|
302 by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff) |
|
303 |
|
304 show "?g j -` {?g j t} \<inter> space M \<in> sets M" |
|
305 proof cases |
|
306 assume "of_nat j \<le> u t" |
|
307 hence "?g j -` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}" |
|
308 unfolding ** f_eq[symmetric] by auto |
|
309 thus "?g j -` {?g j t} \<inter> space M \<in> sets M" |
|
310 using u by auto |
|
311 next |
|
312 assume not_t: "\<not> of_nat j \<le> u t" |
|
313 hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto |
|
314 have split_vimage: "?g j -` {?g j t} \<inter> space M = |
|
315 {x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}" |
|
316 unfolding ** |
|
317 proof safe |
|
318 fix x assume [simp]: "f t j = f x j" |
|
319 have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp |
|
320 hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))" |
|
321 using upper lower by auto |
|
322 hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using * |
|
323 by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
324 thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto |
|
325 next |
|
326 fix x |
|
327 assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" |
|
328 hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))" |
|
329 by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
330 hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto |
|
331 note 2 |
|
332 also have "\<dots> \<le> of_nat (j*2^j)" |
|
333 using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult) |
|
334 finally have bound_ux: "u x < of_nat j" |
|
335 by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
336 show "f t j = f x j" |
|
337 proof (rule antisym) |
|
338 from 1 lower[OF bound_ux] |
|
339 show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm) |
|
340 from upper[OF bound_ux] 2 |
|
341 show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm) |
|
342 qed |
|
343 qed |
|
344 show ?thesis unfolding split_vimage using u by auto |
|
345 qed |
|
346 next |
|
347 fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq) |
|
348 next |
|
349 fix t |
|
350 { fix i |
|
351 have "f t i * 2 \<le> f t (Suc i)" |
|
352 proof (rule fI) |
|
353 assume "of_nat (Suc i) \<le> u t" |
|
354 hence "of_nat i \<le> u t" by (cases "u t") auto |
|
355 thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp |
|
356 next |
|
357 fix k |
|
358 assume *: "u t * 2 ^ Suc i < of_nat (Suc k)" |
|
359 show "f t i * 2 \<le> k" |
|
360 proof (rule fI) |
|
361 assume "of_nat i \<le> u t" |
|
362 hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i" |
|
363 by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
364 also have "\<dots> < of_nat (Suc k)" using * by auto |
|
365 finally show "i * 2 ^ i * 2 \<le> k" |
|
366 by (auto simp del: real_of_nat_mult) |
|
367 next |
|
368 fix j assume "of_nat j \<le> u t * 2 ^ i" |
|
369 with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
370 qed |
|
371 qed |
|
372 thus "?g i t \<le> ?g (Suc i) t" |
|
373 by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) } |
|
374 hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto |
|
375 |
|
376 show "(SUP j. of_nat (f t j) / 2 ^ j) = u t" |
|
377 proof (rule pinfreal_SUPI) |
|
378 fix j show "of_nat (f t j) / 2 ^ j \<le> u t" |
|
379 proof (rule fI) |
|
380 assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t" |
|
381 by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
382 next |
|
383 fix k assume "of_nat k \<le> u t * 2 ^ j" |
|
384 thus "of_nat k / 2 ^ j \<le> u t" |
|
385 by (cases "u t") |
|
386 (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff) |
|
387 qed |
|
388 next |
|
389 fix y :: pinfreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y" |
|
390 show "u t \<le> y" |
|
391 proof (cases "u t") |
|
392 case (preal r) |
|
393 show ?thesis |
|
394 proof (rule ccontr) |
|
395 assume "\<not> u t \<le> y" |
|
396 then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto |
|
397 with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"] |
|
398 obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r - p" by auto |
|
399 let ?N = "max n (natfloor r + 1)" |
|
400 have "u t < of_nat ?N" "n \<le> ?N" |
|
401 using ge_natfloor_plus_one_imp_gt[of r n] preal |
|
402 by (auto simp: max_def real_Suc_natfloor) |
|
403 from lower[OF this(1)] |
|
404 have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq |
|
405 using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm) |
|
406 hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N" |
|
407 using preal by (auto simp: field_simps divide_real_def[symmetric]) |
|
408 with n[OF `n \<le> ?N`] p preal *[of ?N] |
|
409 show False |
|
410 by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm) |
|
411 qed |
|
412 next |
|
413 case infinite |
|
414 { fix j have "f t j = j*2^j" using top[of j t] infinite by simp |
|
415 hence "of_nat j \<le> y" using *[of j] |
|
416 by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) } |
|
417 note all_less_y = this |
|
418 show ?thesis unfolding infinite |
|
419 proof (rule ccontr) |
|
420 assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto |
|
421 moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat) |
|
422 with all_less_y[of n] r show False by auto |
|
423 qed |
|
424 qed |
|
425 qed |
|
426 qed |
|
427 qed |
|
428 |
|
429 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence': |
|
430 fixes u :: "'a \<Rightarrow> pinfreal" |
|
431 assumes "u \<in> borel_measurable M" |
|
432 obtains (x) f where "f \<up> u" "\<And>i. simple_function (f i)" "\<And>i. \<omega>\<notin>f i`space M" |
|
433 proof - |
|
434 from borel_measurable_implies_simple_function_sequence[OF assms] |
|
435 obtain f where x: "\<And>i. simple_function (f i)" "f \<up> u" |
|
436 and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto |
|
437 { fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp } |
|
438 with x show thesis by (auto intro!: that[of f]) |
|
439 qed |
|
440 |
|
441 section "Simple integral" |
|
442 |
|
443 definition (in measure_space) |
|
444 "simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M))" |
|
445 |
|
446 lemma (in measure_space) simple_integral_cong: |
|
447 assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
448 shows "simple_integral f = simple_integral g" |
|
449 proof - |
|
450 have "f ` space M = g ` space M" |
|
451 "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
452 using assms by (auto intro!: image_eqI) |
|
453 thus ?thesis unfolding simple_integral_def by simp |
|
454 qed |
|
455 |
|
456 lemma (in measure_space) simple_integral_const[simp]: |
|
457 "simple_integral (\<lambda>x. c) = c * \<mu> (space M)" |
|
458 proof (cases "space M = {}") |
|
459 case True thus ?thesis unfolding simple_integral_def by simp |
|
460 next |
|
461 case False hence "(\<lambda>x. c) ` space M = {c}" by auto |
|
462 thus ?thesis unfolding simple_integral_def by simp |
|
463 qed |
|
464 |
|
465 lemma (in measure_space) simple_function_partition: |
|
466 assumes "simple_function f" and "simple_function g" |
|
467 shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)" |
|
468 (is "_ = setsum _ (?p ` space M)") |
|
469 proof- |
|
470 let "?sub x" = "?p ` (f -` {x} \<inter> space M)" |
|
471 let ?SIGMA = "Sigma (f`space M) ?sub" |
|
472 |
|
473 have [intro]: |
|
474 "finite (f ` space M)" |
|
475 "finite (g ` space M)" |
|
476 using assms unfolding simple_function_def by simp_all |
|
477 |
|
478 { fix A |
|
479 have "?p ` (A \<inter> space M) \<subseteq> |
|
480 (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)" |
|
481 by auto |
|
482 hence "finite (?p ` (A \<inter> space M))" |
|
483 by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) } |
|
484 note this[intro, simp] |
|
485 |
|
486 { fix x assume "x \<in> space M" |
|
487 have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto |
|
488 moreover { |
|
489 fix x y |
|
490 have *: "f -` {f x} \<inter> g -` {g x} \<inter> space M |
|
491 = (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" by auto |
|
492 assume "x \<in> space M" "y \<in> space M" |
|
493 hence "f -` {f x} \<inter> g -` {g x} \<inter> space M \<in> sets M" |
|
494 using assms unfolding simple_function_def * by auto } |
|
495 ultimately |
|
496 have "\<mu> (f -` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))" |
|
497 by (subst measure_finitely_additive) auto } |
|
498 hence "simple_integral f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)" |
|
499 unfolding simple_integral_def |
|
500 by (subst setsum_Sigma[symmetric], |
|
501 auto intro!: setsum_cong simp: setsum_right_distrib[symmetric]) |
|
502 also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)" |
|
503 proof - |
|
504 have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI) |
|
505 have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M |
|
506 = (\<lambda>x. (f x, ?p x)) ` space M" |
|
507 proof safe |
|
508 fix x assume "x \<in> space M" |
|
509 thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M" |
|
510 by (auto intro!: image_eqI[of _ _ "?p x"]) |
|
511 qed auto |
|
512 thus ?thesis |
|
513 apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI) |
|
514 apply (rule_tac x="xa" in image_eqI) |
|
515 by simp_all |
|
516 qed |
|
517 finally show ?thesis . |
|
518 qed |
|
519 |
|
520 lemma (in measure_space) simple_integral_add[simp]: |
|
521 assumes "simple_function f" and "simple_function g" |
|
522 shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g" |
|
523 proof - |
|
524 { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M" |
|
525 assume "x \<in> space M" |
|
526 hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" |
|
527 "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S" |
|
528 by auto } |
|
529 thus ?thesis |
|
530 unfolding |
|
531 simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] |
|
532 simple_function_partition[OF `simple_function f` `simple_function g`] |
|
533 simple_function_partition[OF `simple_function g` `simple_function f`] |
|
534 apply (subst (3) Int_commute) |
|
535 by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong) |
|
536 qed |
|
537 |
|
538 lemma (in measure_space) simple_integral_setsum[simp]: |
|
539 assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)" |
|
540 shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))" |
|
541 proof cases |
|
542 assume "finite P" |
|
543 from this assms show ?thesis |
|
544 by induct (auto simp: simple_function_setsum simple_integral_add) |
|
545 qed auto |
|
546 |
|
547 lemma (in measure_space) simple_integral_mult[simp]: |
|
548 assumes "simple_function f" |
|
549 shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f" |
|
550 proof - |
|
551 note mult = simple_function_mult[OF simple_function_const[of c] assms] |
|
552 { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M" |
|
553 assume "x \<in> space M" |
|
554 hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" |
|
555 by auto } |
|
556 thus ?thesis |
|
557 unfolding simple_function_partition[OF mult assms] |
|
558 simple_function_partition[OF assms mult] |
|
559 by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) |
|
560 qed |
|
561 |
|
562 lemma (in measure_space) simple_integral_mono: |
|
563 assumes "simple_function f" and "simple_function g" |
|
564 and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x" |
|
565 shows "simple_integral f \<le> simple_integral g" |
|
566 unfolding |
|
567 simple_function_partition[OF `simple_function f` `simple_function g`] |
|
568 simple_function_partition[OF `simple_function g` `simple_function f`] |
|
569 apply (subst Int_commute) |
|
570 proof (safe intro!: setsum_mono) |
|
571 fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M" |
|
572 assume "x \<in> space M" |
|
573 hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto |
|
574 thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S" |
|
575 using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono) |
|
576 qed |
|
577 |
|
578 lemma (in measure_space) simple_integral_indicator: |
|
579 assumes "A \<in> sets M" |
|
580 assumes "simple_function f" |
|
581 shows "simple_integral (\<lambda>x. f x * indicator A x) = |
|
582 (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))" |
|
583 proof cases |
|
584 assume "A = space M" |
|
585 moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f" |
|
586 by (auto intro!: simple_integral_cong) |
|
587 moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto |
|
588 ultimately show ?thesis by (simp add: simple_integral_def) |
|
589 next |
|
590 assume "A \<noteq> space M" |
|
591 then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto |
|
592 have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _") |
|
593 proof safe |
|
594 fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto |
|
595 next |
|
596 fix y assume "y \<in> A" thus "f y \<in> ?I ` space M" |
|
597 using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) |
|
598 next |
|
599 show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) |
|
600 qed |
|
601 have *: "simple_integral (\<lambda>x. f x * indicator A x) = |
|
602 (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))" |
|
603 unfolding simple_integral_def I |
|
604 proof (rule setsum_mono_zero_cong_left) |
|
605 show "finite (f ` space M \<union> {0})" |
|
606 using assms(2) unfolding simple_function_def by auto |
|
607 show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}" |
|
608 using sets_into_space[OF assms(1)] by auto |
|
609 have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}" by (auto simp: image_iff) |
|
610 thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}). |
|
611 i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto |
|
612 next |
|
613 fix x assume "x \<in> f`A \<union> {0}" |
|
614 hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A" |
|
615 by (auto simp: indicator_def split: split_if_asm) |
|
616 thus "x * \<mu> (?I -` {x} \<inter> space M) = |
|
617 x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all |
|
618 qed |
|
619 show ?thesis unfolding * |
|
620 using assms(2) unfolding simple_function_def |
|
621 by (auto intro!: setsum_mono_zero_cong_right) |
|
622 qed |
|
623 |
|
624 lemma (in measure_space) simple_integral_indicator_only[simp]: |
|
625 assumes "A \<in> sets M" |
|
626 shows "simple_integral (indicator A) = \<mu> A" |
|
627 proof cases |
|
628 assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto |
|
629 thus ?thesis unfolding simple_integral_def using `space M = {}` by auto |
|
630 next |
|
631 assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pinfreal}" by auto |
|
632 thus ?thesis |
|
633 using simple_integral_indicator[OF assms simple_function_const[of 1]] |
|
634 using sets_into_space[OF assms] |
|
635 by (auto intro!: arg_cong[where f="\<mu>"]) |
|
636 qed |
|
637 |
|
638 lemma (in measure_space) simple_integral_null_set: |
|
639 assumes "simple_function u" "N \<in> null_sets" |
|
640 shows "simple_integral (\<lambda>x. u x * indicator N x) = 0" |
|
641 proof - |
|
642 have "simple_integral (\<lambda>x. u x * indicator N x) \<le> |
|
643 simple_integral (\<lambda>x. \<omega> * indicator N x)" |
|
644 using assms |
|
645 by (safe intro!: simple_integral_mono simple_function_mult simple_function_indicator simple_function_const) simp |
|
646 also have "... = 0" apply(subst simple_integral_mult) |
|
647 using assms(2) by auto |
|
648 finally show ?thesis by auto |
|
649 qed |
|
650 |
|
651 lemma (in measure_space) simple_integral_cong': |
|
652 assumes f: "simple_function f" and g: "simple_function g" |
|
653 and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" |
|
654 shows "simple_integral f = simple_integral g" |
|
655 proof - |
|
656 let ?h = "\<lambda>h. \<lambda>x. (h x * indicator {x\<in>space M. f x = g x} x |
|
657 + h x * indicator {x\<in>space M. f x \<noteq> g x} x |
|
658 + h x * indicator (-space M) x::pinfreal)" |
|
659 have *:"\<And>h. h = ?h h" unfolding indicator_def apply rule by auto |
|
660 have mea_neq:"{x \<in> space M. f x \<noteq> g x} \<in> sets M" using f g by (auto simp: borel_measurable_simple_function) |
|
661 then have mea_nullset: "{x \<in> space M. f x \<noteq> g x} \<in> null_sets" using mea by auto |
|
662 have h1:"\<And>h::_=>pinfreal. simple_function h \<Longrightarrow> |
|
663 simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x = g x} x)" |
|
664 apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator) |
|
665 using f g by (auto simp: borel_measurable_simple_function) |
|
666 have h2:"\<And>h::_\<Rightarrow>pinfreal. simple_function h \<Longrightarrow> |
|
667 simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x \<noteq> g x} x)" |
|
668 apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator) |
|
669 by(rule mea_neq) |
|
670 have **:"\<And>a b c d e f. a = b \<Longrightarrow> c = d \<Longrightarrow> e = f \<Longrightarrow> a+c+e = b+d+f" by auto |
|
671 note *** = simple_integral_add[OF simple_function_add[OF h1 h2] simple_function_notspace] |
|
672 simple_integral_add[OF h1 h2] |
|
673 show ?thesis apply(subst *[of g]) apply(subst *[of f]) |
|
674 unfolding ***[OF f f] ***[OF g g] |
|
675 proof(rule **) case goal1 show ?case apply(rule arg_cong[where f=simple_integral]) apply rule |
|
676 unfolding indicator_def by auto |
|
677 next note * = simple_integral_null_set[OF _ mea_nullset] |
|
678 case goal2 show ?case unfolding *[OF f] *[OF g] .. |
|
679 next case goal3 show ?case apply(rule simple_integral_cong) by auto |
|
680 qed |
|
681 qed |
|
682 |
|
683 section "Continuous posititve integration" |
|
684 |
|
685 definition (in measure_space) |
|
686 "positive_integral f = |
|
687 (SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)" |
|
688 |
|
689 lemma (in measure_space) positive_integral_alt1: |
|
690 "positive_integral f = |
|
691 (SUP g : {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. simple_integral g)" |
|
692 unfolding positive_integral_def SUPR_def |
|
693 proof (safe intro!: arg_cong[where f=Sup]) |
|
694 fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x" |
|
695 assume "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" |
|
696 hence "?g \<le> f" "simple_function ?g" "simple_integral g = simple_integral ?g" |
|
697 "\<omega> \<notin> g`space M" |
|
698 unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) |
|
699 thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}" |
|
700 by auto |
|
701 next |
|
702 fix g assume "simple_function g" "g \<le> f" "\<omega> \<notin> g`space M" |
|
703 hence "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" |
|
704 by (auto simp add: le_fun_def image_iff) |
|
705 thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}" |
|
706 by auto |
|
707 qed |
|
708 |
|
709 lemma (in measure_space) positive_integral_alt: |
|
710 "positive_integral f = |
|
711 (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)" |
|
712 apply(rule order_class.antisym) unfolding positive_integral_def |
|
713 apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim) |
|
714 proof safe fix u assume u:"simple_function u" and uf:"u \<le> f" |
|
715 let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x" |
|
716 have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] . |
|
717 show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and> |
|
718 (\<lambda>n. simple_integral (b n)) ----> simple_integral u" |
|
719 apply(rule_tac x="?u" in exI, safe) apply(rule su) |
|
720 proof- fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto |
|
721 also note uf finally show "?u n \<le> f" . |
|
722 let ?s = "{x \<in> space M. u x = \<omega>}" |
|
723 show "(\<lambda>n. simple_integral (?u n)) ----> simple_integral u" |
|
724 proof(cases "\<mu> ?s = 0") |
|
725 case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto |
|
726 have *:"\<And>n. simple_integral (?u n) = simple_integral u" |
|
727 apply(rule simple_integral_cong'[OF su u]) unfolding * True .. |
|
728 show ?thesis unfolding * by auto |
|
729 next case False note m0=this |
|
730 have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u by (auto simp: borel_measurable_simple_function) |
|
731 have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)" |
|
732 apply(subst simple_integral_mult) using s |
|
733 unfolding simple_integral_indicator_only[OF s] using False by auto |
|
734 also have "... \<le> simple_integral u" |
|
735 apply (rule simple_integral_mono) |
|
736 apply (rule simple_function_mult) |
|
737 apply (rule simple_function_const) |
|
738 apply(rule ) prefer 3 apply(subst indicator_def) |
|
739 using s u by auto |
|
740 finally have *:"simple_integral u = \<omega>" by auto |
|
741 show ?thesis unfolding * Lim_omega_pos |
|
742 proof safe case goal1 |
|
743 from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this |
|
744 def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0" |
|
745 unfolding N_def using N by auto |
|
746 show ?case apply-apply(rule_tac x=N in exI,safe) |
|
747 proof- case goal1 |
|
748 have "Real B \<le> Real (real N) * \<mu> ?s" |
|
749 proof(cases "\<mu> ?s = \<omega>") |
|
750 case True thus ?thesis using `B>0` N by auto |
|
751 next case False |
|
752 have *:"B \<le> real N * real (\<mu> ?s)" |
|
753 using N(1) apply-apply(subst (asm) pos_divide_le_eq) |
|
754 apply rule using m0 False by auto |
|
755 show ?thesis apply(subst Real_real'[THEN sym,OF False]) |
|
756 apply(subst pinfreal_times,subst if_P) defer |
|
757 apply(subst pinfreal_less_eq,subst if_P) defer |
|
758 using * N `B>0` by(auto intro: mult_nonneg_nonneg) |
|
759 qed |
|
760 also have "... \<le> Real (real n) * \<mu> ?s" |
|
761 apply(rule mult_right_mono) using goal1 by auto |
|
762 also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)" |
|
763 apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s]) |
|
764 unfolding simple_integral_indicator_only[OF s] .. |
|
765 also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)" |
|
766 apply(rule simple_integral_mono) apply(rule simple_function_mult) |
|
767 apply(rule simple_function_const) |
|
768 apply(rule simple_function_indicator) apply(rule s su)+ by auto |
|
769 finally show ?case . |
|
770 qed qed qed |
|
771 fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M" |
|
772 hence "u x = \<omega>" apply-apply(rule ccontr) by auto |
|
773 hence "\<omega> = Real (real n)" using x by auto |
|
774 thus False by auto |
|
775 qed |
|
776 qed |
|
777 |
|
778 lemma (in measure_space) positive_integral_cong: |
|
779 assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" |
|
780 shows "positive_integral f = positive_integral g" |
|
781 proof - |
|
782 have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)" |
|
783 using assms by auto |
|
784 thus ?thesis unfolding positive_integral_alt1 by auto |
|
785 qed |
|
786 |
|
787 lemma (in measure_space) positive_integral_eq_simple_integral: |
|
788 assumes "simple_function f" |
|
789 shows "positive_integral f = simple_integral f" |
|
790 unfolding positive_integral_alt |
|
791 proof (safe intro!: pinfreal_SUPI) |
|
792 fix g assume "simple_function g" "g \<le> f" |
|
793 with assms show "simple_integral g \<le> simple_integral f" |
|
794 by (auto intro!: simple_integral_mono simp: le_fun_def) |
|
795 next |
|
796 fix y assume "\<forall>x. x\<in>{g. simple_function g \<and> g \<le> f} \<longrightarrow> simple_integral x \<le> y" |
|
797 with assms show "simple_integral f \<le> y" by auto |
|
798 qed |
|
799 |
|
800 lemma (in measure_space) positive_integral_mono: |
|
801 assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x" |
|
802 shows "positive_integral u \<le> positive_integral v" |
|
803 unfolding positive_integral_alt1 |
|
804 proof (safe intro!: SUPR_mono) |
|
805 fix a assume a: "simple_function a" and "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>" |
|
806 with mono have "\<forall>x\<in>space M. a x \<le> v x \<and> a x \<noteq> \<omega>" by fastsimp |
|
807 with a show "\<exists>b\<in>{g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. simple_integral a \<le> simple_integral b" |
|
808 by (auto intro!: bexI[of _ a]) |
|
809 qed |
|
810 |
|
811 lemma (in measure_space) positive_integral_SUP_approx: |
|
812 assumes "f \<up> s" |
|
813 and f: "\<And>i. f i \<in> borel_measurable M" |
|
814 and "simple_function u" |
|
815 and le: "u \<le> s" and real: "\<omega> \<notin> u`space M" |
|
816 shows "simple_integral u \<le> (SUP i. positive_integral (f i))" (is "_ \<le> ?S") |
|
817 proof (rule pinfreal_le_mult_one_interval) |
|
818 fix a :: pinfreal assume "0 < a" "a < 1" |
|
819 hence "a \<noteq> 0" by auto |
|
820 let "?B i" = "{x \<in> space M. a * u x \<le> f i x}" |
|
821 have B: "\<And>i. ?B i \<in> sets M" |
|
822 using f `simple_function u` by (auto simp: borel_measurable_simple_function) |
|
823 |
|
824 let "?uB i x" = "u x * indicator (?B i) x" |
|
825 |
|
826 { fix i have "?B i \<subseteq> ?B (Suc i)" |
|
827 proof safe |
|
828 fix i x assume "a * u x \<le> f i x" |
|
829 also have "\<dots> \<le> f (Suc i) x" |
|
830 using `f \<up> s` unfolding isoton_def le_fun_def by auto |
|
831 finally show "a * u x \<le> f (Suc i) x" . |
|
832 qed } |
|
833 note B_mono = this |
|
834 |
|
835 have u: "\<And>x. x \<in> space M \<Longrightarrow> u -` {u x} \<inter> space M \<in> sets M" |
|
836 using `simple_function u` by (auto simp add: simple_function_def) |
|
837 |
|
838 { fix i |
|
839 have "(\<lambda>n. (u -` {i} \<inter> space M) \<inter> ?B n) \<up> (u -` {i} \<inter> space M)" using B_mono unfolding isoton_def |
|
840 proof safe |
|
841 fix x assume "x \<in> space M" |
|
842 show "x \<in> (\<Union>i. (u -` {u x} \<inter> space M) \<inter> ?B i)" |
|
843 proof cases |
|
844 assume "u x = 0" thus ?thesis using `x \<in> space M` by simp |
|
845 next |
|
846 assume "u x \<noteq> 0" |
|
847 with `a < 1` real `x \<in> space M` |
|
848 have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff) |
|
849 also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s` |
|
850 unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) |
|
851 finally obtain i where "a * u x < f i x" unfolding SUPR_def |
|
852 by (auto simp add: less_Sup_iff) |
|
853 hence "a * u x \<le> f i x" by auto |
|
854 thus ?thesis using `x \<in> space M` by auto |
|
855 qed |
|
856 qed auto } |
|
857 note measure_conv = measure_up[OF u Int[OF u B] this] |
|
858 |
|
859 have "simple_integral u = (SUP i. simple_integral (?uB i))" |
|
860 unfolding simple_integral_indicator[OF B `simple_function u`] |
|
861 proof (subst SUPR_pinfreal_setsum, safe) |
|
862 fix x n assume "x \<in> space M" |
|
863 have "\<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x}) |
|
864 \<le> \<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})" |
|
865 using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono) |
|
866 thus "u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B n) |
|
867 \<le> u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B (Suc n))" |
|
868 by (auto intro: mult_left_mono) |
|
869 next |
|
870 show "simple_integral u = |
|
871 (\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u -` {i} \<inter> space M \<inter> ?B n))" |
|
872 using measure_conv unfolding simple_integral_def isoton_def |
|
873 by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult) |
|
874 qed |
|
875 moreover |
|
876 have "a * (SUP i. simple_integral (?uB i)) \<le> ?S" |
|
877 unfolding pinfreal_SUP_cmult[symmetric] |
|
878 proof (safe intro!: SUP_mono) |
|
879 fix i |
|
880 have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)" |
|
881 using B `simple_function u` |
|
882 by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) |
|
883 also have "\<dots> \<le> positive_integral (f i)" |
|
884 proof - |
|
885 have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto |
|
886 hence *: "simple_function (\<lambda>x. a * ?uB i x)" using B assms(3) |
|
887 by (auto intro!: simple_integral_mono) |
|
888 show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric] |
|
889 by (auto intro!: positive_integral_mono simp: indicator_def) |
|
890 qed |
|
891 finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)" |
|
892 by auto |
|
893 qed |
|
894 ultimately show "a * simple_integral u \<le> ?S" by simp |
|
895 qed |
|
896 |
|
897 text {* Beppo-Levi monotone convergence theorem *} |
|
898 lemma (in measure_space) positive_integral_isoton: |
|
899 assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M" |
|
900 shows "(\<lambda>i. positive_integral (f i)) \<up> positive_integral u" |
|
901 unfolding isoton_def |
|
902 proof safe |
|
903 fix i show "positive_integral (f i) \<le> positive_integral (f (Suc i))" |
|
904 apply (rule positive_integral_mono) |
|
905 using `f \<up> u` unfolding isoton_def le_fun_def by auto |
|
906 next |
|
907 have "u \<in> borel_measurable M" |
|
908 using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def) |
|
909 have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto |
|
910 |
|
911 show "(SUP i. positive_integral (f i)) = positive_integral u" |
|
912 proof (rule antisym) |
|
913 from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def] |
|
914 show "(SUP j. positive_integral (f j)) \<le> positive_integral u" |
|
915 by (auto intro!: SUP_leI positive_integral_mono) |
|
916 next |
|
917 show "positive_integral u \<le> (SUP i. positive_integral (f i))" |
|
918 unfolding positive_integral_def[of u] |
|
919 by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) |
|
920 qed |
|
921 qed |
|
922 |
|
923 lemma (in measure_space) SUP_simple_integral_sequences: |
|
924 assumes f: "f \<up> u" "\<And>i. simple_function (f i)" |
|
925 and g: "g \<up> u" "\<And>i. simple_function (g i)" |
|
926 shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))" |
|
927 (is "SUPR _ ?F = SUPR _ ?G") |
|
928 proof - |
|
929 have "(SUP i. ?F i) = (SUP i. positive_integral (f i))" |
|
930 using assms by (simp add: positive_integral_eq_simple_integral) |
|
931 also have "\<dots> = positive_integral u" |
|
932 using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]] |
|
933 unfolding isoton_def by simp |
|
934 also have "\<dots> = (SUP i. positive_integral (g i))" |
|
935 using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]] |
|
936 unfolding isoton_def by simp |
|
937 also have "\<dots> = (SUP i. ?G i)" |
|
938 using assms by (simp add: positive_integral_eq_simple_integral) |
|
939 finally show ?thesis . |
|
940 qed |
|
941 |
|
942 lemma (in measure_space) positive_integral_const[simp]: |
|
943 "positive_integral (\<lambda>x. c) = c * \<mu> (space M)" |
|
944 by (subst positive_integral_eq_simple_integral) auto |
|
945 |
|
946 lemma (in measure_space) positive_integral_isoton_simple: |
|
947 assumes "f \<up> u" and e: "\<And>i. simple_function (f i)" |
|
948 shows "(\<lambda>i. simple_integral (f i)) \<up> positive_integral u" |
|
949 using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]] |
|
950 unfolding positive_integral_eq_simple_integral[OF e] . |
|
951 |
|
952 lemma (in measure_space) positive_integral_linear: |
|
953 assumes f: "f \<in> borel_measurable M" |
|
954 and g: "g \<in> borel_measurable M" |
|
955 shows "positive_integral (\<lambda>x. a * f x + g x) = |
|
956 a * positive_integral f + positive_integral g" |
|
957 (is "positive_integral ?L = _") |
|
958 proof - |
|
959 from borel_measurable_implies_simple_function_sequence'[OF f] guess u . |
|
960 note u = this positive_integral_isoton_simple[OF this(1-2)] |
|
961 from borel_measurable_implies_simple_function_sequence'[OF g] guess v . |
|
962 note v = this positive_integral_isoton_simple[OF this(1-2)] |
|
963 let "?L' i x" = "a * u i x + v i x" |
|
964 |
|
965 have "?L \<in> borel_measurable M" |
|
966 using assms by simp |
|
967 from borel_measurable_implies_simple_function_sequence'[OF this] guess l . |
|
968 note positive_integral_isoton_simple[OF this(1-2)] and l = this |
|
969 moreover have |
|
970 "(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))" |
|
971 proof (rule SUP_simple_integral_sequences[OF l(1-2)]) |
|
972 show "?L' \<up> ?L" "\<And>i. simple_function (?L' i)" |
|
973 using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right) |
|
974 qed |
|
975 moreover from u v have L'_isoton: |
|
976 "(\<lambda>i. simple_integral (?L' i)) \<up> a * positive_integral f + positive_integral g" |
|
977 by (simp add: isoton_add isoton_cmult_right) |
|
978 ultimately show ?thesis by (simp add: isoton_def) |
|
979 qed |
|
980 |
|
981 lemma (in measure_space) positive_integral_cmult: |
|
982 assumes "f \<in> borel_measurable M" |
|
983 shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f" |
|
984 using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto |
|
985 |
|
986 lemma (in measure_space) positive_integral_indicator[simp]: |
|
987 "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A" |
|
988 by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) |
|
989 |
|
990 lemma (in measure_space) positive_integral_cmult_indicator: |
|
991 "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A" |
|
992 by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) |
|
993 |
|
994 lemma (in measure_space) positive_integral_add: |
|
995 assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
996 shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g" |
|
997 using positive_integral_linear[OF assms, of 1] by simp |
|
998 |
|
999 lemma (in measure_space) positive_integral_setsum: |
|
1000 assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" |
|
1001 shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))" |
|
1002 proof cases |
|
1003 assume "finite P" |
|
1004 from this assms show ?thesis |
|
1005 proof induct |
|
1006 case (insert i P) |
|
1007 have "f i \<in> borel_measurable M" |
|
1008 "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" |
|
1009 using insert by (auto intro!: borel_measurable_pinfreal_setsum) |
|
1010 from positive_integral_add[OF this] |
|
1011 show ?case using insert by auto |
|
1012 qed simp |
|
1013 qed simp |
|
1014 |
|
1015 lemma (in measure_space) positive_integral_diff: |
|
1016 assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M" |
|
1017 and fin: "positive_integral g \<noteq> \<omega>" |
|
1018 and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x" |
|
1019 shows "positive_integral (\<lambda>x. f x - g x) = positive_integral f - positive_integral g" |
|
1020 proof - |
|
1021 have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
|
1022 using f g by (rule borel_measurable_pinfreal_diff) |
|
1023 have "positive_integral (\<lambda>x. f x - g x) + positive_integral g = |
|
1024 positive_integral f" |
|
1025 unfolding positive_integral_add[OF borel g, symmetric] |
|
1026 proof (rule positive_integral_cong) |
|
1027 fix x assume "x \<in> space M" |
|
1028 from mono[OF this] show "f x - g x + g x = f x" |
|
1029 by (cases "f x", cases "g x", simp, simp, cases "g x", auto) |
|
1030 qed |
|
1031 with mono show ?thesis |
|
1032 by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono) |
|
1033 qed |
|
1034 |
|
1035 lemma (in measure_space) positive_integral_psuminf: |
|
1036 assumes "\<And>i. f i \<in> borel_measurable M" |
|
1037 shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))" |
|
1038 proof - |
|
1039 have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)" |
|
1040 by (rule positive_integral_isoton) |
|
1041 (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono |
|
1042 arg_cong[where f=Sup] |
|
1043 simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def) |
|
1044 thus ?thesis |
|
1045 by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms]) |
|
1046 qed |
|
1047 |
|
1048 text {* Fatou's lemma: convergence theorem on limes inferior *} |
|
1049 lemma (in measure_space) positive_integral_lim_INF: |
|
1050 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pinfreal" |
|
1051 assumes "\<And>i. u i \<in> borel_measurable M" |
|
1052 shows "positive_integral (SUP n. INF m. u (m + n)) \<le> |
|
1053 (SUP n. INF m. positive_integral (u (m + n)))" |
|
1054 proof - |
|
1055 have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M" |
|
1056 by (auto intro!: borel_measurable_SUP borel_measurable_INF assms) |
|
1057 |
|
1058 have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))" |
|
1059 proof (unfold isoton_def, safe) |
|
1060 fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))" |
|
1061 by (rule INF_mono[where N=Suc]) simp |
|
1062 qed |
|
1063 from positive_integral_isoton[OF this] assms |
|
1064 have "positive_integral (SUP n. INF m. u (m + n)) = |
|
1065 (SUP n. positive_integral (INF m. u (m + n)))" |
|
1066 unfolding isoton_def by (simp add: borel_measurable_INF) |
|
1067 also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))" |
|
1068 by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand) |
|
1069 finally show ?thesis . |
|
1070 qed |
|
1071 |
|
1072 lemma (in measure_space) measure_space_density: |
|
1073 assumes borel: "u \<in> borel_measurable M" |
|
1074 shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v") |
|
1075 proof |
|
1076 show "?v {} = 0" by simp |
|
1077 show "countably_additive M ?v" |
|
1078 unfolding countably_additive_def |
|
1079 proof safe |
|
1080 fix A :: "nat \<Rightarrow> 'a set" |
|
1081 assume "range A \<subseteq> sets M" |
|
1082 hence "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M" |
|
1083 using borel by (auto intro: borel_measurable_indicator) |
|
1084 moreover assume "disjoint_family A" |
|
1085 note psuminf_indicator[OF this] |
|
1086 ultimately show "(\<Sum>\<^isub>\<infinity>n. ?v (A n)) = ?v (\<Union>x. A x)" |
|
1087 by (simp add: positive_integral_psuminf[symmetric]) |
|
1088 qed |
|
1089 qed |
|
1090 |
|
1091 lemma (in measure_space) positive_integral_null_set: |
|
1092 assumes borel: "u \<in> borel_measurable M" and "N \<in> null_sets" |
|
1093 shows "positive_integral (\<lambda>x. u x * indicator N x) = 0" (is "?I = 0") |
|
1094 proof - |
|
1095 have "N \<in> sets M" using `N \<in> null_sets` by auto |
|
1096 have "(\<lambda>i x. min (of_nat i) (u x) * indicator N x) \<up> (\<lambda>x. u x * indicator N x)" |
|
1097 unfolding isoton_fun_expand |
|
1098 proof (safe intro!: isoton_cmult_left, unfold isoton_def, safe) |
|
1099 fix j i show "min (of_nat j) (u i) \<le> min (of_nat (Suc j)) (u i)" |
|
1100 by (rule min_max.inf_mono) auto |
|
1101 next |
|
1102 fix i show "(SUP j. min (of_nat j) (u i)) = u i" |
|
1103 proof (cases "u i") |
|
1104 case infinite |
|
1105 moreover hence "\<And>j. min (of_nat j) (u i) = of_nat j" |
|
1106 by (auto simp: min_def) |
|
1107 ultimately show ?thesis by (simp add: Sup_\<omega>) |
|
1108 next |
|
1109 case (preal r) |
|
1110 obtain j where "r \<le> of_nat j" using ex_le_of_nat .. |
|
1111 hence "u i \<le> of_nat j" using preal by (auto simp: real_of_nat_def) |
|
1112 show ?thesis |
|
1113 proof (rule pinfreal_SUPI) |
|
1114 fix y assume "\<And>j. j \<in> UNIV \<Longrightarrow> min (of_nat j) (u i) \<le> y" |
|
1115 note this[of j] |
|
1116 moreover have "min (of_nat j) (u i) = u i" |
|
1117 using `u i \<le> of_nat j` by (auto simp: min_def) |
|
1118 ultimately show "u i \<le> y" by simp |
|
1119 qed simp |
|
1120 qed |
|
1121 qed |
|
1122 from positive_integral_isoton[OF this] |
|
1123 have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))" |
|
1124 unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator) |
|
1125 also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))" |
|
1126 proof (rule SUP_mono, rule positive_integral_mono) |
|
1127 fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x" |
|
1128 by (cases "x \<in> N") auto |
|
1129 qed |
|
1130 also have "\<dots> = 0" |
|
1131 using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator) |
|
1132 finally show ?thesis by simp |
|
1133 qed |
|
1134 |
|
1135 lemma (in measure_space) positive_integral_Markov_inequality: |
|
1136 assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>" |
|
1137 shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)" |
|
1138 (is "\<mu> ?A \<le> _ * ?PI") |
|
1139 proof - |
|
1140 have "?A \<in> sets M" |
|
1141 using `A \<in> sets M` borel by auto |
|
1142 hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)" |
|
1143 using positive_integral_indicator by simp |
|
1144 also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))" |
|
1145 proof (rule positive_integral_mono) |
|
1146 fix x assume "x \<in> space M" |
|
1147 show "indicator ?A x \<le> c * (u x * indicator A x)" |
|
1148 by (cases "x \<in> ?A") auto |
|
1149 qed |
|
1150 also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)" |
|
1151 using assms |
|
1152 by (auto intro!: positive_integral_cmult borel_measurable_indicator) |
|
1153 finally show ?thesis . |
|
1154 qed |
|
1155 |
|
1156 lemma (in measure_space) positive_integral_0_iff: |
|
1157 assumes borel: "u \<in> borel_measurable M" |
|
1158 shows "positive_integral u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0" |
|
1159 (is "_ \<longleftrightarrow> \<mu> ?A = 0") |
|
1160 proof - |
|
1161 have A: "?A \<in> sets M" using borel by auto |
|
1162 have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u" |
|
1163 by (auto intro!: positive_integral_cong simp: indicator_def) |
|
1164 |
|
1165 show ?thesis |
|
1166 proof |
|
1167 assume "\<mu> ?A = 0" |
|
1168 hence "?A \<in> null_sets" using `?A \<in> sets M` by auto |
|
1169 from positive_integral_null_set[OF borel this] |
|
1170 have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp |
|
1171 thus "positive_integral u = 0" unfolding u by simp |
|
1172 next |
|
1173 assume *: "positive_integral u = 0" |
|
1174 let "?M n" = "{x \<in> space M. 1 \<le> of_nat n * u x}" |
|
1175 have "0 = (SUP n. \<mu> (?M n \<inter> ?A))" |
|
1176 proof - |
|
1177 { fix n |
|
1178 from positive_integral_Markov_inequality[OF borel `?A \<in> sets M`, of "of_nat n"] |
|
1179 have "\<mu> (?M n \<inter> ?A) = 0" unfolding * u by simp } |
|
1180 thus ?thesis by simp |
|
1181 qed |
|
1182 also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)" |
|
1183 proof (safe intro!: continuity_from_below) |
|
1184 fix n show "?M n \<inter> ?A \<in> sets M" |
|
1185 using borel by (auto intro!: Int) |
|
1186 next |
|
1187 fix n x assume "1 \<le> of_nat n * u x" |
|
1188 also have "\<dots> \<le> of_nat (Suc n) * u x" |
|
1189 by (subst (1 2) mult_commute) (auto intro!: pinfreal_mult_cancel) |
|
1190 finally show "1 \<le> of_nat (Suc n) * u x" . |
|
1191 qed |
|
1192 also have "\<dots> = \<mu> ?A" |
|
1193 proof (safe intro!: arg_cong[where f="\<mu>"]) |
|
1194 fix x assume "u x \<noteq> 0" and [simp, intro]: "x \<in> space M" |
|
1195 show "x \<in> (\<Union>n. ?M n \<inter> ?A)" |
|
1196 proof (cases "u x") |
|
1197 case (preal r) |
|
1198 obtain j where "1 / r \<le> of_nat j" using ex_le_of_nat .. |
|
1199 hence "1 / r * r \<le> of_nat j * r" using preal unfolding mult_le_cancel_right by auto |
|
1200 hence "1 \<le> of_nat j * r" using preal `u x \<noteq> 0` by auto |
|
1201 thus ?thesis using `u x \<noteq> 0` preal by (auto simp: real_of_nat_def[symmetric]) |
|
1202 qed auto |
|
1203 qed |
|
1204 finally show "\<mu> ?A = 0" by simp |
|
1205 qed |
|
1206 qed |
|
1207 |
|
1208 lemma (in measure_space) positive_integral_cong_on_null_sets: |
|
1209 assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M" |
|
1210 and measure: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" |
|
1211 shows "positive_integral f = positive_integral g" |
|
1212 proof - |
|
1213 let ?N = "{x\<in>space M. f x \<noteq> g x}" and ?E = "{x\<in>space M. f x = g x}" |
|
1214 let "?A h x" = "h x * indicator ?E x :: pinfreal" |
|
1215 let "?B h x" = "h x * indicator ?N x :: pinfreal" |
|
1216 |
|
1217 have A: "positive_integral (?A f) = positive_integral (?A g)" |
|
1218 by (auto intro!: positive_integral_cong simp: indicator_def) |
|
1219 |
|
1220 have [intro]: "?N \<in> sets M" "?E \<in> sets M" using f g by auto |
|
1221 hence "?N \<in> null_sets" using measure by auto |
|
1222 hence B: "positive_integral (?B f) = positive_integral (?B g)" |
|
1223 using f g by (simp add: positive_integral_null_set) |
|
1224 |
|
1225 have "positive_integral f = positive_integral (\<lambda>x. ?A f x + ?B f x)" |
|
1226 by (auto intro!: positive_integral_cong simp: indicator_def) |
|
1227 also have "\<dots> = positive_integral (?A f) + positive_integral (?B f)" |
|
1228 using f g by (auto intro!: positive_integral_add borel_measurable_indicator) |
|
1229 also have "\<dots> = positive_integral (\<lambda>x. ?A g x + ?B g x)" |
|
1230 unfolding A B using f g by (auto intro!: positive_integral_add[symmetric] borel_measurable_indicator) |
|
1231 also have "\<dots> = positive_integral g" |
|
1232 by (auto intro!: positive_integral_cong simp: indicator_def) |
|
1233 finally show ?thesis by simp |
|
1234 qed |
|
1235 |
|
1236 section "Lebesgue Integral" |
|
1237 |
|
1238 definition (in measure_space) integrable where |
|
1239 "integrable f \<longleftrightarrow> f \<in> borel_measurable M \<and> |
|
1240 positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega> \<and> |
|
1241 positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>" |
|
1242 |
|
1243 lemma (in measure_space) integrableD[dest]: |
|
1244 assumes "integrable f" |
|
1245 shows "f \<in> borel_measurable M" |
|
1246 "positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega>" |
|
1247 "positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>" |
|
1248 using assms unfolding integrable_def by auto |
|
1249 |
|
1250 definition (in measure_space) integral where |
|
1251 "integral f = |
|
1252 real (positive_integral (\<lambda>x. Real (f x))) - |
|
1253 real (positive_integral (\<lambda>x. Real (- f x)))" |
|
1254 |
|
1255 lemma (in measure_space) integral_cong: |
|
1256 assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" |
|
1257 shows "integral f = integral g" |
|
1258 using assms by (simp cong: positive_integral_cong add: integral_def) |
|
1259 |
|
1260 lemma (in measure_space) integrable_cong: |
|
1261 "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable f \<longleftrightarrow> integrable g" |
|
1262 by (simp cong: positive_integral_cong measurable_cong add: integrable_def) |
|
1263 |
|
1264 lemma (in measure_space) integral_eq_positive_integral: |
|
1265 assumes "\<And>x. 0 \<le> f x" |
|
1266 shows "integral f = real (positive_integral (\<lambda>x. Real (f x)))" |
|
1267 proof - |
|
1268 have "\<And>x. Real (- f x) = 0" using assms by simp |
|
1269 thus ?thesis by (simp del: Real_eq_0 add: integral_def) |
|
1270 qed |
|
1271 |
|
1272 lemma (in measure_space) integral_minus[intro, simp]: |
|
1273 assumes "integrable f" |
|
1274 shows "integrable (\<lambda>x. - f x)" "integral (\<lambda>x. - f x) = - integral f" |
|
1275 using assms by (auto simp: integrable_def integral_def) |
|
1276 |
|
1277 lemma (in measure_space) integral_of_positive_diff: |
|
1278 assumes integrable: "integrable u" "integrable v" |
|
1279 and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x" |
|
1280 shows "integrable f" and "integral f = integral u - integral v" |
|
1281 proof - |
|
1282 let ?PI = positive_integral |
|
1283 let "?f x" = "Real (f x)" |
|
1284 let "?mf x" = "Real (- f x)" |
|
1285 let "?u x" = "Real (u x)" |
|
1286 let "?v x" = "Real (v x)" |
|
1287 |
|
1288 from borel_measurable_diff[of u v] integrable |
|
1289 have f_borel: "?f \<in> borel_measurable M" and |
|
1290 mf_borel: "?mf \<in> borel_measurable M" and |
|
1291 v_borel: "?v \<in> borel_measurable M" and |
|
1292 u_borel: "?u \<in> borel_measurable M" and |
|
1293 "f \<in> borel_measurable M" |
|
1294 by (auto simp: f_def[symmetric] integrable_def) |
|
1295 |
|
1296 have "?PI (\<lambda>x. Real (u x - v x)) \<le> ?PI ?u" |
|
1297 using pos by (auto intro!: positive_integral_mono) |
|
1298 moreover have "?PI (\<lambda>x. Real (v x - u x)) \<le> ?PI ?v" |
|
1299 using pos by (auto intro!: positive_integral_mono) |
|
1300 ultimately show f: "integrable f" |
|
1301 using `integrable u` `integrable v` `f \<in> borel_measurable M` |
|
1302 by (auto simp: integrable_def f_def) |
|
1303 hence mf: "integrable (\<lambda>x. - f x)" .. |
|
1304 |
|
1305 have *: "\<And>x. Real (- v x) = 0" "\<And>x. Real (- u x) = 0" |
|
1306 using pos by auto |
|
1307 |
|
1308 have "\<And>x. ?u x + ?mf x = ?v x + ?f x" |
|
1309 unfolding f_def using pos by simp |
|
1310 hence "?PI (\<lambda>x. ?u x + ?mf x) = ?PI (\<lambda>x. ?v x + ?f x)" by simp |
|
1311 hence "real (?PI ?u + ?PI ?mf) = real (?PI ?v + ?PI ?f)" |
|
1312 using positive_integral_add[OF u_borel mf_borel] |
|
1313 using positive_integral_add[OF v_borel f_borel] |
|
1314 by auto |
|
1315 then show "integral f = integral u - integral v" |
|
1316 using f mf `integrable u` `integrable v` |
|
1317 unfolding integral_def integrable_def * |
|
1318 by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?v", cases "?PI ?u") |
|
1319 (auto simp add: field_simps) |
|
1320 qed |
|
1321 |
|
1322 lemma (in measure_space) integral_linear: |
|
1323 assumes "integrable f" "integrable g" and "0 \<le> a" |
|
1324 shows "integrable (\<lambda>t. a * f t + g t)" |
|
1325 and "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g" |
|
1326 proof - |
|
1327 let ?PI = positive_integral |
|
1328 let "?f x" = "Real (f x)" |
|
1329 let "?g x" = "Real (g x)" |
|
1330 let "?mf x" = "Real (- f x)" |
|
1331 let "?mg x" = "Real (- g x)" |
|
1332 let "?p t" = "max 0 (a * f t) + max 0 (g t)" |
|
1333 let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)" |
|
1334 |
|
1335 have pos: "?f \<in> borel_measurable M" "?g \<in> borel_measurable M" |
|
1336 and neg: "?mf \<in> borel_measurable M" "?mg \<in> borel_measurable M" |
|
1337 and p: "?p \<in> borel_measurable M" |
|
1338 and n: "?n \<in> borel_measurable M" |
|
1339 using assms by (simp_all add: integrable_def) |
|
1340 |
|
1341 have *: "\<And>x. Real (?p x) = Real a * ?f x + ?g x" |
|
1342 "\<And>x. Real (?n x) = Real a * ?mf x + ?mg x" |
|
1343 "\<And>x. Real (- ?p x) = 0" |
|
1344 "\<And>x. Real (- ?n x) = 0" |
|
1345 using `0 \<le> a` by (auto simp: max_def min_def zero_le_mult_iff mult_le_0_iff add_nonpos_nonpos) |
|
1346 |
|
1347 note linear = |
|
1348 positive_integral_linear[OF pos] |
|
1349 positive_integral_linear[OF neg] |
|
1350 |
|
1351 have "integrable ?p" "integrable ?n" |
|
1352 "\<And>t. a * f t + g t = ?p t - ?n t" "\<And>t. 0 \<le> ?p t" "\<And>t. 0 \<le> ?n t" |
|
1353 using assms p n unfolding integrable_def * linear by auto |
|
1354 note diff = integral_of_positive_diff[OF this] |
|
1355 |
|
1356 show "integrable (\<lambda>t. a * f t + g t)" by (rule diff) |
|
1357 |
|
1358 from assms show "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g" |
|
1359 unfolding diff(2) unfolding integral_def * linear integrable_def |
|
1360 by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg") |
|
1361 (auto simp add: field_simps zero_le_mult_iff) |
|
1362 qed |
|
1363 |
|
1364 lemma (in measure_space) integral_add[simp, intro]: |
|
1365 assumes "integrable f" "integrable g" |
|
1366 shows "integrable (\<lambda>t. f t + g t)" |
|
1367 and "integral (\<lambda>t. f t + g t) = integral f + integral g" |
|
1368 using assms integral_linear[where a=1] by auto |
|
1369 |
|
1370 lemma (in measure_space) integral_zero[simp, intro]: |
|
1371 shows "integrable (\<lambda>x. 0)" |
|
1372 and "integral (\<lambda>x. 0) = 0" |
|
1373 unfolding integrable_def integral_def |
|
1374 by (auto simp add: borel_measurable_const) |
|
1375 |
|
1376 lemma (in measure_space) integral_cmult[simp, intro]: |
|
1377 assumes "integrable f" |
|
1378 shows "integrable (\<lambda>t. a * f t)" (is ?P) |
|
1379 and "integral (\<lambda>t. a * f t) = a * integral f" (is ?I) |
|
1380 proof - |
|
1381 have "integrable (\<lambda>t. a * f t) \<and> integral (\<lambda>t. a * f t) = a * integral f" |
|
1382 proof (cases rule: le_cases) |
|
1383 assume "0 \<le> a" show ?thesis |
|
1384 using integral_linear[OF assms integral_zero(1) `0 \<le> a`] |
|
1385 by (simp add: integral_zero) |
|
1386 next |
|
1387 assume "a \<le> 0" hence "0 \<le> - a" by auto |
|
1388 have *: "\<And>t. - a * t + 0 = (-a) * t" by simp |
|
1389 show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`] |
|
1390 integral_minus(1)[of "\<lambda>t. - a * f t"] |
|
1391 unfolding * integral_zero by simp |
|
1392 qed |
|
1393 thus ?P ?I by auto |
|
1394 qed |
|
1395 |
|
1396 lemma (in measure_space) integral_mono: |
|
1397 assumes fg: "integrable f" "integrable g" |
|
1398 and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t" |
|
1399 shows "integral f \<le> integral g" |
|
1400 using fg unfolding integral_def integrable_def diff_minus |
|
1401 proof (safe intro!: add_mono real_of_pinfreal_mono le_imp_neg_le positive_integral_mono) |
|
1402 fix x assume "x \<in> space M" from mono[OF this] |
|
1403 show "Real (f x) \<le> Real (g x)" "Real (- g x) \<le> Real (- f x)" by auto |
|
1404 qed |
|
1405 |
|
1406 lemma (in measure_space) integral_diff[simp, intro]: |
|
1407 assumes f: "integrable f" and g: "integrable g" |
|
1408 shows "integrable (\<lambda>t. f t - g t)" |
|
1409 and "integral (\<lambda>t. f t - g t) = integral f - integral g" |
|
1410 using integral_add[OF f integral_minus(1)[OF g]] |
|
1411 unfolding diff_minus integral_minus(2)[OF g] |
|
1412 by auto |
|
1413 |
|
1414 lemma (in measure_space) integral_indicator[simp, intro]: |
|
1415 assumes "a \<in> sets M" and "\<mu> a \<noteq> \<omega>" |
|
1416 shows "integral (indicator a) = real (\<mu> a)" (is ?int) |
|
1417 and "integrable (indicator a)" (is ?able) |
|
1418 proof - |
|
1419 have *: |
|
1420 "\<And>A x. Real (indicator A x) = indicator A x" |
|
1421 "\<And>A x. Real (- indicator A x) = 0" unfolding indicator_def by auto |
|
1422 show ?int ?able |
|
1423 using assms unfolding integral_def integrable_def |
|
1424 by (auto simp: * positive_integral_indicator borel_measurable_indicator) |
|
1425 qed |
|
1426 |
|
1427 lemma (in measure_space) integral_cmul_indicator: |
|
1428 assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<omega>" |
|
1429 shows "integrable (\<lambda>x. c * indicator A x)" (is ?P) |
|
1430 and "integral (\<lambda>x. c * indicator A x) = c * real (\<mu> A)" (is ?I) |
|
1431 proof - |
|
1432 show ?P |
|
1433 proof (cases "c = 0") |
|
1434 case False with assms show ?thesis by simp |
|
1435 qed simp |
|
1436 |
|
1437 show ?I |
|
1438 proof (cases "c = 0") |
|
1439 case False with assms show ?thesis by simp |
|
1440 qed simp |
|
1441 qed |
|
1442 |
|
1443 lemma (in measure_space) integral_setsum[simp, intro]: |
|
1444 assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)" |
|
1445 shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S") |
|
1446 and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S") |
|
1447 proof - |
|
1448 have "?int S \<and> ?I S" |
|
1449 proof (cases "finite S") |
|
1450 assume "finite S" |
|
1451 from this assms show ?thesis by (induct S) simp_all |
|
1452 qed simp |
|
1453 thus "?int S" and "?I S" by auto |
|
1454 qed |
|
1455 |
|
1456 lemma (in measure_space) integrable_abs: |
|
1457 assumes "integrable f" |
|
1458 shows "integrable (\<lambda> x. \<bar>f x\<bar>)" |
|
1459 proof - |
|
1460 have *: |
|
1461 "\<And>x. Real \<bar>f x\<bar> = Real (f x) + Real (- f x)" |
|
1462 "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto |
|
1463 have abs: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" and |
|
1464 f: "(\<lambda>x. Real (f x)) \<in> borel_measurable M" |
|
1465 "(\<lambda>x. Real (- f x)) \<in> borel_measurable M" |
|
1466 using assms unfolding integrable_def by auto |
|
1467 from abs assms show ?thesis unfolding integrable_def * |
|
1468 using positive_integral_linear[OF f, of 1] by simp |
|
1469 qed |
|
1470 |
|
1471 lemma (in measure_space) integrable_bound: |
|
1472 assumes "integrable f" |
|
1473 and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
|
1474 "\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x" |
|
1475 assumes borel: "g \<in> borel_measurable M" |
|
1476 shows "integrable g" |
|
1477 proof - |
|
1478 have "positive_integral (\<lambda>x. Real (g x)) \<le> positive_integral (\<lambda>x. Real \<bar>g x\<bar>)" |
|
1479 by (auto intro!: positive_integral_mono) |
|
1480 also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))" |
|
1481 using f by (auto intro!: positive_integral_mono) |
|
1482 also have "\<dots> < \<omega>" |
|
1483 using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\<omega>) |
|
1484 finally have pos: "positive_integral (\<lambda>x. Real (g x)) < \<omega>" . |
|
1485 |
|
1486 have "positive_integral (\<lambda>x. Real (- g x)) \<le> positive_integral (\<lambda>x. Real (\<bar>g x\<bar>))" |
|
1487 by (auto intro!: positive_integral_mono) |
|
1488 also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))" |
|
1489 using f by (auto intro!: positive_integral_mono) |
|
1490 also have "\<dots> < \<omega>" |
|
1491 using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\<omega>) |
|
1492 finally have neg: "positive_integral (\<lambda>x. Real (- g x)) < \<omega>" . |
|
1493 |
|
1494 from neg pos borel show ?thesis |
|
1495 unfolding integrable_def by auto |
|
1496 qed |
|
1497 |
|
1498 lemma (in measure_space) integrable_abs_iff: |
|
1499 "f \<in> borel_measurable M \<Longrightarrow> integrable (\<lambda> x. \<bar>f x\<bar>) \<longleftrightarrow> integrable f" |
|
1500 by (auto intro!: integrable_bound[where g=f] integrable_abs) |
|
1501 |
|
1502 lemma (in measure_space) integrable_max: |
|
1503 assumes int: "integrable f" "integrable g" |
|
1504 shows "integrable (\<lambda> x. max (f x) (g x))" |
|
1505 proof (rule integrable_bound) |
|
1506 show "integrable (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)" |
|
1507 using int by (simp add: integrable_abs) |
|
1508 show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M" |
|
1509 using int unfolding integrable_def by auto |
|
1510 next |
|
1511 fix x assume "x \<in> space M" |
|
1512 show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" |
|
1513 by auto |
|
1514 qed |
|
1515 |
|
1516 lemma (in measure_space) integrable_min: |
|
1517 assumes int: "integrable f" "integrable g" |
|
1518 shows "integrable (\<lambda> x. min (f x) (g x))" |
|
1519 proof (rule integrable_bound) |
|
1520 show "integrable (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)" |
|
1521 using int by (simp add: integrable_abs) |
|
1522 show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M" |
|
1523 using int unfolding integrable_def by auto |
|
1524 next |
|
1525 fix x assume "x \<in> space M" |
|
1526 show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" |
|
1527 by auto |
|
1528 qed |
|
1529 |
|
1530 lemma (in measure_space) integral_triangle_inequality: |
|
1531 assumes "integrable f" |
|
1532 shows "\<bar>integral f\<bar> \<le> integral (\<lambda>x. \<bar>f x\<bar>)" |
|
1533 proof - |
|
1534 have "\<bar>integral f\<bar> = max (integral f) (- integral f)" by auto |
|
1535 also have "\<dots> \<le> integral (\<lambda>x. \<bar>f x\<bar>)" |
|
1536 using assms integral_minus(2)[of f, symmetric] |
|
1537 by (auto intro!: integral_mono integrable_abs simp del: integral_minus) |
|
1538 finally show ?thesis . |
|
1539 qed |
|
1540 |
|
1541 lemma (in measure_space) integral_positive: |
|
1542 assumes "integrable f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
|
1543 shows "0 \<le> integral f" |
|
1544 proof - |
|
1545 have "0 = integral (\<lambda>x. 0)" by (auto simp: integral_zero) |
|
1546 also have "\<dots> \<le> integral f" |
|
1547 using assms by (rule integral_mono[OF integral_zero(1)]) |
|
1548 finally show ?thesis . |
|
1549 qed |
|
1550 |
|
1551 lemma (in measure_space) integral_monotone_convergence_pos: |
|
1552 assumes i: "\<And>i. integrable (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)" |
|
1553 and pos: "\<And>x i. 0 \<le> f i x" |
|
1554 and lim: "\<And>x. (\<lambda>i. f i x) ----> u x" |
|
1555 and ilim: "(\<lambda>i. integral (f i)) ----> x" |
|
1556 shows "integrable u" |
|
1557 and "integral u = x" |
|
1558 proof - |
|
1559 { fix x have "0 \<le> u x" |
|
1560 using mono pos[of 0 x] incseq_le[OF _ lim, of x 0] |
|
1561 by (simp add: mono_def incseq_def) } |
|
1562 note pos_u = this |
|
1563 |
|
1564 hence [simp]: "\<And>i x. Real (- f i x) = 0" "\<And>x. Real (- u x) = 0" |
|
1565 using pos by auto |
|
1566 |
|
1567 have SUP_F: "\<And>x. (SUP n. Real (f n x)) = Real (u x)" |
|
1568 using mono pos pos_u lim by (rule SUP_eq_LIMSEQ[THEN iffD2]) |
|
1569 |
|
1570 have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M" |
|
1571 using i unfolding integrable_def by auto |
|
1572 hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M" |
|
1573 by auto |
|
1574 hence borel_u: "u \<in> borel_measurable M" |
|
1575 using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F) |
|
1576 |
|
1577 have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))" |
|
1578 using i unfolding integral_def integrable_def by (auto simp: Real_real) |
|
1579 |
|
1580 have pos_integral: "\<And>n. 0 \<le> integral (f n)" |
|
1581 using pos i by (auto simp: integral_positive) |
|
1582 hence "0 \<le> x" |
|
1583 using LIMSEQ_le_const[OF ilim, of 0] by auto |
|
1584 |
|
1585 have "(\<lambda>i. positive_integral (\<lambda>x. Real (f i x))) \<up> positive_integral (\<lambda>x. Real (u x))" |
|
1586 proof (rule positive_integral_isoton) |
|
1587 from SUP_F mono pos |
|
1588 show "(\<lambda>i x. Real (f i x)) \<up> (\<lambda>x. Real (u x))" |
|
1589 unfolding isoton_fun_expand by (auto simp: isoton_def mono_def) |
|
1590 qed (rule borel_f) |
|
1591 hence pI: "positive_integral (\<lambda>x. Real (u x)) = |
|
1592 (SUP n. positive_integral (\<lambda>x. Real (f n x)))" |
|
1593 unfolding isoton_def by simp |
|
1594 also have "\<dots> = Real x" unfolding integral_eq |
|
1595 proof (rule SUP_eq_LIMSEQ[THEN iffD2]) |
|
1596 show "mono (\<lambda>n. integral (f n))" |
|
1597 using mono i by (auto simp: mono_def intro!: integral_mono) |
|
1598 show "\<And>n. 0 \<le> integral (f n)" using pos_integral . |
|
1599 show "0 \<le> x" using `0 \<le> x` . |
|
1600 show "(\<lambda>n. integral (f n)) ----> x" using ilim . |
|
1601 qed |
|
1602 finally show "integrable u" "integral u = x" using borel_u `0 \<le> x` |
|
1603 unfolding integrable_def integral_def by auto |
|
1604 qed |
|
1605 |
|
1606 lemma (in measure_space) integral_monotone_convergence: |
|
1607 assumes f: "\<And>i. integrable (f i)" and "mono f" |
|
1608 and lim: "\<And>x. (\<lambda>i. f i x) ----> u x" |
|
1609 and ilim: "(\<lambda>i. integral (f i)) ----> x" |
|
1610 shows "integrable u" |
|
1611 and "integral u = x" |
|
1612 proof - |
|
1613 have 1: "\<And>i. integrable (\<lambda>x. f i x - f 0 x)" |
|
1614 using f by (auto intro!: integral_diff) |
|
1615 have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f` |
|
1616 unfolding mono_def le_fun_def by auto |
|
1617 have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f` |
|
1618 unfolding mono_def le_fun_def by (auto simp: field_simps) |
|
1619 have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x" |
|
1620 using lim by (auto intro!: LIMSEQ_diff) |
|
1621 have 5: "(\<lambda>i. integral (\<lambda>x. f i x - f 0 x)) ----> x - integral (f 0)" |
|
1622 using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff) |
|
1623 note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5] |
|
1624 have "integrable (\<lambda>x. (u x - f 0 x) + f 0 x)" |
|
1625 using diff(1) f by (rule integral_add(1)) |
|
1626 with diff(2) f show "integrable u" "integral u = x" |
|
1627 by (auto simp: integral_diff) |
|
1628 qed |
|
1629 |
|
1630 lemma (in measure_space) integral_0_iff: |
|
1631 assumes "integrable f" |
|
1632 shows "integral (\<lambda>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0" |
|
1633 proof - |
|
1634 have *: "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto |
|
1635 have "integrable (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs) |
|
1636 hence "(\<lambda>x. Real (\<bar>f x\<bar>)) \<in> borel_measurable M" |
|
1637 "positive_integral (\<lambda>x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto |
|
1638 from positive_integral_0_iff[OF this(1)] this(2) |
|
1639 show ?thesis unfolding integral_def * |
|
1640 by (simp add: real_of_pinfreal_eq_0) |
|
1641 qed |
|
1642 |
|
1643 lemma LIMSEQ_max: |
|
1644 "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0" |
|
1645 by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D) |
|
1646 |
|
1647 lemma (in sigma_algebra) borel_measurable_LIMSEQ: |
|
1648 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real" |
|
1649 assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x" |
|
1650 and u: "\<And>i. u i \<in> borel_measurable M" |
|
1651 shows "u' \<in> borel_measurable M" |
|
1652 proof - |
|
1653 let "?pu x i" = "max (u i x) 0" |
|
1654 let "?nu x i" = "max (- u i x) 0" |
|
1655 |
|
1656 { fix x assume x: "x \<in> space M" |
|
1657 have "(?pu x) ----> max (u' x) 0" |
|
1658 "(?nu x) ----> max (- u' x) 0" |
|
1659 using u'[OF x] by (auto intro!: LIMSEQ_max LIMSEQ_minus) |
|
1660 from LIMSEQ_imp_lim_INF[OF _ this(1)] LIMSEQ_imp_lim_INF[OF _ this(2)] |
|
1661 have "(SUP n. INF m. Real (u (n + m) x)) = Real (u' x)" |
|
1662 "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)" |
|
1663 by (simp_all add: Real_max'[symmetric]) } |
|
1664 note eq = this |
|
1665 |
|
1666 have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x" |
|
1667 by auto |
|
1668 |
|
1669 have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M" |
|
1670 "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M" |
|
1671 using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) |
|
1672 with eq[THEN measurable_cong, of M "\<lambda>x. x" borel_space] |
|
1673 have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M" |
|
1674 "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" |
|
1675 unfolding SUPR_fun_expand INFI_fun_expand by auto |
|
1676 note this[THEN borel_measurable_real] |
|
1677 from borel_measurable_diff[OF this] |
|
1678 show ?thesis unfolding * . |
|
1679 qed |
|
1680 |
|
1681 lemma (in measure_space) integral_dominated_convergence: |
|
1682 assumes u: "\<And>i. integrable (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x" |
|
1683 and w: "integrable w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x" |
|
1684 and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x" |
|
1685 shows "integrable u'" |
|
1686 and "(\<lambda>i. integral (\<lambda>x. \<bar>u i x - u' x\<bar>)) ----> 0" (is "?lim_diff") |
|
1687 and "(\<lambda>i. integral (u i)) ----> integral u'" (is ?lim) |
|
1688 proof - |
|
1689 { fix x j assume x: "x \<in> space M" |
|
1690 from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs) |
|
1691 from LIMSEQ_le_const2[OF this] |
|
1692 have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto } |
|
1693 note u'_bound = this |
|
1694 |
|
1695 from u[unfolded integrable_def] |
|
1696 have u'_borel: "u' \<in> borel_measurable M" |
|
1697 using u' by (blast intro: borel_measurable_LIMSEQ[of u]) |
|
1698 |
|
1699 show "integrable u'" |
|
1700 proof (rule integrable_bound) |
|
1701 show "integrable w" by fact |
|
1702 show "u' \<in> borel_measurable M" by fact |
|
1703 next |
|
1704 fix x assume x: "x \<in> space M" |
|
1705 thus "0 \<le> w x" by fact |
|
1706 show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] . |
|
1707 qed |
|
1708 |
|
1709 let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>" |
|
1710 have diff: "\<And>n. integrable (\<lambda>x. \<bar>u n x - u' x\<bar>)" |
|
1711 using w u `integrable u'` |
|
1712 by (auto intro!: integral_add integral_diff integral_cmult integrable_abs) |
|
1713 |
|
1714 { fix j x assume x: "x \<in> space M" |
|
1715 have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto |
|
1716 also have "\<dots> \<le> w x + w x" |
|
1717 by (rule add_mono[OF bound[OF x] u'_bound[OF x]]) |
|
1718 finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp } |
|
1719 note diff_less_2w = this |
|
1720 |
|
1721 have PI_diff: "\<And>m n. positive_integral (\<lambda>x. Real (?diff (m + n) x)) = |
|
1722 positive_integral (\<lambda>x. Real (2 * w x)) - positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)" |
|
1723 using diff w diff_less_2w |
|
1724 by (subst positive_integral_diff[symmetric]) |
|
1725 (auto simp: integrable_def intro!: positive_integral_cong) |
|
1726 |
|
1727 have "integrable (\<lambda>x. 2 * w x)" |
|
1728 using w by (auto intro: integral_cmult) |
|
1729 hence I2w_fin: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> \<omega>" and |
|
1730 borel_2w: "(\<lambda>x. Real (2 * w x)) \<in> borel_measurable M" |
|
1731 unfolding integrable_def by auto |
|
1732 |
|
1733 have "(INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) = 0" (is "?lim_SUP = 0") |
|
1734 proof cases |
|
1735 assume eq_0: "positive_integral (\<lambda>x. Real (2 * w x)) = 0" |
|
1736 have "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) \<le> positive_integral (\<lambda>x. Real (2 * w x))" |
|
1737 proof (rule positive_integral_mono) |
|
1738 fix i x assume "x \<in> space M" from diff_less_2w[OF this, of i] |
|
1739 show "Real \<bar>u i x - u' x\<bar> \<le> Real (2 * w x)" by auto |
|
1740 qed |
|
1741 hence "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) = 0" using eq_0 by auto |
|
1742 thus ?thesis by simp |
|
1743 next |
|
1744 assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0" |
|
1745 have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))" |
|
1746 proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute) |
|
1747 fix x assume x: "x \<in> space M" |
|
1748 show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))" |
|
1749 proof (rule LIMSEQ_imp_lim_INF[symmetric]) |
|
1750 fix j show "0 \<le> ?diff j x" using diff_less_2w[OF x, of j] by simp |
|
1751 next |
|
1752 have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>" |
|
1753 using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs) |
|
1754 thus "(\<lambda>i. ?diff i x) ----> 2 * w x" by simp |
|
1755 qed |
|
1756 qed |
|
1757 also have "\<dots> \<le> (SUP n. INF m. positive_integral (\<lambda>x. Real (?diff (m + n) x)))" |
|
1758 using u'_borel w u unfolding integrable_def |
|
1759 by (auto intro!: positive_integral_lim_INF) |
|
1760 also have "\<dots> = positive_integral (\<lambda>x. Real (2 * w x)) - |
|
1761 (INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>))" |
|
1762 unfolding PI_diff pinfreal_INF_minus[OF I2w_fin] pinfreal_SUP_minus .. |
|
1763 finally show ?thesis using neq_0 I2w_fin by (rule pinfreal_le_minus_imp_0) |
|
1764 qed |
|
1765 |
|
1766 have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto |
|
1767 |
|
1768 have [simp]: "\<And>n m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>) = |
|
1769 Real (integral (\<lambda>x. \<bar>u (n + m) x - u' x\<bar>))" |
|
1770 using diff by (subst add_commute) (simp add: integral_def integrable_def Real_real) |
|
1771 |
|
1772 have "(SUP n. INF m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) \<le> ?lim_SUP" |
|
1773 (is "?lim_INF \<le> _") by (subst (1 2) add_commute) (rule lim_INF_le_lim_SUP) |
|
1774 hence "?lim_INF = Real 0" "?lim_SUP = Real 0" using `?lim_SUP = 0` by auto |
|
1775 thus ?lim_diff using diff by (auto intro!: integral_positive lim_INF_eq_lim_SUP) |
|
1776 |
|
1777 show ?lim |
|
1778 proof (rule LIMSEQ_I) |
|
1779 fix r :: real assume "0 < r" |
|
1780 from LIMSEQ_D[OF `?lim_diff` this] |
|
1781 obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> integral (\<lambda>x. \<bar>u n x - u' x\<bar>) < r" |
|
1782 using diff by (auto simp: integral_positive) |
|
1783 |
|
1784 show "\<exists>N. \<forall>n\<ge>N. norm (integral (u n) - integral u') < r" |
|
1785 proof (safe intro!: exI[of _ N]) |
|
1786 fix n assume "N \<le> n" |
|
1787 have "\<bar>integral (u n) - integral u'\<bar> = \<bar>integral (\<lambda>x. u n x - u' x)\<bar>" |
|
1788 using u `integrable u'` by (auto simp: integral_diff) |
|
1789 also have "\<dots> \<le> integral (\<lambda>x. \<bar>u n x - u' x\<bar>)" using u `integrable u'` |
|
1790 by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff) |
|
1791 also note N[OF `N \<le> n`] |
|
1792 finally show "norm (integral (u n) - integral u') < r" by simp |
|
1793 qed |
|
1794 qed |
|
1795 qed |
|
1796 |
|
1797 lemma (in measure_space) integral_sums: |
|
1798 assumes borel: "\<And>i. integrable (f i)" |
|
1799 and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)" |
|
1800 and sums: "summable (\<lambda>i. integral (\<lambda>x. \<bar>f i x\<bar>))" |
|
1801 shows "integrable (\<lambda>x. (\<Sum>i. f i x))" (is "integrable ?S") |
|
1802 and "(\<lambda>i. integral (f i)) sums integral (\<lambda>x. (\<Sum>i. f i x))" (is ?integral) |
|
1803 proof - |
|
1804 have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w" |
|
1805 using summable unfolding summable_def by auto |
|
1806 from bchoice[OF this] |
|
1807 obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto |
|
1808 |
|
1809 let "?w y" = "if y \<in> space M then w y else 0" |
|
1810 |
|
1811 obtain x where abs_sum: "(\<lambda>i. integral (\<lambda>x. \<bar>f i x\<bar>)) sums x" |
|
1812 using sums unfolding summable_def .. |
|
1813 |
|
1814 have 1: "\<And>n. integrable (\<lambda>x. \<Sum>i = 0..<n. f i x)" |
|
1815 using borel by (auto intro!: integral_setsum) |
|
1816 |
|
1817 { fix j x assume [simp]: "x \<in> space M" |
|
1818 have "\<bar>\<Sum>i = 0..< j. f i x\<bar> \<le> (\<Sum>i = 0..< j. \<bar>f i x\<bar>)" by (rule setsum_abs) |
|
1819 also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto |
|
1820 finally have "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp } |
|
1821 note 2 = this |
|
1822 |
|
1823 have 3: "integrable ?w" |
|
1824 proof (rule integral_monotone_convergence(1)) |
|
1825 let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)" |
|
1826 let "?w' n y" = "if y \<in> space M then ?F n y else 0" |
|
1827 have "\<And>n. integrable (?F n)" |
|
1828 using borel by (auto intro!: integral_setsum integrable_abs) |
|
1829 thus "\<And>n. integrable (?w' n)" by (simp cong: integrable_cong) |
|
1830 show "mono ?w'" |
|
1831 by (auto simp: mono_def le_fun_def intro!: setsum_mono2) |
|
1832 { fix x show "(\<lambda>n. ?w' n x) ----> ?w x" |
|
1833 using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) } |
|
1834 have *: "\<And>n. integral (?w' n) = (\<Sum>i = 0..< n. integral (\<lambda>x. \<bar>f i x\<bar>))" |
|
1835 using borel by (simp add: integral_setsum integrable_abs cong: integral_cong) |
|
1836 from abs_sum |
|
1837 show "(\<lambda>i. integral (?w' i)) ----> x" unfolding * sums_def . |
|
1838 qed |
|
1839 |
|
1840 have 4: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> ?w x" using 2[of _ 0] by simp |
|
1841 |
|
1842 from summable[THEN summable_rabs_cancel] |
|
1843 have 5: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)" |
|
1844 by (auto intro: summable_sumr_LIMSEQ_suminf) |
|
1845 |
|
1846 note int = integral_dominated_convergence(1,3)[OF 1 2 3 4 5] |
|
1847 |
|
1848 from int show "integrable ?S" by simp |
|
1849 |
|
1850 show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel] |
|
1851 using int(2) by simp |
|
1852 qed |
|
1853 |
|
1854 section "Lebesgue integration on countable spaces" |
|
1855 |
|
1856 lemma (in measure_space) integral_on_countable: |
|
1857 assumes f: "f \<in> borel_measurable M" |
|
1858 and bij: "bij_betw enum S (f ` space M)" |
|
1859 and enum_zero: "enum ` (-S) \<subseteq> {0}" |
|
1860 and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>" |
|
1861 and abs_summable: "summable (\<lambda>r. \<bar>enum r * real (\<mu> (f -` {enum r} \<inter> space M))\<bar>)" |
|
1862 shows "integrable f" |
|
1863 and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral f" (is ?sums) |
|
1864 proof - |
|
1865 let "?A r" = "f -` {enum r} \<inter> space M" |
|
1866 let "?F r x" = "enum r * indicator (?A r) x" |
|
1867 have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral (?F r)" |
|
1868 using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
|
1869 |
|
1870 { fix x assume "x \<in> space M" |
|
1871 hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto |
|
1872 then obtain i where "i\<in>S" "enum i = f x" by auto |
|
1873 have F: "\<And>j. ?F j x = (if j = i then f x else 0)" |
|
1874 proof cases |
|
1875 fix j assume "j = i" |
|
1876 thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def) |
|
1877 next |
|
1878 fix j assume "j \<noteq> i" |
|
1879 show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero |
|
1880 by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def) |
|
1881 qed |
|
1882 hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto |
|
1883 have "(\<lambda>i. ?F i x) sums f x" |
|
1884 "(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>" |
|
1885 by (auto intro!: sums_single simp: F F_abs) } |
|
1886 note F_sums_f = this(1) and F_abs_sums_f = this(2) |
|
1887 |
|
1888 have int_f: "integral f = integral (\<lambda>x. \<Sum>r. ?F r x)" "integrable f = integrable (\<lambda>x. \<Sum>r. ?F r x)" |
|
1889 using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff) |
|
1890 |
|
1891 { fix r |
|
1892 have "integral (\<lambda>x. \<bar>?F r x\<bar>) = integral (\<lambda>x. \<bar>enum r\<bar> * indicator (?A r) x)" |
|
1893 by (auto simp: indicator_def intro!: integral_cong) |
|
1894 also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))" |
|
1895 using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
|
1896 finally have "integral (\<lambda>x. \<bar>?F r x\<bar>) = \<bar>enum r * real (\<mu> (?A r))\<bar>" |
|
1897 by (simp add: abs_mult_pos real_pinfreal_pos) } |
|
1898 note int_abs_F = this |
|
1899 |
|
1900 have 1: "\<And>i. integrable (\<lambda>x. ?F i x)" |
|
1901 using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
|
1902 |
|
1903 have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)" |
|
1904 using F_abs_sums_f unfolding sums_iff by auto |
|
1905 |
|
1906 from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] |
|
1907 show ?sums unfolding enum_eq int_f by simp |
|
1908 |
|
1909 from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] |
|
1910 show "integrable f" unfolding int_f by simp |
|
1911 qed |
|
1912 |
|
1913 section "Lebesgue integration on finite space" |
|
1914 |
|
1915 lemma (in measure_space) integral_on_finite: |
|
1916 assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)" |
|
1917 and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>" |
|
1918 shows "integrable f" |
|
1919 and "integral (\<lambda>x. f x) = |
|
1920 (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral") |
|
1921 proof - |
|
1922 let "?A r" = "f -` {r} \<inter> space M" |
|
1923 let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x" |
|
1924 |
|
1925 { fix x assume "x \<in> space M" |
|
1926 have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)" |
|
1927 using finite `x \<in> space M` by (simp add: setsum_cases) |
|
1928 also have "\<dots> = ?S x" |
|
1929 by (auto intro!: setsum_cong) |
|
1930 finally have "f x = ?S x" . } |
|
1931 note f_eq = this |
|
1932 |
|
1933 have f_eq_S: "integrable f \<longleftrightarrow> integrable ?S" "integral f = integral ?S" |
|
1934 by (auto intro!: integrable_cong integral_cong simp only: f_eq) |
|
1935 |
|
1936 show "integrable f" ?integral using fin f f_eq_S |
|
1937 by (simp_all add: integral_cmul_indicator borel_measurable_vimage) |
|
1938 qed |
|
1939 |
|
1940 lemma sigma_algebra_cong: |
|
1941 fixes M :: "('a, 'b) algebra_scheme" and M' :: "('a, 'c) algebra_scheme" |
|
1942 assumes *: "sigma_algebra M" |
|
1943 and cong: "space M = space M'" "sets M = sets M'" |
|
1944 shows "sigma_algebra M'" |
|
1945 using * unfolding sigma_algebra_def algebra_def sigma_algebra_axioms_def unfolding cong . |
|
1946 |
|
1947 lemma finite_Pow_additivity_sufficient: |
|
1948 assumes "finite (space M)" and "sets M = Pow (space M)" |
|
1949 and "positive \<mu>" and "additive M \<mu>" |
|
1950 and "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<omega>" |
|
1951 shows "finite_measure_space M \<mu>" |
|
1952 proof - |
|
1953 have "sigma_algebra M" |
|
1954 using assms by (auto intro!: sigma_algebra_cong[OF sigma_algebra_Pow]) |
|
1955 |
|
1956 have "measure_space M \<mu>" |
|
1957 by (rule sigma_algebra.finite_additivity_sufficient) (fact+) |
|
1958 thus ?thesis |
|
1959 unfolding finite_measure_space_def finite_measure_space_axioms_def |
|
1960 using assms by simp |
|
1961 qed |
|
1962 |
|
1963 lemma finite_measure_spaceI: |
|
1964 assumes "measure_space M \<mu>" and "finite (space M)" and "sets M = Pow (space M)" |
|
1965 and "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<omega>" |
|
1966 shows "finite_measure_space M \<mu>" |
|
1967 unfolding finite_measure_space_def finite_measure_space_axioms_def |
|
1968 using assms by simp |
|
1969 |
|
1970 lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: |
|
1971 fixes f :: "'a \<Rightarrow> real" |
|
1972 shows "f \<in> borel_measurable M" |
|
1973 unfolding measurable_def sets_eq_Pow by auto |
|
1974 |
|
1975 lemma (in finite_measure_space) integral_finite_singleton: |
|
1976 shows "integrable f" |
|
1977 and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I) |
|
1978 proof - |
|
1979 have 1: "f \<in> borel_measurable M" |
|
1980 unfolding measurable_def sets_eq_Pow by auto |
|
1981 |
|
1982 have 2: "finite (f`space M)" using finite_space by simp |
|
1983 |
|
1984 have 3: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>" |
|
1985 using finite_measure[unfolded sets_eq_Pow] by simp |
|
1986 |
|
1987 show "integrable f" |
|
1988 by (rule integral_on_finite(1)[OF 1 2 3]) simp |
|
1989 |
|
1990 { fix r let ?x = "f -` {r} \<inter> space M" |
|
1991 have "?x \<subseteq> space M" by auto |
|
1992 with finite_space sets_eq_Pow finite_single_measure |
|
1993 have "real (\<mu> ?x) = (\<Sum>i \<in> ?x. real (\<mu> {i}))" |
|
1994 using real_measure_setsum_singleton[of ?x] by auto } |
|
1995 note measure_eq_setsum = this |
|
1996 |
|
1997 have "integral f = (\<Sum>r\<in>f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" |
|
1998 by (rule integral_on_finite(2)[OF 1 2 3]) simp |
|
1999 also have "\<dots> = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" |
|
2000 unfolding measure_eq_setsum setsum_right_distrib |
|
2001 apply (subst setsum_Sigma) |
|
2002 apply (simp add: finite_space) |
|
2003 apply (simp add: finite_space) |
|
2004 proof (rule setsum_reindex_cong[symmetric]) |
|
2005 fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)" |
|
2006 thus "(\<lambda>(x, y). x * real (\<mu> {y})) a = f (snd a) * real (\<mu> {snd a})" |
|
2007 by auto |
|
2008 qed (auto intro!: image_eqI inj_onI) |
|
2009 finally show ?I . |
|
2010 qed |
|
2011 |
|
2012 end |