35582

1 
theory Probability_Space

38656

2 
imports Lebesgue_Integration

35582

3 
begin


4 

38656

5 
lemma (in measure_space) measure_inter_full_set:


6 
assumes "S \<in> sets M" "T \<in> sets M" and not_\<omega>: "\<mu> (T  S) \<noteq> \<omega>"


7 
assumes T: "\<mu> T = \<mu> (space M)"


8 
shows "\<mu> (S \<inter> T) = \<mu> S"


9 
proof (rule antisym)


10 
show " \<mu> (S \<inter> T) \<le> \<mu> S"


11 
using assms by (auto intro!: measure_mono)


12 


13 
show "\<mu> S \<le> \<mu> (S \<inter> T)"


14 
proof (rule ccontr)


15 
assume contr: "\<not> ?thesis"


16 
have "\<mu> (space M) = \<mu> ((T  S) \<union> (S \<inter> T))"


17 
unfolding T[symmetric] by (auto intro!: arg_cong[where f="\<mu>"])


18 
also have "\<dots> \<le> \<mu> (T  S) + \<mu> (S \<inter> T)"


19 
using assms by (auto intro!: measure_subadditive)


20 
also have "\<dots> < \<mu> (T  S) + \<mu> S"


21 
by (rule pinfreal_less_add[OF not_\<omega>]) (insert contr, auto)


22 
also have "\<dots> = \<mu> (T \<union> S)"


23 
using assms by (subst measure_additive) auto


24 
also have "\<dots> \<le> \<mu> (space M)"


25 
using assms sets_into_space by (auto intro!: measure_mono)


26 
finally show False ..


27 
qed


28 
qed


29 


30 
lemma (in finite_measure) finite_measure_inter_full_set:


31 
assumes "S \<in> sets M" "T \<in> sets M"


32 
assumes T: "\<mu> T = \<mu> (space M)"


33 
shows "\<mu> (S \<inter> T) = \<mu> S"


34 
using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms


35 
by auto


36 

35582

37 
locale prob_space = measure_space +

38656

38 
assumes measure_space_1: "\<mu> (space M) = 1"


39 


40 
sublocale prob_space < finite_measure


41 
proof


42 
from measure_space_1 show "\<mu> (space M) \<noteq> \<omega>" by simp


43 
qed


44 


45 
context prob_space

35582

46 
begin


47 


48 
abbreviation "events \<equiv> sets M"

38656

49 
abbreviation "prob \<equiv> \<lambda>A. real (\<mu> A)"

35582

50 
abbreviation "prob_preserving \<equiv> measure_preserving"


51 
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"


52 
abbreviation "expectation \<equiv> integral"


53 


54 
definition


55 
"indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"


56 


57 
definition


58 
"indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"


59 


60 
definition

38656

61 
"distribution X = (\<lambda>s. \<mu> ((X ` s) \<inter> (space M)))"

35582

62 

36624

63 
abbreviation


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

35582

65 

38656

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


67 
unfolding measure_space_1 by simp

35582

68 

38656

69 
lemma measure_le_1[simp, intro]:


70 
assumes "A \<in> events" shows "\<mu> A \<le> 1"


71 
proof 


72 
have "\<mu> A \<le> \<mu> (space M)"


73 
using assms sets_into_space by(auto intro!: measure_mono)


74 
also note measure_space_1


75 
finally show ?thesis .


76 
qed

35582

77 

38656

78 
lemma measure_finite[simp, intro]:


79 
assumes "A \<in> events" shows "\<mu> A \<noteq> \<omega>"


80 
using measure_le_1[OF assms] by auto

35582

81 


82 
lemma prob_compl:

38656

83 
assumes "A \<in> events"


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


85 
using `A \<in> events`[THEN sets_into_space] `A \<in> events` measure_space_1


86 
by (subst real_finite_measure_Diff) auto

35582

87 


88 
lemma indep_space:


89 
assumes "s \<in> events"


