1 (* Title: HOL/Probability/Nonnegative_Lebesgue_Integration.thy |
|
2 Author: Johannes Hölzl, TU München |
|
3 Author: Armin Heller, TU München |
|
4 *) |
|
5 |
|
6 section \<open>Lebesgue Integration for Nonnegative Functions\<close> |
|
7 |
|
8 theory Nonnegative_Lebesgue_Integration |
|
9 imports Measure_Space Borel_Space |
|
10 begin |
|
11 |
|
12 subsection "Simple function" |
|
13 |
|
14 text \<open> |
|
15 |
|
16 Our simple functions are not restricted to nonnegative real numbers. Instead |
|
17 they are just functions with a finite range and are measurable when singleton |
|
18 sets are measurable. |
|
19 |
|
20 \<close> |
|
21 |
|
22 definition "simple_function M g \<longleftrightarrow> |
|
23 finite (g ` space M) \<and> |
|
24 (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)" |
|
25 |
|
26 lemma simple_functionD: |
|
27 assumes "simple_function M g" |
|
28 shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M" |
|
29 proof - |
|
30 show "finite (g ` space M)" |
|
31 using assms unfolding simple_function_def by auto |
|
32 have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto |
|
33 also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto |
|
34 finally show "g -` X \<inter> space M \<in> sets M" using assms |
|
35 by (auto simp del: UN_simps simp: simple_function_def) |
|
36 qed |
|
37 |
|
38 lemma measurable_simple_function[measurable_dest]: |
|
39 "simple_function M f \<Longrightarrow> f \<in> measurable M (count_space UNIV)" |
|
40 unfolding simple_function_def measurable_def |
|
41 proof safe |
|
42 fix A assume "finite (f ` space M)" "\<forall>x\<in>f ` space M. f -` {x} \<inter> space M \<in> sets M" |
|
43 then have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) \<in> sets M" |
|
44 by (intro sets.finite_UN) auto |
|
45 also have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) = f -` A \<inter> space M" |
|
46 by (auto split: if_split_asm) |
|
47 finally show "f -` A \<inter> space M \<in> sets M" . |
|
48 qed simp |
|
49 |
|
50 lemma borel_measurable_simple_function: |
|
51 "simple_function M f \<Longrightarrow> f \<in> borel_measurable M" |
|
52 by (auto dest!: measurable_simple_function simp: measurable_def) |
|
53 |
|
54 lemma simple_function_measurable2[intro]: |
|
55 assumes "simple_function M f" "simple_function M g" |
|
56 shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M" |
|
57 proof - |
|
58 have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)" |
|
59 by auto |
|
60 then show ?thesis using assms[THEN simple_functionD(2)] by auto |
|
61 qed |
|
62 |
|
63 lemma simple_function_indicator_representation: |
|
64 fixes f ::"'a \<Rightarrow> ennreal" |
|
65 assumes f: "simple_function M f" and x: "x \<in> space M" |
|
66 shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)" |
|
67 (is "?l = ?r") |
|
68 proof - |
|
69 have "?r = (\<Sum>y \<in> f ` space M. |
|
70 (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))" |
|
71 by (auto intro!: setsum.cong) |
|
72 also have "... = f x * indicator (f -` {f x} \<inter> space M) x" |
|
73 using assms by (auto dest: simple_functionD simp: setsum.delta) |
|
74 also have "... = f x" using x by (auto simp: indicator_def) |
|
75 finally show ?thesis by auto |
|
76 qed |
|
77 |
|
78 lemma simple_function_notspace: |
|
79 "simple_function M (\<lambda>x. h x * indicator (- space M) x::ennreal)" (is "simple_function M ?h") |
|
80 proof - |
|
81 have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto |
|
82 hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) |
|
83 have "?h -` {0} \<inter> space M = space M" by auto |
|
84 thus ?thesis unfolding simple_function_def by auto |
|
85 qed |
|
86 |
|
87 lemma simple_function_cong: |
|
88 assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
89 shows "simple_function M f \<longleftrightarrow> simple_function M g" |
|
90 proof - |
|
91 have "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
92 using assms by auto |
|
93 with assms show ?thesis |
|
94 by (simp add: simple_function_def cong: image_cong) |
|
95 qed |
|
96 |
|
97 lemma simple_function_cong_algebra: |
|
98 assumes "sets N = sets M" "space N = space M" |
|
99 shows "simple_function M f \<longleftrightarrow> simple_function N f" |
|
100 unfolding simple_function_def assms .. |
|
101 |
|
102 lemma simple_function_borel_measurable: |
|
103 fixes f :: "'a \<Rightarrow> 'x::{t2_space}" |
|
104 assumes "f \<in> borel_measurable M" and "finite (f ` space M)" |
|
105 shows "simple_function M f" |
|
106 using assms unfolding simple_function_def |
|
107 by (auto intro: borel_measurable_vimage) |
|
108 |
|
109 lemma simple_function_iff_borel_measurable: |
|
110 fixes f :: "'a \<Rightarrow> 'x::{t2_space}" |
|
111 shows "simple_function M f \<longleftrightarrow> finite (f ` space M) \<and> f \<in> borel_measurable M" |
|
112 by (metis borel_measurable_simple_function simple_functionD(1) simple_function_borel_measurable) |
|
113 |
|
114 lemma simple_function_eq_measurable: |
|
115 "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> measurable M (count_space UNIV)" |
|
116 using measurable_simple_function[of M f] by (fastforce simp: simple_function_def) |
|
117 |
|
118 lemma simple_function_const[intro, simp]: |
|
119 "simple_function M (\<lambda>x. c)" |
|
120 by (auto intro: finite_subset simp: simple_function_def) |
|
121 lemma simple_function_compose[intro, simp]: |
|
122 assumes "simple_function M f" |
|
123 shows "simple_function M (g \<circ> f)" |
|
124 unfolding simple_function_def |
|
125 proof safe |
|
126 show "finite ((g \<circ> f) ` space M)" |
|
127 using assms unfolding simple_function_def by (auto simp: image_comp [symmetric]) |
|
128 next |
|
129 fix x assume "x \<in> space M" |
|
130 let ?G = "g -` {g (f x)} \<inter> (f`space M)" |
|
131 have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M = |
|
132 (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto |
|
133 show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M" |
|
134 using assms unfolding simple_function_def * |
|
135 by (rule_tac sets.finite_UN) auto |
|
136 qed |
|
137 |
|
138 lemma simple_function_indicator[intro, simp]: |
|
139 assumes "A \<in> sets M" |
|
140 shows "simple_function M (indicator A)" |
|
141 proof - |
|
142 have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _") |
|
143 by (auto simp: indicator_def) |
|
144 hence "finite ?S" by (rule finite_subset) simp |
|
145 moreover have "- A \<inter> space M = space M - A" by auto |
|
146 ultimately show ?thesis unfolding simple_function_def |
|
147 using assms by (auto simp: indicator_def [abs_def]) |
|
148 qed |
|
149 |
|
150 lemma simple_function_Pair[intro, simp]: |
|
151 assumes "simple_function M f" |
|
152 assumes "simple_function M g" |
|
153 shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p") |
|
154 unfolding simple_function_def |
|
155 proof safe |
|
156 show "finite (?p ` space M)" |
|
157 using assms unfolding simple_function_def |
|
158 by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto |
|
159 next |
|
160 fix x assume "x \<in> space M" |
|
161 have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = |
|
162 (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" |
|
163 by auto |
|
164 with \<open>x \<in> space M\<close> show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M" |
|
165 using assms unfolding simple_function_def by auto |
|
166 qed |
|
167 |
|
168 lemma simple_function_compose1: |
|
169 assumes "simple_function M f" |
|
170 shows "simple_function M (\<lambda>x. g (f x))" |
|
171 using simple_function_compose[OF assms, of g] |
|
172 by (simp add: comp_def) |
|
173 |
|
174 lemma simple_function_compose2: |
|
175 assumes "simple_function M f" and "simple_function M g" |
|
176 shows "simple_function M (\<lambda>x. h (f x) (g x))" |
|
177 proof - |
|
178 have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))" |
|
179 using assms by auto |
|
180 thus ?thesis by (simp_all add: comp_def) |
|
181 qed |
|
182 |
|
183 lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] |
|
184 and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] |
|
185 and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] |
|
186 and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] |
|
187 and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] |
|
188 and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] |
|
189 and simple_function_max[intro, simp] = simple_function_compose2[where h=max] |
|
190 |
|
191 lemma simple_function_setsum[intro, simp]: |
|
192 assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)" |
|
193 shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)" |
|
194 proof cases |
|
195 assume "finite P" from this assms show ?thesis by induct auto |
|
196 qed auto |
|
197 |
|
198 lemma simple_function_ennreal[intro, simp]: |
|
199 fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f" |
|
200 shows "simple_function M (\<lambda>x. ennreal (f x))" |
|
201 by (rule simple_function_compose1[OF sf]) |
|
202 |
|
203 lemma simple_function_real_of_nat[intro, simp]: |
|
204 fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f" |
|
205 shows "simple_function M (\<lambda>x. real (f x))" |
|
206 by (rule simple_function_compose1[OF sf]) |
|
207 |
|
208 lemma borel_measurable_implies_simple_function_sequence: |
|
209 fixes u :: "'a \<Rightarrow> ennreal" |
|
210 assumes u[measurable]: "u \<in> borel_measurable M" |
|
211 shows "\<exists>f. incseq f \<and> (\<forall>i. (\<forall>x. f i x < top) \<and> simple_function M (f i)) \<and> u = (SUP i. f i)" |
|
212 proof - |
|
213 define f where [abs_def]: |
|
214 "f i x = real_of_int (floor (enn2real (min i (u x)) * 2^i)) / 2^i" for i x |
|
215 |
|
216 have [simp]: "0 \<le> f i x" for i x |
|
217 by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg enn2real_nonneg) |
|
218 |
|
219 have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x |
|
220 by simp |
|
221 |
|
222 have "real_of_int \<lfloor>real i * 2 ^ i\<rfloor> = real_of_int \<lfloor>i * 2 ^ i\<rfloor>" for i |
|
223 by (intro arg_cong[where f=real_of_int]) simp |
|
224 then have [simp]: "real_of_int \<lfloor>real i * 2 ^ i\<rfloor> = i * 2 ^ i" for i |
|
225 unfolding floor_of_nat by simp |
|
226 |
|
227 have "incseq f" |
|
228 proof (intro monoI le_funI) |
|
229 fix m n :: nat and x assume "m \<le> n" |
|
230 moreover |
|
231 { fix d :: nat |
|
232 have "\<lfloor>2^d::real\<rfloor> * \<lfloor>2^m * enn2real (min (of_nat m) (u x))\<rfloor> \<le> |
|
233 \<lfloor>2^d * (2^m * enn2real (min (of_nat m) (u x)))\<rfloor>" |
|
234 by (rule le_mult_floor) (auto simp: enn2real_nonneg) |
|
235 also have "\<dots> \<le> \<lfloor>2^d * (2^m * enn2real (min (of_nat d + of_nat m) (u x)))\<rfloor>" |
|
236 by (intro floor_mono mult_mono enn2real_mono min.mono) |
|
237 (auto simp: enn2real_nonneg min_less_iff_disj of_nat_less_top) |
|
238 finally have "f m x \<le> f (m + d) x" |
|
239 unfolding f_def |
|
240 by (auto simp: field_simps power_add * simp del: of_int_mult) } |
|
241 ultimately show "f m x \<le> f n x" |
|
242 by (auto simp add: le_iff_add) |
|
243 qed |
|
244 then have inc_f: "incseq (\<lambda>i. ennreal (f i x))" for x |
|
245 by (auto simp: incseq_def le_fun_def) |
|
246 then have "incseq (\<lambda>i x. ennreal (f i x))" |
|
247 by (auto simp: incseq_def le_fun_def) |
|
248 moreover |
|
249 have "simple_function M (f i)" for i |
|
250 proof (rule simple_function_borel_measurable) |
|
251 have "\<lfloor>enn2real (min (of_nat i) (u x)) * 2 ^ i\<rfloor> \<le> \<lfloor>int i * 2 ^ i\<rfloor>" for x |
|
252 by (cases "u x" rule: ennreal_cases) |
|
253 (auto split: split_min intro!: floor_mono) |
|
254 then have "f i ` space M \<subseteq> (\<lambda>n. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}" |
|
255 unfolding floor_of_int by (auto simp: f_def enn2real_nonneg intro!: imageI) |
|
256 then show "finite (f i ` space M)" |
|
257 by (rule finite_subset) auto |
|
258 show "f i \<in> borel_measurable M" |
|
259 unfolding f_def enn2real_def by measurable |
|
260 qed |
|
261 moreover |
|
262 { fix x |
|
263 have "(SUP i. ennreal (f i x)) = u x" |
|
264 proof (cases "u x" rule: ennreal_cases) |
|
265 case top then show ?thesis |
|
266 by (simp add: f_def inf_min[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] |
|
267 ennreal_SUP_of_nat_eq_top) |
|
268 next |
|
269 case (real r) |
|
270 obtain n where "r \<le> of_nat n" using real_arch_simple by auto |
|
271 then have min_eq_r: "\<forall>\<^sub>F x in sequentially. min (real x) r = r" |
|
272 by (auto simp: eventually_sequentially intro!: exI[of _ n] split: split_min) |
|
273 |
|
274 have "(\<lambda>i. real_of_int \<lfloor>min (real i) r * 2^i\<rfloor> / 2^i) \<longlonglongrightarrow> r" |
|
275 proof (rule tendsto_sandwich) |
|
276 show "(\<lambda>n. r - (1/2)^n) \<longlonglongrightarrow> r" |
|
277 by (auto intro!: tendsto_eq_intros LIMSEQ_power_zero) |
|
278 show "\<forall>\<^sub>F n in sequentially. real_of_int \<lfloor>min (real n) r * 2 ^ n\<rfloor> / 2 ^ n \<le> r" |
|
279 using min_eq_r by eventually_elim (auto simp: field_simps) |
|
280 have *: "r * (2 ^ n * 2 ^ n) \<le> 2^n + 2^n * real_of_int \<lfloor>r * 2 ^ n\<rfloor>" for n |
|
281 using real_of_int_floor_ge_diff_one[of "r * 2^n", THEN mult_left_mono, of "2^n"] |
|
282 by (auto simp: field_simps) |
|
283 show "\<forall>\<^sub>F n in sequentially. r - (1/2)^n \<le> real_of_int \<lfloor>min (real n) r * 2 ^ n\<rfloor> / 2 ^ n" |
|
284 using min_eq_r by eventually_elim (insert *, auto simp: field_simps) |
|
285 qed auto |
|
286 then have "(\<lambda>i. ennreal (f i x)) \<longlonglongrightarrow> ennreal r" |
|
287 by (simp add: real f_def ennreal_of_nat_eq_real_of_nat min_ennreal) |
|
288 from LIMSEQ_unique[OF LIMSEQ_SUP[OF inc_f] this] |
|
289 show ?thesis |
|
290 by (simp add: real) |
|
291 qed } |
|
292 ultimately show ?thesis |
|
293 by (intro exI[of _ "\<lambda>i x. ennreal (f i x)"]) auto |
|
294 qed |
|
295 |
|
296 lemma borel_measurable_implies_simple_function_sequence': |
|
297 fixes u :: "'a \<Rightarrow> ennreal" |
|
298 assumes u: "u \<in> borel_measurable M" |
|
299 obtains f where |
|
300 "\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x" |
|
301 using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast |
|
302 |
|
303 lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]: |
|
304 fixes u :: "'a \<Rightarrow> ennreal" |
|
305 assumes u: "simple_function M u" |
|
306 assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" |
|
307 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
|
308 assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
|
309 assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
|
310 shows "P u" |
|
311 proof (rule cong) |
|
312 from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" |
|
313 proof eventually_elim |
|
314 fix x assume x: "x \<in> space M" |
|
315 from simple_function_indicator_representation[OF u x] |
|
316 show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" .. |
|
317 qed |
|
318 next |
|
319 from u have "finite (u ` space M)" |
|
320 unfolding simple_function_def by auto |
|
321 then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)" |
|
322 proof induct |
|
323 case empty show ?case |
|
324 using set[of "{}"] by (simp add: indicator_def[abs_def]) |
|
325 qed (auto intro!: add mult set simple_functionD u) |
|
326 next |
|
327 show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))" |
|
328 apply (subst simple_function_cong) |
|
329 apply (rule simple_function_indicator_representation[symmetric]) |
|
330 apply (auto intro: u) |
|
331 done |
|
332 qed fact |
|
333 |
|
334 lemma simple_function_induct_nn[consumes 1, case_names cong set mult add]: |
|
335 fixes u :: "'a \<Rightarrow> ennreal" |
|
336 assumes u: "simple_function M u" |
|
337 assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" |
|
338 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
|
339 assumes mult: "\<And>u c. simple_function M u \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
|
340 assumes add: "\<And>u v. simple_function M u \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
|
341 shows "P u" |
|
342 proof - |
|
343 show ?thesis |
|
344 proof (rule cong) |
|
345 fix x assume x: "x \<in> space M" |
|
346 from simple_function_indicator_representation[OF u x] |
|
347 show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" .. |
|
348 next |
|
349 show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))" |
|
350 apply (subst simple_function_cong) |
|
351 apply (rule simple_function_indicator_representation[symmetric]) |
|
352 apply (auto intro: u) |
|
353 done |
|
354 next |
|
355 from u have "finite (u ` space M)" |
|
356 unfolding simple_function_def by auto |
|
357 then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)" |
|
358 proof induct |
|
359 case empty show ?case |
|
360 using set[of "{}"] by (simp add: indicator_def[abs_def]) |
|
361 next |
|
362 case (insert x S) |
|
363 { fix z have "(\<Sum>y\<in>S. y * indicator (u -` {y} \<inter> space M) z) = 0 \<or> |
|
364 x * indicator (u -` {x} \<inter> space M) z = 0" |
|
365 using insert by (subst setsum_eq_0_iff) (auto simp: indicator_def) } |
|
366 note disj = this |
|
367 from insert show ?case |
|
368 by (auto intro!: add mult set simple_functionD u simple_function_setsum disj) |
|
369 qed |
|
370 qed fact |
|
371 qed |
|
372 |
|
373 lemma borel_measurable_induct[consumes 1, case_names cong set mult add seq, induct set: borel_measurable]: |
|
374 fixes u :: "'a \<Rightarrow> ennreal" |
|
375 assumes u: "u \<in> borel_measurable M" |
|
376 assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f" |
|
377 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
|
378 assumes mult': "\<And>u c. c < top \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
|
379 assumes add: "\<And>u v. u \<in> borel_measurable M\<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> v x < top) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
|
380 assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. x \<in> space M \<Longrightarrow> U i x < top) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> u = (SUP i. U i) \<Longrightarrow> P (SUP i. U i)" |
|
381 shows "P u" |
|
382 using u |
|
383 proof (induct rule: borel_measurable_implies_simple_function_sequence') |
|
384 fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x" |
|
385 have u_eq: "u = (SUP i. U i)" |
|
386 using u sup by auto |
|
387 |
|
388 have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top" |
|
389 using U by (auto simp: image_iff eq_commute) |
|
390 |
|
391 from U have "\<And>i. U i \<in> borel_measurable M" |
|
392 by (simp add: borel_measurable_simple_function) |
|
393 |
|
394 show "P u" |
|
395 unfolding u_eq |
|
396 proof (rule seq) |
|
397 fix i show "P (U i)" |
|
398 using \<open>simple_function M (U i)\<close> not_inf[of _ i] |
|
399 proof (induct rule: simple_function_induct_nn) |
|
400 case (mult u c) |
|
401 show ?case |
|
402 proof cases |
|
403 assume "c = 0 \<or> space M = {} \<or> (\<forall>x\<in>space M. u x = 0)" |
|
404 with mult(1) show ?thesis |
|
405 by (intro cong[of "\<lambda>x. c * u x" "indicator {}"] set) |
|
406 (auto dest!: borel_measurable_simple_function) |
|
407 next |
|
408 assume "\<not> (c = 0 \<or> space M = {} \<or> (\<forall>x\<in>space M. u x = 0))" |
|
409 then obtain x where "space M \<noteq> {}" and x: "x \<in> space M" "u x \<noteq> 0" "c \<noteq> 0" |
|
410 by auto |
|
411 with mult(3)[of x] have "c < top" |
|
412 by (auto simp: ennreal_mult_less_top) |
|
413 then have u_fin: "x' \<in> space M \<Longrightarrow> u x' < top" for x' |
|
414 using mult(3)[of x'] \<open>c \<noteq> 0\<close> by (auto simp: ennreal_mult_less_top) |
|
415 then have "P u" |
|
416 by (rule mult) |
|
417 with u_fin \<open>c < top\<close> mult(1) show ?thesis |
|
418 by (intro mult') (auto dest!: borel_measurable_simple_function) |
|
419 qed |
|
420 qed (auto intro: cong intro!: set add dest!: borel_measurable_simple_function) |
|
421 qed fact+ |
|
422 qed |
|
423 |
|
424 lemma simple_function_If_set: |
|
425 assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M" |
|
426 shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF") |
|
427 proof - |
|
428 define F where "F x = f -` {x} \<inter> space M" for x |
|
429 define G where "G x = g -` {x} \<inter> space M" for x |
|
430 show ?thesis unfolding simple_function_def |
|
431 proof safe |
|
432 have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto |
|
433 from finite_subset[OF this] assms |
|
434 show "finite (?IF ` space M)" unfolding simple_function_def by auto |
|
435 next |
|
436 fix x assume "x \<in> space M" |
|
437 then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A |
|
438 then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M)))) |
|
439 else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))" |
|
440 using sets.sets_into_space[OF A] by (auto split: if_split_asm simp: G_def F_def) |
|
441 have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M" |
|
442 unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto |
|
443 show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto |
|
444 qed |
|
445 qed |
|
446 |
|
447 lemma simple_function_If: |
|
448 assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M" |
|
449 shows "simple_function M (\<lambda>x. if P x then f x else g x)" |
|
450 proof - |
|
451 have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto |
|
452 with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp |
|
453 qed |
|
454 |
|
455 lemma simple_function_subalgebra: |
|
456 assumes "simple_function N f" |
|
457 and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M" |
|
458 shows "simple_function M f" |
|
459 using assms unfolding simple_function_def by auto |
|
460 |
|
461 lemma simple_function_comp: |
|
462 assumes T: "T \<in> measurable M M'" |
|
463 and f: "simple_function M' f" |
|
464 shows "simple_function M (\<lambda>x. f (T x))" |
|
465 proof (intro simple_function_def[THEN iffD2] conjI ballI) |
|
466 have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" |
|
467 using T unfolding measurable_def by auto |
|
468 then show "finite ((\<lambda>x. f (T x)) ` space M)" |
|
469 using f unfolding simple_function_def by (auto intro: finite_subset) |
|
470 fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M" |
|
471 then have "i \<in> f ` space M'" |
|
472 using T unfolding measurable_def by auto |
|
473 then have "f -` {i} \<inter> space M' \<in> sets M'" |
|
474 using f unfolding simple_function_def by auto |
|
475 then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M" |
|
476 using T unfolding measurable_def by auto |
|
477 also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M" |
|
478 using T unfolding measurable_def by auto |
|
479 finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" . |
|
480 qed |
|
481 |
|
482 subsection "Simple integral" |
|
483 |
|
484 definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>S") where |
|
485 "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))" |
|
486 |
|
487 syntax |
|
488 "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110) |
|
489 |
|
490 translations |
|
491 "\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)" |
|
492 |
|
493 lemma simple_integral_cong: |
|
494 assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
495 shows "integral\<^sup>S M f = integral\<^sup>S M g" |
|
496 proof - |
|
497 have "f ` space M = g ` space M" |
|
498 "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
499 using assms by (auto intro!: image_eqI) |
|
500 thus ?thesis unfolding simple_integral_def by simp |
|
501 qed |
|
502 |
|
503 lemma simple_integral_const[simp]: |
|
504 "(\<integral>\<^sup>Sx. c \<partial>M) = c * (emeasure M) (space M)" |
|
505 proof (cases "space M = {}") |
|
506 case True thus ?thesis unfolding simple_integral_def by simp |
|
507 next |
|
508 case False hence "(\<lambda>x. c) ` space M = {c}" by auto |
|
509 thus ?thesis unfolding simple_integral_def by simp |
|
510 qed |
|
511 |
|
512 lemma simple_function_partition: |
|
513 assumes f: "simple_function M f" and g: "simple_function M g" |
|
514 assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y" |
|
515 assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)" |
|
516 shows "integral\<^sup>S M f = (\<Sum>y\<in>g ` space M. v y * emeasure M {x\<in>space M. g x = y})" |
|
517 (is "_ = ?r") |
|
518 proof - |
|
519 from f g have [simp]: "finite (f`space M)" "finite (g`space M)" |
|
520 by (auto simp: simple_function_def) |
|
521 from f g have [measurable]: "f \<in> measurable M (count_space UNIV)" "g \<in> measurable M (count_space UNIV)" |
|
522 by (auto intro: measurable_simple_function) |
|
523 |
|
524 { fix y assume "y \<in> space M" |
|
525 then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}" |
|
526 by (auto cong: sub simp: v[symmetric]) } |
|
527 note eq = this |
|
528 |
|
529 have "integral\<^sup>S M f = |
|
530 (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. |
|
531 if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))" |
|
532 unfolding simple_integral_def |
|
533 proof (safe intro!: setsum.cong ennreal_mult_left_cong) |
|
534 fix y assume y: "y \<in> space M" "f y \<noteq> 0" |
|
535 have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = |
|
536 {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" |
|
537 by auto |
|
538 have eq:"(\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i}) = |
|
539 f -` {f y} \<inter> space M" |
|
540 by (auto simp: eq_commute cong: sub rev_conj_cong) |
|
541 have "finite (g`space M)" by simp |
|
542 then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" |
|
543 by (rule rev_finite_subset) auto |
|
544 then show "emeasure M (f -` {f y} \<inter> space M) = |
|
545 (\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then emeasure M {x \<in> space M. g x = z} else 0)" |
|
546 apply (simp add: setsum.If_cases) |
|
547 apply (subst setsum_emeasure) |
|
548 apply (auto simp: disjoint_family_on_def eq) |
|
549 done |
|
550 qed |
|
551 also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. |
|
552 if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))" |
|
553 by (auto intro!: setsum.cong simp: setsum_right_distrib) |
|
554 also have "\<dots> = ?r" |
|
555 by (subst setsum.commute) |
|
556 (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq) |
|
557 finally show "integral\<^sup>S M f = ?r" . |
|
558 qed |
|
559 |
|
560 lemma simple_integral_add[simp]: |
|
561 assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x" |
|
562 shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g" |
|
563 proof - |
|
564 have "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = |
|
565 (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. (fst y + snd y) * emeasure M {x\<in>space M. (f x, g x) = y})" |
|
566 by (intro simple_function_partition) (auto intro: f g) |
|
567 also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) + |
|
568 (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y})" |
|
569 using assms(2,4) by (auto intro!: setsum.cong distrib_right simp: setsum.distrib[symmetric]) |
|
570 also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. f x \<partial>M)" |
|
571 by (intro simple_function_partition[symmetric]) (auto intro: f g) |
|
572 also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. g x \<partial>M)" |
|
573 by (intro simple_function_partition[symmetric]) (auto intro: f g) |
|
574 finally show ?thesis . |
|
575 qed |
|
576 |
|
577 lemma simple_integral_setsum[simp]: |
|
578 assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i x" |
|
579 assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)" |
|
580 shows "(\<integral>\<^sup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>S M (f i))" |
|
581 proof cases |
|
582 assume "finite P" |
|
583 from this assms show ?thesis |
|
584 by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg) |
|
585 qed auto |
|
586 |
|
587 lemma simple_integral_mult[simp]: |
|
588 assumes f: "simple_function M f" |
|
589 shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f" |
|
590 proof - |
|
591 have "(\<integral>\<^sup>Sx. c * f x \<partial>M) = (\<Sum>y\<in>f ` space M. (c * y) * emeasure M {x\<in>space M. f x = y})" |
|
592 using f by (intro simple_function_partition) auto |
|
593 also have "\<dots> = c * integral\<^sup>S M f" |
|
594 using f unfolding simple_integral_def |
|
595 by (subst setsum_right_distrib) (auto simp: mult.assoc Int_def conj_commute) |
|
596 finally show ?thesis . |
|
597 qed |
|
598 |
|
599 lemma simple_integral_mono_AE: |
|
600 assumes f[measurable]: "simple_function M f" and g[measurable]: "simple_function M g" |
|
601 and mono: "AE x in M. f x \<le> g x" |
|
602 shows "integral\<^sup>S M f \<le> integral\<^sup>S M g" |
|
603 proof - |
|
604 let ?\<mu> = "\<lambda>P. emeasure M {x\<in>space M. P x}" |
|
605 have "integral\<^sup>S M f = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * ?\<mu> (\<lambda>x. (f x, g x) = y))" |
|
606 using f g by (intro simple_function_partition) auto |
|
607 also have "\<dots> \<le> (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * ?\<mu> (\<lambda>x. (f x, g x) = y))" |
|
608 proof (clarsimp intro!: setsum_mono) |
|
609 fix x assume "x \<in> space M" |
|
610 let ?M = "?\<mu> (\<lambda>y. f y = f x \<and> g y = g x)" |
|
611 show "f x * ?M \<le> g x * ?M" |
|
612 proof cases |
|
613 assume "?M \<noteq> 0" |
|
614 then have "0 < ?M" |
|
615 by (simp add: less_le) |
|
616 also have "\<dots> \<le> ?\<mu> (\<lambda>y. f x \<le> g x)" |
|
617 using mono by (intro emeasure_mono_AE) auto |
|
618 finally have "\<not> \<not> f x \<le> g x" |
|
619 by (intro notI) auto |
|
620 then show ?thesis |
|
621 by (intro mult_right_mono) auto |
|
622 qed simp |
|
623 qed |
|
624 also have "\<dots> = integral\<^sup>S M g" |
|
625 using f g by (intro simple_function_partition[symmetric]) auto |
|
626 finally show ?thesis . |
|
627 qed |
|
628 |
|
629 lemma simple_integral_mono: |
|
630 assumes "simple_function M f" and "simple_function M g" |
|
631 and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x" |
|
632 shows "integral\<^sup>S M f \<le> integral\<^sup>S M g" |
|
633 using assms by (intro simple_integral_mono_AE) auto |
|
634 |
|
635 lemma simple_integral_cong_AE: |
|
636 assumes "simple_function M f" and "simple_function M g" |
|
637 and "AE x in M. f x = g x" |
|
638 shows "integral\<^sup>S M f = integral\<^sup>S M g" |
|
639 using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) |
|
640 |
|
641 lemma simple_integral_cong': |
|
642 assumes sf: "simple_function M f" "simple_function M g" |
|
643 and mea: "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" |
|
644 shows "integral\<^sup>S M f = integral\<^sup>S M g" |
|
645 proof (intro simple_integral_cong_AE sf AE_I) |
|
646 show "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" by fact |
|
647 show "{x \<in> space M. f x \<noteq> g x} \<in> sets M" |
|
648 using sf[THEN borel_measurable_simple_function] by auto |
|
649 qed simp |
|
650 |
|
651 lemma simple_integral_indicator: |
|
652 assumes A: "A \<in> sets M" |
|
653 assumes f: "simple_function M f" |
|
654 shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = |
|
655 (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))" |
|
656 proof - |
|
657 have eq: "(\<lambda>x. (f x, indicator A x)) ` space M \<inter> {x. snd x = 1} = (\<lambda>x. (f x, 1::ennreal))`A" |
|
658 using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: if_split_asm) |
|
659 have eq2: "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}" |
|
660 by (auto simp: image_iff) |
|
661 |
|
662 have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = |
|
663 (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x))`space M. (fst y * snd y) * emeasure M {x\<in>space M. (f x, indicator A x) = y})" |
|
664 using assms by (intro simple_function_partition) auto |
|
665 also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M. |
|
666 if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)" |
|
667 by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum.cong) |
|
668 also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))" |
|
669 using assms by (subst setsum.If_cases) (auto intro!: simple_functionD(1) simp: eq) |
|
670 also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))" |
|
671 by (subst setsum.reindex [of fst]) (auto simp: inj_on_def) |
|
672 also have "\<dots> = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))" |
|
673 using A[THEN sets.sets_into_space] |
|
674 by (intro setsum.mono_neutral_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2) |
|
675 finally show ?thesis . |
|
676 qed |
|
677 |
|
678 lemma simple_integral_indicator_only[simp]: |
|
679 assumes "A \<in> sets M" |
|
680 shows "integral\<^sup>S M (indicator A) = emeasure M A" |
|
681 using simple_integral_indicator[OF assms, of "\<lambda>x. 1"] sets.sets_into_space[OF assms] |
|
682 by (simp_all add: image_constant_conv Int_absorb1 split: if_split_asm) |
|
683 |
|
684 lemma simple_integral_null_set: |
|
685 assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M" |
|
686 shows "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = 0" |
|
687 proof - |
|
688 have "AE x in M. indicator N x = (0 :: ennreal)" |
|
689 using \<open>N \<in> null_sets M\<close> by (auto simp: indicator_def intro!: AE_I[of _ _ N]) |
|
690 then have "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^sup>Sx. 0 \<partial>M)" |
|
691 using assms apply (intro simple_integral_cong_AE) by auto |
|
692 then show ?thesis by simp |
|
693 qed |
|
694 |
|
695 lemma simple_integral_cong_AE_mult_indicator: |
|
696 assumes sf: "simple_function M f" and eq: "AE x in M. x \<in> S" and "S \<in> sets M" |
|
697 shows "integral\<^sup>S M f = (\<integral>\<^sup>Sx. f x * indicator S x \<partial>M)" |
|
698 using assms by (intro simple_integral_cong_AE) auto |
|
699 |
|
700 lemma simple_integral_cmult_indicator: |
|
701 assumes A: "A \<in> sets M" |
|
702 shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * emeasure M A" |
|
703 using simple_integral_mult[OF simple_function_indicator[OF A]] |
|
704 unfolding simple_integral_indicator_only[OF A] by simp |
|
705 |
|
706 lemma simple_integral_nonneg: |
|
707 assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x" |
|
708 shows "0 \<le> integral\<^sup>S M f" |
|
709 proof - |
|
710 have "integral\<^sup>S M (\<lambda>x. 0) \<le> integral\<^sup>S M f" |
|
711 using simple_integral_mono_AE[OF _ f ae] by auto |
|
712 then show ?thesis by simp |
|
713 qed |
|
714 |
|
715 subsection \<open>Integral on nonnegative functions\<close> |
|
716 |
|
717 definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where |
|
718 "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)" |
|
719 |
|
720 syntax |
|
721 "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110) |
|
722 |
|
723 translations |
|
724 "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)" |
|
725 |
|
726 lemma nn_integral_def_finite: |
|
727 "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)" |
|
728 (is "_ = SUPREMUM ?A ?f") |
|
729 unfolding nn_integral_def |
|
730 proof (safe intro!: antisym SUP_least) |
|
731 fix g assume g[measurable]: "simple_function M g" "g \<le> f" |
|
732 |
|
733 show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f" |
|
734 proof cases |
|
735 assume ae: "AE x in M. g x \<noteq> top" |
|
736 let ?G = "{x \<in> space M. g x \<noteq> top}" |
|
737 have "integral\<^sup>S M g = integral\<^sup>S M (\<lambda>x. g x * indicator ?G x)" |
|
738 proof (rule simple_integral_cong_AE) |
|
739 show "AE x in M. g x = g x * indicator ?G x" |
|
740 using ae AE_space by eventually_elim auto |
|
741 qed (insert g, auto) |
|
742 also have "\<dots> \<le> SUPREMUM ?A ?f" |
|
743 using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator) |
|
744 finally show ?thesis . |
|
745 next |
|
746 assume nAE: "\<not> (AE x in M. g x \<noteq> top)" |
|
747 then have "emeasure M {x\<in>space M. g x = top} \<noteq> 0" (is "emeasure M ?G \<noteq> 0") |
|
748 by (subst (asm) AE_iff_measurable[OF _ refl]) auto |
|
749 then have "top = (SUP n. (\<integral>\<^sup>Sx. of_nat n * indicator ?G x \<partial>M))" |
|
750 by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric]) |
|
751 also have "\<dots> \<le> SUPREMUM ?A ?f" |
|
752 using g |
|
753 by (safe intro!: SUP_least SUP_upper) |
|
754 (auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator |
|
755 intro: order_trans[of _ "g x" "f x" for x, OF order_trans[of _ top]]) |
|
756 finally show ?thesis |
|
757 by (simp add: top_unique del: SUP_eq_top_iff Sup_eq_top_iff) |
|
758 qed |
|
759 qed (auto intro: SUP_upper) |
|
760 |
|
761 lemma nn_integral_mono_AE: |
|
762 assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>N M u \<le> integral\<^sup>N M v" |
|
763 unfolding nn_integral_def |
|
764 proof (safe intro!: SUP_mono) |
|
765 fix n assume n: "simple_function M n" "n \<le> u" |
|
766 from ae[THEN AE_E] guess N . note N = this |
|
767 then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in) |
|
768 let ?n = "\<lambda>x. n x * indicator (space M - N) x" |
|
769 have "AE x in M. n x \<le> ?n x" "simple_function M ?n" |
|
770 using n N ae_N by auto |
|
771 moreover |
|
772 { fix x have "?n x \<le> v x" |
|
773 proof cases |
|
774 assume x: "x \<in> space M - N" |
|
775 with N have "u x \<le> v x" by auto |
|
776 with n(2)[THEN le_funD, of x] x show ?thesis |
|
777 by (auto simp: max_def split: if_split_asm) |
|
778 qed simp } |
|
779 then have "?n \<le> v" by (auto simp: le_funI) |
|
780 moreover have "integral\<^sup>S M n \<le> integral\<^sup>S M ?n" |
|
781 using ae_N N n by (auto intro!: simple_integral_mono_AE) |
|
782 ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> v}. integral\<^sup>S M n \<le> integral\<^sup>S M m" |
|
783 by force |
|
784 qed |
|
785 |
|
786 lemma nn_integral_mono: |
|
787 "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v" |
|
788 by (auto intro: nn_integral_mono_AE) |
|
789 |
|
790 lemma mono_nn_integral: "mono F \<Longrightarrow> mono (\<lambda>x. integral\<^sup>N M (F x))" |
|
791 by (auto simp add: mono_def le_fun_def intro!: nn_integral_mono) |
|
792 |
|
793 lemma nn_integral_cong_AE: |
|
794 "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v" |
|
795 by (auto simp: eq_iff intro!: nn_integral_mono_AE) |
|
796 |
|
797 lemma nn_integral_cong: |
|
798 "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v" |
|
799 by (auto intro: nn_integral_cong_AE) |
|
800 |
|
801 lemma nn_integral_cong_simp: |
|
802 "(\<And>x. x \<in> space M =simp=> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v" |
|
803 by (auto intro: nn_integral_cong simp: simp_implies_def) |
|
804 |
|
805 lemma nn_integral_cong_strong: |
|
806 "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v" |
|
807 by (auto intro: nn_integral_cong) |
|
808 |
|
809 lemma incseq_nn_integral: |
|
810 assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))" |
|
811 proof - |
|
812 have "\<And>i x. f i x \<le> f (Suc i) x" |
|
813 using assms by (auto dest!: incseq_SucD simp: le_fun_def) |
|
814 then show ?thesis |
|
815 by (auto intro!: incseq_SucI nn_integral_mono) |
|
816 qed |
|
817 |
|
818 lemma nn_integral_eq_simple_integral: |
|
819 assumes f: "simple_function M f" shows "integral\<^sup>N M f = integral\<^sup>S M f" |
|
820 proof - |
|
821 let ?f = "\<lambda>x. f x * indicator (space M) x" |
|
822 have f': "simple_function M ?f" using f by auto |
|
823 have "integral\<^sup>N M ?f \<le> integral\<^sup>S M ?f" using f' |
|
824 by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def) |
|
825 moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>N M ?f" |
|
826 unfolding nn_integral_def |
|
827 using f' by (auto intro!: SUP_upper) |
|
828 ultimately show ?thesis |
|
829 by (simp cong: nn_integral_cong simple_integral_cong) |
|
830 qed |
|
831 |
|
832 text \<open>Beppo-Levi monotone convergence theorem\<close> |
|
833 lemma nn_integral_monotone_convergence_SUP: |
|
834 assumes f: "incseq f" and [measurable]: "\<And>i. f i \<in> borel_measurable M" |
|
835 shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" |
|
836 proof (rule antisym) |
|
837 show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" |
|
838 unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"] |
|
839 proof (safe intro!: SUP_least) |
|
840 fix u assume sf_u[simp]: "simple_function M u" and |
|
841 u: "u \<le> (\<lambda>x. SUP i. f i x)" and u_range: "\<forall>x. u x < top" |
|
842 note sf_u[THEN borel_measurable_simple_function, measurable] |
|
843 show "integral\<^sup>S M u \<le> (SUP j. \<integral>\<^sup>+x. f j x \<partial>M)" |
|
844 proof (rule ennreal_approx_unit) |
|
845 fix a :: ennreal assume "a < 1" |
|
846 let ?au = "\<lambda>x. a * u x" |
|
847 |
|
848 let ?B = "\<lambda>c i. {x\<in>space M. ?au x = c \<and> c \<le> f i x}" |
|
849 have "integral\<^sup>S M ?au = (\<Sum>c\<in>?au`space M. c * (SUP i. emeasure M (?B c i)))" |
|
850 unfolding simple_integral_def |
|
851 proof (intro setsum.cong ennreal_mult_left_cong refl) |
|
852 fix c assume "c \<in> ?au ` space M" "c \<noteq> 0" |
|
853 { fix x' assume x': "x' \<in> space M" "?au x' = c" |
|
854 with \<open>c \<noteq> 0\<close> u_range have "?au x' < 1 * u x'" |
|
855 by (intro ennreal_mult_strict_right_mono \<open>a < 1\<close>) (auto simp: less_le) |
|
856 also have "\<dots> \<le> (SUP i. f i x')" |
|
857 using u by (auto simp: le_fun_def) |
|
858 finally have "\<exists>i. ?au x' \<le> f i x'" |
|
859 by (auto simp: less_SUP_iff intro: less_imp_le) } |
|
860 then have *: "?au -` {c} \<inter> space M = (\<Union>i. ?B c i)" |
|
861 by auto |
|
862 show "emeasure M (?au -` {c} \<inter> space M) = (SUP i. emeasure M (?B c i))" |
|
863 unfolding * using f |
|
864 by (intro SUP_emeasure_incseq[symmetric]) |
|
865 (auto simp: incseq_def le_fun_def intro: order_trans) |
|
866 qed |
|
867 also have "\<dots> = (SUP i. \<Sum>c\<in>?au`space M. c * emeasure M (?B c i))" |
|
868 unfolding SUP_mult_left_ennreal using f |
|
869 by (intro ennreal_SUP_setsum[symmetric]) |
|
870 (auto intro!: mult_mono emeasure_mono simp: incseq_def le_fun_def intro: order_trans) |
|
871 also have "\<dots> \<le> (SUP i. integral\<^sup>N M (f i))" |
|
872 proof (intro SUP_subset_mono order_refl) |
|
873 fix i |
|
874 have "(\<Sum>c\<in>?au`space M. c * emeasure M (?B c i)) = |
|
875 (\<integral>\<^sup>Sx. (a * u x) * indicator {x\<in>space M. a * u x \<le> f i x} x \<partial>M)" |
|
876 by (subst simple_integral_indicator) |
|
877 (auto intro!: setsum.cong ennreal_mult_left_cong arg_cong2[where f=emeasure]) |
|
878 also have "\<dots> = (\<integral>\<^sup>+x. (a * u x) * indicator {x\<in>space M. a * u x \<le> f i x} x \<partial>M)" |
|
879 by (rule nn_integral_eq_simple_integral[symmetric]) simp |
|
880 also have "\<dots> \<le> (\<integral>\<^sup>+x. f i x \<partial>M)" |
|
881 by (intro nn_integral_mono) (auto split: split_indicator) |
|
882 finally show "(\<Sum>c\<in>?au`space M. c * emeasure M (?B c i)) \<le> (\<integral>\<^sup>+x. f i x \<partial>M)" . |
|
883 qed |
|
884 finally show "a * integral\<^sup>S M u \<le> (SUP i. integral\<^sup>N M (f i))" |
|
885 by simp |
|
886 qed |
|
887 qed |
|
888 qed (auto intro!: SUP_least SUP_upper nn_integral_mono) |
|
889 |
|
890 lemma sup_continuous_nn_integral[order_continuous_intros]: |
|
891 assumes f: "\<And>y. sup_continuous (f y)" |
|
892 assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M" |
|
893 shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
|
894 unfolding sup_continuous_def |
|
895 proof safe |
|
896 fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C" |
|
897 with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
|
898 unfolding sup_continuousD[OF f C] |
|
899 by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def) |
|
900 qed |
|
901 |
|
902 lemma nn_integral_monotone_convergence_SUP_AE: |
|
903 assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x" "\<And>i. f i \<in> borel_measurable M" |
|
904 shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" |
|
905 proof - |
|
906 from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x" |
|
907 by (simp add: AE_all_countable) |
|
908 from this[THEN AE_E] guess N . note N = this |
|
909 let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0" |
|
910 have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N]) |
|
911 then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)" |
|
912 by (auto intro!: nn_integral_cong_AE) |
|
913 also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))" |
|
914 proof (rule nn_integral_monotone_convergence_SUP) |
|
915 show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI) |
|
916 { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M" |
|
917 using f N(3) by (intro measurable_If_set) auto } |
|
918 qed |
|
919 also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" |
|
920 using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext) |
|
921 finally show ?thesis . |
|
922 qed |
|
923 |
|
924 lemma nn_integral_monotone_convergence_simple: |
|
925 "incseq f \<Longrightarrow> (\<And>i. simple_function M (f i)) \<Longrightarrow> (SUP i. \<integral>\<^sup>S x. f i x \<partial>M) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
|
926 using nn_integral_monotone_convergence_SUP[of f M] |
|
927 by (simp add: nn_integral_eq_simple_integral[symmetric] borel_measurable_simple_function) |
|
928 |
|
929 lemma SUP_simple_integral_sequences: |
|
930 assumes f: "incseq f" "\<And>i. simple_function M (f i)" |
|
931 and g: "incseq g" "\<And>i. simple_function M (g i)" |
|
932 and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" |
|
933 shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" |
|
934 (is "SUPREMUM _ ?F = SUPREMUM _ ?G") |
|
935 proof - |
|
936 have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
|
937 using f by (rule nn_integral_monotone_convergence_simple) |
|
938 also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)" |
|
939 unfolding eq[THEN nn_integral_cong_AE] .. |
|
940 also have "\<dots> = (SUP i. ?G i)" |
|
941 using g by (rule nn_integral_monotone_convergence_simple[symmetric]) |
|
942 finally show ?thesis by simp |
|
943 qed |
|
944 |
|
945 lemma nn_integral_const[simp]: "(\<integral>\<^sup>+ x. c \<partial>M) = c * emeasure M (space M)" |
|
946 by (subst nn_integral_eq_simple_integral) auto |
|
947 |
|
948 lemma nn_integral_linear: |
|
949 assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M" |
|
950 shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g" |
|
951 (is "integral\<^sup>N M ?L = _") |
|
952 proof - |
|
953 from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u . |
|
954 note u = nn_integral_monotone_convergence_simple[OF this(2,1)] this |
|
955 from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v . |
|
956 note v = nn_integral_monotone_convergence_simple[OF this(2,1)] this |
|
957 let ?L' = "\<lambda>i x. a * u i x + v i x" |
|
958 |
|
959 have "?L \<in> borel_measurable M" using assms by auto |
|
960 from borel_measurable_implies_simple_function_sequence'[OF this] guess l . |
|
961 note l = nn_integral_monotone_convergence_simple[OF this(2,1)] this |
|
962 |
|
963 have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))" |
|
964 using u v by (auto simp: incseq_Suc_iff le_fun_def intro!: add_mono mult_left_mono simple_integral_mono) |
|
965 |
|
966 have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))" |
|
967 proof (rule SUP_simple_integral_sequences[OF l(3,2)]) |
|
968 show "incseq ?L'" "\<And>i. simple_function M (?L' i)" |
|
969 using u v unfolding incseq_Suc_iff le_fun_def |
|
970 by (auto intro!: add_mono mult_left_mono) |
|
971 { fix x |
|
972 have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)" |
|
973 using u(3) v(3) u(4)[of _ x] v(4)[of _ x] unfolding SUP_mult_left_ennreal |
|
974 by (auto intro!: ennreal_SUP_add simp: incseq_Suc_iff le_fun_def add_mono mult_left_mono) } |
|
975 then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)" |
|
976 unfolding l(5) using u(5) v(5) by (intro AE_I2) auto |
|
977 qed |
|
978 also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))" |
|
979 using u(2) v(2) by auto |
|
980 finally show ?thesis |
|
981 unfolding l(5)[symmetric] l(1)[symmetric] |
|
982 by (simp add: ennreal_SUP_add[OF inc] v u SUP_mult_left_ennreal[symmetric]) |
|
983 qed |
|
984 |
|
985 lemma nn_integral_cmult: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>N M f" |
|
986 using nn_integral_linear[of f M "\<lambda>x. 0" c] by simp |
|
987 |
|
988 lemma nn_integral_multc: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c" |
|
989 unfolding mult.commute[of _ c] nn_integral_cmult by simp |
|
990 |
|
991 lemma nn_integral_divide: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c" |
|
992 unfolding divide_ennreal_def by (rule nn_integral_multc) |
|
993 |
|
994 lemma nn_integral_indicator[simp]: "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A" |
|
995 by (subst nn_integral_eq_simple_integral) (auto simp: simple_integral_indicator) |
|
996 |
|
997 lemma nn_integral_cmult_indicator: "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. c * indicator A x \<partial>M) = c * emeasure M A" |
|
998 by (subst nn_integral_eq_simple_integral) |
|
999 (auto simp: simple_function_indicator simple_integral_indicator) |
|
1000 |
|
1001 lemma nn_integral_indicator': |
|
1002 assumes [measurable]: "A \<inter> space M \<in> sets M" |
|
1003 shows "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)" |
|
1004 proof - |
|
1005 have "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = (\<integral>\<^sup>+ x. indicator (A \<inter> space M) x \<partial>M)" |
|
1006 by (intro nn_integral_cong) (simp split: split_indicator) |
|
1007 also have "\<dots> = emeasure M (A \<inter> space M)" |
|
1008 by simp |
|
1009 finally show ?thesis . |
|
1010 qed |
|
1011 |
|
1012 lemma nn_integral_indicator_singleton[simp]: |
|
1013 assumes [measurable]: "{y} \<in> sets M" shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = f y * emeasure M {y}" |
|
1014 proof - |
|
1015 have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. f y * indicator {y} x \<partial>M)" |
|
1016 by (auto intro!: nn_integral_cong split: split_indicator) |
|
1017 then show ?thesis |
|
1018 by (simp add: nn_integral_cmult) |
|
1019 qed |
|
1020 |
|
1021 lemma nn_integral_set_ennreal: |
|
1022 "(\<integral>\<^sup>+x. ennreal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ennreal (f x * indicator A x) \<partial>M)" |
|
1023 by (rule nn_integral_cong) (simp split: split_indicator) |
|
1024 |
|
1025 lemma nn_integral_indicator_singleton'[simp]: |
|
1026 assumes [measurable]: "{y} \<in> sets M" |
|
1027 shows "(\<integral>\<^sup>+x. ennreal (f x * indicator {y} x) \<partial>M) = f y * emeasure M {y}" |
|
1028 by (subst nn_integral_set_ennreal[symmetric]) (simp add: nn_integral_indicator_singleton) |
|
1029 |
|
1030 lemma nn_integral_add: |
|
1031 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>N M f + integral\<^sup>N M g" |
|
1032 using nn_integral_linear[of f M g 1] by simp |
|
1033 |
|
1034 lemma nn_integral_setsum: |
|
1035 "(\<And>i. i \<in> P \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))" |
|
1036 by (induction P rule: infinite_finite_induct) (auto simp: nn_integral_add) |
|
1037 |
|
1038 lemma nn_integral_suminf: |
|
1039 assumes f: "\<And>i. f i \<in> borel_measurable M" |
|
1040 shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))" |
|
1041 proof - |
|
1042 have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x" |
|
1043 using assms by (auto simp: AE_all_countable) |
|
1044 have "(\<Sum>i. integral\<^sup>N M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>N M (f i))" |
|
1045 by (rule suminf_eq_SUP) |
|
1046 also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)" |
|
1047 unfolding nn_integral_setsum[OF f] .. |
|
1048 also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos |
|
1049 by (intro nn_integral_monotone_convergence_SUP_AE[symmetric]) |
|
1050 (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3) |
|
1051 also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos |
|
1052 by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP) |
|
1053 finally show ?thesis by simp |
|
1054 qed |
|
1055 |
|
1056 lemma nn_integral_bound_simple_function: |
|
1057 assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>" |
|
1058 assumes f[measurable]: "simple_function M f" |
|
1059 assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>" |
|
1060 shows "nn_integral M f < \<infinity>" |
|
1061 proof cases |
|
1062 assume "space M = {}" |
|
1063 then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)" |
|
1064 by (intro nn_integral_cong) auto |
|
1065 then show ?thesis by simp |
|
1066 next |
|
1067 assume "space M \<noteq> {}" |
|
1068 with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>" |
|
1069 by (subst Max_less_iff) (auto simp: Max_ge_iff) |
|
1070 |
|
1071 have "nn_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)" |
|
1072 proof (rule nn_integral_mono) |
|
1073 fix x assume "x \<in> space M" |
|
1074 with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x" |
|
1075 by (auto split: split_indicator intro!: Max_ge simple_functionD) |
|
1076 qed |
|
1077 also have "\<dots> < \<infinity>" |
|
1078 using bnd supp by (subst nn_integral_cmult) (auto simp: ennreal_mult_less_top) |
|
1079 finally show ?thesis . |
|
1080 qed |
|
1081 |
|
1082 lemma nn_integral_Markov_inequality: |
|
1083 assumes u: "u \<in> borel_measurable M" and "A \<in> sets M" |
|
1084 shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)" |
|
1085 (is "(emeasure M) ?A \<le> _ * ?PI") |
|
1086 proof - |
|
1087 have "?A \<in> sets M" |
|
1088 using \<open>A \<in> sets M\<close> u by auto |
|
1089 hence "(emeasure M) ?A = (\<integral>\<^sup>+ x. indicator ?A x \<partial>M)" |
|
1090 using nn_integral_indicator by simp |
|
1091 also have "\<dots> \<le> (\<integral>\<^sup>+ x. c * (u x * indicator A x) \<partial>M)" |
|
1092 using u by (auto intro!: nn_integral_mono_AE simp: indicator_def) |
|
1093 also have "\<dots> = c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)" |
|
1094 using assms by (auto intro!: nn_integral_cmult) |
|
1095 finally show ?thesis . |
|
1096 qed |
|
1097 |
|
1098 lemma nn_integral_noteq_infinite: |
|
1099 assumes g: "g \<in> borel_measurable M" and "integral\<^sup>N M g \<noteq> \<infinity>" |
|
1100 shows "AE x in M. g x \<noteq> \<infinity>" |
|
1101 proof (rule ccontr) |
|
1102 assume c: "\<not> (AE x in M. g x \<noteq> \<infinity>)" |
|
1103 have "(emeasure M) {x\<in>space M. g x = \<infinity>} \<noteq> 0" |
|
1104 using c g by (auto simp add: AE_iff_null) |
|
1105 then have "0 < (emeasure M) {x\<in>space M. g x = \<infinity>}" |
|
1106 by (auto simp: zero_less_iff_neq_zero) |
|
1107 then have "\<infinity> = \<infinity> * (emeasure M) {x\<in>space M. g x = \<infinity>}" |
|
1108 by (auto simp: ennreal_top_eq_mult_iff) |
|
1109 also have "\<dots> \<le> (\<integral>\<^sup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)" |
|
1110 using g by (subst nn_integral_cmult_indicator) auto |
|
1111 also have "\<dots> \<le> integral\<^sup>N M g" |
|
1112 using assms by (auto intro!: nn_integral_mono_AE simp: indicator_def) |
|
1113 finally show False |
|
1114 using \<open>integral\<^sup>N M g \<noteq> \<infinity>\<close> by (auto simp: top_unique) |
|
1115 qed |
|
1116 |
|
1117 lemma nn_integral_PInf: |
|
1118 assumes f: "f \<in> borel_measurable M" and not_Inf: "integral\<^sup>N M f \<noteq> \<infinity>" |
|
1119 shows "emeasure M (f -` {\<infinity>} \<inter> space M) = 0" |
|
1120 proof - |
|
1121 have "\<infinity> * emeasure M (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)" |
|
1122 using f by (subst nn_integral_cmult_indicator) (auto simp: measurable_sets) |
|
1123 also have "\<dots> \<le> integral\<^sup>N M f" |
|
1124 by (auto intro!: nn_integral_mono simp: indicator_def) |
|
1125 finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>N M f" |
|
1126 by simp |
|
1127 then show ?thesis |
|
1128 using assms by (auto simp: ennreal_top_mult top_unique split: if_split_asm) |
|
1129 qed |
|
1130 |
|
1131 lemma simple_integral_PInf: |
|
1132 "simple_function M f \<Longrightarrow> integral\<^sup>S M f \<noteq> \<infinity> \<Longrightarrow> emeasure M (f -` {\<infinity>} \<inter> space M) = 0" |
|
1133 by (rule nn_integral_PInf) (auto simp: nn_integral_eq_simple_integral borel_measurable_simple_function) |
|
1134 |
|
1135 lemma nn_integral_PInf_AE: |
|
1136 assumes "f \<in> borel_measurable M" "integral\<^sup>N M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>" |
|
1137 proof (rule AE_I) |
|
1138 show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0" |
|
1139 by (rule nn_integral_PInf[OF assms]) |
|
1140 show "f -` {\<infinity>} \<inter> space M \<in> sets M" |
|
1141 using assms by (auto intro: borel_measurable_vimage) |
|
1142 qed auto |
|
1143 |
|
1144 lemma nn_integral_diff: |
|
1145 assumes f: "f \<in> borel_measurable M" |
|
1146 and g: "g \<in> borel_measurable M" |
|
1147 and fin: "integral\<^sup>N M g \<noteq> \<infinity>" |
|
1148 and mono: "AE x in M. g x \<le> f x" |
|
1149 shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>N M f - integral\<^sup>N M g" |
|
1150 proof - |
|
1151 have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
|
1152 using assms by auto |
|
1153 have "AE x in M. f x = f x - g x + g x" |
|
1154 using diff_add_cancel_ennreal mono nn_integral_noteq_infinite[OF g fin] assms by auto |
|
1155 then have **: "integral\<^sup>N M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>N M g" |
|
1156 unfolding nn_integral_add[OF diff g, symmetric] |
|
1157 by (rule nn_integral_cong_AE) |
|
1158 show ?thesis unfolding ** |
|
1159 using fin |
|
1160 by (cases rule: ennreal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>N M g"]) auto |
|
1161 qed |
|
1162 |
|
1163 lemma nn_integral_mult_bounded_inf: |
|
1164 assumes f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and c: "c \<noteq> \<infinity>" and ae: "AE x in M. g x \<le> c * f x" |
|
1165 shows "(\<integral>\<^sup>+x. g x \<partial>M) < \<infinity>" |
|
1166 proof - |
|
1167 have "(\<integral>\<^sup>+x. g x \<partial>M) \<le> (\<integral>\<^sup>+x. c * f x \<partial>M)" |
|
1168 by (intro nn_integral_mono_AE ae) |
|
1169 also have "(\<integral>\<^sup>+x. c * f x \<partial>M) < \<infinity>" |
|
1170 using c f by (subst nn_integral_cmult) (auto simp: ennreal_mult_less_top top_unique not_less) |
|
1171 finally show ?thesis . |
|
1172 qed |
|
1173 |
|
1174 text \<open>Fatou's lemma: convergence theorem on limes inferior\<close> |
|
1175 |
|
1176 lemma nn_integral_monotone_convergence_INF_AE': |
|
1177 assumes f: "\<And>i. AE x in M. f (Suc i) x \<le> f i x" and [measurable]: "\<And>i. f i \<in> borel_measurable M" |
|
1178 and *: "(\<integral>\<^sup>+ x. f 0 x \<partial>M) < \<infinity>" |
|
1179 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
|
1180 proof (rule ennreal_minus_cancel) |
|
1181 have "integral\<^sup>N M (f 0) - (\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (\<integral>\<^sup>+x. f 0 x - (INF i. f i x) \<partial>M)" |
|
1182 proof (rule nn_integral_diff[symmetric]) |
|
1183 have "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) \<le> (\<integral>\<^sup>+ x. f 0 x \<partial>M)" |
|
1184 by (intro nn_integral_mono INF_lower) simp |
|
1185 with * show "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) \<noteq> \<infinity>" |
|
1186 by simp |
|
1187 qed (auto intro: INF_lower) |
|
1188 also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. f 0 x - f i x) \<partial>M)" |
|
1189 by (simp add: ennreal_INF_const_minus) |
|
1190 also have "\<dots> = (SUP i. (\<integral>\<^sup>+x. f 0 x - f i x \<partial>M))" |
|
1191 proof (intro nn_integral_monotone_convergence_SUP_AE) |
|
1192 show "AE x in M. f 0 x - f i x \<le> f 0 x - f (Suc i) x" for i |
|
1193 using f[of i] by eventually_elim (auto simp: ennreal_mono_minus) |
|
1194 qed simp |
|
1195 also have "\<dots> = (SUP i. nn_integral M (f 0) - (\<integral>\<^sup>+x. f i x \<partial>M))" |
|
1196 proof (subst nn_integral_diff[symmetric]) |
|
1197 fix i |
|
1198 have dec: "AE x in M. \<forall>i. f (Suc i) x \<le> f i x" |
|
1199 unfolding AE_all_countable using f by auto |
|
1200 then show "AE x in M. f i x \<le> f 0 x" |
|
1201 using dec by eventually_elim (auto intro: lift_Suc_antimono_le[of "\<lambda>i. f i x" 0 i for x]) |
|
1202 then have "(\<integral>\<^sup>+ x. f i x \<partial>M) \<le> (\<integral>\<^sup>+ x. f 0 x \<partial>M)" |
|
1203 by (rule nn_integral_mono_AE) |
|
1204 with * show "(\<integral>\<^sup>+ x. f i x \<partial>M) \<noteq> \<infinity>" |
|
1205 by simp |
|
1206 qed (insert f, auto simp: decseq_def le_fun_def) |
|
1207 finally show "integral\<^sup>N M (f 0) - (\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = |
|
1208 integral\<^sup>N M (f 0) - (INF i. \<integral>\<^sup>+ x. f i x \<partial>M)" |
|
1209 by (simp add: ennreal_INF_const_minus) |
|
1210 qed (insert *, auto intro!: nn_integral_mono intro: INF_lower) |
|
1211 |
|
1212 lemma nn_integral_monotone_convergence_INF_AE: |
|
1213 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
|
1214 assumes f: "\<And>i. AE x in M. f (Suc i) x \<le> f i x" |
|
1215 and [measurable]: "\<And>i. f i \<in> borel_measurable M" |
|
1216 and fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
|
1217 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
|
1218 proof - |
|
1219 { fix f :: "nat \<Rightarrow> ennreal" and j assume "decseq f" |
|
1220 then have "(INF i. f i) = (INF i. f (i + j))" |
|
1221 apply (intro INF_eq) |
|
1222 apply (rule_tac x="i" in bexI) |
|
1223 apply (auto simp: decseq_def le_fun_def) |
|
1224 done } |
|
1225 note INF_shift = this |
|
1226 have mono: "AE x in M. \<forall>i. f (Suc i) x \<le> f i x" |
|
1227 using f by (auto simp: AE_all_countable) |
|
1228 then have "AE x in M. (INF i. f i x) = (INF n. f (n + i) x)" |
|
1229 by eventually_elim (auto intro!: decseq_SucI INF_shift) |
|
1230 then have "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (INF n. f (n + i) x) \<partial>M)" |
|
1231 by (rule nn_integral_cong_AE) |
|
1232 also have "\<dots> = (INF n. (\<integral>\<^sup>+ x. f (n + i) x \<partial>M))" |
|
1233 by (rule nn_integral_monotone_convergence_INF_AE') (insert assms, auto) |
|
1234 also have "\<dots> = (INF n. (\<integral>\<^sup>+ x. f n x \<partial>M))" |
|
1235 by (intro INF_shift[symmetric] decseq_SucI nn_integral_mono_AE f) |
|
1236 finally show ?thesis . |
|
1237 qed |
|
1238 |
|
1239 lemma nn_integral_monotone_convergence_INF_decseq: |
|
1240 assumes f: "decseq f" and *: "\<And>i. f i \<in> borel_measurable M" "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
|
1241 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
|
1242 using nn_integral_monotone_convergence_INF_AE[of f M i, OF _ *] f by (auto simp: decseq_Suc_iff le_fun_def) |
|
1243 |
|
1244 lemma nn_integral_liminf: |
|
1245 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
|
1246 assumes u: "\<And>i. u i \<in> borel_measurable M" |
|
1247 shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
|
1248 proof - |
|
1249 have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)" |
|
1250 unfolding liminf_SUP_INF using u |
|
1251 by (intro nn_integral_monotone_convergence_SUP_AE) |
|
1252 (auto intro!: AE_I2 intro: INF_greatest INF_superset_mono) |
|
1253 also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
|
1254 by (auto simp: liminf_SUP_INF intro!: SUP_mono INF_greatest nn_integral_mono INF_lower) |
|
1255 finally show ?thesis . |
|
1256 qed |
|
1257 |
|
1258 lemma nn_integral_limsup: |
|
1259 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
|
1260 assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M" |
|
1261 assumes bounds: "\<And>i. AE x in M. u i x \<le> w x" and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
|
1262 shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)" |
|
1263 proof - |
|
1264 have bnd: "AE x in M. \<forall>i. u i x \<le> w x" |
|
1265 using bounds by (auto simp: AE_all_countable) |
|
1266 then have "(\<integral>\<^sup>+ x. (SUP n. u n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. w x \<partial>M)" |
|
1267 by (auto intro!: nn_integral_mono_AE elim: eventually_mono intro: SUP_least) |
|
1268 then have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (INF n. \<integral>\<^sup>+ x. (SUP i:{n..}. u i x) \<partial>M)" |
|
1269 unfolding limsup_INF_SUP using bnd w |
|
1270 by (intro nn_integral_monotone_convergence_INF_AE') |
|
1271 (auto intro!: AE_I2 intro: SUP_least SUP_subset_mono) |
|
1272 also have "\<dots> \<ge> limsup (\<lambda>n. integral\<^sup>N M (u n))" |
|
1273 by (auto simp: limsup_INF_SUP intro!: INF_mono SUP_least exI nn_integral_mono SUP_upper) |
|
1274 finally (xtrans) show ?thesis . |
|
1275 qed |
|
1276 |
|
1277 lemma nn_integral_LIMSEQ: |
|
1278 assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" |
|
1279 and u: "\<And>x. (\<lambda>i. f i x) \<longlonglongrightarrow> u x" |
|
1280 shows "(\<lambda>n. integral\<^sup>N M (f n)) \<longlonglongrightarrow> integral\<^sup>N M u" |
|
1281 proof - |
|
1282 have "(\<lambda>n. integral\<^sup>N M (f n)) \<longlonglongrightarrow> (SUP n. integral\<^sup>N M (f n))" |
|
1283 using f by (intro LIMSEQ_SUP[of "\<lambda>n. integral\<^sup>N M (f n)"] incseq_nn_integral) |
|
1284 also have "(SUP n. integral\<^sup>N M (f n)) = integral\<^sup>N M (\<lambda>x. SUP n. f n x)" |
|
1285 using f by (intro nn_integral_monotone_convergence_SUP[symmetric]) |
|
1286 also have "integral\<^sup>N M (\<lambda>x. SUP n. f n x) = integral\<^sup>N M (\<lambda>x. u x)" |
|
1287 using f by (subst LIMSEQ_SUP[THEN LIMSEQ_unique, OF _ u]) (auto simp: incseq_def le_fun_def) |
|
1288 finally show ?thesis . |
|
1289 qed |
|
1290 |
|
1291 lemma nn_integral_dominated_convergence: |
|
1292 assumes [measurable]: |
|
1293 "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M" |
|
1294 and bound: "\<And>j. AE x in M. u j x \<le> w x" |
|
1295 and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
|
1296 and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
|
1297 shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. u' x \<partial>M)" |
|
1298 proof - |
|
1299 have "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)" |
|
1300 by (intro nn_integral_limsup[OF _ _ bound w]) auto |
|
1301 moreover have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)" |
|
1302 using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot) |
|
1303 moreover have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)" |
|
1304 using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot) |
|
1305 moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
|
1306 by (intro nn_integral_liminf) auto |
|
1307 moreover have "liminf (\<lambda>n. integral\<^sup>N M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>N M (u n))" |
|
1308 by (intro Liminf_le_Limsup sequentially_bot) |
|
1309 ultimately show ?thesis |
|
1310 by (intro Liminf_eq_Limsup) auto |
|
1311 qed |
|
1312 |
|
1313 lemma inf_continuous_nn_integral[order_continuous_intros]: |
|
1314 assumes f: "\<And>y. inf_continuous (f y)" |
|
1315 assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M" |
|
1316 assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>" |
|
1317 shows "inf_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
|
1318 unfolding inf_continuous_def |
|
1319 proof safe |
|
1320 fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C" |
|
1321 then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
|
1322 using inf_continuous_mono[OF f] bnd |
|
1323 by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top |
|
1324 intro!: nn_integral_monotone_convergence_INF_decseq) |
|
1325 qed |
|
1326 |
|
1327 lemma nn_integral_null_set: |
|
1328 assumes "N \<in> null_sets M" shows "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = 0" |
|
1329 proof - |
|
1330 have "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)" |
|
1331 proof (intro nn_integral_cong_AE AE_I) |
|
1332 show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N" |
|
1333 by (auto simp: indicator_def) |
|
1334 show "(emeasure M) N = 0" "N \<in> sets M" |
|
1335 using assms by auto |
|
1336 qed |
|
1337 then show ?thesis by simp |
|
1338 qed |
|
1339 |
|
1340 lemma nn_integral_0_iff: |
|
1341 assumes u: "u \<in> borel_measurable M" |
|
1342 shows "integral\<^sup>N M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0" |
|
1343 (is "_ \<longleftrightarrow> (emeasure M) ?A = 0") |
|
1344 proof - |
|
1345 have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>N M u" |
|
1346 by (auto intro!: nn_integral_cong simp: indicator_def) |
|
1347 show ?thesis |
|
1348 proof |
|
1349 assume "(emeasure M) ?A = 0" |
|
1350 with nn_integral_null_set[of ?A M u] u |
|
1351 show "integral\<^sup>N M u = 0" by (simp add: u_eq null_sets_def) |
|
1352 next |
|
1353 assume *: "integral\<^sup>N M u = 0" |
|
1354 let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}" |
|
1355 have "0 = (SUP n. (emeasure M) (?M n \<inter> ?A))" |
|
1356 proof - |
|
1357 { fix n :: nat |
|
1358 from nn_integral_Markov_inequality[OF u, of ?A "of_nat n"] u |
|
1359 have "(emeasure M) (?M n \<inter> ?A) \<le> 0" |
|
1360 by (simp add: ennreal_of_nat_eq_real_of_nat u_eq *) |
|
1361 moreover have "0 \<le> (emeasure M) (?M n \<inter> ?A)" using u by auto |
|
1362 ultimately have "(emeasure M) (?M n \<inter> ?A) = 0" by auto } |
|
1363 thus ?thesis by simp |
|
1364 qed |
|
1365 also have "\<dots> = (emeasure M) (\<Union>n. ?M n \<inter> ?A)" |
|
1366 proof (safe intro!: SUP_emeasure_incseq) |
|
1367 fix n show "?M n \<inter> ?A \<in> sets M" |
|
1368 using u by (auto intro!: sets.Int) |
|
1369 next |
|
1370 show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})" |
|
1371 proof (safe intro!: incseq_SucI) |
|
1372 fix n :: nat and x |
|
1373 assume *: "1 \<le> real n * u x" |
|
1374 also have "real n * u x \<le> real (Suc n) * u x" |
|
1375 by (auto intro!: mult_right_mono) |
|
1376 finally show "1 \<le> real (Suc n) * u x" by auto |
|
1377 qed |
|
1378 qed |
|
1379 also have "\<dots> = (emeasure M) {x\<in>space M. 0 < u x}" |
|
1380 proof (safe intro!: arg_cong[where f="(emeasure M)"]) |
|
1381 fix x assume "0 < u x" and [simp, intro]: "x \<in> space M" |
|
1382 show "x \<in> (\<Union>n. ?M n \<inter> ?A)" |
|
1383 proof (cases "u x" rule: ennreal_cases) |
|
1384 case (real r) with \<open>0 < u x\<close> have "0 < r" by auto |
|
1385 obtain j :: nat where "1 / r \<le> real j" using real_arch_simple .. |
|
1386 hence "1 / r * r \<le> real j * r" unfolding mult_le_cancel_right using \<open>0 < r\<close> by auto |
|
1387 hence "1 \<le> real j * r" using real \<open>0 < r\<close> by auto |
|
1388 thus ?thesis using \<open>0 < r\<close> real |
|
1389 by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_1[symmetric] ennreal_mult[symmetric] |
|
1390 simp del: ennreal_1) |
|
1391 qed (insert \<open>0 < u x\<close>, auto simp: ennreal_mult_top) |
|
1392 qed (auto simp: zero_less_iff_neq_zero) |
|
1393 finally show "emeasure M ?A = 0" |
|
1394 by (simp add: zero_less_iff_neq_zero) |
|
1395 qed |
|
1396 qed |
|
1397 |
|
1398 lemma nn_integral_0_iff_AE: |
|
1399 assumes u: "u \<in> borel_measurable M" |
|
1400 shows "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. u x = 0)" |
|
1401 proof - |
|
1402 have sets: "{x\<in>space M. u x \<noteq> 0} \<in> sets M" |
|
1403 using u by auto |
|
1404 show "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. u x = 0)" |
|
1405 using nn_integral_0_iff[of u] AE_iff_null[OF sets] u by auto |
|
1406 qed |
|
1407 |
|
1408 lemma AE_iff_nn_integral: |
|
1409 "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^sup>N M (indicator {x. \<not> P x}) = 0" |
|
1410 by (subst nn_integral_0_iff_AE) (auto simp: indicator_def[abs_def]) |
|
1411 |
|
1412 lemma nn_integral_less: |
|
1413 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
1414 assumes f: "(\<integral>\<^sup>+x. f x \<partial>M) \<noteq> \<infinity>" |
|
1415 assumes ord: "AE x in M. f x \<le> g x" "\<not> (AE x in M. g x \<le> f x)" |
|
1416 shows "(\<integral>\<^sup>+x. f x \<partial>M) < (\<integral>\<^sup>+x. g x \<partial>M)" |
|
1417 proof - |
|
1418 have "0 < (\<integral>\<^sup>+x. g x - f x \<partial>M)" |
|
1419 proof (intro order_le_neq_trans notI) |
|
1420 assume "0 = (\<integral>\<^sup>+x. g x - f x \<partial>M)" |
|
1421 then have "AE x in M. g x - f x = 0" |
|
1422 using nn_integral_0_iff_AE[of "\<lambda>x. g x - f x" M] by simp |
|
1423 with ord(1) have "AE x in M. g x \<le> f x" |
|
1424 by eventually_elim (auto simp: ennreal_minus_eq_0) |
|
1425 with ord show False |
|
1426 by simp |
|
1427 qed simp |
|
1428 also have "\<dots> = (\<integral>\<^sup>+x. g x \<partial>M) - (\<integral>\<^sup>+x. f x \<partial>M)" |
|
1429 using f by (subst nn_integral_diff) (auto simp: ord) |
|
1430 finally show ?thesis |
|
1431 using f by (auto dest!: ennreal_minus_pos_iff[rotated] simp: less_top) |
|
1432 qed |
|
1433 |
|
1434 lemma nn_integral_subalgebra: |
|
1435 assumes f: "f \<in> borel_measurable N" |
|
1436 and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A" |
|
1437 shows "integral\<^sup>N N f = integral\<^sup>N M f" |
|
1438 proof - |
|
1439 have [simp]: "\<And>f :: 'a \<Rightarrow> ennreal. f \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable M" |
|
1440 using N by (auto simp: measurable_def) |
|
1441 have [simp]: "\<And>P. (AE x in N. P x) \<Longrightarrow> (AE x in M. P x)" |
|
1442 using N by (auto simp add: eventually_ae_filter null_sets_def subset_eq) |
|
1443 have [simp]: "\<And>A. A \<in> sets N \<Longrightarrow> A \<in> sets M" |
|
1444 using N by auto |
|
1445 from f show ?thesis |
|
1446 apply induct |
|
1447 apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N) |
|
1448 apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric]) |
|
1449 done |
|
1450 qed |
|
1451 |
|
1452 lemma nn_integral_nat_function: |
|
1453 fixes f :: "'a \<Rightarrow> nat" |
|
1454 assumes "f \<in> measurable M (count_space UNIV)" |
|
1455 shows "(\<integral>\<^sup>+x. of_nat (f x) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})" |
|
1456 proof - |
|
1457 define F where "F i = {x\<in>space M. i < f x}" for i |
|
1458 with assms have [measurable]: "\<And>i. F i \<in> sets M" |
|
1459 by auto |
|
1460 |
|
1461 { fix x assume "x \<in> space M" |
|
1462 have "(\<lambda>i. if i < f x then 1 else 0) sums (of_nat (f x)::real)" |
|
1463 using sums_If_finite[of "\<lambda>i. i < f x" "\<lambda>_. 1::real"] by simp |
|
1464 then have "(\<lambda>i. ennreal (if i < f x then 1 else 0)) sums of_nat(f x)" |
|
1465 unfolding ennreal_of_nat_eq_real_of_nat |
|
1466 by (subst sums_ennreal) auto |
|
1467 moreover have "\<And>i. ennreal (if i < f x then 1 else 0) = indicator (F i) x" |
|
1468 using \<open>x \<in> space M\<close> by (simp add: one_ennreal_def F_def) |
|
1469 ultimately have "of_nat (f x) = (\<Sum>i. indicator (F i) x :: ennreal)" |
|
1470 by (simp add: sums_iff) } |
|
1471 then have "(\<integral>\<^sup>+x. of_nat (f x) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)" |
|
1472 by (simp cong: nn_integral_cong) |
|
1473 also have "\<dots> = (\<Sum>i. emeasure M (F i))" |
|
1474 by (simp add: nn_integral_suminf) |
|
1475 finally show ?thesis |
|
1476 by (simp add: F_def) |
|
1477 qed |
|
1478 |
|
1479 lemma nn_integral_lfp: |
|
1480 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
|
1481 assumes f: "sup_continuous f" |
|
1482 assumes g: "sup_continuous g" |
|
1483 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
|
1484 assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s" |
|
1485 shows "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = lfp g s" |
|
1486 proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f and P="\<lambda>f. f \<in> borel_measurable N", symmetric]) |
|
1487 fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ennreal" assume "incseq C" "\<And>i. C i \<in> borel_measurable N" |
|
1488 then show "(\<lambda>s. \<integral>\<^sup>+x. (SUP i. C i) x \<partial>M s) = (SUP i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))" |
|
1489 unfolding SUP_apply[abs_def] |
|
1490 by (subst nn_integral_monotone_convergence_SUP) |
|
1491 (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets) |
|
1492 qed (auto simp add: step le_fun_def SUP_apply[abs_def] bot_fun_def bot_ennreal intro!: meas f g) |
|
1493 |
|
1494 lemma nn_integral_gfp: |
|
1495 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
|
1496 assumes f: "inf_continuous f" and g: "inf_continuous g" |
|
1497 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
|
1498 assumes bound: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>" |
|
1499 assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0" |
|
1500 assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s" |
|
1501 shows "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = gfp g s" |
|
1502 proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f |
|
1503 and P="\<lambda>F. F \<in> borel_measurable N \<and> (\<forall>s. (\<integral>\<^sup>+x. F x \<partial>M s) < \<infinity>)", symmetric]) |
|
1504 fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ennreal" assume "decseq C" "\<And>i. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" |
|
1505 then show "(\<lambda>s. \<integral>\<^sup>+x. (INF i. C i) x \<partial>M s) = (INF i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))" |
|
1506 unfolding INF_apply[abs_def] |
|
1507 by (subst nn_integral_monotone_convergence_INF_decseq) |
|
1508 (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets) |
|
1509 next |
|
1510 show "\<And>x. g x \<le> (\<lambda>s. integral\<^sup>N (M s) (f top))" |
|
1511 by (subst step) |
|
1512 (auto simp add: top_fun_def less_le non_zero le_fun_def ennreal_top_mult |
|
1513 cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD]) |
|
1514 next |
|
1515 fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C" |
|
1516 with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)" |
|
1517 unfolding INF_apply[abs_def] |
|
1518 by (subst nn_integral_monotone_convergence_INF_decseq) |
|
1519 (auto simp: INF_less_iff cong: measurable_cong_sets intro!: borel_measurable_INF) |
|
1520 next |
|
1521 show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow> |
|
1522 (\<lambda>s. integral\<^sup>N (M s) (f x)) = g (\<lambda>s. integral\<^sup>N (M s) x)" |
|
1523 by (subst step) auto |
|
1524 qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g) |
|
1525 |
|
1526 subsection \<open>Integral under concrete measures\<close> |
|
1527 |
|
1528 lemma nn_integral_mono_measure: |
|
1529 assumes "sets M = sets N" "M \<le> N" shows "nn_integral M f \<le> nn_integral N f" |
|
1530 unfolding nn_integral_def |
|
1531 proof (intro SUP_subset_mono) |
|
1532 note \<open>sets M = sets N\<close>[simp] \<open>sets M = sets N\<close>[THEN sets_eq_imp_space_eq, simp] |
|
1533 show "{g. simple_function M g \<and> g \<le> f} \<subseteq> {g. simple_function N g \<and> g \<le> f}" |
|
1534 by (simp add: simple_function_def) |
|
1535 show "integral\<^sup>S M x \<le> integral\<^sup>S N x" for x |
|
1536 using le_measureD3[OF \<open>M \<le> N\<close>] |
|
1537 by (auto simp add: simple_integral_def intro!: setsum_mono mult_mono) |
|
1538 qed |
|
1539 |
|
1540 lemma nn_integral_empty: |
|
1541 assumes "space M = {}" |
|
1542 shows "nn_integral M f = 0" |
|
1543 proof - |
|
1544 have "(\<integral>\<^sup>+ x. f x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)" |
|
1545 by(rule nn_integral_cong)(simp add: assms) |
|
1546 thus ?thesis by simp |
|
1547 qed |
|
1548 |
|
1549 lemma nn_integral_bot[simp]: "nn_integral bot f = 0" |
|
1550 by (simp add: nn_integral_empty) |
|
1551 |
|
1552 subsubsection \<open>Distributions\<close> |
|
1553 |
|
1554 lemma nn_integral_distr: |
|
1555 assumes T: "T \<in> measurable M M'" and f: "f \<in> borel_measurable (distr M M' T)" |
|
1556 shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)" |
|
1557 using f |
|
1558 proof induct |
|
1559 case (cong f g) |
|
1560 with T show ?case |
|
1561 apply (subst nn_integral_cong[of _ f g]) |
|
1562 apply simp |
|
1563 apply (subst nn_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"]) |
|
1564 apply (simp add: measurable_def Pi_iff) |
|
1565 apply simp |
|
1566 done |
|
1567 next |
|
1568 case (set A) |
|
1569 then have eq: "\<And>x. x \<in> space M \<Longrightarrow> indicator A (T x) = indicator (T -` A \<inter> space M) x" |
|
1570 by (auto simp: indicator_def) |
|
1571 from set T show ?case |
|
1572 by (subst nn_integral_cong[OF eq]) |
|
1573 (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets) |
|
1574 qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add |
|
1575 nn_integral_monotone_convergence_SUP le_fun_def incseq_def) |
|
1576 |
|
1577 subsubsection \<open>Counting space\<close> |
|
1578 |
|
1579 lemma simple_function_count_space[simp]: |
|
1580 "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)" |
|
1581 unfolding simple_function_def by simp |
|
1582 |
|
1583 lemma nn_integral_count_space: |
|
1584 assumes A: "finite {a\<in>A. 0 < f a}" |
|
1585 shows "integral\<^sup>N (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)" |
|
1586 proof - |
|
1587 have *: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>count_space A) = |
|
1588 (\<integral>\<^sup>+ x. (\<Sum>a|a\<in>A \<and> 0 < f a. f a * indicator {a} x) \<partial>count_space A)" |
|
1589 by (auto intro!: nn_integral_cong |
|
1590 simp add: indicator_def if_distrib setsum.If_cases[OF A] max_def le_less) |
|
1591 also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. \<integral>\<^sup>+ x. f a * indicator {a} x \<partial>count_space A)" |
|
1592 by (subst nn_integral_setsum) (simp_all add: AE_count_space less_imp_le) |
|
1593 also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)" |
|
1594 by (auto intro!: setsum.cong simp: one_ennreal_def[symmetric] max_def) |
|
1595 finally show ?thesis by (simp add: max.absorb2) |
|
1596 qed |
|
1597 |
|
1598 lemma nn_integral_count_space_finite: |
|
1599 "finite A \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)" |
|
1600 by (auto intro!: setsum.mono_neutral_left simp: nn_integral_count_space less_le) |
|
1601 |
|
1602 lemma nn_integral_count_space': |
|
1603 assumes "finite A" "\<And>x. x \<in> B \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0" "A \<subseteq> B" |
|
1604 shows "(\<integral>\<^sup>+x. f x \<partial>count_space B) = (\<Sum>x\<in>A. f x)" |
|
1605 proof - |
|
1606 have "(\<integral>\<^sup>+x. f x \<partial>count_space B) = (\<Sum>a | a \<in> B \<and> 0 < f a. f a)" |
|
1607 using assms(2,3) |
|
1608 by (intro nn_integral_count_space finite_subset[OF _ \<open>finite A\<close>]) (auto simp: less_le) |
|
1609 also have "\<dots> = (\<Sum>a\<in>A. f a)" |
|
1610 using assms by (intro setsum.mono_neutral_cong_left) (auto simp: less_le) |
|
1611 finally show ?thesis . |
|
1612 qed |
|
1613 |
|
1614 lemma nn_integral_bij_count_space: |
|
1615 assumes g: "bij_betw g A B" |
|
1616 shows "(\<integral>\<^sup>+x. f (g x) \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)" |
|
1617 using g[THEN bij_betw_imp_funcset] |
|
1618 by (subst distr_bij_count_space[OF g, symmetric]) |
|
1619 (auto intro!: nn_integral_distr[symmetric]) |
|
1620 |
|
1621 lemma nn_integral_indicator_finite: |
|
1622 fixes f :: "'a \<Rightarrow> ennreal" |
|
1623 assumes f: "finite A" and [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M" |
|
1624 shows "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<Sum>x\<in>A. f x * emeasure M {x})" |
|
1625 proof - |
|
1626 from f have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)" |
|
1627 by (intro nn_integral_cong) (auto simp: indicator_def if_distrib[where f="\<lambda>a. x * a" for x] setsum.If_cases) |
|
1628 also have "\<dots> = (\<Sum>a\<in>A. f a * emeasure M {a})" |
|
1629 by (subst nn_integral_setsum) auto |
|
1630 finally show ?thesis . |
|
1631 qed |
|
1632 |
|
1633 lemma nn_integral_count_space_nat: |
|
1634 fixes f :: "nat \<Rightarrow> ennreal" |
|
1635 shows "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) = (\<Sum>i. f i)" |
|
1636 proof - |
|
1637 have "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) = |
|
1638 (\<integral>\<^sup>+i. (\<Sum>j. f j * indicator {j} i) \<partial>count_space UNIV)" |
|
1639 proof (intro nn_integral_cong) |
|
1640 fix i |
|
1641 have "f i = (\<Sum>j\<in>{i}. f j * indicator {j} i)" |
|
1642 by simp |
|
1643 also have "\<dots> = (\<Sum>j. f j * indicator {j} i)" |
|
1644 by (rule suminf_finite[symmetric]) auto |
|
1645 finally show "f i = (\<Sum>j. f j * indicator {j} i)" . |
|
1646 qed |
|
1647 also have "\<dots> = (\<Sum>j. (\<integral>\<^sup>+i. f j * indicator {j} i \<partial>count_space UNIV))" |
|
1648 by (rule nn_integral_suminf) auto |
|
1649 finally show ?thesis |
|
1650 by simp |
|
1651 qed |
|
1652 |
|
1653 lemma nn_integral_enat_function: |
|
1654 assumes f: "f \<in> measurable M (count_space UNIV)" |
|
1655 shows "(\<integral>\<^sup>+ x. ennreal_of_enat (f x) \<partial>M) = (\<Sum>t. emeasure M {x \<in> space M. t < f x})" |
|
1656 proof - |
|
1657 define F where "F i = {x\<in>space M. i < f x}" for i :: nat |
|
1658 with assms have [measurable]: "\<And>i. F i \<in> sets M" |
|
1659 by auto |
|
1660 |
|
1661 { fix x assume "x \<in> space M" |
|
1662 have "(\<lambda>i::nat. if i < f x then 1 else 0) sums ennreal_of_enat (f x)" |
|
1663 using sums_If_finite[of "\<lambda>r. r < f x" "\<lambda>_. 1 :: ennreal"] |
|
1664 by (cases "f x") (simp_all add: sums_def of_nat_tendsto_top_ennreal) |
|
1665 also have "(\<lambda>i. (if i < f x then 1 else 0)) = (\<lambda>i. indicator (F i) x)" |
|
1666 using \<open>x \<in> space M\<close> by (simp add: one_ennreal_def F_def fun_eq_iff) |
|
1667 finally have "ennreal_of_enat (f x) = (\<Sum>i. indicator (F i) x)" |
|
1668 by (simp add: sums_iff) } |
|
1669 then have "(\<integral>\<^sup>+x. ennreal_of_enat (f x) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)" |
|
1670 by (simp cong: nn_integral_cong) |
|
1671 also have "\<dots> = (\<Sum>i. emeasure M (F i))" |
|
1672 by (simp add: nn_integral_suminf) |
|
1673 finally show ?thesis |
|
1674 by (simp add: F_def) |
|
1675 qed |
|
1676 |
|
1677 lemma nn_integral_count_space_nn_integral: |
|
1678 fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ennreal" |
|
1679 assumes "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M" |
|
1680 shows "(\<integral>\<^sup>+x. \<integral>\<^sup>+i. f i x \<partial>count_space I \<partial>M) = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. f i x \<partial>M \<partial>count_space I)" |
|
1681 proof cases |
|
1682 assume "finite I" then show ?thesis |
|
1683 by (simp add: nn_integral_count_space_finite nn_integral_setsum) |
|
1684 next |
|
1685 assume "infinite I" |
|
1686 then have [simp]: "I \<noteq> {}" |
|
1687 by auto |
|
1688 note * = bij_betw_from_nat_into[OF \<open>countable I\<close> \<open>infinite I\<close>] |
|
1689 have **: "\<And>f. (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<integral>\<^sup>+i. f i \<partial>count_space I) = (\<Sum>n. f (from_nat_into I n))" |
|
1690 by (simp add: nn_integral_bij_count_space[symmetric, OF *] nn_integral_count_space_nat) |
|
1691 show ?thesis |
|
1692 by (simp add: ** nn_integral_suminf from_nat_into) |
|
1693 qed |
|
1694 |
|
1695 lemma emeasure_UN_countable: |
|
1696 assumes sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I" |
|
1697 assumes disj: "disjoint_family_on X I" |
|
1698 shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)" |
|
1699 proof - |
|
1700 have eq: "\<And>x. indicator (UNION I X) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I" |
|
1701 proof cases |
|
1702 fix x assume x: "x \<in> UNION I X" |
|
1703 then obtain j where j: "x \<in> X j" "j \<in> I" |
|
1704 by auto |
|
1705 with disj have "\<And>i. i \<in> I \<Longrightarrow> indicator (X i) x = (indicator {j} i::ennreal)" |
|
1706 by (auto simp: disjoint_family_on_def split: split_indicator) |
|
1707 with x j show "?thesis x" |
|
1708 by (simp cong: nn_integral_cong_simp) |
|
1709 qed (auto simp: nn_integral_0_iff_AE) |
|
1710 |
|
1711 note sets.countable_UN'[unfolded subset_eq, measurable] |
|
1712 have "emeasure M (UNION I X) = (\<integral>\<^sup>+x. indicator (UNION I X) x \<partial>M)" |
|
1713 by simp |
|
1714 also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>count_space I)" |
|
1715 by (simp add: eq nn_integral_count_space_nn_integral) |
|
1716 finally show ?thesis |
|
1717 by (simp cong: nn_integral_cong_simp) |
|
1718 qed |
|
1719 |
|
1720 lemma emeasure_countable_singleton: |
|
1721 assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" and X: "countable X" |
|
1722 shows "emeasure M X = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)" |
|
1723 proof - |
|
1724 have "emeasure M (\<Union>i\<in>X. {i}) = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)" |
|
1725 using assms by (intro emeasure_UN_countable) (auto simp: disjoint_family_on_def) |
|
1726 also have "(\<Union>i\<in>X. {i}) = X" by auto |
|
1727 finally show ?thesis . |
|
1728 qed |
|
1729 |
|
1730 lemma measure_eqI_countable: |
|
1731 assumes [simp]: "sets M = Pow A" "sets N = Pow A" and A: "countable A" |
|
1732 assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}" |
|
1733 shows "M = N" |
|
1734 proof (rule measure_eqI) |
|
1735 fix X assume "X \<in> sets M" |
|
1736 then have X: "X \<subseteq> A" by auto |
|
1737 moreover from A X have "countable X" by (auto dest: countable_subset) |
|
1738 ultimately have |
|
1739 "emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)" |
|
1740 "emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)" |
|
1741 by (auto intro!: emeasure_countable_singleton) |
|
1742 moreover have "(\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X) = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)" |
|
1743 using X by (intro nn_integral_cong eq) auto |
|
1744 ultimately show "emeasure M X = emeasure N X" |
|
1745 by simp |
|
1746 qed simp |
|
1747 |
|
1748 lemma measure_eqI_countable_AE: |
|
1749 assumes [simp]: "sets M = UNIV" "sets N = UNIV" |
|
1750 assumes ae: "AE x in M. x \<in> \<Omega>" "AE x in N. x \<in> \<Omega>" and [simp]: "countable \<Omega>" |
|
1751 assumes eq: "\<And>x. x \<in> \<Omega> \<Longrightarrow> emeasure M {x} = emeasure N {x}" |
|
1752 shows "M = N" |
|
1753 proof (rule measure_eqI) |
|
1754 fix A |
|
1755 have "emeasure N A = emeasure N {x\<in>\<Omega>. x \<in> A}" |
|
1756 using ae by (intro emeasure_eq_AE) auto |
|
1757 also have "\<dots> = (\<integral>\<^sup>+x. emeasure N {x} \<partial>count_space {x\<in>\<Omega>. x \<in> A})" |
|
1758 by (intro emeasure_countable_singleton) auto |
|
1759 also have "\<dots> = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space {x\<in>\<Omega>. x \<in> A})" |
|
1760 by (intro nn_integral_cong eq[symmetric]) auto |
|
1761 also have "\<dots> = emeasure M {x\<in>\<Omega>. x \<in> A}" |
|
1762 by (intro emeasure_countable_singleton[symmetric]) auto |
|
1763 also have "\<dots> = emeasure M A" |
|
1764 using ae by (intro emeasure_eq_AE) auto |
|
1765 finally show "emeasure M A = emeasure N A" .. |
|
1766 qed simp |
|
1767 |
|
1768 lemma nn_integral_monotone_convergence_SUP_nat: |
|
1769 fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal" |
|
1770 assumes chain: "Complete_Partial_Order.chain op \<le> (f ` Y)" |
|
1771 and nonempty: "Y \<noteq> {}" |
|
1772 shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))" |
|
1773 (is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _") |
|
1774 proof (rule order_class.order.antisym) |
|
1775 show "?rhs \<le> ?lhs" |
|
1776 by (auto intro!: SUP_least SUP_upper nn_integral_mono) |
|
1777 next |
|
1778 have "\<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)" for x |
|
1779 by (rule ennreal_Sup_countable_SUP) (simp add: nonempty) |
|
1780 then obtain g where incseq: "\<And>x. incseq (g x)" |
|
1781 and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y" |
|
1782 and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura |
|
1783 from incseq have incseq': "incseq (\<lambda>i x. g x i)" |
|
1784 by(blast intro: incseq_SucI le_funI dest: incseq_SucD) |
|
1785 |
|
1786 have "?lhs = \<integral>\<^sup>+ x. (SUP i. g x i) \<partial>?M" by(simp add: sup) |
|
1787 also have "\<dots> = (SUP i. \<integral>\<^sup>+ x. g x i \<partial>?M)" using incseq' |
|
1788 by(rule nn_integral_monotone_convergence_SUP) simp |
|
1789 also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)" |
|
1790 proof(rule SUP_least) |
|
1791 fix n |
|
1792 have "\<And>x. \<exists>i. g x n = f i x \<and> i \<in> Y" using range by blast |
|
1793 then obtain I where I: "\<And>x. g x n = f (I x) x" "\<And>x. I x \<in> Y" by moura |
|
1794 |
|
1795 have "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) = (\<Sum>x. g x n)" |
|
1796 by(rule nn_integral_count_space_nat) |
|
1797 also have "\<dots> = (SUP m. \<Sum>x<m. g x n)" |
|
1798 by(rule suminf_eq_SUP) |
|
1799 also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)" |
|
1800 proof(rule SUP_mono) |
|
1801 fix m |
|
1802 show "\<exists>m'\<in>Y. (\<Sum>x<m. g x n) \<le> (\<integral>\<^sup>+ x. f m' x \<partial>?M)" |
|
1803 proof(cases "m > 0") |
|
1804 case False |
|
1805 thus ?thesis using nonempty by auto |
|
1806 next |
|
1807 case True |
|
1808 let ?Y = "I ` {..<m}" |
|
1809 have "f ` ?Y \<subseteq> f ` Y" using I by auto |
|
1810 with chain have chain': "Complete_Partial_Order.chain op \<le> (f ` ?Y)" by(rule chain_subset) |
|
1811 hence "Sup (f ` ?Y) \<in> f ` ?Y" |
|
1812 by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff) |
|
1813 then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto |
|
1814 have "I m' \<in> Y" using I by blast |
|
1815 have "(\<Sum>x<m. g x n) \<le> (\<Sum>x<m. f (I m') x)" |
|
1816 proof(rule setsum_mono) |
|
1817 fix x |
|
1818 assume "x \<in> {..<m}" |
|
1819 hence "x < m" by simp |
|
1820 have "g x n = f (I x) x" by(simp add: I) |
|
1821 also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image |
|
1822 using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI]) |
|
1823 also have "\<dots> = f (I m') x" unfolding m' by simp |
|
1824 finally show "g x n \<le> f (I m') x" . |
|
1825 qed |
|
1826 also have "\<dots> \<le> (SUP m. (\<Sum>x<m. f (I m') x))" |
|
1827 by(rule SUP_upper) simp |
|
1828 also have "\<dots> = (\<Sum>x. f (I m') x)" |
|
1829 by(rule suminf_eq_SUP[symmetric]) |
|
1830 also have "\<dots> = (\<integral>\<^sup>+ x. f (I m') x \<partial>?M)" |
|
1831 by(rule nn_integral_count_space_nat[symmetric]) |
|
1832 finally show ?thesis using \<open>I m' \<in> Y\<close> by blast |
|
1833 qed |
|
1834 qed |
|
1835 finally show "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) \<le> \<dots>" . |
|
1836 qed |
|
1837 finally show "?lhs \<le> ?rhs" . |
|
1838 qed |
|
1839 |
|
1840 lemma power_series_tendsto_at_left: |
|
1841 assumes nonneg: "\<And>i. 0 \<le> f i" and summable: "\<And>z. 0 \<le> z \<Longrightarrow> z < 1 \<Longrightarrow> summable (\<lambda>n. f n * z^n)" |
|
1842 shows "((\<lambda>z. ennreal (\<Sum>n. f n * z^n)) \<longlongrightarrow> (\<Sum>n. ennreal (f n))) (at_left (1::real))" |
|
1843 proof (intro tendsto_at_left_sequentially) |
|
1844 show "0 < (1::real)" by simp |
|
1845 fix S :: "nat \<Rightarrow> real" assume S: "\<And>n. S n < 1" "\<And>n. 0 < S n" "S \<longlonglongrightarrow> 1" "incseq S" |
|
1846 then have S_nonneg: "\<And>i. 0 \<le> S i" by (auto intro: less_imp_le) |
|
1847 |
|
1848 have "(\<lambda>i. (\<integral>\<^sup>+n. f n * S i^n \<partial>count_space UNIV)) \<longlonglongrightarrow> (\<integral>\<^sup>+n. ennreal (f n) \<partial>count_space UNIV)" |
|
1849 proof (rule nn_integral_LIMSEQ) |
|
1850 show "incseq (\<lambda>i n. ennreal (f n * S i^n))" |
|
1851 using S by (auto intro!: mult_mono power_mono nonneg ennreal_leI |
|
1852 simp: incseq_def le_fun_def less_imp_le) |
|
1853 fix n have "(\<lambda>i. ennreal (f n * S i^n)) \<longlonglongrightarrow> ennreal (f n * 1^n)" |
|
1854 by (intro tendsto_intros tendsto_ennrealI S) |
|
1855 then show "(\<lambda>i. ennreal (f n * S i^n)) \<longlonglongrightarrow> ennreal (f n)" |
|
1856 by simp |
|
1857 qed (auto simp: S_nonneg intro!: mult_nonneg_nonneg nonneg) |
|
1858 also have "(\<lambda>i. (\<integral>\<^sup>+n. f n * S i^n \<partial>count_space UNIV)) = (\<lambda>i. \<Sum>n. f n * S i^n)" |
|
1859 by (subst nn_integral_count_space_nat) |
|
1860 (intro ext suminf_ennreal2 mult_nonneg_nonneg nonneg S_nonneg |
|
1861 zero_le_power summable S)+ |
|
1862 also have "(\<integral>\<^sup>+n. ennreal (f n) \<partial>count_space UNIV) = (\<Sum>n. ennreal (f n))" |
|
1863 by (simp add: nn_integral_count_space_nat nonneg) |
|
1864 finally show "(\<lambda>n. ennreal (\<Sum>na. f na * S n ^ na)) \<longlonglongrightarrow> (\<Sum>n. ennreal (f n))" . |
|
1865 qed |
|
1866 |
|
1867 subsubsection \<open>Measures with Restricted Space\<close> |
|
1868 |
|
1869 lemma simple_function_restrict_space_ennreal: |
|
1870 fixes f :: "'a \<Rightarrow> ennreal" |
|
1871 assumes "\<Omega> \<inter> space M \<in> sets M" |
|
1872 shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator \<Omega> x)" |
|
1873 proof - |
|
1874 { assume "finite (f ` space (restrict_space M \<Omega>))" |
|
1875 then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp |
|
1876 then have "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)" |
|
1877 by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } |
|
1878 moreover |
|
1879 { assume "finite ((\<lambda>x. f x * indicator \<Omega> x) ` space M)" |
|
1880 then have "finite (f ` space (restrict_space M \<Omega>))" |
|
1881 by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } |
|
1882 ultimately show ?thesis |
|
1883 unfolding |
|
1884 simple_function_iff_borel_measurable borel_measurable_restrict_space_iff_ennreal[OF assms] |
|
1885 by auto |
|
1886 qed |
|
1887 |
|
1888 lemma simple_function_restrict_space: |
|
1889 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
|
1890 assumes "\<Omega> \<inter> space M \<in> sets M" |
|
1891 shows "simple_function (restrict_space M \<Omega>) f \<longleftrightarrow> simple_function M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)" |
|
1892 proof - |
|
1893 { assume "finite (f ` space (restrict_space M \<Omega>))" |
|
1894 then have "finite (f ` space (restrict_space M \<Omega>) \<union> {0})" by simp |
|
1895 then have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)" |
|
1896 by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } |
|
1897 moreover |
|
1898 { assume "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x) ` space M)" |
|
1899 then have "finite (f ` space (restrict_space M \<Omega>))" |
|
1900 by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } |
|
1901 ultimately show ?thesis |
|
1902 unfolding simple_function_iff_borel_measurable |
|
1903 borel_measurable_restrict_space_iff[OF assms] |
|
1904 by auto |
|
1905 qed |
|
1906 |
|
1907 lemma simple_integral_restrict_space: |
|
1908 assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" "simple_function (restrict_space M \<Omega>) f" |
|
1909 shows "simple_integral (restrict_space M \<Omega>) f = simple_integral M (\<lambda>x. f x * indicator \<Omega> x)" |
|
1910 using simple_function_restrict_space_ennreal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)] |
|
1911 by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def |
|
1912 split: split_indicator split_indicator_asm |
|
1913 intro!: setsum.mono_neutral_cong_left ennreal_mult_left_cong arg_cong2[where f=emeasure]) |
|
1914 |
|
1915 lemma nn_integral_restrict_space: |
|
1916 assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M" |
|
1917 shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M (\<lambda>x. f x * indicator \<Omega> x)" |
|
1918 proof - |
|
1919 let ?R = "restrict_space M \<Omega>" and ?X = "\<lambda>M f. {s. simple_function M s \<and> s \<le> f \<and> (\<forall>x. s x < top)}" |
|
1920 have "integral\<^sup>S ?R ` ?X ?R f = integral\<^sup>S M ` ?X M (\<lambda>x. f x * indicator \<Omega> x)" |
|
1921 proof (safe intro!: image_eqI) |
|
1922 fix s assume s: "simple_function ?R s" "s \<le> f" "\<forall>x. s x < top" |
|
1923 from s show "integral\<^sup>S (restrict_space M \<Omega>) s = integral\<^sup>S M (\<lambda>x. s x * indicator \<Omega> x)" |
|
1924 by (intro simple_integral_restrict_space) auto |
|
1925 from s show "simple_function M (\<lambda>x. s x * indicator \<Omega> x)" |
|
1926 by (simp add: simple_function_restrict_space_ennreal) |
|
1927 from s show "(\<lambda>x. s x * indicator \<Omega> x) \<le> (\<lambda>x. f x * indicator \<Omega> x)" |
|
1928 "\<And>x. s x * indicator \<Omega> x < top" |
|
1929 by (auto split: split_indicator simp: le_fun_def image_subset_iff) |
|
1930 next |
|
1931 fix s assume s: "simple_function M s" "s \<le> (\<lambda>x. f x * indicator \<Omega> x)" "\<forall>x. s x < top" |
|
1932 then have "simple_function M (\<lambda>x. s x * indicator (\<Omega> \<inter> space M) x)" (is ?s') |
|
1933 by (intro simple_function_mult simple_function_indicator) auto |
|
1934 also have "?s' \<longleftrightarrow> simple_function M (\<lambda>x. s x * indicator \<Omega> x)" |
|
1935 by (rule simple_function_cong) (auto split: split_indicator) |
|
1936 finally show sf: "simple_function (restrict_space M \<Omega>) s" |
|
1937 by (simp add: simple_function_restrict_space_ennreal) |
|
1938 |
|
1939 from s have s_eq: "s = (\<lambda>x. s x * indicator \<Omega> x)" |
|
1940 by (auto simp add: fun_eq_iff le_fun_def image_subset_iff |
|
1941 split: split_indicator split_indicator_asm |
|
1942 intro: antisym) |
|
1943 |
|
1944 show "integral\<^sup>S M s = integral\<^sup>S (restrict_space M \<Omega>) s" |
|
1945 by (subst s_eq) (rule simple_integral_restrict_space[symmetric, OF \<Omega> sf]) |
|
1946 show "\<And>x. s x < top" |
|
1947 using s by (auto simp: image_subset_iff) |
|
1948 from s show "s \<le> f" |
|
1949 by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm) |
|
1950 qed |
|
1951 then show ?thesis |
|
1952 unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong) |
|
1953 qed |
|
1954 |
|
1955 lemma nn_integral_count_space_indicator: |
|
1956 assumes "NO_MATCH (UNIV::'a set) (X::'a set)" |
|
1957 shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)" |
|
1958 by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space) |
|
1959 |
|
1960 lemma nn_integral_count_space_eq: |
|
1961 "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow> |
|
1962 (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)" |
|
1963 by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator) |
|
1964 |
|
1965 lemma nn_integral_ge_point: |
|
1966 assumes "x \<in> A" |
|
1967 shows "p x \<le> \<integral>\<^sup>+ x. p x \<partial>count_space A" |
|
1968 proof - |
|
1969 from assms have "p x \<le> \<integral>\<^sup>+ x. p x \<partial>count_space {x}" |
|
1970 by(auto simp add: nn_integral_count_space_finite max_def) |
|
1971 also have "\<dots> = \<integral>\<^sup>+ x'. p x' * indicator {x} x' \<partial>count_space A" |
|
1972 using assms by(auto simp add: nn_integral_count_space_indicator indicator_def intro!: nn_integral_cong) |
|
1973 also have "\<dots> \<le> \<integral>\<^sup>+ x. p x \<partial>count_space A" |
|
1974 by(rule nn_integral_mono)(simp add: indicator_def) |
|
1975 finally show ?thesis . |
|
1976 qed |
|
1977 |
|
1978 subsubsection \<open>Measure spaces with an associated density\<close> |
|
1979 |
|
1980 definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
|
1981 "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)" |
|
1982 |
|
1983 lemma |
|
1984 shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M" |
|
1985 and space_density[simp]: "space (density M f) = space M" |
|
1986 by (auto simp: density_def) |
|
1987 |
|
1988 (* FIXME: add conversion to simplify space, sets and measurable *) |
|
1989 lemma space_density_imp[measurable_dest]: |
|
1990 "\<And>x M f. x \<in> space (density M f) \<Longrightarrow> x \<in> space M" by auto |
|
1991 |
|
1992 lemma |
|
1993 shows measurable_density_eq1[simp]: "g \<in> measurable (density Mg f) Mg' \<longleftrightarrow> g \<in> measurable Mg Mg'" |
|
1994 and measurable_density_eq2[simp]: "h \<in> measurable Mh (density Mh' f) \<longleftrightarrow> h \<in> measurable Mh Mh'" |
|
1995 and simple_function_density_eq[simp]: "simple_function (density Mu f) u \<longleftrightarrow> simple_function Mu u" |
|
1996 unfolding measurable_def simple_function_def by simp_all |
|
1997 |
|
1998 lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow> |
|
1999 (AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'" |
|
2000 unfolding density_def by (auto intro!: measure_of_eq nn_integral_cong_AE sets.space_closed) |
|
2001 |
|
2002 lemma emeasure_density: |
|
2003 assumes f[measurable]: "f \<in> borel_measurable M" and A[measurable]: "A \<in> sets M" |
|
2004 shows "emeasure (density M f) A = (\<integral>\<^sup>+ x. f x * indicator A x \<partial>M)" |
|
2005 (is "_ = ?\<mu> A") |
|
2006 unfolding density_def |
|
2007 proof (rule emeasure_measure_of_sigma) |
|
2008 show "sigma_algebra (space M) (sets M)" .. |
|
2009 show "positive (sets M) ?\<mu>" |
|
2010 using f by (auto simp: positive_def) |
|
2011 show "countably_additive (sets M) ?\<mu>" |
|
2012 proof (intro countably_additiveI) |
|
2013 fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M" |
|
2014 then have "\<And>i. A i \<in> sets M" by auto |
|
2015 then have *: "\<And>i. (\<lambda>x. f x * indicator (A i) x) \<in> borel_measurable M" |
|
2016 by auto |
|
2017 assume disj: "disjoint_family A" |
|
2018 then have "(\<Sum>n. ?\<mu> (A n)) = (\<integral>\<^sup>+ x. (\<Sum>n. f x * indicator (A n) x) \<partial>M)" |
|
2019 using f * by (subst nn_integral_suminf) auto |
|
2020 also have "(\<integral>\<^sup>+ x. (\<Sum>n. f x * indicator (A n) x) \<partial>M) = (\<integral>\<^sup>+ x. f x * (\<Sum>n. indicator (A n) x) \<partial>M)" |
|
2021 using f by (auto intro!: ennreal_suminf_cmult nn_integral_cong_AE) |
|
2022 also have "\<dots> = (\<integral>\<^sup>+ x. f x * indicator (\<Union>n. A n) x \<partial>M)" |
|
2023 unfolding suminf_indicator[OF disj] .. |
|
2024 finally show "(\<Sum>i. \<integral>\<^sup>+ x. f x * indicator (A i) x \<partial>M) = \<integral>\<^sup>+ x. f x * indicator (\<Union>i. A i) x \<partial>M" . |
|
2025 qed |
|
2026 qed fact |
|
2027 |
|
2028 lemma null_sets_density_iff: |
|
2029 assumes f: "f \<in> borel_measurable M" |
|
2030 shows "A \<in> null_sets (density M f) \<longleftrightarrow> A \<in> sets M \<and> (AE x in M. x \<in> A \<longrightarrow> f x = 0)" |
|
2031 proof - |
|
2032 { assume "A \<in> sets M" |
|
2033 have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> emeasure M {x \<in> space M. f x * indicator A x \<noteq> 0} = 0" |
|
2034 using f \<open>A \<in> sets M\<close> by (intro nn_integral_0_iff) auto |
|
2035 also have "\<dots> \<longleftrightarrow> (AE x in M. f x * indicator A x = 0)" |
|
2036 using f \<open>A \<in> sets M\<close> by (intro AE_iff_measurable[OF _ refl, symmetric]) auto |
|
2037 also have "(AE x in M. f x * indicator A x = 0) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" |
|
2038 by (auto simp add: indicator_def max_def split: if_split_asm) |
|
2039 finally have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" . } |
|
2040 with f show ?thesis |
|
2041 by (simp add: null_sets_def emeasure_density cong: conj_cong) |
|
2042 qed |
|
2043 |
|
2044 lemma AE_density: |
|
2045 assumes f: "f \<in> borel_measurable M" |
|
2046 shows "(AE x in density M f. P x) \<longleftrightarrow> (AE x in M. 0 < f x \<longrightarrow> P x)" |
|
2047 proof |
|
2048 assume "AE x in density M f. P x" |
|
2049 with f obtain N where "{x \<in> space M. \<not> P x} \<subseteq> N" "N \<in> sets M" and ae: "AE x in M. x \<in> N \<longrightarrow> f x = 0" |
|
2050 by (auto simp: eventually_ae_filter null_sets_density_iff) |
|
2051 then have "AE x in M. x \<notin> N \<longrightarrow> P x" by auto |
|
2052 with ae show "AE x in M. 0 < f x \<longrightarrow> P x" |
|
2053 by (rule eventually_elim2) auto |
|
2054 next |
|
2055 fix N assume ae: "AE x in M. 0 < f x \<longrightarrow> P x" |
|
2056 then obtain N where "{x \<in> space M. \<not> (0 < f x \<longrightarrow> P x)} \<subseteq> N" "N \<in> null_sets M" |
|
2057 by (auto simp: eventually_ae_filter) |
|
2058 then have *: "{x \<in> space (density M f). \<not> P x} \<subseteq> N \<union> {x\<in>space M. f x = 0}" |
|
2059 "N \<union> {x\<in>space M. f x = 0} \<in> sets M" and ae2: "AE x in M. x \<notin> N" |
|
2060 using f by (auto simp: subset_eq zero_less_iff_neq_zero intro!: AE_not_in) |
|
2061 show "AE x in density M f. P x" |
|
2062 using ae2 |
|
2063 unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f] |
|
2064 by (intro exI[of _ "N \<union> {x\<in>space M. f x = 0}"] conjI *) (auto elim: eventually_elim2) |
|
2065 qed |
|
2066 |
|
2067 lemma nn_integral_density: |
|
2068 assumes f: "f \<in> borel_measurable M" |
|
2069 assumes g: "g \<in> borel_measurable M" |
|
2070 shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)" |
|
2071 using g proof induct |
|
2072 case (cong u v) |
|
2073 then show ?case |
|
2074 apply (subst nn_integral_cong[OF cong(3)]) |
|
2075 apply (simp_all cong: nn_integral_cong) |
|
2076 done |
|
2077 next |
|
2078 case (set A) then show ?case |
|
2079 by (simp add: emeasure_density f) |
|
2080 next |
|
2081 case (mult u c) |
|
2082 moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps) |
|
2083 ultimately show ?case |
|
2084 using f by (simp add: nn_integral_cmult) |
|
2085 next |
|
2086 case (add u v) |
|
2087 then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x" |
|
2088 by (simp add: distrib_left) |
|
2089 with add f show ?case |
|
2090 by (auto simp add: nn_integral_add intro!: nn_integral_add[symmetric]) |
|
2091 next |
|
2092 case (seq U) |
|
2093 have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)" |
|
2094 by eventually_elim (simp add: SUP_mult_left_ennreal seq) |
|
2095 from seq f show ?case |
|
2096 apply (simp add: nn_integral_monotone_convergence_SUP) |
|
2097 apply (subst nn_integral_cong_AE[OF eq]) |
|
2098 apply (subst nn_integral_monotone_convergence_SUP_AE) |
|
2099 apply (auto simp: incseq_def le_fun_def intro!: mult_left_mono) |
|
2100 done |
|
2101 qed |
|
2102 |
|
2103 lemma density_distr: |
|
2104 assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N" |
|
2105 shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X" |
|
2106 by (intro measure_eqI) |
|
2107 (auto simp add: emeasure_density nn_integral_distr emeasure_distr |
|
2108 split: split_indicator intro!: nn_integral_cong) |
|
2109 |
|
2110 lemma emeasure_restricted: |
|
2111 assumes S: "S \<in> sets M" and X: "X \<in> sets M" |
|
2112 shows "emeasure (density M (indicator S)) X = emeasure M (S \<inter> X)" |
|
2113 proof - |
|
2114 have "emeasure (density M (indicator S)) X = (\<integral>\<^sup>+x. indicator S x * indicator X x \<partial>M)" |
|
2115 using S X by (simp add: emeasure_density) |
|
2116 also have "\<dots> = (\<integral>\<^sup>+x. indicator (S \<inter> X) x \<partial>M)" |
|
2117 by (auto intro!: nn_integral_cong simp: indicator_def) |
|
2118 also have "\<dots> = emeasure M (S \<inter> X)" |
|
2119 using S X by (simp add: sets.Int) |
|
2120 finally show ?thesis . |
|
2121 qed |
|
2122 |
|
2123 lemma measure_restricted: |
|
2124 "S \<in> sets M \<Longrightarrow> X \<in> sets M \<Longrightarrow> measure (density M (indicator S)) X = measure M (S \<inter> X)" |
|
2125 by (simp add: emeasure_restricted measure_def) |
|
2126 |
|
2127 lemma (in finite_measure) finite_measure_restricted: |
|
2128 "S \<in> sets M \<Longrightarrow> finite_measure (density M (indicator S))" |
|
2129 by standard (simp add: emeasure_restricted) |
|
2130 |
|
2131 lemma emeasure_density_const: |
|
2132 "A \<in> sets M \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A" |
|
2133 by (auto simp: nn_integral_cmult_indicator emeasure_density) |
|
2134 |
|
2135 lemma measure_density_const: |
|
2136 "A \<in> sets M \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = enn2real c * measure M A" |
|
2137 by (auto simp: emeasure_density_const measure_def enn2real_mult) |
|
2138 |
|
2139 lemma density_density_eq: |
|
2140 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> |
|
2141 density (density M f) g = density M (\<lambda>x. f x * g x)" |
|
2142 by (auto intro!: measure_eqI simp: emeasure_density nn_integral_density ac_simps) |
|
2143 |
|
2144 lemma distr_density_distr: |
|
2145 assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M" |
|
2146 and inv: "\<forall>x\<in>space M. T' (T x) = x" |
|
2147 assumes f: "f \<in> borel_measurable M'" |
|
2148 shows "distr (density (distr M M' T) f) M T' = density M (f \<circ> T)" (is "?R = ?L") |
|
2149 proof (rule measure_eqI) |
|
2150 fix A assume A: "A \<in> sets ?R" |
|
2151 { fix x assume "x \<in> space M" |
|
2152 with sets.sets_into_space[OF A] |
|
2153 have "indicator (T' -` A \<inter> space M') (T x) = (indicator A x :: ennreal)" |
|
2154 using T inv by (auto simp: indicator_def measurable_space) } |
|
2155 with A T T' f show "emeasure ?R A = emeasure ?L A" |
|
2156 by (simp add: measurable_comp emeasure_density emeasure_distr |
|
2157 nn_integral_distr measurable_sets cong: nn_integral_cong) |
|
2158 qed simp |
|
2159 |
|
2160 lemma density_density_divide: |
|
2161 fixes f g :: "'a \<Rightarrow> real" |
|
2162 assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" |
|
2163 assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" |
|
2164 assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0" |
|
2165 shows "density (density M f) (\<lambda>x. g x / f x) = density M g" |
|
2166 proof - |
|
2167 have "density M g = density M (\<lambda>x. ennreal (f x) * ennreal (g x / f x))" |
|
2168 using f g ac by (auto intro!: density_cong measurable_If simp: ennreal_mult[symmetric]) |
|
2169 then show ?thesis |
|
2170 using f g by (subst density_density_eq) auto |
|
2171 qed |
|
2172 |
|
2173 lemma density_1: "density M (\<lambda>_. 1) = M" |
|
2174 by (intro measure_eqI) (auto simp: emeasure_density) |
|
2175 |
|
2176 lemma emeasure_density_add: |
|
2177 assumes X: "X \<in> sets M" |
|
2178 assumes Mf[measurable]: "f \<in> borel_measurable M" |
|
2179 assumes Mg[measurable]: "g \<in> borel_measurable M" |
|
2180 shows "emeasure (density M f) X + emeasure (density M g) X = |
|
2181 emeasure (density M (\<lambda>x. f x + g x)) X" |
|
2182 using assms |
|
2183 apply (subst (1 2 3) emeasure_density, simp_all) [] |
|
2184 apply (subst nn_integral_add[symmetric], simp_all) [] |
|
2185 apply (intro nn_integral_cong, simp split: split_indicator) |
|
2186 done |
|
2187 |
|
2188 subsubsection \<open>Point measure\<close> |
|
2189 |
|
2190 definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
|
2191 "point_measure A f = density (count_space A) f" |
|
2192 |
|
2193 lemma |
|
2194 shows space_point_measure: "space (point_measure A f) = A" |
|
2195 and sets_point_measure: "sets (point_measure A f) = Pow A" |
|
2196 by (auto simp: point_measure_def) |
|
2197 |
|
2198 lemma sets_point_measure_count_space[measurable_cong]: "sets (point_measure A f) = sets (count_space A)" |
|
2199 by (simp add: sets_point_measure) |
|
2200 |
|
2201 lemma measurable_point_measure_eq1[simp]: |
|
2202 "g \<in> measurable (point_measure A f) M \<longleftrightarrow> g \<in> A \<rightarrow> space M" |
|
2203 unfolding point_measure_def by simp |
|
2204 |
|
2205 lemma measurable_point_measure_eq2_finite[simp]: |
|
2206 "finite A \<Longrightarrow> |
|
2207 g \<in> measurable M (point_measure A f) \<longleftrightarrow> |
|
2208 (g \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. g -` {a} \<inter> space M \<in> sets M))" |
|
2209 unfolding point_measure_def by (simp add: measurable_count_space_eq2) |
|
2210 |
|
2211 lemma simple_function_point_measure[simp]: |
|
2212 "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)" |
|
2213 by (simp add: point_measure_def) |
|
2214 |
|
2215 lemma emeasure_point_measure: |
|
2216 assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A" |
|
2217 shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)" |
|
2218 proof - |
|
2219 have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}" |
|
2220 using \<open>X \<subseteq> A\<close> by auto |
|
2221 with A show ?thesis |
|
2222 by (simp add: emeasure_density nn_integral_count_space point_measure_def indicator_def) |
|
2223 qed |
|
2224 |
|
2225 lemma emeasure_point_measure_finite: |
|
2226 "finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)" |
|
2227 by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum.mono_neutral_left simp: less_le) |
|
2228 |
|
2229 lemma emeasure_point_measure_finite2: |
|
2230 "X \<subseteq> A \<Longrightarrow> finite X \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)" |
|
2231 by (subst emeasure_point_measure) |
|
2232 (auto dest: finite_subset intro!: setsum.mono_neutral_left simp: less_le) |
|
2233 |
|
2234 lemma null_sets_point_measure_iff: |
|
2235 "X \<in> null_sets (point_measure A f) \<longleftrightarrow> X \<subseteq> A \<and> (\<forall>x\<in>X. f x = 0)" |
|
2236 by (auto simp: AE_count_space null_sets_density_iff point_measure_def) |
|
2237 |
|
2238 lemma AE_point_measure: |
|
2239 "(AE x in point_measure A f. P x) \<longleftrightarrow> (\<forall>x\<in>A. 0 < f x \<longrightarrow> P x)" |
|
2240 unfolding point_measure_def |
|
2241 by (subst AE_density) (auto simp: AE_density AE_count_space point_measure_def) |
|
2242 |
|
2243 lemma nn_integral_point_measure: |
|
2244 "finite {a\<in>A. 0 < f a \<and> 0 < g a} \<Longrightarrow> |
|
2245 integral\<^sup>N (point_measure A f) g = (\<Sum>a|a\<in>A \<and> 0 < f a \<and> 0 < g a. f a * g a)" |
|
2246 unfolding point_measure_def |
|
2247 by (subst nn_integral_density) |
|
2248 (simp_all add: nn_integral_density nn_integral_count_space ennreal_zero_less_mult_iff) |
|
2249 |
|
2250 lemma nn_integral_point_measure_finite: |
|
2251 "finite A \<Longrightarrow> integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)" |
|
2252 by (subst nn_integral_point_measure) (auto intro!: setsum.mono_neutral_left simp: less_le) |
|
2253 |
|
2254 subsubsection \<open>Uniform measure\<close> |
|
2255 |
|
2256 definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)" |
|
2257 |
|
2258 lemma |
|
2259 shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M" |
|
2260 and space_uniform_measure[simp]: "space (uniform_measure M A) = space M" |
|
2261 by (auto simp: uniform_measure_def) |
|
2262 |
|
2263 lemma emeasure_uniform_measure[simp]: |
|
2264 assumes A: "A \<in> sets M" and B: "B \<in> sets M" |
|
2265 shows "emeasure (uniform_measure M A) B = emeasure M (A \<inter> B) / emeasure M A" |
|
2266 proof - |
|
2267 from A B have "emeasure (uniform_measure M A) B = (\<integral>\<^sup>+x. (1 / emeasure M A) * indicator (A \<inter> B) x \<partial>M)" |
|
2268 by (auto simp add: uniform_measure_def emeasure_density divide_ennreal_def split: split_indicator |
|
2269 intro!: nn_integral_cong) |
|
2270 also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A" |
|
2271 using A B |
|
2272 by (subst nn_integral_cmult_indicator) (simp_all add: sets.Int divide_ennreal_def mult.commute) |
|
2273 finally show ?thesis . |
|
2274 qed |
|
2275 |
|
2276 lemma measure_uniform_measure[simp]: |
|
2277 assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" and B: "B \<in> sets M" |
|
2278 shows "measure (uniform_measure M A) B = measure M (A \<inter> B) / measure M A" |
|
2279 using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A |
|
2280 by (cases "emeasure M A" "emeasure M (A \<inter> B)" rule: ennreal2_cases) |
|
2281 (simp_all add: measure_def divide_ennreal top_ennreal.rep_eq top_ereal_def ennreal_top_divide) |
|
2282 |
|
2283 lemma AE_uniform_measureI: |
|
2284 "A \<in> sets M \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x) \<Longrightarrow> (AE x in uniform_measure M A. P x)" |
|
2285 unfolding uniform_measure_def by (auto simp: AE_density divide_ennreal_def) |
|
2286 |
|
2287 lemma emeasure_uniform_measure_1: |
|
2288 "emeasure M S \<noteq> 0 \<Longrightarrow> emeasure M S \<noteq> \<infinity> \<Longrightarrow> emeasure (uniform_measure M S) S = 1" |
|
2289 by (subst emeasure_uniform_measure) |
|
2290 (simp_all add: emeasure_neq_0_sets emeasure_eq_ennreal_measure divide_ennreal |
|
2291 zero_less_iff_neq_zero[symmetric]) |
|
2292 |
|
2293 lemma nn_integral_uniform_measure: |
|
2294 assumes f[measurable]: "f \<in> borel_measurable M" and S[measurable]: "S \<in> sets M" |
|
2295 shows "(\<integral>\<^sup>+x. f x \<partial>uniform_measure M S) = (\<integral>\<^sup>+x. f x * indicator S x \<partial>M) / emeasure M S" |
|
2296 proof - |
|
2297 { assume "emeasure M S = \<infinity>" |
|
2298 then have ?thesis |
|
2299 by (simp add: uniform_measure_def nn_integral_density f) } |
|
2300 moreover |
|
2301 { assume [simp]: "emeasure M S = 0" |
|
2302 then have ae: "AE x in M. x \<notin> S" |
|
2303 using sets.sets_into_space[OF S] |
|
2304 by (subst AE_iff_measurable[OF _ refl]) (simp_all add: subset_eq cong: rev_conj_cong) |
|
2305 from ae have "(\<integral>\<^sup>+ x. indicator S x / 0 * f x \<partial>M) = 0" |
|
2306 by (subst nn_integral_0_iff_AE) auto |
|
2307 moreover from ae have "(\<integral>\<^sup>+ x. f x * indicator S x \<partial>M) = 0" |
|
2308 by (subst nn_integral_0_iff_AE) auto |
|
2309 ultimately have ?thesis |
|
2310 by (simp add: uniform_measure_def nn_integral_density f) } |
|
2311 moreover have "emeasure M S \<noteq> 0 \<Longrightarrow> emeasure M S \<noteq> \<infinity> \<Longrightarrow> ?thesis" |
|
2312 unfolding uniform_measure_def |
|
2313 by (subst nn_integral_density) |
|
2314 (auto simp: ennreal_times_divide f nn_integral_divide[symmetric] mult.commute) |
|
2315 ultimately show ?thesis by blast |
|
2316 qed |
|
2317 |
|
2318 lemma AE_uniform_measure: |
|
2319 assumes "emeasure M A \<noteq> 0" "emeasure M A < \<infinity>" |
|
2320 shows "(AE x in uniform_measure M A. P x) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x)" |
|
2321 proof - |
|
2322 have "A \<in> sets M" |
|
2323 using \<open>emeasure M A \<noteq> 0\<close> by (metis emeasure_notin_sets) |
|
2324 moreover have "\<And>x. 0 < indicator A x / emeasure M A \<longleftrightarrow> x \<in> A" |
|
2325 using assms |
|
2326 by (cases "emeasure M A") (auto split: split_indicator simp: ennreal_zero_less_divide) |
|
2327 ultimately show ?thesis |
|
2328 unfolding uniform_measure_def by (simp add: AE_density) |
|
2329 qed |
|
2330 |
|
2331 subsubsection \<open>Null measure\<close> |
|
2332 |
|
2333 lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)" |
|
2334 by (intro measure_eqI) (simp_all add: emeasure_density) |
|
2335 |
|
2336 lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0" |
|
2337 by (auto simp add: nn_integral_def simple_integral_def SUP_constant bot_ennreal_def le_fun_def |
|
2338 intro!: exI[of _ "\<lambda>x. 0"]) |
|
2339 |
|
2340 lemma density_null_measure[simp]: "density (null_measure M) f = null_measure M" |
|
2341 proof (intro measure_eqI) |
|
2342 fix A show "emeasure (density (null_measure M) f) A = emeasure (null_measure M) A" |
|
2343 by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure) |
|
2344 qed simp |
|
2345 |
|
2346 subsubsection \<open>Uniform count measure\<close> |
|
2347 |
|
2348 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)" |
|
2349 |
|
2350 lemma |
|
2351 shows space_uniform_count_measure: "space (uniform_count_measure A) = A" |
|
2352 and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A" |
|
2353 unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure) |
|
2354 |
|
2355 lemma sets_uniform_count_measure_count_space[measurable_cong]: |
|
2356 "sets (uniform_count_measure A) = sets (count_space A)" |
|
2357 by (simp add: sets_uniform_count_measure) |
|
2358 |
|
2359 lemma emeasure_uniform_count_measure: |
|
2360 "finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (uniform_count_measure A) X = card X / card A" |
|
2361 by (simp add: emeasure_point_measure_finite uniform_count_measure_def divide_inverse ennreal_mult |
|
2362 ennreal_of_nat_eq_real_of_nat) |
|
2363 |
|
2364 lemma measure_uniform_count_measure: |
|
2365 "finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> measure (uniform_count_measure A) X = card X / card A" |
|
2366 by (simp add: emeasure_point_measure_finite uniform_count_measure_def measure_def enn2real_mult) |
|
2367 |
|
2368 lemma space_uniform_count_measure_empty_iff [simp]: |
|
2369 "space (uniform_count_measure X) = {} \<longleftrightarrow> X = {}" |
|
2370 by(simp add: space_uniform_count_measure) |
|
2371 |
|
2372 lemma sets_uniform_count_measure_eq_UNIV [simp]: |
|
2373 "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True" |
|
2374 "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True" |
|
2375 by(simp_all add: sets_uniform_count_measure) |
|
2376 |
|
2377 subsubsection \<open>Scaled measure\<close> |
|
2378 |
|
2379 lemma nn_integral_scale_measure: |
|
2380 assumes f: "f \<in> borel_measurable M" |
|
2381 shows "nn_integral (scale_measure r M) f = r * nn_integral M f" |
|
2382 using f |
|
2383 proof induction |
|
2384 case (cong f g) |
|
2385 thus ?case |
|
2386 by(simp add: cong.hyps space_scale_measure cong: nn_integral_cong_simp) |
|
2387 next |
|
2388 case (mult f c) |
|
2389 thus ?case |
|
2390 by(simp add: nn_integral_cmult max_def mult.assoc mult.left_commute) |
|
2391 next |
|
2392 case (add f g) |
|
2393 thus ?case |
|
2394 by(simp add: nn_integral_add distrib_left) |
|
2395 next |
|
2396 case (seq U) |
|
2397 thus ?case |
|
2398 by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal) |
|
2399 qed simp |
|
2400 |
|
2401 end |
|