author  hoelzl 
Thu, 26 Aug 2010 15:20:41 +0200  
changeset 39082  54dbe0368dc6 
parent 39080  cae59dc0a094 
child 39088  ca17017c10e6 
permissions  rwrr 
35833  1 
theory Product_Measure 
38656  2 
imports Lebesgue_Integration 
35833  3 
begin 
4 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

5 
definition "dynkin M \<longleftrightarrow> 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

6 
space M \<in> sets M \<and> 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

7 
(\<forall> A \<in> sets M. A \<subseteq> space M) \<and> 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

8 
(\<forall> a \<in> sets M. \<forall> b \<in> sets M. b  a \<in> sets M) \<and> 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

9 
(\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 
39080  10 

11 
lemma dynkinI: 

12 
assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" 

13 
assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b  a \<in> sets M" 

14 
assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}) 

15 
\<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M" 

16 
shows "dynkin M" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

17 
using assms unfolding dynkin_def sorry 
39080  18 

19 
lemma dynkin_subset: 

20 
assumes "dynkin M" 

21 
shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" 

22 
using assms unfolding dynkin_def by auto 

23 

24 
lemma dynkin_space: 

25 
assumes "dynkin M" 

26 
shows "space M \<in> sets M" 

27 
using assms unfolding dynkin_def by auto 

28 

29 
lemma dynkin_diff: 

30 
assumes "dynkin M" 

31 
shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b  a \<in> sets M" 

32 
using assms unfolding dynkin_def by auto 

33 

34 
lemma dynkin_UN: 

35 
assumes "dynkin M" 

36 
assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" 

37 
assumes "\<forall> i :: nat. a i \<in> sets M" 

38 
shows "UNION UNIV a \<in> sets M" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

39 
using assms unfolding dynkin_def sorry 
39080  40 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

41 
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" 
39080  42 

43 
lemma dynkin_trivial: 

44 
shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>" 

45 
by (rule dynkinI) auto 

46 

47 
lemma 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

48 
fixes D :: "'a algebra" 
39080  49 
assumes stab: "Int_stable E" 
50 
and spac: "space E = space D" 

51 
and subsED: "sets E \<subseteq> sets D" 

52 
and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)" 

53 
and dyn: "dynkin D" 

54 
shows "sigma (space E) (sets E) = D" 

55 
proof  

56 
def sets_\<delta>E == "\<Inter> {sets d  d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}" 

57 
def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>" 

58 
have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d  d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}" 

59 
using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp 

60 
hence not_empty: "{sets (d :: 'a algebra)  d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}" 

61 
using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified] 

62 
by auto 

63 

64 
have "sets_\<delta>E \<subseteq> sets D" 

65 
unfolding sets_\<delta>E_def using assms by auto 

66 

67 
have \<delta>ynkin: "dynkin \<delta>E" 

68 
proof (rule dynkinI, safe) 

69 
fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A" 

70 
{ fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

71 
hence "A \<subseteq> space d" using dynkin_subset by auto } 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

72 
show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

73 
by simp (metis dynkin_subset in_mono mem_def) 
39080  74 
next 
75 
show "space \<delta>E \<in> sets \<delta>E" 

76 
unfolding \<delta>E_def sets_\<delta>E_def 

77 
using dynkin_space by fastsimp 

78 
next 

79 
fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" 

80 
thus "b  a \<in> sets \<delta>E" 

81 
unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff) 

82 
next 

83 
fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E" 

84 
thus "UNION UNIV a \<in> sets \<delta>E" 

85 
unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)]) 

86 
by blast 

87 
qed 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

88 

39080  89 
def Dy == "\<lambda> d. {A  A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}" 
90 
{ fix d assume dasm: "d \<in> sets_\<delta>E" 

91 
have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

92 
proof (rule dynkinI, safe, simp_all) 
39080  93 
fix A x assume "A \<in> Dy d" "x \<in> A" 
94 
thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

95 
by simp (metis dynkin_subset in_mono mem_def) 
39080  96 
next 
97 
show "space E \<in> Dy d" 

98 
unfolding Dy_def \<delta>E_def sets_\<delta>E_def 

99 
proof auto 

100 
fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d" 

101 
hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto 

102 
thus "space E \<in> sets d" using asm by auto 

103 
next 

104 
fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da" 

105 
have d: "d = space E \<inter> d" 

106 
using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin] 

