262 by auto |
262 by auto |
263 thus ?thesis using f g |
263 thus ?thesis using f g |
264 by (simp add: borel_measurable_eq_borel_measurable compl_sets) |
264 by (simp add: borel_measurable_eq_borel_measurable compl_sets) |
265 qed |
265 qed |
266 |
266 |
267 lemma (in measure_space) borel_measurable_plus_borel_measurable: |
267 lemma (in measure_space) borel_measurable_add_borel_measurable: |
268 assumes f: "f \<in> borel_measurable M" |
268 assumes f: "f \<in> borel_measurable M" |
269 assumes g: "g \<in> borel_measurable M" |
269 assumes g: "g \<in> borel_measurable M" |
270 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
270 shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" |
271 proof - |
271 proof - |
272 have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}" |
272 have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}" |
350 assumes g: "g \<in> borel_measurable M" |
350 assumes g: "g \<in> borel_measurable M" |
351 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
351 shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" |
352 proof - |
352 proof - |
353 have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M" |
353 have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M" |
354 by (fast intro: affine_borel_measurable borel_measurable_square |
354 by (fast intro: affine_borel_measurable borel_measurable_square |
355 borel_measurable_plus_borel_measurable f g) |
355 borel_measurable_add_borel_measurable f g) |
356 have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = |
356 have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = |
357 (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))" |
357 (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))" |
358 by (simp add: Ring_and_Field.minus_divide_right) |
358 by (simp add: Ring_and_Field.minus_divide_right) |
359 also have "... \<in> borel_measurable M" |
359 also have "... \<in> borel_measurable M" |
360 by (fast intro: affine_borel_measurable borel_measurable_square |
360 by (fast intro: affine_borel_measurable borel_measurable_square |
361 borel_measurable_plus_borel_measurable |
361 borel_measurable_add_borel_measurable |
362 borel_measurable_uminus_borel_measurable f g) |
362 borel_measurable_uminus_borel_measurable f g) |
363 finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" . |
363 finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" . |
364 show ?thesis |
364 show ?thesis |
365 apply (simp add: times_eq_sum_squares real_diff_def) |
365 apply (simp add: times_eq_sum_squares real_diff_def) |
366 using 1 2 apply (simp add: borel_measurable_plus_borel_measurable) |
366 using 1 2 apply (simp add: borel_measurable_add_borel_measurable) |
367 done |
367 done |
368 qed |
368 qed |
369 |
369 |
370 lemma (in measure_space) borel_measurable_diff_borel_measurable: |
370 lemma (in measure_space) borel_measurable_diff_borel_measurable: |
371 assumes f: "f \<in> borel_measurable M" |
371 assumes f: "f \<in> borel_measurable M" |
372 assumes g: "g \<in> borel_measurable M" |
372 assumes g: "g \<in> borel_measurable M" |
373 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
373 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
374 unfolding real_diff_def |
374 unfolding real_diff_def |
375 by (fast intro: borel_measurable_plus_borel_measurable |
375 by (fast intro: borel_measurable_add_borel_measurable |
376 borel_measurable_uminus_borel_measurable f g) |
376 borel_measurable_uminus_borel_measurable f g) |
377 |
377 |
378 lemma (in measure_space) mono_convergent_borel_measurable: |
378 lemma (in measure_space) mono_convergent_borel_measurable: |
379 assumes u: "!!n. u n \<in> borel_measurable M" |
379 assumes u: "!!n. u n \<in> borel_measurable M" |
380 assumes mc: "mono_convergent u f (space M)" |
380 assumes mc: "mono_convergent u f (space M)" |
407 } |
407 } |
408 thus ?thesis |
408 thus ?thesis |
409 by (auto simp add: borel_measurable_le_iff) |
409 by (auto simp add: borel_measurable_le_iff) |
410 qed |
410 qed |
411 |
411 |
412 lemma (in measure_space) borel_measurable_SIGMA_borel_measurable: |
412 lemma (in measure_space) borel_measurable_setsum_borel_measurable: |
413 assumes s: "finite s" |
413 assumes s: "finite s" |
414 shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s |
414 shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s |
415 proof (induct s) |
415 proof (induct s) |
416 case empty |
416 case empty |
417 thus ?case |
417 thus ?case |
418 by (simp add: borel_measurable_const) |
418 by (simp add: borel_measurable_const) |
419 next |
419 next |
420 case (insert x s) |
420 case (insert x s) |
421 thus ?case |
421 thus ?case |
422 by (auto simp add: borel_measurable_plus_borel_measurable) |
422 by (auto simp add: borel_measurable_add_borel_measurable) |
423 qed |
423 qed |
424 |
424 |
425 end |
425 end |