90 
shows "indep (space M) s"

38656

91 
using assms prob_space by (simp add: indep_def)

35582

92 

38656

93 
lemma prob_space_increasing: "increasing M prob"


94 
by (auto intro!: real_measure_mono simp: increasing_def)

35582

95 


96 
lemma prob_zero_union:


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


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

38656

99 
using assms

35582

100 
proof 


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

38656

102 
using real_finite_measure_subadditive[of s t] assms by auto

35582

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

38656

104 
using assms by (blast intro: real_measure_mono)

35582

105 
ultimately show ?thesis by simp


106 
qed


107 


108 
lemma prob_eq_compl:


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


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


111 
shows "prob s = prob t"

38656

112 
using assms prob_compl by auto

35582

113 


114 
lemma prob_one_inter:


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


116 
assumes "prob t = 1"


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


118 
proof 

38656

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


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


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


122 
by blast


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


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

35582

125 
qed


126 


127 
lemma prob_eq_bigunion_image:


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


129 
assumes "disjoint_family f" "disjoint_family g"


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


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


132 
using assms


133 
proof 

38656

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


135 
by (rule real_finite_measure_UNION[OF assms(1,3)])


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


137 
by (rule real_finite_measure_UNION[OF assms(2,4)])


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

35582

139 
qed


140 


141 
lemma prob_countably_zero:


142 
assumes "range c \<subseteq> events"


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

38656

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


145 
proof (rule antisym)


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


147 
using real_finite_measurable_countably_subadditive[OF assms(1)]


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


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

35582

150 
qed


151 


152 
lemma indep_sym:


153 
"indep a b \<Longrightarrow> indep b a"


154 
unfolding indep_def using Int_commute[of a b] by auto


155 


156 
lemma indep_refl:


157 
assumes "a \<in> events"


158 
shows "indep a a = (prob a = 0) \<or> (prob a = 1)"


159 
using assms unfolding indep_def by auto


160 


161 
lemma prob_equiprobable_finite_unions:

38656

162 
assumes "s \<in> events"


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

35582

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

38656

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

35582

166 
proof (cases "s = {}")

38656

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

35582

168 
from someI_ex[OF this] assms


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


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

38656

171 
using real_finite_measure_finite_singelton[OF s_finite] by simp

35582

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

38656

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


174 
using setsum_constant assms by (simp add: real_eq_of_nat)

35582

175 
finally show ?thesis by simp

38656

176 
qed simp

35582

177 


178 
lemma prob_real_sum_image_fn:


179 
assumes "e \<in> events"


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


181 
assumes "finite s"

38656

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


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

35582

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


185 
proof 

38656

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


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


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


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


190 
proof (rule real_finite_measure_finite_Union)


191 
show "finite s" by fact


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


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


194 
using disjoint by (auto simp: disjoint_family_on_def)


195 
qed


196 
finally show ?thesis .

35582

197 
qed


198 


199 
lemma distribution_prob_space:

38656

200 
fixes S :: "('c, 'd) algebra_scheme"


201 
assumes "sigma_algebra S" "random_variable S X"


202 
shows "prob_space S (distribution X)"

35582

203 
proof 

38656

204 
interpret S: sigma_algebra S by fact


205 
show ?thesis


206 
proof


207 
show "distribution X {} = 0" unfolding distribution_def by simp


208 
have "X ` space S \<inter> space M = space M"


209 
using `random_variable S X` by (auto simp: measurable_def)


210 
then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def)

35582

211 

38656

212 
show "countably_additive S (distribution X)"


213 
proof (unfold countably_additive_def, safe)


214 
fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A"


215 
hence *: "\<And>i. X ` A i \<inter> space M \<in> sets M"


216 
using `random_variable S X` by (auto simp: measurable_def)


217 
moreover hence "\<And>i. \<mu> (X ` A i \<inter> space M) \<noteq> \<omega>"


218 
using finite_measure by auto


