512 lemma |
512 lemma |
513 shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N" |
513 shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N" |
514 and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)" |
514 and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)" |
515 by (simp_all add: distributed_def borel_measurable_ereal_iff) |
515 by (simp_all add: distributed_def borel_measurable_ereal_iff) |
516 |
516 |
517 lemma |
517 lemma distributed_real_measurable': |
518 assumes D: "distributed M N X (\<lambda>x. ereal (f x))" |
518 "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" |
519 shows distributed_real_measurable'[measurable_dest]: |
519 by simp |
520 "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" |
520 |
521 using distributed_real_measurable[OF D] |
521 lemma joint_distributed_measurable1: |
522 by simp_all |
522 "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S" |
523 |
523 by simp |
524 lemma |
524 |
525 assumes D: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f" |
525 lemma joint_distributed_measurable2: |
526 shows joint_distributed_measurable1[measurable_dest]: |
526 "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T" |
527 "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S" |
527 by simp |
528 and joint_distributed_measurable2[measurable_dest]: |
|
529 "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T" |
|
530 using measurable_compose[OF distributed_measurable[OF D] measurable_fst] |
|
531 using measurable_compose[OF distributed_measurable[OF D] measurable_snd] |
|
532 by auto |
|
533 |
528 |
534 lemma distributed_count_space: |
529 lemma distributed_count_space: |
535 assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" |
530 assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" |
536 shows "P a = emeasure M (X -` {a} \<inter> space M)" |
531 shows "P a = emeasure M (X -` {a} \<inter> space M)" |
537 proof - |
532 proof - |