35833

1 
theory Product_Measure

38656

2 
imports Lebesgue_Integration

35833

3 
begin


4 

38656

5 
definition prod_sets where


6 
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"


7 

35833

8 
definition

38656

9 
"prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) ` A)))"

35833

10 


11 
definition

38656

12 
"prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"


13 


14 
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"


15 
by (auto simp add: prod_sets_def)

35833

16 

38656

17 
lemma sigma_prod_sets_finite:


18 
assumes "finite A" and "finite B"


19 
shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)"


20 
proof safe


21 
have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)

35833

22 

38656

23 
fix x assume subset: "x \<subseteq> A \<times> B"


24 
hence "finite x" using fin by (rule finite_subset)


25 
from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"


26 
(is "x \<in> sigma_sets ?prod ?sets")


27 
proof (induct x)


28 
case empty show ?case by (rule sigma_sets.Empty)


29 
next


30 
case (insert a x)


31 
hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)


32 
moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto


33 
ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)


34 
qed


35 
next


36 
fix x a b


37 
assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"


38 
from sigma_sets_into_sp[OF _ this(1)] this(2)


39 
show "a \<in> A" and "b \<in> B"


40 
by (auto simp: prod_sets_def)

35833

41 
qed


42 

38656

43 
lemma (in sigma_algebra) measurable_prod_sigma:


44 
assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2"


45 
assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"


46 
shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))


47 
(prod_sets (sets a1) (sets a2)))"

35977

48 
proof 

38656

49 
from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"


50 
and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) ` y \<inter> space M \<in> sets M"


51 
by (auto simp add: measurable_def)


52 
from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"


53 
and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) ` y \<inter> space M \<in> sets M"


54 
by (auto simp add: measurable_def)


55 
show ?thesis


56 
proof (rule measurable_sigma)


57 
show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2


58 
by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)


59 
next


60 
show "f \<in> space M \<rightarrow> space a1 \<times> space a2"


61 
by (rule prod_final [OF fn1 fn2])


62 
next


63 
fix z


64 
assume z: "z \<in> prod_sets (sets a1) (sets a2)"


65 
thus "f ` z \<inter> space M \<in> sets M"


66 
proof (auto simp add: prod_sets_def vimage_Times)


67 
fix x y


68 
assume x: "x \<in> sets a1" and y: "y \<in> sets a2"


69 
have "(fst \<circ> f) ` x \<inter> (snd \<circ> f) ` y \<inter> space M =


70 
((fst \<circ> f) ` x \<inter> space M) \<inter> ((snd \<circ> f) ` y \<inter> space M)"


71 
by blast


72 
also have "... \<in> sets M" using x y q1 q2


73 
by blast


74 
finally show "(fst \<circ> f) ` x \<inter> (snd \<circ> f) ` y \<inter> space M \<in> sets M" .


75 
qed


76 
qed

35977

77 
qed

35833

78 

38656

79 
lemma (in sigma_finite_measure) prod_measure_times:


80 
assumes "sigma_finite_measure N \<nu>"


81 
and "A1 \<in> sets M" "A2 \<in> sets N"


82 
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"


83 
oops

35833

84 

38656

85 
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space:


86 
assumes "sigma_finite_measure N \<nu>"


87 
shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"


88 
oops


89 


90 
lemma (in finite_measure_space) simple_function_finite:


91 
"simple_function f"


92 
unfolding simple_function_def sets_eq_Pow using finite_space by auto


93 


94 
lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"


95 
unfolding measurable_def sets_eq_Pow by auto

35833

96 

38656

97 
lemma (in finite_measure_space) positive_integral_finite_eq_setsum:


98 
"positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"


99 
proof 


100 
have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"


101 
by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])


102 
show ?thesis unfolding * using borel_measurable_finite[of f]


103 
by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)


104 
qed

35833

105 

38656

106 
lemma (in finite_measure_space) finite_prod_measure_times:


107 
assumes "finite_measure_space N \<nu>"


108 
and "A1 \<in> sets M" "A2 \<in> sets N"


109 
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"


110 
proof 


111 
interpret N: finite_measure_space N \<nu> by fact


112 
have *: "\<And>x. \<nu> (Pair x ` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)"


113 
by (auto simp: vimage_Times comp_def)


114 
have "finite A1"


115 
using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset)


116 
then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M`


117 
by (auto intro!: measure_finite_singleton simp: sets_eq_Pow)


118 
then show ?thesis using `A1 \<in> sets M`


119 
unfolding prod_measure_def positive_integral_finite_eq_setsum *


120 
by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space])

35833

121 
qed


122 

38656

123 
lemma (in finite_measure_space) finite_prod_measure_space:


124 
assumes "finite_measure_space N \<nu>"


125 
shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>"

35977

126 
proof 

38656

127 
interpret N: finite_measure_space N \<nu> by fact


128 
show ?thesis using finite_space N.finite_space


129 
by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow)

35833

130 
qed


131 

38656

132 
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure:


133 
assumes "finite_measure_space N \<nu>"


134 
shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"


135 
unfolding finite_prod_measure_space[OF assms]


136 
proof (rule finite_measure_spaceI)


137 
interpret N: finite_measure_space N \<nu> by fact


138 


139 
let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>"


140 
show "measure_space ?P (prod_measure M \<mu> N \<nu>)"


141 
proof (rule sigma_algebra.finite_additivity_sufficient)


142 
show "sigma_algebra ?P" by (rule sigma_algebra_Pow)


143 
show "finite (space ?P)" using finite_space N.finite_space by auto


144 
from finite_prod_measure_times[OF assms, of "{}" "{}"]


145 
show "positive (prod_measure M \<mu> N \<nu>)"


146 
unfolding positive_def by simp


147 


148 
show "additive ?P (prod_measure M \<mu> N \<nu>)"


149 
unfolding additive_def


150 
apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric]


151 
intro!: positive_integral_cong)


152 
apply (subst N.measure_additive[symmetric])


153 
by (auto simp: N.sets_eq_Pow sets_eq_Pow)


154 
qed


155 
show "finite (space ?P)" using finite_space N.finite_space by auto


156 
show "sets ?P = Pow (space ?P)" by simp


157 


158 
fix x assume "x \<in> space ?P"


159 
with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"]


160 
finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"]


161 
show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>"


162 
by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE)


163 
qed


164 


165 
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive:


166 
assumes N: "finite_measure_space N \<nu>"


167 
shows "finite_measure_space \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr> (prod_measure M \<mu> N \<nu>)"


168 
(is "finite_measure_space ?M ?m")


169 
unfolding finite_prod_measure_space[OF N, symmetric]


170 
using finite_measure_space_finite_prod_measure[OF N] .


171 

35833

172 
end 