107 
unfolding \<delta>E_def by auto 

108 
hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def 

109 
using dasm by auto 

110 
have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm 

111 
by auto 

112 
thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin] 

113 
unfolding \<delta>E_def by auto 

114 
qed 

115 
next 

116 
fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" 

117 
hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" 

118 
unfolding Dy_def \<delta>E_def by auto 

119 
hence *: "b  a \<in> sets \<delta>E" 

120 
using dynkin_diff[OF \<delta>ynkin] by auto 

121 
have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E" 

122 
using absm unfolding Dy_def \<delta>E_def by auto 

123 
hence "(b \<inter> d)  (a \<inter> d) \<in> sets \<delta>E" 

124 
using dynkin_diff[OF \<delta>ynkin] by auto 

125 
hence **: "(b  a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2) 

126 
thus "b  a \<in> Dy d" 

127 
using * ** unfolding Dy_def \<delta>E_def by auto 

128 
next 

129 
fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d" 

130 
hence "\<forall> i. a i \<in> sets \<delta>E" 

131 
unfolding Dy_def \<delta>E_def by auto 

132 
from dynkin_UN[OF \<delta>ynkin aasm(1) this] 

133 
have *: "UNION UNIV a \<in> sets \<delta>E" by auto 

134 
from aasm 

135 
have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E" 

136 
unfolding Dy_def \<delta>E_def by auto 

137 
from aasm 

138 
have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto 

139 
from dynkin_UN[OF \<delta>ynkin this] 

140 
have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E" 

141 
using aE by auto 

142 
hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto 

143 
from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto 

144 
qed } note Dy_nkin = this 

145 
have E_\<delta>E: "sets E \<subseteq> sets \<delta>E" 

146 
unfolding \<delta>E_def sets_\<delta>E_def by auto 

147 
{ fix d assume dasm: "d \<in> sets \<delta>E" 

148 
{ fix e assume easm: "e \<in> sets E" 

149 
hence deasm: "e \<in> sets \<delta>E" 

150 
unfolding \<delta>E_def sets_\<delta>E_def by auto 

151 
have subset: "Dy e \<subseteq> sets \<delta>E" 

152 
unfolding Dy_def \<delta>E_def by auto 

153 
{ fix e' assume e'asm: "e' \<in> sets E" 

154 
have "e' \<inter> e \<in> sets E" 

155 
using easm e'asm stab unfolding Int_stable_def by auto 

156 
hence "e' \<inter> e \<in> sets \<delta>E" 

157 
unfolding \<delta>E_def sets_\<delta>E_def by auto 

158 
hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto } 

159 
hence E_Dy: "sets E \<subseteq> Dy e" by auto 

160 
have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d  d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}" 

161 
using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto 

162 
hence "sets_\<delta>E \<subseteq> Dy e" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

163 
unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac) 
39080  164 
hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto 
165 
hence "d \<inter> e \<in> sets \<delta>E" 

166 
using dasm easm deasm unfolding Dy_def \<delta>E_def by auto 

167 
hence "e \<in> Dy d" using deasm 

168 
unfolding Dy_def \<delta>E_def 

169 
by (auto simp add:Int_commute) } 

170 
hence "sets E \<subseteq> Dy d" by auto 

171 
hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]] 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

172 
unfolding \<delta>E_def sets_\<delta>E_def 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

173 
by auto (metis `sets E <= Dy d` simps(1) simps(2) spac) 
39080  174 
hence *: "sets \<delta>E = Dy d" 
175 
unfolding Dy_def \<delta>E_def by auto 

176 
fix a assume aasm: "a \<in> sets \<delta>E" 

177 
hence "a \<inter> d \<in> sets \<delta>E" 

178 
using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this 

179 
have "sigma_algebra D" 

180 
apply unfold_locales 

181 
using dynkin_subset[OF dyn] 

182 
using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]] 

183 
using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]] 

184 
using dynkin_space[OF dyn] 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

185 
sorry 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