219 
moreover have "(\<Union>i. X ` A i \<inter> space M) \<in> sets M"


220 
using * by blast


221 
moreover hence "\<mu> (\<Union>i. X ` A i \<inter> space M) \<noteq> \<omega>"


222 
using finite_measure by auto


223 
moreover have **: "disjoint_family (\<lambda>i. X ` A i \<inter> space M)"


224 
using `disjoint_family A` by (auto simp: disjoint_family_on_def)


225 
ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)"


226 
using measure_countably_additive[OF _ **]


227 
by (auto simp: distribution_def Real_real comp_def vimage_UN)


228 
qed

35582

229 
qed


230 
qed


231 


232 
lemma distribution_lebesgue_thm1:


233 
assumes "random_variable s X"


234 
assumes "A \<in> sets s"

38656

235 
shows "real (distribution X A) = expectation (indicator (X ` A \<inter> space M))"

35582

236 
unfolding distribution_def


237 
using assms unfolding measurable_def

38656

238 
using integral_indicator by auto

35582

239 


240 
lemma distribution_lebesgue_thm2:

38656

241 
assumes "sigma_algebra S" "random_variable S X" and "A \<in> sets S"


242 
shows "distribution X A =


243 
measure_space.positive_integral S (distribution X) (indicator A)"


244 
(is "_ = measure_space.positive_integral _ ?D _")

35582

245 
proof 

38656

246 
interpret S: prob_space S "distribution X" using assms(1,2) by (rule distribution_prob_space)

35582

247 


248 
show ?thesis

38656

249 
using S.positive_integral_indicator(1)

35582

250 
using assms unfolding distribution_def by auto


251 
qed


252 


253 
lemma finite_expectation1:

38656

254 
assumes "finite (X`space M)" and rv: "random_variable borel_space X"

35582

255 
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X ` {r} \<inter> space M))"

38656

256 
proof (rule integral_on_finite(2)[OF assms(2,1)])


257 
fix x have "X ` {x} \<inter> space M \<in> sets M"


258 
using rv unfolding measurable_def by auto


259 
thus "\<mu> (X ` {x} \<inter> space M) \<noteq> \<omega>" using finite_measure by simp


260 
qed

35582

261 


262 
lemma finite_expectation:

38656

263 
assumes "finite (space M)" "random_variable borel_space X"


264 
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * real (distribution X {r}))"


265 
using assms unfolding distribution_def using finite_expectation1 by auto


266 

35582

267 
lemma prob_x_eq_1_imp_prob_y_eq_0:


268 
assumes "{x} \<in> events"

38656

269 
assumes "prob {x} = 1"

35582

270 
assumes "{y} \<in> events"


271 
assumes "y \<noteq> x"


272 
shows "prob {y} = 0"


273 
using prob_one_inter[of "{y}" "{x}"] assms by auto


274 

38656

275 
lemma distribution_empty[simp]: "distribution X {} = 0"


276 
unfolding distribution_def by simp


277 


278 
lemma distribution_space[simp]: "distribution X (X ` space M) = 1"


279 
proof 


280 
have "X ` X ` space M \<inter> space M = space M" by auto


281 
thus ?thesis unfolding distribution_def by (simp add: measure_space_1)


282 
qed


283 


284 
lemma distribution_one:


285 
assumes "random_variable M X" and "A \<in> events"


286 
shows "distribution X A \<le> 1"


287 
proof 


288 
have "distribution X A \<le> \<mu> (space M)" unfolding distribution_def


289 
using assms[unfolded measurable_def] by (auto intro!: measure_mono)


290 
thus ?thesis by (simp add: measure_space_1)


291 
qed


292 


293 
lemma distribution_finite:


294 
assumes "random_variable M X" and "A \<in> events"


295 
shows "distribution X A \<noteq> \<omega>"


296 
using distribution_one[OF assms] by auto


297 

35582

298 
lemma distribution_x_eq_1_imp_distribution_y_eq_0:


299 
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"

38656

