32 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
32 "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" |
33 |
33 |
34 lemma (in prob_space) distribution_cong: |
34 lemma (in prob_space) distribution_cong: |
35 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" |
35 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" |
36 shows "distribution X = distribution Y" |
36 shows "distribution X = distribution Y" |
37 unfolding distribution_def ext_iff |
37 unfolding distribution_def fun_eq_iff |
38 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
38 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
39 |
39 |
40 lemma (in prob_space) joint_distribution_cong: |
40 lemma (in prob_space) joint_distribution_cong: |
41 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" |
41 assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" |
42 assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" |
42 assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" |
43 shows "joint_distribution X Y = joint_distribution X' Y'" |
43 shows "joint_distribution X Y = joint_distribution X' Y'" |
44 unfolding distribution_def ext_iff |
44 unfolding distribution_def fun_eq_iff |
45 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
45 using assms by (auto intro!: arg_cong[where f="\<mu>"]) |
46 |
46 |
47 lemma prob_space: "prob (space M) = 1" |
47 lemma prob_space: "prob (space M) = 1" |
48 unfolding measure_space_1 by simp |
48 unfolding measure_space_1 by simp |
49 |
49 |