186 
(* 
39080  187 
proof auto 
188 
fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D" 

189 
"\<And>a. a \<in> sets D \<Longrightarrow> space D  a \<in> sets D" 

190 
"{} \<in> sets D" "space D \<in> sets D" 

191 
let "?A i" = "A i  (\<Inter> j \<in> {..< i}. A j)" 

192 
{ fix i :: nat assume "i > 0" 

39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

193 
have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E" sorry } 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

194 
oops 
39080  195 
qed 
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

196 
*) 
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

197 

54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset

198 
show ?thesis sorry 
39080  199 
qed 
200 

38656  201 
definition prod_sets where 
202 
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}" 

203 

35833  204 
definition 
38656  205 
"prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) ` A)))" 
35833  206 

207 
definition 

38656  208 
"prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))" 
209 

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

211 
by (auto simp add: prod_sets_def) 

35833  212 

38656  213 
lemma sigma_prod_sets_finite: 
214 
assumes "finite A" and "finite B" 

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

216 
proof safe 

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

35833  218 

38656  219 
fix x assume subset: "x \<subseteq> A \<times> B" 
220 
hence "finite x" using fin by (rule finite_subset) 

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

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

223 
proof (induct x) 

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

225 
next 

226 
case (insert a x) 

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

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

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

230 
qed 

231 
next 

232 
fix x a b 

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

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

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

236 
by (auto simp: prod_sets_def) 

35833  237 
qed 
238 

38656  239 
lemma (in sigma_algebra) measurable_prod_sigma: 
240 
assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2" 

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

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

243 
(prod_sets (sets a1) (sets a2)))" 

35977  244 
proof  
38656  245 
from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1" 
246 
and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) ` y \<inter> space M \<in> sets M" 

247 
by (auto simp add: measurable_def) 

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

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

250 
by (auto simp add: measurable_def) 

251 
show ?thesis 

252 
proof (rule measurable_sigma) 

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

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

255 
next 

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

257 
by (rule prod_final [OF fn1 fn2]) 

258 
next 

259 
fix z 

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

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

262 
proof (auto simp add: prod_sets_def vimage_Times) 

263 
fix x y 

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

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

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

267 
by blast 

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

269 
by blast 

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

271 
qed 

272 
qed 

35977  273 
qed 
35833  274 

38656  275 
lemma (in sigma_finite_measure) prod_measure_times: 
276 
assumes "sigma_finite_measure N \<nu>" 

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

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

279 
oops 

35833  280 

38656  281 
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space: 
282 
assumes "sigma_finite_measure N \<nu>" 

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

284 
oops 

285 

286 
lemma (in finite_measure_space) finite_prod_measure_times: 

287 
assumes "finite_measure_space N \<nu>" 

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

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

290 
proof  

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

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

293 
by (auto simp: vimage_Times comp_def) 

294 
have "finite A1" 

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

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

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

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

299 
unfolding prod_measure_def positive_integral_finite_eq_setsum * 

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

35833  301 
qed 
302 

38656  303 
lemma (in finite_measure_space) finite_prod_measure_space: 
304 
assumes "finite_measure_space N \<nu>" 

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

35977  306 
proof  
38656  307 
interpret N: finite_measure_space N \<nu> by fact 
308 
show ?thesis using finite_space N.finite_space 

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

35833  310 
qed 
311 

38656  312 
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure: 
313 
assumes "finite_measure_space N \<nu>" 

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

315 
unfolding finite_prod_measure_space[OF assms] 

316 
proof (rule finite_measure_spaceI) 

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

318 

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

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

321 
proof (rule sigma_algebra.finite_additivity_sufficient) 

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

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

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

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

326 
unfolding positive_def by simp 

327 

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

329 
unfolding additive_def 

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

331 
intro!: positive_integral_cong) 

332 
apply (subst N.measure_additive[symmetric]) 

333 
by (auto simp: N.sets_eq_Pow sets_eq_Pow) 

334 
qed 

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

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

337 

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

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

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

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

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

343 
qed 

344 

345 
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive: 

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

347 
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>)" 

348 
(is "finite_measure_space ?M ?m") 

349 
unfolding finite_prod_measure_space[OF N, symmetric] 

350 
using finite_measure_space_finite_prod_measure[OF N] . 

351 

35833  352 
end 