35833

1 
theory Product_Measure


2 
imports "~~/src/HOL/Probability/Lebesgue"


3 
begin


4 


5 
definition


6 
"prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) ` a)))"


7 


8 
definition


9 
"prod_measure_space M M' \<equiv>


10 
\<lparr> space = space M \<times> space M',


11 
sets = sets (sigma (space M \<times> space M') (prod_sets (sets M) (sets M'))),


12 
measure = prod_measure M M' \<rparr>"


13 


14 
lemma prod_measure_times:


15 
assumes "measure_space M" and "measure_space M'" and a: "a \<in> sets M"


16 
shows "prod_measure M M' (a \<times> a') = measure M a * measure M' a'"


17 
proof 


18 
interpret M: measure_space M by fact


19 
interpret M': measure_space M' by fact


20 


21 
{ fix \<omega>


22 
have "(\<lambda>\<omega>'. (\<omega>, \<omega>')) ` (a \<times> a') = (if \<omega> \<in> a then a' else {})"


23 
by auto


24 
hence "measure M' ((\<lambda>\<omega>'. (\<omega>, \<omega>')) ` (a \<times> a')) =


25 
measure M' a' * indicator_fn a \<omega>"


26 
unfolding indicator_fn_def by auto }


27 
note vimage_eq_indicator = this


28 


29 
show ?thesis


30 
unfolding prod_measure_def vimage_eq_indicator


31 
M.integral_cmul_indicator(1)[OF `a \<in> sets M`]


32 
by simp


33 
qed


34 


35 


36 


37 
lemma measure_space_finite_prod_measure:


38 
fixes M :: "('a, 'b) measure_space_scheme"


39 
and M' :: "('c, 'd) measure_space_scheme"


40 
assumes "measure_space M" and "measure_space M'"


41 
and finM: "finite (space M)" "Pow (space M) = sets M"


42 
and finM': "finite (space M')" "Pow (space M') = sets M'"


43 
shows "measure_space (prod_measure_space M M')"


44 
proof (rule finite_additivity_sufficient)


45 
interpret M: measure_space M by fact


46 
interpret M': measure_space M' by fact


47 


48 
have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"


49 
unfolding prod_measure_space_def by simp


50 


51 
have prod_sets: "prod_sets (sets M) (sets M') \<subseteq> Pow (space M \<times> space M')"


52 
using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto


53 
show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def


54 
by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"])


55 
(simp_all add: sigma_def prod_sets)


56 


57 
then interpret sa: sigma_algebra "prod_measure_space M M'" .


58 


59 
{ fix x y assume "y \<in> sets (prod_measure_space M M')" and "x \<in> space M"


60 
hence "y \<subseteq> space M \<times> space M'"


61 
using sa.sets_into_space unfolding prod_measure_space_def by simp


62 
hence "Pair x ` y \<in> sets M'"


63 
using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }


64 
note Pair_in_sets = this


65 


66 
show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))"


67 
unfolding measure additive_def


68 
proof safe


69 
fix x y assume x: "x \<in> sets (prod_measure_space M M')" and y: "y \<in> sets (prod_measure_space M M')"


70 
and disj_x_y: "x \<inter> y = {}"


71 
{ fix z have "Pair z ` x \<inter> Pair z ` y = {}" using disj_x_y by auto }


72 
note Pair_disj = this


73 


74 
from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]


75 
show "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"


76 
unfolding prod_measure_def


77 
apply (subst (1 2 3) M.integral_finite_singleton[OF finM])


78 
by (simp_all add: setsum_addf[symmetric] field_simps)


79 
qed


80 


81 
show "finite (space (prod_measure_space M M'))"


82 
unfolding prod_measure_space_def using finM finM' by simp


83 


84 
have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"


85 
unfolding finM(2)[symmetric] by simp


86 


87 
show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))"


88 
unfolding positive_def


89 
proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def)


90 
fix Q assume "Q \<in> sets (prod_measure_space M M')"


91 
from Pair_in_sets[OF this]


92 
show "0 \<le> measure (prod_measure_space M M') Q"


93 
unfolding prod_measure_space_def prod_measure_def


94 
apply (subst M.integral_finite_singleton[OF finM])


95 
using M.positive M'.positive singletonM


96 
by (auto intro!: setsum_nonneg mult_nonneg_nonneg)


97 
qed


98 
qed


99 


100 
lemma measure_space_finite_prod_measure_alterantive:


101 
assumes "measure_space M" and "measure_space M'"


102 
and finM: "finite (space M)" "Pow (space M) = sets M"


103 
and finM': "finite (space M')" "Pow (space M') = sets M'"


104 
shows "measure_space \<lparr> space = space M \<times> space M',


105 
sets = Pow (space M \<times> space M'),


106 
measure = prod_measure M M' \<rparr>"


107 
(is "measure_space ?space")


108 
proof (rule finite_additivity_sufficient)


109 
interpret M: measure_space M by fact


110 
interpret M': measure_space M' by fact


111 


112 
show "sigma_algebra ?space"


113 
using sigma_algebra.sigma_algebra_extend[where M="\<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M') \<rparr>"]


114 
by (auto intro!: sigma_algebra_Pow)


115 
then interpret sa: sigma_algebra ?space .


116 


117 
have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"


118 
unfolding prod_measure_space_def by simp


119 


120 
{ fix x y assume "y \<in> sets ?space" and "x \<in> space M"


121 
hence "y \<subseteq> space M \<times> space M'"


122 
using sa.sets_into_space by simp


123 
hence "Pair x ` y \<in> sets M'"


124 
using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }


125 
note Pair_in_sets = this


126 


127 
show "additive ?space (measure ?space)"


128 
unfolding measure additive_def


129 
proof safe


130 
fix x y assume x: "x \<in> sets ?space" and y: "y \<in> sets ?space"


131 
and disj_x_y: "x \<inter> y = {}"


132 
{ fix z have "Pair z ` x \<inter> Pair z ` y = {}" using disj_x_y by auto }


133 
note Pair_disj = this


134 


135 
from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]


136 
show "measure ?space (x \<union> y) = measure ?space x + measure ?space y"


137 
apply (simp add: prod_measure_def)


138 
apply (subst (1 2 3) M.integral_finite_singleton[OF finM])


139 
by (simp_all add: setsum_addf[symmetric] field_simps)


140 
qed


141 


142 
show "finite (space ?space)" using finM finM' by simp


143 


144 
have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"


145 
unfolding finM(2)[symmetric] by simp


146 


147 
show "positive ?space (measure ?space)"


148 
unfolding positive_def


149 
proof (safe, simp add: M.integral_zero prod_measure_def)


150 
fix Q assume "Q \<in> sets ?space"


151 
from Pair_in_sets[OF this]


152 
show "0 \<le> measure ?space Q"


153 
unfolding prod_measure_space_def prod_measure_def


154 
apply (subst M.integral_finite_singleton[OF finM])


155 
using M.positive M'.positive singletonM


156 
by (auto intro!: setsum_nonneg mult_nonneg_nonneg)


157 
qed


158 
qed


159 


160 
end 