474 |
474 |
475 lemma measurable_compose_Pair1: |
475 lemma measurable_compose_Pair1: |
476 "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L" |
476 "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L" |
477 by (rule measurable_compose[OF measurable_Pair]) auto |
477 by (rule measurable_compose[OF measurable_Pair]) auto |
478 |
478 |
479 lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: |
479 lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst': |
480 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x" |
480 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x" |
481 shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" |
481 shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" |
482 using f proof induct |
482 using f proof induct |
483 case (cong u v) |
483 case (cong u v) |
484 then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M2 \<Longrightarrow> u (w, x) = v (w, x)" |
484 then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M2 \<Longrightarrow> u (w, x) = v (w, x)" |
510 ultimately show ?case |
510 ultimately show ?case |
511 by (simp cong: positive_integral_cong) |
511 by (simp cong: positive_integral_cong) |
512 qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add |
512 qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add |
513 positive_integral_monotone_convergence_SUP |
513 positive_integral_monotone_convergence_SUP |
514 measurable_compose_Pair1 positive_integral_positive |
514 measurable_compose_Pair1 positive_integral_positive |
515 borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def |
515 borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def |
516 cong: positive_integral_cong) |
516 cong: positive_integral_cong) |
517 |
517 |
518 lemma (in pair_sigma_finite) positive_integral_fst_measurable: |
518 lemma (in pair_sigma_finite) positive_integral_fst_measurable: |
519 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" |
519 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" |
520 shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" |
520 shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" |
521 (is "?C f \<in> borel_measurable M1") |
521 (is "?C f \<in> borel_measurable M1") |
522 and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" |
522 and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" |
523 using f |
523 using f |
524 borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"] |
524 borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"] |
525 positive_integral_fst[of "\<lambda>x. max 0 (f x)"] |
525 positive_integral_fst[of "\<lambda>x. max 0 (f x)"] |
526 unfolding positive_integral_max_0 by auto |
526 unfolding positive_integral_max_0 by auto |
|
527 |
|
528 lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: |
|
529 "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1" |
|
530 using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp |
|
531 |
|
532 lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd: |
|
533 assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2" |
|
534 proof - |
|
535 interpret Q: pair_sigma_finite M2 M1 by default |
|
536 from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp |
|
537 qed |
527 |
538 |
528 lemma (in pair_sigma_finite) positive_integral_snd_measurable: |
539 lemma (in pair_sigma_finite) positive_integral_snd_measurable: |
529 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" |
540 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" |
530 shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" |
541 shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" |
531 proof - |
542 proof - |