imports Lebesgue_Measure

   imports Lebesgue_Measure Radon_Nikodym

 locale prob_space = finite_measure +

 lemma funset_eq_UN_fun_upd_I:

   assumes measure_space_1: "measure M (space M) = 1"

   assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"

   and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"

 lemma prob_spaceI[Pure.intro!]:

   and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"

   assumes "measure_space M"

   shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"

   assumes *: "measure M (space M) = 1"

 proof safe

   shows "prob_space M"

   fix f assume f: "f \<in> F (insert a A)"

 proof -

   show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"

   interpret finite_measure M

   proof (rule UN_I[of "f(a := d)"])

   proof

     show "f(a := d) \<in> F A" using *[OF f] .

     show "measure_space M" by fact

     show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"

     show "measure M (space M) \<noteq> \<infinity>" using * by simp 

     proof (rule image_eqI[of _ _ "f a"])

       show "f a \<in> G (f(a := d))" using **[OF f] .

     qed simp

   show "prob_space M" by default fact

 next

 qed

   fix f x assume "f \<in> F A" "x \<in> G f"

   from ***[OF this] show "f(a := x) \<in> F (insert a A)" .

 abbreviation (in prob_space) "events \<equiv> sets M"

 qed

 abbreviation (in prob_space) "prob \<equiv> \<mu>'"

 abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'"

 lemma extensional_funcset_insert_eq[simp]:

 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M"

   assumes "a \<notin> A"

   shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"

 definition (in prob_space)

   apply (rule funset_eq_UN_fun_upd_I)

   "distribution X A = \<mu>' (X -` A \<inter> space M)"

   using assms

   by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)

 abbreviation (in prob_space)

   "joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))"

 lemma finite_extensional_funcset[simp, intro]:

   assumes "finite A" "finite B"

 lemma (in prob_space) prob_space_cong:

   shows "finite (extensional A \<inter> (A \<rightarrow> B))"

   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"

   using assms by induct auto

   shows "prob_space N"

 proof

 lemma finite_PiE[simp, intro]:

   show "measure_space N" by (intro measure_space_cong assms)

   assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"

   show "measure N (space N) = 1"

   shows "finite (Pi\<^isub>E A B)"

     using measure_space_1 assms by simp

 proof -

 qed

   have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto

   show ?thesis

 lemma (in prob_space) distribution_cong:

     using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto

   assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"

 qed

   shows "distribution X = distribution Y"

   unfolding distribution_def fun_eq_iff

   using assms by (auto intro!: arg_cong[where f="\<mu>'"])

 lemma countably_additiveI[case_names countably]:

   assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"

 lemma (in prob_space) joint_distribution_cong:

   shows "countably_additive M \<mu>"

   assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"

   using assms unfolding countably_additive_def by auto

   assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"

   shows "joint_distribution X Y = joint_distribution X' Y'"

   unfolding distribution_def fun_eq_iff

   using assms by (auto intro!: arg_cong[where f="\<mu>'"])

 lemma (in prob_space) distribution_id[simp]:

   "N \<in> events \<Longrightarrow> distribution (\<lambda>x. x) N = prob N"

   by (auto simp: distribution_def intro!: arg_cong[where f=prob])

 lemma (in prob_space) prob_space: "prob (space M) = 1"

   using measure_space_1 unfolding \<mu>'_def by (simp add: one_ereal_def)

 lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1"

   using bounded_measure[of A] by (simp add: prob_space)

 lemma (in prob_space) distribution_positive[simp, intro]:

   "0 \<le> distribution X A" unfolding distribution_def by auto

 lemma (in prob_space) not_zero_less_distribution[simp]:

   "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0"

   using distribution_positive[of X A] by arith

 lemma (in prob_space) joint_distribution_remove[simp]:

     "joint_distribution X X {(x, x)} = distribution X {x}"

   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

 lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"

   unfolding distribution_def using prob_space by auto

 lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"

   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

 lemma (in prob_space) not_empty: "space M \<noteq> {}"

   using prob_space empty_measure' by auto

 lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"

   unfolding measure_space_1[symmetric]

   using sets_into_space

   by (intro measure_mono) auto

 lemma (in prob_space) AE_I_eq_1:

   assumes "\<mu> {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"

   shows "AE x. P x"

 proof (rule AE_I)

   show "\<mu> (space M - {x \<in> space M. P x}) = 0"

     using assms measure_space_1 by (simp add: measure_compl)

 qed (insert assms, auto)

 lemma (in prob_space) distribution_1:

   "distribution X A \<le> 1"

   unfolding distribution_def by simp

 lemma (in prob_space) prob_compl:

   assumes A: "A \<in> events"

   shows "prob (space M - A) = 1 - prob A"

   using finite_measure_compl[OF A] by (simp add: prob_space)

 lemma (in prob_space) prob_space_increasing: "increasing M prob"

   by (auto intro!: finite_measure_mono simp: increasing_def)

 lemma (in prob_space) prob_zero_union:

   assumes "s \<in> events" "t \<in> events" "prob t = 0"

   shows "prob (s \<union> t) = prob s"

 using assms

 proof -

   have "prob (s \<union> t) \<le> prob s"

     using finite_measure_subadditive[of s t] assms by auto

   moreover have "prob (s \<union> t) \<ge> prob s"

     using assms by (blast intro: finite_measure_mono)

   ultimately show ?thesis by simp

 qed

 lemma (in prob_space) prob_eq_compl:

   assumes "s \<in> events" "t \<in> events"

   assumes "prob (space M - s) = prob (space M - t)"

   shows "prob s = prob t"

   using assms prob_compl by auto

 lemma (in prob_space) prob_one_inter:

   assumes events:"s \<in> events" "t \<in> events"

   assumes "prob t = 1"

   shows "prob (s \<inter> t) = prob s"

 proof -

   have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"

     using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)

   also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"

     by blast

   finally show "prob (s \<inter> t) = prob s"

     using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])

 qed

 lemma (in prob_space) prob_eq_bigunion_image:

   assumes "range f \<subseteq> events" "range g \<subseteq> events"

   assumes "disjoint_family f" "disjoint_family g"

   assumes "\<And> n :: nat. prob (f n) = prob (g n)"

   shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"

 using assms

 proof -

   have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))"

     by (rule finite_measure_UNION[OF assms(1,3)])

   have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"

     by (rule finite_measure_UNION[OF assms(2,4)])

   show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp

 qed

 lemma (in prob_space) prob_countably_zero:

   assumes "range c \<subseteq> events"

   assumes "\<And> i. prob (c i) = 0"

   shows "prob (\<Union> i :: nat. c i) = 0"

 proof (rule antisym)

   show "prob (\<Union> i :: nat. c i) \<le> 0"

     using finite_measure_countably_subadditive[OF assms(1)]

     by (simp add: assms(2) suminf_zero summable_zero)

 qed simp

 lemma (in prob_space) prob_equiprobable_finite_unions:

   assumes "s \<in> events"

   assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"

   assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"

   shows "prob s = real (card s) * prob {SOME x. x \<in> s}"

 proof (cases "s = {}")

   case False hence "\<exists> x. x \<in> s" by blast

   from someI_ex[OF this] assms

   have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast

   have "prob s = (\<Sum> x \<in> s. prob {x})"

     using finite_measure_finite_singleton[OF s_finite] by simp

   also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto

   also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"

     using setsum_constant assms by (simp add: real_eq_of_nat)

   finally show ?thesis by simp

 qed simp

 lemma (in prob_space) prob_real_sum_image_fn:

   assumes "e \<in> events"

   assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"

   assumes "finite s"

   assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"

   assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"

   shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"

 proof -

   have e: "e = (\<Union> i \<in> s. e \<inter> f i)"

     using `e \<in> events` sets_into_space upper by blast

   hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp

   also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"

   proof (rule finite_measure_finite_Union)

     show "finite s" by fact

     show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact

     show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"

       using disjoint by (auto simp: disjoint_family_on_def)

   qed

   finally show ?thesis .

 qed

 lemma (in prob_space) prob_space_vimage:

   assumes S: "sigma_algebra S"

   assumes T: "T \<in> measure_preserving M S"

   shows "prob_space S"

 proof

   interpret S: measure_space S

     using S and T by (rule measure_space_vimage)

   show "measure_space S" ..

   from T[THEN measure_preservingD2]

   have "T -` space S \<inter> space M = space M"

     by (auto simp: measurable_def)

   with T[THEN measure_preservingD, of "space S", symmetric]

   show  "measure S (space S) = 1"

     using measure_space_1 by simp

 qed

 lemma prob_space_unique_Int_stable:

   fixes E :: "('a, 'b) algebra_scheme" and A :: "nat \<Rightarrow> 'a set"

   assumes E: "Int_stable E" "space E \<in> sets E"

   and M: "prob_space M" "space M = space E" "sets M = sets (sigma E)"

   and N: "prob_space N" "space N = space E" "sets N = sets (sigma E)"

   and eq: "\<And>X. X \<in> sets E \<Longrightarrow> finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"

   assumes "X \<in> sets (sigma E)"

   shows "finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"

 proof -

   interpret M!: prob_space M by fact

   interpret N!: prob_space N by fact

   have "measure M X = measure N X"

   proof (rule measure_unique_Int_stable[OF `Int_stable E`])

     show "range (\<lambda>i. space M) \<subseteq> sets E" "incseq (\<lambda>i. space M)" "(\<Union>i. space M) = space E"

       using E M N by auto

     show "\<And>i. M.\<mu> (space M) \<noteq> \<infinity>"

       using M.measure_space_1 by simp

     show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = M.\<mu>\<rparr>"

       using E M N by (auto intro!: M.measure_space_cong)

     show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = N.\<mu>\<rparr>"

       using E M N by (auto intro!: N.measure_space_cong)

     { fix X assume "X \<in> sets E"

       then have "X \<in> sets (sigma E)"

         by (auto simp: sets_sigma sigma_sets.Basic)

       with eq[OF `X \<in> sets E`] M N show "M.\<mu> X = N.\<mu> X"

         by (simp add: M.finite_measure_eq N.finite_measure_eq) }

   qed fact

   with `X \<in> sets (sigma E)` M N show ?thesis

     by (simp add: M.finite_measure_eq N.finite_measure_eq)

 qed

 lemma (in prob_space) distribution_prob_space:

   assumes X: "random_variable S X"

   shows "prob_space (S\<lparr>measure := ereal \<circ> distribution X\<rparr>)" (is "prob_space ?S")

 proof (rule prob_space_vimage)

   show "X \<in> measure_preserving M ?S"

     using X

     unfolding measure_preserving_def distribution_def [abs_def]

     by (auto simp: finite_measure_eq measurable_sets)

   show "sigma_algebra ?S" using X by simp

 qed

 lemma (in prob_space) AE_distribution:

   assumes X: "random_variable MX X" and "AE x in MX\<lparr>measure := ereal \<circ> distribution X\<rparr>. Q x"

   shows "AE x. Q (X x)"

 proof -

   interpret X: prob_space "MX\<lparr>measure := ereal \<circ> distribution X\<rparr>" using X by (rule distribution_prob_space)

   obtain N where N: "N \<in> sets MX" "distribution X N = 0" "{x\<in>space MX. \<not> Q x} \<subseteq> N"

     using assms unfolding X.almost_everywhere_def by auto

   from X[unfolded measurable_def] N show "AE x. Q (X x)"

     by (intro AE_I'[where N="X -` N \<inter> space M"])

        (auto simp: finite_measure_eq distribution_def measurable_sets)

 qed

 lemma (in prob_space) distribution_eq_integral:

   "random_variable S X \<Longrightarrow> A \<in> sets S \<Longrightarrow> distribution X A = expectation (indicator (X -` A \<inter> space M))"

   using finite_measure_eq[of "X -` A \<inter> space M"]

   by (auto simp: measurable_sets distribution_def)

 lemma (in prob_space) expectation_less:

   assumes [simp]: "integrable M X"

   assumes gt: "\<forall>x\<in>space M. X x < b"

   shows "expectation X < b"

 proof -

   have "expectation X < expectation (\<lambda>x. b)"

     using gt measure_space_1

     by (intro integral_less_AE_space) auto

   then show ?thesis using prob_space by simp

 qed

 lemma (in prob_space) expectation_greater:

   assumes [simp]: "integrable M X"

   assumes gt: "\<forall>x\<in>space M. a < X x"

   shows "a < expectation X"

 proof -

   have "expectation (\<lambda>x. a) < expectation X"

     using gt measure_space_1

     by (intro integral_less_AE_space) auto

   then show ?thesis using prob_space by simp

 qed

       by (auto simp: mem_ball dist_real_def field_simps split: split_min)

       by (auto simp: dist_real_def field_simps split: split_min)

     with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: mem_ball dist_real_def)

     with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)

       by (auto simp: mem_ball dist_real_def field_simps)

       by (auto simp: dist_real_def field_simps)

       then have "x + e / 2 \<in> ball x e" by (auto simp: mem_ball dist_real_def)

       then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)

       using prob_space

       using prob_space by (simp add: X)

       by (simp add: integral_add integral_cmult integral_diff lebesgue_integral_const X)

   assumes X: "random_variable MX X" and Y: "random_variable MY Y"

   "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY

     and A: "A \<in> sets MX" and B: "B \<in> sets MY"

     \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A"

   shows "joint_distribution X Y (A \<times> B) \<le> distribution X A"

   by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)

   unfolding distribution_def

 proof (intro finite_measure_mono)

   show "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M \<subseteq> X -` A \<inter> space M" by force

   show "X -` A \<inter> space M \<in> events"

     using X A unfolding measurable_def by simp

   have *: "(\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M =

     (X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto

 qed

 lemma (in prob_space) joint_distribution_commute:

   "joint_distribution X Y x = joint_distribution Y X ((\<lambda>(x,y). (y,x))`x)"

   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

   assumes X: "random_variable MX X" and Y: "random_variable MY Y"

   "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY

     and A: "A \<in> sets MX" and B: "B \<in> sets MY"

     \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B"

   shows "joint_distribution X Y (A \<times> B) \<le> distribution Y B"

   by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)

   using assms

   by (subst joint_distribution_commute)

 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2

      (simp add: swap_product joint_distribution_Times_le_fst)

 sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"

 lemma (in prob_space) random_variable_pairI:

   assumes "random_variable MX X"

   assumes "random_variable MY Y"

   shows "random_variable (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))"

   interpret MX: sigma_algebra MX using assms by simp

   show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"

   interpret MY: sigma_algebra MY using assms by simp

     by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)

   interpret P: pair_sigma_algebra MX MY by default

 qed

   show "sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default

   have sa: "sigma_algebra M" by default

 locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +

   show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)"

     unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)

 qed

 lemma (in prob_space) joint_distribution_commute_singleton:

   "joint_distribution X Y {(x, y)} = joint_distribution Y X {(y, x)}"

   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

 lemma (in prob_space) joint_distribution_assoc_singleton:

   "joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} =

    joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}"

   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2

 sublocale pair_prob_space \<subseteq> P: prob_space P

 proof

   show "measure_space P" ..

   show "measure P (space P) = 1"

     by (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure)

 qed

 lemma countably_additiveI[case_names countably]:

   assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow>

     (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"

   shows "countably_additive M \<mu>"

   using assms unfolding countably_additive_def by auto

 lemma (in prob_space) joint_distribution_prob_space:

   assumes "random_variable MX X" "random_variable MY Y"

   shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := ereal \<circ> joint_distribution X Y\<rparr>)"

   using random_variable_pairI[OF assms] by (rule distribution_prob_space)

 locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +

   show "measure_space P" ..

   show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1"

   show "measure P (space P) = 1"

     by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM)

     by (simp add: measure_times M.measure_space_1 setprod_1)

   have "ereal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)"

   have "ereal (measure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)) = emeasure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)"

     using X by (intro finite_measure_eq[symmetric] in_P) auto

     using X by (simp add: emeasure_eq_measure)

   also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i (X i))"

   also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"

   also have "\<dots> = ereal (\<Prod>i\<in>I. M.\<mu>' i (X i))"

   also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))"

     using X by (simp add: M.finite_measure_eq setprod_ereal)

     using X by (simp add: M.emeasure_eq_measure setprod_ereal)

 lemma (in prob_space) random_variable_restrict:

 section {* Distributions *}

   assumes I: "finite I"

   assumes X: "\<And>i. i \<in> I \<Longrightarrow> random_variable (N i) (X i)"

 definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 

   shows "random_variable (Pi\<^isub>M I N) (\<lambda>x. \<lambda>i\<in>I. X i x)"

   f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"

 lemma

   shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"

     and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"

     and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"

     and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"

   by (simp_all add: distributed_def)

 lemma

   shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"

     and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"

   by (simp_all add: distributed_def borel_measurable_ereal_iff)

 lemma distributed_count_space:

   assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"

   shows "P a = emeasure M (X -` {a} \<inter> space M)"

 proof -

   have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"

     using X a A by (simp add: distributed_measurable emeasure_distr)

   also have "\<dots> = emeasure (density (count_space A) P) {a}"

     using X by (simp add: distributed_distr_eq_density)

   also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"

     using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)

   also have "\<dots> = P a"

     using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)

   finally show ?thesis ..

 qed

 lemma distributed_cong_density:

   "(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow>

     distributed M N X f \<longleftrightarrow> distributed M N X g"

   by (auto simp: distributed_def intro!: density_cong)

 lemma subdensity:

   assumes T: "T \<in> measurable P Q"

   assumes f: "distributed M P X f"

   assumes g: "distributed M Q Y g"

   assumes Y: "Y = T \<circ> X"

   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"

 proof -

   have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))"

     using g Y by (auto simp: null_sets_density_iff distributed_def)

   also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T"

     using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])

   finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)"

     using T by (subst (asm) null_sets_distr_iff) auto

   also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}"

     using T by (auto dest: measurable_space)

   finally show ?thesis

     using f g by (auto simp add: null_sets_density_iff distributed_def)

 qed

 lemma subdensity_real:

   fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real"

   assumes T: "T \<in> measurable P Q"

   assumes f: "distributed M P X f"

   assumes g: "distributed M Q Y g"

   assumes Y: "Y = T \<circ> X"

   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"

   using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto

 lemma distributed_integral:

   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"

   by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable

                  distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)

 lemma distributed_transform_integral:

   assumes Px: "distributed M N X Px"

   assumes "distributed M P Y Py"

   assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"

   shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)"

 proof -

   have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)"

     by (rule distributed_integral) fact+

   also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)"

     using Y by simp

   also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)"

     using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)

   finally show ?thesis .

 qed

 lemma distributed_marginal_eq_joint:

   assumes T: "sigma_finite_measure T"

   assumes S: "sigma_finite_measure S"

   assumes Px: "distributed M S X Px"

   assumes Py: "distributed M T Y Py"

   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"

   shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"

 proof (rule sigma_finite_measure.density_unique[OF T])

   interpret ST: pair_sigma_finite S T using S T unfolding pair_sigma_finite_def by simp

   show "Py \<in> borel_measurable T" "AE y in T. 0 \<le> Py y"

     "(\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S) \<in> borel_measurable T" "AE y in T. 0 \<le> \<integral>\<^isup>+ x. Pxy (x, y) \<partial>S"

     using Pxy[THEN distributed_borel_measurable]

     by (auto intro!: Py[THEN distributed_borel_measurable] Py[THEN distributed_AE]

                      ST.positive_integral_snd_measurable' positive_integral_positive)

   show "density T Py = density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)"

   proof (rule measure_eqI)

     fix A assume A: "A \<in> sets (density T Py)"

     have *: "\<And>x y. x \<in> space S \<Longrightarrow> indicator (space S \<times> A) (x, y) = indicator A y"

       by (auto simp: indicator_def)

     have "emeasure (density T Py) A = emeasure (distr M T Y) A"

       unfolding Py[THEN distributed_distr_eq_density] ..

     also have "\<dots> = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (space S \<times> A)"

       using A Px Py Pxy

       by (subst (1 2) emeasure_distr)

          (auto dest: measurable_space distributed_measurable intro!: arg_cong[where f="emeasure M"])

     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (space S \<times> A)"

       unfolding Pxy[THEN distributed_distr_eq_density] ..

     also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator (space S \<times> A) x \<partial>(S \<Otimes>\<^isub>M T))"

       using A Pxy by (simp add: emeasure_density distributed_borel_measurable)

     also have "\<dots> = (\<integral>\<^isup>+y. \<integral>\<^isup>+x. Pxy (x, y) * indicator (space S \<times> A) (x, y) \<partial>S \<partial>T)"

       using A Pxy

       by (subst ST.positive_integral_snd_measurable) (simp_all add: emeasure_density distributed_borel_measurable)

     also have "\<dots> = (\<integral>\<^isup>+y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S) * indicator A y \<partial>T)"

       using measurable_comp[OF measurable_Pair1[OF measurable_identity] distributed_borel_measurable[OF Pxy]]

       using distributed_borel_measurable[OF Pxy] distributed_AE[OF Pxy, THEN ST.AE_pair]

       by (subst (asm) ST.AE_commute) (auto intro!: positive_integral_cong_AE positive_integral_multc cong: positive_integral_cong simp: * comp_def)

     also have "\<dots> = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A"

       using A by (intro emeasure_density[symmetric])  (auto intro!: ST.positive_integral_snd_measurable' Pxy[THEN distributed_borel_measurable])

     finally show "emeasure (density T Py) A = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" .

   qed simp

 qed

 lemma (in prob_space) distr_marginal1:

   fixes Pxy :: "('b \<times> 'c) \<Rightarrow> real"

   assumes "sigma_finite_measure S" "sigma_finite_measure T"

   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"

   defines "Px \<equiv> \<lambda>x. real (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"

   shows "distributed M S X Px"

   unfolding distributed_def

 proof safe

   interpret S: sigma_finite_measure S by fact

   interpret T: sigma_finite_measure T by fact

   interpret ST: pair_sigma_finite S T by default

   have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"

     using Pxy by (rule distributed_measurable)

   then show X: "X \<in> measurable M S"

     unfolding measurable_pair_iff by (simp add: comp_def)

   from XY have Y: "Y \<in> measurable M T"

     unfolding measurable_pair_iff by (simp add: comp_def)

   from Pxy show borel: "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S"

     by (auto intro!: ST.positive_integral_fst_measurable borel_measurable_real_of_ereal dest!: distributed_real_measurable simp: Px_def)

   interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"

     using XY by (rule prob_space_distr)

   have "(\<integral>\<^isup>+ x. max 0 (ereal (- Pxy x)) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"

     using Pxy

     by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_real_measurable distributed_real_AE)

   then have Pxy_integrable: "integrable (S \<Otimes>\<^isub>M T) Pxy"

     using Pxy Pxy.emeasure_space_1

     by (simp add: integrable_def emeasure_density positive_integral_max_0 distributed_def borel_measurable_ereal_iff cong: positive_integral_cong)

   show "distr M S X = density S Px"

   proof (rule measure_eqI)

     fix A assume A: "A \<in> sets (distr M S X)"

     with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"

       by (auto simp add: emeasure_distr

                intro!: arg_cong[where f="emeasure M"] dest: measurable_space)

     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"

       using Pxy by (simp add: distributed_def)

     also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"

       using A borel Pxy

       by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def)

     also have "\<dots> = \<integral>\<^isup>+ x. ereal (Px x) * indicator A x \<partial>S"

       apply (rule positive_integral_cong_AE)

       using Pxy[THEN distributed_real_AE, THEN ST.AE_pair] ST.integrable_fst_measurable(1)[OF Pxy_integrable] AE_space

     proof eventually_elim

       fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" and i: "integrable T (\<lambda>y. Pxy (x, y))"

       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"

         by (auto simp: indicator_def)

       ultimately have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) =

           (\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) * indicator A x"

         using Pxy[THEN distributed_real_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)

       also have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) = Px x"

         using i by (simp add: Px_def ereal_real integrable_def positive_integral_positive)

       finally show "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = ereal (Px x) * indicator A x" .

     qed

     finally show "emeasure (distr M S X) A = emeasure (density S Px) A"

       using A borel Pxy by (simp add: emeasure_density)

   qed simp

   show "AE x in S. 0 \<le> ereal (Px x)"

     by (simp add: Px_def positive_integral_positive real_of_ereal_pos)

 qed

 definition

   "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>

     finite (X`space M)"

 lemma simple_distributed:

   "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px"

   unfolding simple_distributed_def by auto

 lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)"

   by (simp add: simple_distributed_def)

 lemma (in prob_space) distributed_simple_function_superset:

   assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"

   assumes A: "X`space M \<subseteq> A" "finite A"

   defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)"

   shows "distributed M S X P'"

   unfolding distributed_def

 proof safe

   show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp

   show "AE x in S. 0 \<le> ereal (P' x)"

     using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg)

   show "distr M S X = density S P'"

   proof (rule measure_eqI_finite)

     show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"

       using A unfolding S_def by auto

     show "finite A" by fact

     fix a assume a: "a \<in> A"

     then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto

     with A a X have "emeasure (distr M S X) {a} = P' a"

       by (subst emeasure_distr)

          (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure

                intro!: arg_cong[where f=prob])

     also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"

       using A X a

       by (subst positive_integral_cmult_indicator)

          (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)

     also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)"

       by (auto simp: indicator_def intro!: positive_integral_cong)

     also have "\<dots> = emeasure (density S P') {a}"

       using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)

     finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .

   qed

   show "random_variable S X"

     using X(1) A by (auto simp: measurable_def simple_functionD S_def)

 qed

 lemma (in prob_space) simple_distributedI:

   assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"

   shows "simple_distributed M X P"

   unfolding simple_distributed_def

   { fix i assume "i \<in> I"

   have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))"

     with X interpret N: sigma_algebra "N i" by simp

     (is "?A")

     have "sets (N i) \<subseteq> Pow (space (N i))" by (rule N.space_closed) }

     using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto

   note N_closed = this

   also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))"

   then show "sigma_algebra (Pi\<^isub>M I N)"

     by (rule distributed_cong_density) auto

     by (simp add: product_algebra_def)

   finally show "\<dots>" .

        (intro sigma_algebra_sigma product_algebra_generator_sets_into_space)

 qed (rule simple_functionD[OF X(1)])

   show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"

     using X by (intro measurable_restrict[OF I N_closed]) auto

 lemma simple_distributed_joint_finite:

 qed

   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"

   shows "finite (X ` space M)" "finite (Y ` space M)"

 section "Probability spaces on finite sets"

 proof -

   have "finite ((\<lambda>x. (X x, Y x)) ` space M)"

 locale finite_prob_space = prob_space + finite_measure_space

     using X by (auto simp: simple_distributed_def simple_functionD)

   then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)"

 abbreviation (in prob_space) "finite_random_variable M' X \<equiv> finite_sigma_algebra M' \<and> X \<in> measurable M M'"

     by auto

   then show fin: "finite (X ` space M)" "finite (Y ` space M)"

 lemma (in prob_space) finite_random_variableD:

     by (auto simp: image_image)

   assumes "finite_random_variable M' X" shows "random_variable M' X"

 qed

 proof -

   interpret M': finite_sigma_algebra M' using assms by simp

 lemma simple_distributed_joint2_finite:

   show "random_variable M' X" using assms by simp default

   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"

 qed

   shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"

 proof -

 lemma (in prob_space) distribution_finite_prob_space:

   have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)"

   assumes "finite_random_variable MX X"

     using X by (auto simp: simple_distributed_def simple_functionD)

   shows "finite_prob_space (MX\<lparr>measure := ereal \<circ> distribution X\<rparr>)"

   then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"

 proof -

     "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"

   interpret X: prob_space "MX\<lparr>measure := ereal \<circ> distribution X\<rparr>"

     "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"

     using assms[THEN finite_random_variableD] by (rule distribution_prob_space)

     by auto

   interpret MX: finite_sigma_algebra MX

   then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"

     using assms by auto

     by (auto simp: image_image)

   show ?thesis by default (simp_all add: MX.finite_space)

 qed

 qed

 lemma simple_distributed_simple_function:

 lemma (in prob_space) simple_function_imp_finite_random_variable[simp, intro]:

   "simple_distributed M X Px \<Longrightarrow> simple_function M X"

   assumes "simple_function M X"

   unfolding simple_distributed_def distributed_def

   shows "finite_random_variable \<lparr> space = X`space M, sets = Pow (X`space M), \<dots> = x \<rparr> X"

   by (auto simp: simple_function_def)

     (is "finite_random_variable ?X _")

 proof (intro conjI)

 lemma simple_distributed_measure:

   have [simp]: "finite (X ` space M)" using assms unfolding simple_function_def by simp

   "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"

   interpret X: sigma_algebra ?X by (rule sigma_algebra_Pow)

   using distributed_count_space[of M "X`space M" X P a, symmetric]

   show "finite_sigma_algebra ?X"

   by (auto simp: simple_distributed_def measure_def)

     by default auto

   show "X \<in> measurable M ?X"

 lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)"

   proof (unfold measurable_def, clarsimp)

   by (auto simp: simple_distributed_measure measure_nonneg)

     fix A assume A: "A \<subseteq> X`space M"

     then have "finite A" by (rule finite_subset) simp

 lemma (in prob_space) simple_distributed_joint:

     then have "X -` (\<Union>a\<in>A. {a}) \<inter> space M \<in> events"

   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"

       unfolding vimage_UN UN_extend_simps

   defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)"

       apply (rule finite_UN)

   defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"

       using A assms unfolding simple_function_def by auto

   shows "distributed M S (\<lambda>x. (X x, Y x)) P"

     then show "X -` A \<inter> space M \<in> events" by simp

 proof -

   qed

   from simple_distributed_joint_finite[OF X, simp]

 qed

   have S_eq: "S = count_space (X`space M \<times> Y`space M)"

     by (simp add: S_def pair_measure_count_space)

 lemma (in prob_space) simple_function_imp_random_variable[simp, intro]:

   show ?thesis

   assumes "simple_function M X"

     unfolding S_eq P_def

   shows "random_variable \<lparr> space = X`space M, sets = Pow (X`space M), \<dots> = ext \<rparr> X"

   proof (rule distributed_simple_function_superset)

   using simple_function_imp_finite_random_variable[OF assms, of ext]

     show "simple_function M (\<lambda>x. (X x, Y x))"

   by (auto dest!: finite_random_variableD)

       using X by (rule simple_distributed_simple_function)

     fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"

 lemma (in prob_space) sum_over_space_real_distribution:

     from simple_distributed_measure[OF X this]

   "simple_function M X \<Longrightarrow> (\<Sum>x\<in>X`space M. distribution X {x}) = 1"

     show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" .

   unfolding distribution_def prob_space[symmetric]

   qed auto

   by (subst finite_measure_finite_Union[symmetric])

 qed

      (auto simp add: disjoint_family_on_def simple_function_def

            intro!: arg_cong[where f=prob])

 lemma (in prob_space) simple_distributed_joint2:

   assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"

 lemma (in prob_space) finite_random_variable_pairI:

   defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M) \<Otimes>\<^isub>M count_space (Z`space M)"

   assumes "finite_random_variable MX X"

   defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)"

   assumes "finite_random_variable MY Y"

   shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P"

   shows "finite_random_variable (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))"

 proof -

   from simple_distributed_joint2_finite[OF X, simp]

   have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)"

     by (simp add: S_def pair_measure_count_space)

   show ?thesis

     unfolding S_eq P_def

   proof (rule distributed_simple_function_superset)

     show "simple_function M (\<lambda>x. (X x, Y x, Z x))"

       using X by (rule simple_distributed_simple_function)

     fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M"

     from simple_distributed_measure[OF X this]

     show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" .

   qed auto

 qed

 lemma (in prob_space) simple_distributed_setsum_space:

   assumes X: "simple_distributed M X f"

   shows "setsum f (X`space M) = 1"

 proof -

   from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)"

     by (subst finite_measure_finite_Union)

        (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD

              intro!: setsum_cong arg_cong[where f="prob"])

   also have "\<dots> = prob (space M)"

     by (auto intro!: arg_cong[where f=prob])

   finally show ?thesis

     using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def)

 qed

 lemma (in prob_space) distributed_marginal_eq_joint_simple:

   assumes Px: "simple_function M X"

   assumes Py: "simple_distributed M Y Py"

   assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"

   assumes y: "y \<in> Y`space M"

   shows "Py y = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)"

 proof -

   note Px = simple_distributedI[OF Px refl]

   have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)"

     by (simp add: setsum_ereal[symmetric] zero_ereal_def)

   from distributed_marginal_eq_joint[OF sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite

     simple_distributed[OF Px] simple_distributed[OF Py] simple_distributed_joint[OF Pxy],

     OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]

     y Px[THEN simple_distributed_finite] Py[THEN simple_distributed_finite]

     Pxy[THEN simple_distributed, THEN distributed_real_AE]

   show ?thesis

     unfolding AE_count_space

     apply (elim ballE[where x=y])

     apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)

     done

 qed

 lemma prob_space_uniform_measure:

   assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"

   shows "prob_space (uniform_measure M A)"

   interpret MX: finite_sigma_algebra MX using assms by simp

   show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"

   interpret MY: finite_sigma_algebra MY using assms by simp

     using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]

   interpret P: pair_finite_sigma_algebra MX MY by default

     using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A

   show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" ..

     by (simp add: Int_absorb2 emeasure_nonneg)

   have sa: "sigma_algebra M" by default

 qed

   show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)"

     unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)

 lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"

 qed