300 
(is "random_variable ?S X")


301 
assumes "distribution X {x} = 1"

35582

302 
assumes "y \<noteq> x"


303 
shows "distribution X {y} = 0"


304 
proof 

38656

305 
have "sigma_algebra ?S" by (rule sigma_algebra_Pow)


306 
from distribution_prob_space[OF this X]


307 
interpret S: prob_space ?S "distribution X" by simp


308 


309 
have x: "{x} \<in> sets ?S"


310 
proof (rule ccontr)


311 
assume "{x} \<notin> sets ?S"

35582

312 
hence "X ` {x} \<inter> space M = {}" by auto

38656

313 
thus "False" using assms unfolding distribution_def by auto


314 
qed


315 


316 
have [simp]: "{y} \<inter> {x} = {}" "{x}  {y} = {x}" using `y \<noteq> x` by auto


317 


318 
show ?thesis


319 
proof cases


320 
assume "{y} \<in> sets ?S"


321 
with `{x} \<in> sets ?S` assms show "distribution X {y} = 0"


322 
using S.measure_inter_full_set[of "{y}" "{x}"]


323 
by simp


324 
next


325 
assume "{y} \<notin> sets ?S"

35582

326 
hence "X ` {y} \<inter> space M = {}" by auto

38656

327 
thus "distribution X {y} = 0" unfolding distribution_def by auto


328 
qed

35582

329 
qed


330 


331 
end


332 

35977

333 
locale finite_prob_space = prob_space + finite_measure_space


334 

36624

335 
lemma finite_prob_space_eq:

38656

336 
"finite_prob_space M \<mu> \<longleftrightarrow> finite_measure_space M \<mu> \<and> \<mu> (space M) = 1"

36624

337 
unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def


338 
by auto


339 


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


341 
using prob_space empty_measure by auto


342 

38656

343 
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1"


344 
using measure_space_1 sum_over_space by simp

36624

345 


346 
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x"

38656

347 
unfolding distribution_def by simp

36624

348 


349 
lemma (in finite_prob_space) joint_distribution_restriction_fst:


350 
"joint_distribution X Y A \<le> distribution X (fst ` A)"


351 
unfolding distribution_def


352 
proof (safe intro!: measure_mono)


353 
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"


354 
show "x \<in> X ` fst ` A"


355 
by (auto intro!: image_eqI[OF _ *])


356 
qed (simp_all add: sets_eq_Pow)


357 


358 
lemma (in finite_prob_space) joint_distribution_restriction_snd:


359 
"joint_distribution X Y A \<le> distribution Y (snd ` A)"


360 
unfolding distribution_def


361 
proof (safe intro!: measure_mono)


362 
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A"


363 
show "x \<in> Y ` snd ` A"


364 
by (auto intro!: image_eqI[OF _ *])


365 
qed (simp_all add: sets_eq_Pow)


366 


367 
lemma (in finite_prob_space) distribution_order:


368 
shows "0 \<le> distribution X x'"


369 
and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')"


370 
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}"


371 
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}"


372 
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}"


373 
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}"


374 
and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"


375 
and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0"


376 
using positive_distribution[of X x']


377 
positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"]


378 
joint_distribution_restriction_fst[of X Y "{(x, y)}"]


379 
joint_distribution_restriction_snd[of X Y "{(x, y)}"]


380 
by auto


381 


382 
lemma (in finite_prob_space) finite_product_measure_space:

35977

383 
assumes "finite s1" "finite s2"

38656

384 
shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2)\<rparr> (joint_distribution X Y)"


385 
(is "finite_measure_space ?M ?D")

35977

386 
proof (rule finite_Pow_additivity_sufficient)

38656

387 
show "positive ?D"


388 
unfolding positive_def using assms sets_eq_Pow

36624

389 
by (simp add: distribution_def)

35977

390 

38656

391 
show "additive ?M ?D" unfolding additive_def

35977

392 
proof safe


393 
fix x y


