[STATEMENT]
lemma (in prob_space) simple_distributed_joint:
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)"
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"
  shows "distributed M S (\<lambda>x. (X x, Y x)) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
from simple_distributed_joint_finite[OF X, simp]
[PROOF STATE]
proof (chain)
picking this:
finite (X ` space M)
finite (Y ` space M)
[PROOF STEP]
have S_eq: "S = count_space (X`space M \<times> Y`space M)"
[PROOF STATE]
proof (prove)
using this:
finite (X ` space M)
finite (Y ` space M)

goal (1 subgoal):
 1. S = count_space (X ` space M \<times> Y ` space M)
[PROOF STEP]
by (simp add: S_def pair_measure_count_space)
[PROOF STATE]
proof (state)
this:
S = count_space (X ` space M \<times> Y ` space M)

goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
unfolding S_eq P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M (count_space (X ` space M \<times> Y ` space M)) (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Px x else 0))
[PROOF STEP]
proof (rule distributed_simple_function_superset)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. simple_function M (\<lambda>x. (X x, Y x))
 2. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 3. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 4. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
show "simple_function M (\<lambda>x. (X x, Y x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_function M (\<lambda>x. (X x, Y x))
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
simple_distributed M (\<lambda>x. (X x, Y x)) Px

goal (1 subgoal):
 1. simple_function M (\<lambda>x. (X x, Y x))
[PROOF STEP]
by (rule simple_distributed_simple_function)
[PROOF STATE]
proof (state)
this:
simple_function M (\<lambda>x. (X x, Y x))

goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. (X x, Y x)) ` space M

goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
from simple_distributed_measure[OF X this]
[PROOF STATE]
proof (chain)
picking this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
[PROOF STEP]
show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
[PROOF STATE]
proof (prove)
using this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)

goal (1 subgoal):
 1. Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)

goal (2 subgoals):
 1. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 2. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))

goal:
No subgoals!
[PROOF STEP]
qed