394 
have A: "((\<lambda>x. (X x, Y x)) ` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto


395 
have B: "((\<lambda>x. (X x, Y x)) ` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto


396 
assume "x \<inter> y = {}"

38656

397 
hence "(\<lambda>x. (X x, Y x)) ` x \<inter> space M \<inter> ((\<lambda>x. (X x, Y x)) ` y \<inter> space M) = {}"


398 
by auto

35977

399 
from additive[unfolded additive_def, rule_format, OF A B] this

38656

400 
finite_measure[OF A] finite_measure[OF B]


401 
show "?D (x \<union> y) = ?D x + ?D y"

36624

402 
apply (simp add: distribution_def)

35977

403 
apply (subst Int_Un_distrib2)

38656

404 
by (auto simp: real_of_pinfreal_add)

35977

405 
qed


406 


407 
show "finite (space ?M)"


408 
using assms by auto


409 


410 
show "sets ?M = Pow (space ?M)"


411 
by simp

38656

412 


413 
{ fix x assume "x \<in> space ?M" thus "?D {x} \<noteq> \<omega>"


414 
unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) }

35977

415 
qed


416 

36624

417 
lemma (in finite_prob_space) finite_product_measure_space_of_images:

35977

418 
shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,

38656

419 
sets = Pow (X ` space M \<times> Y ` space M) \<rparr>


420 
(joint_distribution X Y)"

36624

421 
using finite_space by (auto intro!: finite_product_measure_space)


422 


423 
lemma (in finite_prob_space) finite_measure_space:

38656

424 
shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"


425 
(is "finite_measure_space ?S _")

36624

426 
proof (rule finite_Pow_additivity_sufficient, simp_all)


427 
show "finite (X ` space M)" using finite_space by simp


428 

38656

429 
show "positive (distribution X)"


430 
unfolding distribution_def positive_def using sets_eq_Pow by auto

36624

431 


432 
show "additive ?S (distribution X)" unfolding additive_def distribution_def


433 
proof (simp, safe)


434 
fix x y


435 
have x: "(X ` x) \<inter> space M \<in> sets M"


436 
and y: "(X ` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto


437 
assume "x \<inter> y = {}"

38656

438 
hence "X ` x \<inter> space M \<inter> (X ` y \<inter> space M) = {}" by auto

36624

439 
from additive[unfolded additive_def, rule_format, OF x y] this

38656

440 
finite_measure[OF x] finite_measure[OF y]


441 
have "\<mu> (((X ` x) \<union> (X ` y)) \<inter> space M) =


442 
\<mu> ((X ` x) \<inter> space M) + \<mu> ((X ` y) \<inter> space M)"


443 
by (subst Int_Un_distrib2) auto


444 
thus "\<mu> ((X ` x \<union> X ` y) \<inter> space M) = \<mu> (X ` x \<inter> space M) + \<mu> (X ` y \<inter> space M)"

36624

445 
by auto


446 
qed

38656

447 


448 
{ fix x assume "x \<in> X ` space M" thus "distribution X {x} \<noteq> \<omega>"


449 
unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) }

36624

450 
qed


451 


452 
lemma (in finite_prob_space) finite_prob_space_of_images:

38656

453 
"finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)"


454 
by (simp add: finite_prob_space_eq finite_measure_space)

36624

455 


456 
lemma (in finite_prob_space) finite_product_prob_space_of_images:

38656

457 
"finite_prob_space \<lparr> space = X ` space M \<times> Y ` space M, sets = Pow (X ` space M \<times> Y ` space M)\<rparr>


458 
(joint_distribution X Y)"


459 
(is "finite_prob_space ?S _")


460 
proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images)

36624

461 
have "X ` X ` space M \<inter> Y ` Y ` space M \<inter> space M = space M" by auto


462 
thus "joint_distribution X Y (X ` space M \<times> Y ` space M) = 1"

38656

463 
by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)

36624

464 
qed

35977

465 

35582

466 
end
