author  hoelzl 
Wed, 01 Dec 2010 19:20:30 +0100  
changeset 40859  de0b30e6c2d2 
parent 39098  21e9bd6cf0a8 
child 40871  688f6ff859e1 
permissions  rwrr 
35833  1 
theory Product_Measure 
38656  2 
imports Lebesgue_Integration 
35833  3 
begin 
4 

40859  5 
lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)" 
6 
unfolding sigma_def by (auto intro!: sigma_sets.Basic) 

39080  7 

40859  8 
lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M" 
9 
unfolding sigma_def sigma_sets_eq by simp 

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

10 

40859  11 
lemma vimage_algebra_sigma: 
12 
assumes E: "sets E \<subseteq> Pow (space E)" 

13 
and f: "f \<in> space F \<rightarrow> space E" 

14 
and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f ` X \<inter> space F) ` sets E" 

15 
and "\<And>A. A \<in> sets E \<Longrightarrow> f ` A \<inter> space F \<in> sets F" 

16 
shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F" 

17 
proof  

18 
interpret sigma_algebra "sigma E" 

19 
using assms by (intro sigma_algebra_sigma) auto 

20 
have eq: "sets F = (\<lambda>X. f ` X \<inter> space F) ` sets E" 

21 
using assms by auto 

22 
show "vimage_algebra (space F) f = sigma F" 

23 
unfolding vimage_algebra_def using assms 

24 
by (simp add: sigma_def eq sigma_sets_vimage) 

39094  25 
qed 
26 

40859  27 
lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" 
28 
by auto 

29 

30 
lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x ` (A \<times> B) = (if x \<in> A then B else {})" 

31 
by auto 

32 

33 
lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) ` (A \<times> B) = (if y \<in> B then A else {})" 

34 
by auto 

35 

36 
lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))" 

37 
by (cases x) simp 

38 

39 
abbreviation 

40 
"Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A" 

39094  41 

40859  42 
abbreviation 
43 
funcset_extensional :: "['a set, 'b set] => ('a => 'b) set" 

44 
(infixr ">\<^isub>E" 60) where 

45 
"A >\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)" 

46 

47 
notation (xsymbols) 

48 
funcset_extensional (infixr "\<rightarrow>\<^isub>E" 60) 

49 

50 
lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}" 

51 
by safe (auto simp add: extensional_def fun_eq_iff) 

52 

53 
lemma extensional_insert[intro, simp]: 

54 
assumes "a \<in> extensional (insert i I)" 

55 
shows "a(i := b) \<in> extensional (insert i I)" 

56 
using assms unfolding extensional_def by auto 

57 

58 
lemma extensional_Int[simp]: 

59 
"extensional I \<inter> extensional I' = extensional (I \<inter> I')" 

60 
unfolding extensional_def by auto 

38656  61 

35833  62 
definition 
40859  63 
"merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)" 
64 

65 
lemma merge_apply[simp]: 

66 
"I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i" 

67 
"I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i" 

68 
"J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i" 

69 
"J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i" 

70 
"i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined" 

71 
unfolding merge_def by auto 

72 

73 
lemma merge_commute: 

74 
"I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x" 

75 
by (auto simp: merge_def intro!: ext) 

76 

77 
lemma Pi_cancel_merge_range[simp]: 

78 
"I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A" 

79 
"I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A" 

80 
"J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A" 

81 
"J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A" 

82 
by (auto simp: Pi_def) 

83 

84 
lemma Pi_cancel_merge[simp]: 

85 
"I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B" 

86 
"J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B" 

87 
"I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B" 

88 
"J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B" 

89 
by (auto simp: Pi_def) 

90 

91 
lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)" 

92 
by (auto simp: extensional_def) 

93 

94 
lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A" 

95 
by (auto simp: restrict_def Pi_def) 

96 

97 
lemma restrict_merge[simp]: 

98 
"I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I" 

99 
"I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J" 

100 
"J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I" 

101 
"J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J" 

102 
by (auto simp: restrict_def intro!: ext) 

103 

104 
lemma extensional_insert_undefined[intro, simp]: 

105 
assumes "a \<in> extensional (insert i I)" 

106 
shows "a(i := undefined) \<in> extensional I" 

107 
using assms unfolding extensional_def by auto 

108 

109 
lemma extensional_insert_cancel[intro, simp]: 

110 
assumes "a \<in> extensional I" 

111 
shows "a \<in> extensional (insert i I)" 

112 
using assms unfolding extensional_def by auto 

113 

114 
lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)" 

115 
by auto 

116 

117 
lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B" 

118 
by (auto simp: Pi_def) 

119 

120 
lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i" 

121 
by (auto simp: Pi_def) 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

122 

40859  123 
lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X" 
124 
by (auto simp: Pi_def) 

125 

126 
lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B" 

127 
by (auto simp: Pi_def) 

128 

129 
section "Binary products" 

130 

131 
definition 

132 
"pair_algebra A B = \<lparr> space = space A \<times> space B, 

133 
sets = {a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B} \<rparr>" 

134 

135 
locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2 

136 
for M1 M2 

137 

138 
abbreviation (in pair_sigma_algebra) 

139 
"E \<equiv> pair_algebra M1 M2" 

140 

141 
abbreviation (in pair_sigma_algebra) 

142 
"P \<equiv> sigma E" 

143 

144 
sublocale pair_sigma_algebra \<subseteq> sigma_algebra P 

145 
using M1.sets_into_space M2.sets_into_space 

146 
by (force simp: pair_algebra_def intro!: sigma_algebra_sigma) 

147 

148 
lemma pair_algebraI[intro, simp]: 

149 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (pair_algebra A B)" 

150 
by (auto simp add: pair_algebra_def) 

151 

152 
lemma space_pair_algebra: 

153 
"space (pair_algebra A B) = space A \<times> space B" 

154 
by (simp add: pair_algebra_def) 

155 

156 
lemma pair_algebra_Int_snd: 

157 
assumes "sets S1 \<subseteq> Pow (space S1)" 

158 
shows "pair_algebra S1 (algebra.restricted_space S2 A) = 

159 
algebra.restricted_space (pair_algebra S1 S2) (space S1 \<times> A)" 

160 
(is "?L = ?R") 

161 
proof (intro algebra.equality set_eqI iffI) 

162 
fix X assume "X \<in> sets ?L" 

163 
then obtain A1 A2 where X: "X = A1 \<times> (A \<inter> A2)" and "A1 \<in> sets S1" "A2 \<in> sets S2" 

164 
by (auto simp: pair_algebra_def) 

165 
then show "X \<in> sets ?R" unfolding pair_algebra_def 

166 
using assms apply simp by (intro image_eqI[of _ _ "A1 \<times> A2"]) auto 

167 
next 

168 
fix X assume "X \<in> sets ?R" 

169 
then obtain A1 A2 where "X = space S1 \<times> A \<inter> A1 \<times> A2" "A1 \<in> sets S1" "A2 \<in> sets S2" 

170 
by (auto simp: pair_algebra_def) 

171 
moreover then have "X = A1 \<times> (A \<inter> A2)" 

172 
using assms by auto 

173 
ultimately show "X \<in> sets ?L" 

174 
unfolding pair_algebra_def by auto 

175 
qed (auto simp add: pair_algebra_def) 

176 

177 
lemma (in pair_sigma_algebra) 

178 
shows measurable_fst[intro!, simp]: 

179 
"fst \<in> measurable P M1" (is ?fst) 

180 
and measurable_snd[intro!, simp]: 

181 
"snd \<in> measurable P M2" (is ?snd) 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

182 
proof  
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

183 
{ fix X assume "X \<in> sets M1" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

184 
then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst ` X \<inter> space M1 \<times> space M2 = X1 \<times> X2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

185 
apply  apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"]) 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

186 
using M1.sets_into_space by force+ } 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

187 
moreover 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

188 
{ fix X assume "X \<in> sets M2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

189 
then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd ` X \<inter> space M1 \<times> space M2 = X1 \<times> X2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

190 
apply  apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X]) 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

191 
using M2.sets_into_space by force+ } 
40859  192 
ultimately have "?fst \<and> ?snd" 
193 
by (fastsimp simp: measurable_def sets_sigma space_pair_algebra 

194 
intro!: sigma_sets.Basic) 

195 
then show ?fst ?snd by auto 

196 
qed 

197 

198 
lemma (in pair_sigma_algebra) measurable_pair: 

199 
assumes "sigma_algebra M" 

200 
shows "f \<in> measurable M P \<longleftrightarrow> 

201 
(fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" 

202 
proof  

203 
interpret M: sigma_algebra M by fact 

204 
from assms show ?thesis 

205 
proof (safe intro!: measurable_comp[where b=P]) 

206 
assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2" 

207 
show "f \<in> measurable M P" 

208 
proof (rule M.measurable_sigma) 

209 
show "sets (pair_algebra M1 M2) \<subseteq> Pow (space E)" 

210 
unfolding pair_algebra_def using M1.sets_into_space M2.sets_into_space by auto 

211 
show "f \<in> space M \<rightarrow> space E" 

212 
using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma space_pair_algebra) 

213 
fix A assume "A \<in> sets E" 

214 
then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C" 

215 
unfolding pair_algebra_def by auto 

216 
moreover have "(fst \<circ> f) ` B \<inter> space M \<in> sets M" 

217 
using f `B \<in> sets M1` unfolding measurable_def by auto 

218 
moreover have "(snd \<circ> f) ` C \<inter> space M \<in> sets M" 

219 
using s `C \<in> sets M2` unfolding measurable_def by auto 

220 
moreover have "f ` A \<inter> space M = ((fst \<circ> f) ` B \<inter> space M) \<inter> ((snd \<circ> f) ` C \<inter> space M)" 

221 
unfolding `A = B \<times> C` by (auto simp: vimage_Times) 

222 
ultimately show "f ` A \<inter> space M \<in> sets M" by auto 

223 
qed 

224 
qed 

225 
qed 

226 

227 
lemma (in pair_sigma_algebra) measurable_prod_sigma: 

228 
assumes "sigma_algebra M" 

229 
assumes 1: "(fst \<circ> f) \<in> measurable M M1" and 2: "(snd \<circ> f) \<in> measurable M M2" 

230 
shows "f \<in> measurable M P" 

231 
proof  

232 
interpret M: sigma_algebra M by fact 

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

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

235 
by (auto simp add: measurable_def) 

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

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

238 
by (auto simp add: measurable_def) 

239 
show ?thesis 

240 
proof (rule M.measurable_sigma) 

241 
show "sets E \<subseteq> Pow (space E)" 

242 
using M1.space_closed M2.space_closed 

243 
by (auto simp add: sigma_algebra_iff pair_algebra_def) 

244 
next 

245 
show "f \<in> space M \<rightarrow> space E" 

246 
by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2]) 

247 
next 

248 
fix z 

249 
assume z: "z \<in> sets E" 

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

251 
proof (auto simp add: pair_algebra_def vimage_Times) 

252 
fix x y 

253 
assume x: "x \<in> sets M1" and y: "y \<in> sets M2" 

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

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

256 
by blast 

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

258 
by blast 

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

260 
qed 

261 
qed 

262 
qed 

263 

264 
lemma pair_algebraE: 

265 
assumes "X \<in> sets (pair_algebra M1 M2)" 

266 
obtains A B where "X = A \<times> B" "A \<in> sets M1" "B \<in> sets M2" 

267 
using assms unfolding pair_algebra_def by auto 

268 

269 
lemma (in pair_sigma_algebra) pair_algebra_swap: 

270 
"(\<lambda>X. (\<lambda>(x,y). (y,x)) ` X \<inter> space M2 \<times> space M1) ` sets E = sets (pair_algebra M2 M1)" 

271 
proof (safe elim!: pair_algebraE) 

272 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 

273 
moreover then have "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 = B \<times> A" 

274 
using M1.sets_into_space M2.sets_into_space by auto 

275 
ultimately show "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 \<in> sets (pair_algebra M2 M1)" 

276 
by (auto intro: pair_algebraI) 

277 
next 

278 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 

279 
then show "B \<times> A \<in> (\<lambda>X. (\<lambda>(x, y). (y, x)) ` X \<inter> space M2 \<times> space M1) ` sets E" 

280 
using M1.sets_into_space M2.sets_into_space 

281 
by (auto intro!: image_eqI[where x="A \<times> B"] pair_algebraI) 

282 
qed 

283 

284 
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap: 

285 
assumes Q: "Q \<in> sets P" 

286 
shows "(\<lambda>(x,y). (y, x)) ` Q \<in> sets (sigma (pair_algebra M2 M1))" (is "_ \<in> sets ?Q") 

287 
proof  

288 
have *: "(\<lambda>(x,y). (y, x)) \<in> space M2 \<times> space M1 \<rightarrow> (space M1 \<times> space M2)" 

289 
"sets (pair_algebra M1 M2) \<subseteq> Pow (space M1 \<times> space M2)" 

290 
using M1.sets_into_space M2.sets_into_space by (auto elim!: pair_algebraE) 

291 
from Q sets_into_space show ?thesis 

292 
by (auto intro!: image_eqI[where x=Q] 

293 
simp: pair_algebra_swap[symmetric] sets_sigma 

294 
sigma_sets_vimage[OF *] space_pair_algebra) 

295 
qed 

296 

297 
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable: 

298 
shows "(\<lambda>(x,y). (y, x)) \<in> measurable P (sigma (pair_algebra M2 M1))" 

299 
(is "?f \<in> measurable ?P ?Q") 

300 
unfolding measurable_def 

301 
proof (intro CollectI conjI Pi_I ballI) 

302 
fix x assume "x \<in> space ?P" then show "(case x of (x, y) \<Rightarrow> (y, x)) \<in> space ?Q" 

303 
unfolding pair_algebra_def by auto 

304 
next 

305 
fix A assume "A \<in> sets ?Q" 

306 
interpret Q: pair_sigma_algebra M2 M1 by default 

307 
have "?f ` A \<inter> space ?P = (\<lambda>(x,y). (y, x)) ` A" 

308 
using Q.sets_into_space `A \<in> sets ?Q` by (auto simp: pair_algebra_def) 

309 
with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets ?Q`] 

310 
show "?f ` A \<inter> space ?P \<in> sets ?P" by simp 

311 
qed 

312 

313 
lemma (in pair_sigma_algebra) measurable_cut_fst: 

314 
assumes "Q \<in> sets P" shows "Pair x ` Q \<in> sets M2" 

315 
proof  

316 
let ?Q' = "{Q. Q \<subseteq> space P \<and> Pair x ` Q \<in> sets M2}" 

317 
let ?Q = "\<lparr> space = space P, sets = ?Q' \<rparr>" 

318 
interpret Q: sigma_algebra ?Q 

319 
proof qed (auto simp: vimage_UN vimage_Diff space_pair_algebra) 

320 
have "sets E \<subseteq> sets ?Q" 

321 
using M1.sets_into_space M2.sets_into_space 

322 
by (auto simp: pair_algebra_def space_pair_algebra) 

323 
then have "sets P \<subseteq> sets ?Q" 

324 
by (subst pair_algebra_def, intro Q.sets_sigma_subset) 

325 
(simp_all add: pair_algebra_def) 

326 
with assms show ?thesis by auto 

327 
qed 

328 

329 
lemma (in pair_sigma_algebra) measurable_cut_snd: 

330 
assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) ` Q \<in> sets M1" (is "?cut Q \<in> sets M1") 

331 
proof  

332 
interpret Q: pair_sigma_algebra M2 M1 by default 

333 
have "Pair y ` (\<lambda>(x, y). (y, x)) ` Q = (\<lambda>x. (x, y)) ` Q" by auto 

334 
with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y] 

335 
show ?thesis by simp 

336 
qed 

337 

338 
lemma (in pair_sigma_algebra) measurable_pair_image_snd: 

339 
assumes m: "f \<in> measurable P M" and "x \<in> space M1" 

340 
shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M" 

341 
unfolding measurable_def 

342 
proof (intro CollectI conjI Pi_I ballI) 

343 
fix y assume "y \<in> space M2" with `f \<in> measurable P M` `x \<in> space M1` 

344 
show "f (x, y) \<in> space M" unfolding measurable_def pair_algebra_def by auto 

345 
next 

346 
fix A assume "A \<in> sets M" 

347 
then have "Pair x ` (f ` A \<inter> space P) \<in> sets M2" (is "?C \<in> _") 

348 
using `f \<in> measurable P M` 

349 
by (intro measurable_cut_fst) (auto simp: measurable_def) 

350 
also have "?C = (\<lambda>y. f (x, y)) ` A \<inter> space M2" 

351 
using `x \<in> space M1` by (auto simp: pair_algebra_def) 

352 
finally show "(\<lambda>y. f (x, y)) ` A \<inter> space M2 \<in> sets M2" . 

353 
qed 

354 

355 
lemma (in pair_sigma_algebra) measurable_pair_image_fst: 

356 
assumes m: "f \<in> measurable P M" and "y \<in> space M2" 

357 
shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M" 

358 
proof  

359 
interpret Q: pair_sigma_algebra M2 M1 by default 

360 
from Q.measurable_pair_image_snd[OF measurable_comp `y \<in> space M2`, 

361 
OF Q.pair_sigma_algebra_swap_measurable m] 

362 
show ?thesis by simp 

363 
qed 

364 

365 
lemma (in pair_sigma_algebra) Int_stable_pair_algebra: "Int_stable E" 

366 
unfolding Int_stable_def 

367 
proof (intro ballI) 

368 
fix A B assume "A \<in> sets E" "B \<in> sets E" 

369 
then obtain A1 A2 B1 B2 where "A = A1 \<times> A2" "B = B1 \<times> B2" 

370 
"A1 \<in> sets M1" "A2 \<in> sets M2" "B1 \<in> sets M1" "B2 \<in> sets M2" 

371 
unfolding pair_algebra_def by auto 

372 
then show "A \<inter> B \<in> sets E" 

373 
by (auto simp add: times_Int_times pair_algebra_def) 

374 
qed 

375 

376 
lemma finite_measure_cut_measurable: 

377 
fixes M1 :: "'a algebra" and M2 :: "'b algebra" 

378 
assumes "sigma_finite_measure M1 \<mu>1" "finite_measure M2 \<mu>2" 

379 
assumes "Q \<in> sets (sigma (pair_algebra M1 M2))" 

380 
shows "(\<lambda>x. \<mu>2 (Pair x ` Q)) \<in> borel_measurable M1" 

381 
(is "?s Q \<in> _") 

382 
proof  

383 
interpret M1: sigma_finite_measure M1 \<mu>1 by fact 

384 
interpret M2: finite_measure M2 \<mu>2 by fact 

385 
interpret pair_sigma_algebra M1 M2 by default 

386 
have [intro]: "sigma_algebra M1" by fact 

387 
have [intro]: "sigma_algebra M2" by fact 

388 
let ?D = "\<lparr> space = space P, sets = {A\<in>sets P. ?s A \<in> borel_measurable M1} \<rparr>" 

389 
note space_pair_algebra[simp] 

390 
interpret dynkin_system ?D 

391 
proof (intro dynkin_systemI) 

392 
fix A assume "A \<in> sets ?D" then show "A \<subseteq> space ?D" 

393 
using sets_into_space by simp 

394 
next 

395 
from top show "space ?D \<in> sets ?D" 

396 
by (auto simp add: if_distrib intro!: M1.measurable_If) 

397 
next 

398 
fix A assume "A \<in> sets ?D" 

399 
with sets_into_space have "\<And>x. \<mu>2 (Pair x ` (space M1 \<times> space M2  A)) = 

400 
(if x \<in> space M1 then \<mu>2 (space M2)  ?s A x else 0)" 

401 
by (auto intro!: M2.finite_measure_compl measurable_cut_fst 

402 
simp: vimage_Diff) 

403 
with `A \<in> sets ?D` top show "space ?D  A \<in> sets ?D" 

404 
by (auto intro!: Diff M1.measurable_If M1.borel_measurable_pinfreal_diff) 

405 
next 

406 
fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> sets ?D" 

407 
moreover then have "\<And>x. \<mu>2 (\<Union>i. Pair x ` F i) = (\<Sum>\<^isub>\<infinity> i. ?s (F i) x)" 

408 
by (intro M2.measure_countably_additive[symmetric]) 

409 
(auto intro!: measurable_cut_fst simp: disjoint_family_on_def) 

410 
ultimately show "(\<Union>i. F i) \<in> sets ?D" 

411 
by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf) 

412 
qed 

413 
have "P = ?D" 

414 
proof (intro dynkin_lemma) 

415 
show "Int_stable E" by (rule Int_stable_pair_algebra) 

416 
from M1.sets_into_space have "\<And>A. A \<in> sets M1 \<Longrightarrow> {x \<in> space M1. x \<in> A} = A" 

417 
by auto 

418 
then show "sets E \<subseteq> sets ?D" 

419 
by (auto simp: pair_algebra_def sets_sigma if_distrib 

420 
intro: sigma_sets.Basic intro!: M1.measurable_If) 

421 
qed auto 

422 
with `Q \<in> sets P` have "Q \<in> sets ?D" by simp 

423 
then show "?s Q \<in> borel_measurable M1" by simp 

424 
qed 

425 

426 
subsection {* Binary products of $\sigma$finite measure spaces *} 

427 

428 
locale pair_sigma_finite = M1: sigma_finite_measure M1 \<mu>1 + M2: sigma_finite_measure M2 \<mu>2 

429 
for M1 \<mu>1 M2 \<mu>2 

430 

431 
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 

432 
by default 

433 

434 
lemma (in pair_sigma_finite) measure_cut_measurable_fst: 

435 
assumes "Q \<in> sets P" shows "(\<lambda>x. \<mu>2 (Pair x ` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") 

436 
proof  

437 
have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+ 

438 
have M1: "sigma_finite_measure M1 \<mu>1" by default 

439 

440 
from M2.disjoint_sigma_finite guess F .. note F = this 

441 
let "?C x i" = "F i \<inter> Pair x ` Q" 

442 
{ fix i 

443 
let ?R = "M2.restricted_space (F i)" 

444 
have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i" 

445 
using F M2.sets_into_space by auto 

446 
have "(\<lambda>x. \<mu>2 (Pair x ` (space M1 \<times> F i \<inter> Q))) \<in> borel_measurable M1" 

447 
proof (intro finite_measure_cut_measurable[OF M1]) 

448 
show "finite_measure (M2.restricted_space (F i)) \<mu>2" 

449 
using F by (intro M2.restricted_to_finite_measure) auto 

450 
have "space M1 \<times> F i \<in> sets P" 

451 
using M1.top F by blast 

452 
from sigma_sets_Int[symmetric, 

453 
OF this[unfolded pair_sigma_algebra_def sets_sigma]] 

454 
show "(space M1 \<times> F i) \<inter> Q \<in> sets (sigma (pair_algebra M1 ?R))" 

455 
using `Q \<in> sets P` 

456 
using pair_algebra_Int_snd[OF M1.space_closed, of "F i" M2] 

457 
by (auto simp: pair_algebra_def sets_sigma) 

458 
qed 

459 
moreover have "\<And>x. Pair x ` (space M1 \<times> F i \<inter> Q) = ?C x i" 

460 
using `Q \<in> sets P` sets_into_space by (auto simp: space_pair_algebra) 

461 
ultimately have "(\<lambda>x. \<mu>2 (?C x i)) \<in> borel_measurable M1" 

462 
by simp } 

463 
moreover 

464 
{ fix x 

465 
have "(\<Sum>\<^isub>\<infinity>i. \<mu>2 (?C x i)) = \<mu>2 (\<Union>i. ?C x i)" 

466 
proof (intro M2.measure_countably_additive) 

467 
show "range (?C x) \<subseteq> sets M2" 

468 
using F `Q \<in> sets P` by (auto intro!: M2.Int measurable_cut_fst) 

469 
have "disjoint_family F" using F by auto 

470 
show "disjoint_family (?C x)" 

471 
by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto 

472 
qed 

473 
also have "(\<Union>i. ?C x i) = Pair x ` Q" 

474 
using F sets_into_space `Q \<in> sets P` 

475 
by (auto simp: space_pair_algebra) 

476 
finally have "\<mu>2 (Pair x ` Q) = (\<Sum>\<^isub>\<infinity>i. \<mu>2 (?C x i))" 

477 
by simp } 

478 
ultimately show ?thesis 

479 
by (auto intro!: M1.borel_measurable_psuminf) 

480 
qed 

481 

482 
lemma (in pair_sigma_finite) measure_cut_measurable_snd: 

483 
assumes "Q \<in> sets P" shows "(\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) ` Q)) \<in> borel_measurable M2" 

484 
proof  

485 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 

486 
have [simp]: "\<And>y. (Pair y ` (\<lambda>(x, y). (y, x)) ` Q) = (\<lambda>x. (x, y)) ` Q" 

487 
by auto 

488 
note sets_pair_sigma_algebra_swap[OF assms] 

489 
from Q.measure_cut_measurable_fst[OF this] 

490 
show ?thesis by simp 

491 
qed 

492 

493 
lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable: 

494 
assumes "f \<in> measurable P M" 

495 
shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (sigma (pair_algebra M2 M1)) M" 

496 
proof  

497 
interpret Q: pair_sigma_algebra M2 M1 by default 

498 
have *: "(\<lambda>(x,y). f (y, x)) = f \<circ> (\<lambda>(x,y). (y, x))" by (simp add: fun_eq_iff) 

499 
show ?thesis 

500 
using Q.pair_sigma_algebra_swap_measurable assms 

501 
unfolding * by (rule measurable_comp) 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

502 
qed 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

503 

40859  504 
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap: 
505 
"sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))" 

506 
unfolding vimage_algebra_def 

507 
apply (simp add: sets_sigma) 

508 
apply (subst sigma_sets_vimage[symmetric]) 

509 
apply (fastsimp simp: pair_algebra_def) 

510 
using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def) 

511 
proof  

512 
have "(\<lambda>X. (\<lambda>(x, y). (y, x)) ` X \<inter> space M2 \<times> space M1) ` sets E 

513 
= sets (pair_algebra M2 M1)" (is "?S = _") 

514 
by (rule pair_algebra_swap) 

515 
then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1, 

516 
sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>" 

517 
by (simp add: pair_algebra_def sigma_def) 

518 
qed 

519 

520 
definition (in pair_sigma_finite) 

521 
"pair_measure A = M1.positive_integral (\<lambda>x. 

522 
M2.positive_integral (\<lambda>y. indicator A (x, y)))" 

523 

524 
lemma (in pair_sigma_finite) pair_measure_alt: 

525 
assumes "A \<in> sets P" 

526 
shows "pair_measure A = M1.positive_integral (\<lambda>x. \<mu>2 (Pair x ` A))" 

527 
unfolding pair_measure_def 

528 
proof (rule M1.positive_integral_cong) 

529 
fix x assume "x \<in> space M1" 

530 
have *: "\<And>y. indicator A (x, y) = (indicator (Pair x ` A) y :: pinfreal)" 

531 
unfolding indicator_def by auto 

532 
show "M2.positive_integral (\<lambda>y. indicator A (x, y)) = \<mu>2 (Pair x ` A)" 

533 
unfolding * 

534 
apply (subst M2.positive_integral_indicator) 

535 
apply (rule measurable_cut_fst[OF assms]) 

536 
by simp 

537 
qed 

538 

539 
lemma (in pair_sigma_finite) pair_measure_times: 

540 
assumes A: "A \<in> sets M1" and "B \<in> sets M2" 

541 
shows "pair_measure (A \<times> B) = \<mu>1 A * \<mu>2 B" 

542 
proof  

543 
from assms have "pair_measure (A \<times> B) = 

544 
M1.positive_integral (\<lambda>x. \<mu>2 B * indicator A x)" 

545 
by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt) 

546 
with assms show ?thesis 

547 
by (simp add: M1.positive_integral_cmult_indicator ac_simps) 

548 
qed 

549 

550 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra: 

551 
"\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> F \<up> space E \<and> 

552 
(\<forall>i. pair_measure (F i) \<noteq> \<omega>)" 

553 
proof  

554 
obtain F1 :: "nat \<Rightarrow> 'a set" and F2 :: "nat \<Rightarrow> 'b set" where 

555 
F1: "range F1 \<subseteq> sets M1" "F1 \<up> space M1" "\<And>i. \<mu>1 (F1 i) \<noteq> \<omega>" and 

556 
F2: "range F2 \<subseteq> sets M2" "F2 \<up> space M2" "\<And>i. \<mu>2 (F2 i) \<noteq> \<omega>" 

557 
using M1.sigma_finite_up M2.sigma_finite_up by auto 

558 
then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" 

559 
unfolding isoton_def by auto 

560 
let ?F = "\<lambda>i. F1 i \<times> F2 i" 

561 
show ?thesis unfolding isoton_def space_pair_algebra 

562 
proof (intro exI[of _ ?F] conjI allI) 

563 
show "range ?F \<subseteq> sets E" using F1 F2 

564 
by (fastsimp intro!: pair_algebraI) 

565 
next 

566 
have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)" 

567 
proof (intro subsetI) 

568 
fix x assume "x \<in> space M1 \<times> space M2" 

569 
then obtain i j where "fst x \<in> F1 i" "snd x \<in> F2 j" 

570 
by (auto simp: space) 

571 
then have "fst x \<in> F1 (max i j)" "snd x \<in> F2 (max j i)" 

572 
using `F1 \<up> space M1` `F2 \<up> space M2` 

573 
by (auto simp: max_def dest: isoton_mono_le) 

574 
then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)" 

575 
by (intro SigmaI) (auto simp add: min_max.sup_commute) 

576 
then show "x \<in> (\<Union>i. ?F i)" by auto 

577 
qed 

578 
then show "(\<Union>i. ?F i) = space M1 \<times> space M2" 

579 
using space by (auto simp: space) 

580 
next 

581 
fix i show "F1 i \<times> F2 i \<subseteq> F1 (Suc i) \<times> F2 (Suc i)" 

582 
using `F1 \<up> space M1` `F2 \<up> space M2` unfolding isoton_def 

583 
by auto 

584 
next 

585 
fix i 

586 
from F1 F2 have "F1 i \<in> sets M1" "F2 i \<in> sets M2" by auto 

587 
with F1 F2 show "pair_measure (F1 i \<times> F2 i) \<noteq> \<omega>" 

588 
by (simp add: pair_measure_times) 

589 
qed 

590 
qed 

591 

592 
sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P pair_measure 

593 
proof 

594 
show "pair_measure {} = 0" 

595 
unfolding pair_measure_def by auto 

596 

597 
show "countably_additive P pair_measure" 

598 
unfolding countably_additive_def 

599 
proof (intro allI impI) 

600 
fix F :: "nat \<Rightarrow> ('a \<times> 'b) set" 

601 
assume F: "range F \<subseteq> sets P" "disjoint_family F" 

602 
from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto 

603 
moreover from F have "\<And>i. (\<lambda>x. \<mu>2 (Pair x ` F i)) \<in> borel_measurable M1" 

604 
by (intro measure_cut_measurable_fst) auto 

605 
moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x ` F i)" 

606 
by (intro disjoint_family_on_bisimulation[OF F(2)]) auto 

607 
moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> range (\<lambda>i. Pair x ` F i) \<subseteq> sets M2" 

608 
using F by (auto intro!: measurable_cut_fst) 

609 
ultimately show "(\<Sum>\<^isub>\<infinity>n. pair_measure (F n)) = pair_measure (\<Union>i. F i)" 

610 
by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric] 

611 
M2.measure_countably_additive 

612 
cong: M1.positive_integral_cong) 

613 
qed 

614 

615 
from sigma_finite_up_in_pair_algebra guess F :: "nat \<Rightarrow> ('a \<times> 'c) set" .. note F = this 

616 
show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets P \<and> (\<Union>i. F i) = space P \<and> (\<forall>i. pair_measure (F i) \<noteq> \<omega>)" 

617 
proof (rule exI[of _ F], intro conjI) 

618 
show "range F \<subseteq> sets P" using F by auto 

619 
show "(\<Union>i. F i) = space P" 

620 
using F by (auto simp: space_pair_algebra isoton_def) 

621 
show "\<forall>i. pair_measure (F i) \<noteq> \<omega>" using F by auto 

622 
qed 

623 
qed 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

624 

40859  625 
lemma (in pair_sigma_finite) pair_measure_alt2: 
626 
assumes "A \<in> sets P" 

627 
shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) ` A))" 

628 
(is "_ = ?\<nu> A") 

629 
proof  

630 
from sigma_finite_up_in_pair_algebra guess F :: "nat \<Rightarrow> ('a \<times> 'c) set" .. note F = this 

631 
show ?thesis 

632 
proof (rule measure_unique_Int_stable[where \<nu>="?\<nu>", OF Int_stable_pair_algebra], 

633 
simp_all add: pair_sigma_algebra_def[symmetric]) 

634 
show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. pair_measure (F i) \<noteq> \<omega>" 

635 
using F by auto 

636 
show "measure_space P pair_measure" by default 

637 
next 

638 
show "measure_space P ?\<nu>" 

639 
proof 

640 
show "?\<nu> {} = 0" by auto 

641 
show "countably_additive P ?\<nu>" 

642 
unfolding countably_additive_def 

643 
proof (intro allI impI) 

644 
fix F :: "nat \<Rightarrow> ('a \<times> 'b) set" 

645 
assume F: "range F \<subseteq> sets P" "disjoint_family F" 

646 
from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto 

647 
moreover from F have "\<And>i. (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) ` F i)) \<in> borel_measurable M2" 

648 
by (intro measure_cut_measurable_snd) auto 

649 
moreover have "\<And>y. disjoint_family (\<lambda>i. (\<lambda>x. (x, y)) ` F i)" 

650 
by (intro disjoint_family_on_bisimulation[OF F(2)]) auto 

651 
moreover have "\<And>y. y \<in> space M2 \<Longrightarrow> range (\<lambda>i. (\<lambda>x. (x, y)) ` F i) \<subseteq> sets M1" 

652 
using F by (auto intro!: measurable_cut_snd) 

653 
ultimately show "(\<Sum>\<^isub>\<infinity>n. ?\<nu> (F n)) = ?\<nu> (\<Union>i. F i)" 

654 
by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric] 

655 
M1.measure_countably_additive 

656 
cong: M2.positive_integral_cong) 

657 
qed 

658 
qed 

659 
next 

660 
fix X assume "X \<in> sets E" 

661 
then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2" 

662 
unfolding pair_algebra_def by auto 

663 
show "pair_measure X = ?\<nu> X" 

664 
proof  

665 
from AB have "?\<nu> (A \<times> B) = 

666 
M2.positive_integral (\<lambda>y. \<mu>1 A * indicator B y)" 

667 
by (auto intro!: M2.positive_integral_cong) 

668 
with AB show ?thesis 

669 
unfolding pair_measure_times[OF AB] X 

670 
by (simp add: M2.positive_integral_cmult_indicator ac_simps) 

671 
qed 

672 
qed fact 

673 
qed 

674 

675 
section "Fubinis theorem" 

676 

677 
lemma (in pair_sigma_finite) simple_function_cut: 

678 
assumes f: "simple_function f" 

679 
shows "(\<lambda>x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1" 

680 
and "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y))) 

681 
= positive_integral f" 

682 
proof  

683 
have f_borel: "f \<in> borel_measurable P" 

684 
using f by (rule borel_measurable_simple_function) 

685 
let "?F z" = "f ` {z} \<inter> space P" 

686 
let "?F' x z" = "Pair x ` ?F z" 

687 
{ fix x assume "x \<in> space M1" 

688 
have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y" 

689 
by (auto simp: indicator_def) 

690 
have "\<And>y. y \<in> space M2 \<Longrightarrow> (x, y) \<in> space P" using `x \<in> space M1` 

691 
by (simp add: space_pair_algebra) 

692 
moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel 

693 
by (intro borel_measurable_vimage measurable_cut_fst) 

694 
ultimately have "M2.simple_function (\<lambda> y. f (x, y))" 

695 
apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _]) 

696 
apply (rule simple_function_indicator_representation[OF f]) 

697 
using `x \<in> space M1` by (auto simp del: space_sigma) } 

698 
note M2_sf = this 

699 
{ fix x assume x: "x \<in> space M1" 

700 
then have "M2.positive_integral (\<lambda> y. f (x, y)) = 

701 
(\<Sum>z\<in>f ` space P. z * \<mu>2 (?F' x z))" 

702 
unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]] 

703 
unfolding M2.simple_integral_def 

704 
proof (safe intro!: setsum_mono_zero_cong_left) 

705 
from f show "finite (f ` space P)" by (rule simple_functionD) 

706 
next 

707 
fix y assume "y \<in> space M2" then show "f (x, y) \<in> f ` space P" 

708 
using `x \<in> space M1` by (auto simp: space_pair_algebra) 

709 
next 

710 
fix x' y assume "(x', y) \<in> space P" 

711 
"f (x', y) \<notin> (\<lambda>y. f (x, y)) ` space M2" 

712 
then have *: "?F' x (f (x', y)) = {}" 

713 
by (force simp: space_pair_algebra) 

714 
show "f (x', y) * \<mu>2 (?F' x (f (x', y))) = 0" 

715 
unfolding * by simp 

716 
qed (simp add: vimage_compose[symmetric] comp_def 

717 
space_pair_algebra) } 

718 
note eq = this 

719 
moreover have "\<And>z. ?F z \<in> sets P" 

720 
by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma) 

721 
moreover then have "\<And>z. (\<lambda>x. \<mu>2 (?F' x z)) \<in> borel_measurable M1" 

722 
by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int) 

723 
ultimately 

724 
show "(\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1" 

725 
and "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y))) 

726 
= positive_integral f" 

727 
by (auto simp del: vimage_Int cong: measurable_cong 

728 
intro!: M1.borel_measurable_pinfreal_setsum 

729 
simp add: M1.positive_integral_setsum simple_integral_def 

730 
M1.positive_integral_cmult 

731 
M1.positive_integral_cong[OF eq] 

732 
positive_integral_eq_simple_integral[OF f] 

733 
pair_measure_alt[symmetric]) 

734 
qed 

735 

736 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

737 
assumes f: "f \<in> borel_measurable P" 

738 
shows "(\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1" 

739 
(is "?C f \<in> borel_measurable M1") 

740 
and "M1.positive_integral (\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) = 

741 
positive_integral f" 

742 
proof  

743 
from borel_measurable_implies_simple_function_sequence[OF f] 

744 
obtain F where F: "\<And>i. simple_function (F i)" "F \<up> f" by auto 

745 
then have F_borel: "\<And>i. F i \<in> borel_measurable P" 

746 
and F_mono: "\<And>i x. F i x \<le> F (Suc i) x" 

747 
and F_SUPR: "\<And>x. (SUP i. F i x) = f x" 

748 
unfolding isoton_def le_fun_def SUPR_fun_expand 

749 
by (auto intro: borel_measurable_simple_function) 

750 
note sf = simple_function_cut[OF F(1)] 

751 
then have "(SUP i. ?C (F i)) \<in> borel_measurable M1" 

752 
using F(1) by (auto intro!: M1.borel_measurable_SUP) 

753 
moreover 

754 
{ fix x assume "x \<in> space M1" 

755 
have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))" 

756 
using `F \<up> f` unfolding isoton_fun_expand 

757 
by (auto simp: isoton_def) 

758 
note measurable_pair_image_snd[OF F_borel`x \<in> space M1`] 

759 
from M2.positive_integral_isoton[OF isotone this] 

760 
have "(SUP i. ?C (F i) x) = ?C f x" 

761 
by (simp add: isoton_def) } 

762 
note SUPR_C = this 

763 
ultimately show "?C f \<in> borel_measurable M1" 

764 
unfolding SUPR_fun_expand by (simp cong: measurable_cong) 

765 
have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))" 

766 
using F_borel F_mono 

767 
by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric]) 

768 
also have "(SUP i. positive_integral (F i)) = 

769 
(SUP i. M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. F i (x, y))))" 

770 
unfolding sf(2) by simp 

771 
also have "\<dots> = M1.positive_integral (\<lambda>x. SUP i. M2.positive_integral (\<lambda>y. F i (x, y)))" 

772 
by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)] 

773 
M2.positive_integral_mono F_mono) 

774 
also have "\<dots> = M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. SUP i. F i (x, y)))" 

775 
using F_borel F_mono 

776 
by (auto intro!: M2.positive_integral_monotone_convergence_SUP 

777 
M1.positive_integral_cong measurable_pair_image_snd) 

778 
finally show "M1.positive_integral (\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) = 

779 
positive_integral f" 

780 
unfolding F_SUPR by simp 

781 
qed 

782 

783 
lemma (in pair_sigma_finite) positive_integral_snd_measurable: 

784 
assumes f: "f \<in> borel_measurable P" 

785 
shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) = 

786 
positive_integral f" 

787 
proof  

788 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 

789 

790 
have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp 

791 
have t: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by (auto simp: fun_eq_iff) 

792 

793 
have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)" 

794 
by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def) 

795 

796 
note pair_sigma_algebra_measurable[OF f] 

797 
from Q.positive_integral_fst_measurable[OF this] 

798 
have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) = 

799 
Q.positive_integral (\<lambda>(x, y). f (y, x))" 

800 
by simp 

801 
also have "\<dots> = positive_integral f" 

802 
unfolding positive_integral_vimage[OF bij, of f] t 

803 
unfolding pair_sigma_algebra_swap[symmetric] 

804 
proof (rule Q.positive_integral_cong_measure[symmetric]) 

805 
fix A assume "A \<in> sets Q.P" 

806 
from this Q.sets_pair_sigma_algebra_swap[OF this] 

807 
show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A" 

808 
by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2] 

809 
simp: pair_measure_alt Q.pair_measure_alt2) 

810 
qed 

811 
finally show ?thesis . 

812 
qed 

813 

814 
lemma (in pair_sigma_finite) Fubini: 

815 
assumes f: "f \<in> borel_measurable P" 

816 
shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) = 

817 
M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y)))" 

818 
unfolding positive_integral_snd_measurable[OF assms] 

819 
unfolding positive_integral_fst_measurable[OF assms] .. 

820 

821 
lemma (in pair_sigma_finite) AE_pair: 

822 
assumes "almost_everywhere (\<lambda>x. Q x)" 

823 
shows "M1.almost_everywhere (\<lambda>x. M2.almost_everywhere (\<lambda>y. Q (x, y)))" 

824 
proof  

825 
obtain N where N: "N \<in> sets P" "pair_measure N = 0" "{x\<in>space P. \<not> Q x} \<subseteq> N" 

826 
using assms unfolding almost_everywhere_def by auto 

827 
show ?thesis 

828 
proof (rule M1.AE_I) 

829 
from N measure_cut_measurable_fst[OF `N \<in> sets P`] 

830 
show "\<mu>1 {x\<in>space M1. \<mu>2 (Pair x ` N) \<noteq> 0} = 0" 

831 
by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def) 

832 
show "{x \<in> space M1. \<mu>2 (Pair x ` N) \<noteq> 0} \<in> sets M1" 

833 
by (intro M1.borel_measurable_pinfreal_neq_const measure_cut_measurable_fst N) 

834 
{ fix x assume "x \<in> space M1" "\<mu>2 (Pair x ` N) = 0" 

835 
have "M2.almost_everywhere (\<lambda>y. Q (x, y))" 

836 
proof (rule M2.AE_I) 

837 
show "\<mu>2 (Pair x ` N) = 0" by fact 

838 
show "Pair x ` N \<in> sets M2" by (intro measurable_cut_fst N) 

839 
show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x ` N" 

840 
using N `x \<in> space M1` unfolding space_sigma space_pair_algebra by auto 

841 
qed } 

842 
then show "{x \<in> space M1. \<not> M2.almost_everywhere (\<lambda>y. Q (x, y))} \<subseteq> {x \<in> space M1. \<mu>2 (Pair x ` N) \<noteq> 0}" 

843 
by auto 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

844 
qed 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

845 
qed 
35833  846 

40859  847 
section "Finite product spaces" 
848 

849 
section "Products" 

850 

851 
locale product_sigma_algebra = 

852 
fixes M :: "'i \<Rightarrow> 'a algebra" 

853 
assumes sigma_algebras: "\<And>i. sigma_algebra (M i)" 

854 

855 
locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \<Rightarrow> 'a algebra" + 

856 
fixes I :: "'i set" 

857 
assumes finite_index: "finite I" 

858 

859 
syntax 

860 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10) 

861 

862 
syntax (xsymbols) 

863 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 

864 

865 
syntax (HTML output) 

866 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 

867 

868 
translations 

869 
"PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)" 

870 

35833  871 
definition 
40859  872 
"product_algebra M I = \<lparr> space = (\<Pi>\<^isub>E i\<in>I. space (M i)), sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)) \<rparr>" 
873 

874 
abbreviation (in finite_product_sigma_algebra) "G \<equiv> product_algebra M I" 

875 
abbreviation (in finite_product_sigma_algebra) "P \<equiv> sigma G" 

876 

877 
sublocale product_sigma_algebra \<subseteq> M: sigma_algebra "M i" for i by (rule sigma_algebras) 

878 

879 
lemma (in finite_product_sigma_algebra) product_algebra_into_space: 

880 
"sets G \<subseteq> Pow (space G)" 

881 
using M.sets_into_space unfolding product_algebra_def 

882 
by auto blast 

883 

884 
sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P 

885 
using product_algebra_into_space by (rule sigma_algebra_sigma) 

886 

887 
lemma space_product_algebra[simp]: 

888 
"space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))" 

889 
unfolding product_algebra_def by simp 

890 

891 
lemma (in finite_product_sigma_algebra) P_empty: 

892 
"I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>" 

893 
unfolding product_algebra_def by (simp add: sigma_def) 

894 

895 
lemma (in finite_product_sigma_algebra) in_P[simp, intro]: 

896 
"\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P" 

897 
by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic) 

898 

899 
lemma bij_betw_prod_fold: 

900 
assumes "i \<notin> I" 

901 
shows "bij_betw (\<lambda>x. (x(i:=undefined), x i)) (\<Pi>\<^isub>E j\<in>insert i I. space (M j)) ((\<Pi>\<^isub>E j\<in>I. space (M j)) \<times> space (M i))" 

902 
(is "bij_betw ?f ?P ?F") 

903 
using `i \<notin> I` 

904 
proof (unfold bij_betw_def, intro conjI set_eqI iffI) 

905 
show "inj_on ?f ?P" 

906 
proof (safe intro!: inj_onI ext) 

907 
fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i" 

908 
then show "a x = b x" 

909 
by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm) 

910 
qed 

911 
next 

912 
fix X assume *: "X \<in> ?F" show "X \<in> ?f ` ?P" 

913 
proof (cases X) 

914 
case (Pair a b) with * `i \<notin> I` show ?thesis 

915 
by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def) 

916 
qed 

917 
qed auto 

918 

919 
section "Generating set generates also product algebra" 

920 

921 
lemma pair_sigma_algebra_sigma: 

922 
assumes 1: "S1 \<up> (space E1)" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)" 

923 
assumes 2: "S2 \<up> (space E2)" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)" 

924 
shows "sigma (pair_algebra (sigma E1) (sigma E2)) = sigma (pair_algebra E1 E2)" 

925 
(is "?S = ?E") 

926 
proof  

927 
interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma) 

928 
interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma) 

929 
have P: "sets (pair_algebra E1 E2) \<subseteq> Pow (space E1 \<times> space E2)" 

930 
using E1 E2 by (auto simp add: pair_algebra_def) 

931 
interpret E: sigma_algebra ?E unfolding pair_algebra_def 

932 
using E1 E2 by (intro sigma_algebra_sigma) auto 

933 

934 
{ fix A assume "A \<in> sets E1" 

935 
then have "fst ` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)" 

936 
using E1 2 unfolding isoton_def pair_algebra_def by auto 

937 
also have "\<dots> = (\<Union>i. A \<times> S2 i)" by auto 

938 
also have "\<dots> \<in> sets ?E" unfolding pair_algebra_def sets_sigma 

939 
using 2 `A \<in> sets E1` 

940 
by (intro sigma_sets.Union) 

941 
(auto simp: image_subset_iff intro!: sigma_sets.Basic) 

942 
finally have "fst ` A \<inter> space ?E \<in> sets ?E" . } 

943 
moreover 

944 
{ fix B assume "B \<in> sets E2" 

945 
then have "snd ` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B" 

946 
using E2 1 unfolding isoton_def pair_algebra_def by auto 

947 
also have "\<dots> = (\<Union>i. S1 i \<times> B)" by auto 

948 
also have "\<dots> \<in> sets ?E" 

949 
using 1 `B \<in> sets E2` unfolding pair_algebra_def sets_sigma 

950 
by (intro sigma_sets.Union) 

951 
(auto simp: image_subset_iff intro!: sigma_sets.Basic) 

952 
finally have "snd ` B \<inter> space ?E \<in> sets ?E" . } 

953 
ultimately have proj: 

954 
"fst \<in> measurable ?E (sigma E1) \<and> snd \<in> measurable ?E (sigma E2)" 

955 
using E1 E2 by (subst (1 2) E.measurable_iff_sigma) 

956 
(auto simp: pair_algebra_def sets_sigma) 

957 

958 
{ fix A B assume A: "A \<in> sets (sigma E1)" and B: "B \<in> sets (sigma E2)" 

959 
with proj have "fst ` A \<inter> space ?E \<in> sets ?E" "snd ` B \<inter> space ?E \<in> sets ?E" 

960 
unfolding measurable_def by simp_all 

961 
moreover have "A \<times> B = (fst ` A \<inter> space ?E) \<inter> (snd ` B \<inter> space ?E)" 

962 
using A B M1.sets_into_space M2.sets_into_space 

963 
by (auto simp: pair_algebra_def) 

964 
ultimately have "A \<times> B \<in> sets ?E" by auto } 

965 
then have "sigma_sets (space ?E) (sets (pair_algebra (sigma E1) (sigma E2))) \<subseteq> sets ?E" 

966 
by (intro E.sigma_sets_subset) (auto simp add: pair_algebra_def sets_sigma) 

967 
then have subset: "sets ?S \<subseteq> sets ?E" 

968 
by (simp add: sets_sigma pair_algebra_def) 

969 

970 
have "sets ?S = sets ?E" 

971 
proof (intro set_eqI iffI) 

972 
fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S" 

973 
unfolding sets_sigma 

974 
proof induct 

975 
case (Basic A) then show ?case 

976 
by (auto simp: pair_algebra_def sets_sigma intro: sigma_sets.Basic) 

977 
qed (auto intro: sigma_sets.intros simp: pair_algebra_def) 

978 
next 

979 
fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto 

980 
qed 

981 
then show ?thesis 

982 
by (simp add: pair_algebra_def sigma_def) 

983 
qed 

984 

985 
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I  {i}) B \<and> f i \<in> A" 

986 
apply auto 

987 
apply (drule_tac x=x in Pi_mem) 

988 
apply (simp_all split: split_if_asm) 

989 
apply (drule_tac x=i in Pi_mem) 

990 
apply (auto dest!: Pi_mem) 

991 
done 

992 

993 
lemma Pi_UN: 

994 
fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set" 

995 
assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i" 

996 
shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)" 

997 
proof (intro set_eqI iffI) 

998 
fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)" 

999 
then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto 

1000 
from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto 

1001 
obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k" 

1002 
using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto 

1003 
have "f \<in> Pi I (A k)" 

1004 
proof (intro Pi_I) 

1005 
fix i assume "i \<in> I" 

1006 
from mono[OF this, of "n i" k] k[OF this] n[OF this] 

1007 
show "f i \<in> A k i" by auto 

1008 
qed 

1009 
then show "f \<in> (\<Union>n. Pi I (A n))" by auto 

1010 
qed auto 

1011 

1012 
lemma PiE_cong: 

1013 
assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i" 

1014 
shows "Pi\<^isub>E I A = Pi\<^isub>E I B" 

1015 
using assms by (auto intro!: Pi_cong) 

1016 

1017 
lemma sigma_product_algebra_sigma_eq: 

1018 
assumes "finite I" 

1019 
assumes isotone: "\<And>i. i \<in> I \<Longrightarrow> (S i) \<up> (space (E i))" 

1020 
assumes sets_into: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> sets (E i)" 

1021 
and E: "\<And>i. sets (E i) \<subseteq> Pow (space (E i))" 

1022 
shows "sigma (product_algebra (\<lambda>i. sigma (E i)) I) = sigma (product_algebra E I)" 

1023 
(is "?S = ?E") 

1024 
proof cases 

1025 
assume "I = {}" then show ?thesis by (simp add: product_algebra_def) 

1026 
next 

1027 
assume "I \<noteq> {}" 

1028 
interpret E: sigma_algebra "sigma (E i)" for i 

1029 
using E by (rule sigma_algebra_sigma) 

1030 

1031 
have into_space[intro]: "\<And>i x A. A \<in> sets (E i) \<Longrightarrow> x i \<in> A \<Longrightarrow> x i \<in> space (E i)" 

1032 
using E by auto 

1033 

1034 
interpret G: sigma_algebra ?E 

1035 
unfolding product_algebra_def using E 

1036 
by (intro sigma_algebra_sigma) (auto dest: Pi_mem) 

1037 

1038 
{ fix A i assume "i \<in> I" and A: "A \<in> sets (E i)" 

1039 
then have "(\<lambda>x. x i) ` A \<inter> space ?E = (\<Pi>\<^isub>E j\<in>I. if j = i then A else \<Union>n. S j n) \<inter> space ?E" 

1040 
using isotone unfolding isoton_def product_algebra_def by (auto dest: Pi_mem) 

1041 
also have "\<dots> = (\<Union>n. (\<Pi>\<^isub>E j\<in>I. if j = i then A else S j n))" 

1042 
unfolding product_algebra_def 

1043 
apply simp 

1044 
apply (subst Pi_UN[OF `finite I`]) 

1045 
using isotone[THEN isoton_mono_le] apply simp 

1046 
apply (simp add: PiE_Int) 

1047 
apply (intro PiE_cong) 

1048 
using A sets_into by (auto intro!: into_space) 

1049 
also have "\<dots> \<in> sets ?E" unfolding product_algebra_def sets_sigma 

1050 
using sets_into `A \<in> sets (E i)` 

1051 
by (intro sigma_sets.Union) 

1052 
(auto simp: image_subset_iff intro!: sigma_sets.Basic) 

1053 
finally have "(\<lambda>x. x i) ` A \<inter> space ?E \<in> sets ?E" . } 

1054 
then have proj: 

1055 
"\<And>i. i\<in>I \<Longrightarrow> (\<lambda>x. x i) \<in> measurable ?E (sigma (E i))" 

1056 
using E by (subst G.measurable_iff_sigma) 

1057 
(auto simp: product_algebra_def sets_sigma) 

1058 

1059 
{ fix A assume A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (sigma (E i))" 

1060 
with proj have basic: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) ` (A i) \<inter> space ?E \<in> sets ?E" 

1061 
unfolding measurable_def by simp 

1062 
have "Pi\<^isub>E I A = (\<Inter>i\<in>I. (\<lambda>x. x i) ` (A i) \<inter> space ?E)" 

1063 
using A E.sets_into_space `I \<noteq> {}` unfolding product_algebra_def by auto blast 

1064 
then have "Pi\<^isub>E I A \<in> sets ?E" 

1065 
using G.finite_INT[OF `finite I` `I \<noteq> {}` basic, of "\<lambda>i. i"] by simp } 

1066 
then have "sigma_sets (space ?E) (sets (product_algebra (\<lambda>i. sigma (E i)) I)) \<subseteq> sets ?E" 

1067 
by (intro G.sigma_sets_subset) (auto simp add: sets_sigma product_algebra_def) 

1068 
then have subset: "sets ?S \<subseteq> sets ?E" 

1069 
by (simp add: sets_sigma product_algebra_def) 

1070 

1071 
have "sets ?S = sets ?E" 

1072 
proof (intro set_eqI iffI) 

1073 
fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S" 

1074 
unfolding sets_sigma 

1075 
proof induct 

1076 
case (Basic A) then show ?case 

1077 
by (auto simp: sets_sigma product_algebra_def intro: sigma_sets.Basic) 

1078 
qed (auto intro: sigma_sets.intros simp: product_algebra_def) 

1079 
next 

1080 
fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto 

1081 
qed 

1082 
then show ?thesis 

1083 
by (simp add: product_algebra_def sigma_def) 

1084 
qed 

1085 

1086 
lemma (in finite_product_sigma_algebra) pair_sigma_algebra_finite_product_space: 

1087 
"sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))" 

1088 
proof  

1089 
have "sigma (pair_algebra P (M i)) = sigma (pair_algebra P (sigma (M i)))" by simp 

1090 
also have "\<dots> = sigma (pair_algebra G (M i))" 

1091 
proof (rule pair_sigma_algebra_sigma) 

1092 
show "(\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<up> space G" 

1093 
"(\<lambda>_. space (M i)) \<up> space (M i)" 

1094 
by (simp_all add: isoton_const) 

1095 
show "range (\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<subseteq> sets G" "range (\<lambda>_. space (M i)) \<subseteq> sets (M i)" 

1096 
by (auto intro!: image_eqI[where x="\<lambda>i\<in>I. space (M i)"] dest: Pi_mem 

1097 
simp: product_algebra_def) 

1098 
show "sets G \<subseteq> Pow (space G)" "sets (M i) \<subseteq> Pow (space (M i))" 

1099 
using product_algebra_into_space M.sets_into_space by auto 

1100 
qed 

1101 
finally show ?thesis . 

1102 
qed 

1103 

1104 
lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)" 

1105 
unfolding pair_algebra_def by auto 

1106 

1107 
lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_eq: 

1108 
"sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))) = 

1109 
sigma (pair_algebra (product_algebra M I) (product_algebra M J))" 

1110 
using M.sets_into_space 

1111 
by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. \<Pi>\<^isub>E i\<in>J. space (M i)"]) 

1112 
(auto simp: isoton_const product_algebra_def, blast+) 

1113 

1114 
lemma (in product_sigma_algebra) product_product_vimage_algebra: 

1115 
assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J" 

1116 
shows "sigma_algebra.vimage_algebra 

1117 
(sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))) 

1118 
(space (product_algebra M (I \<union> J))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) = 

1119 
sigma (product_algebra M (I \<union> J))" 

1120 
(is "sigma_algebra.vimage_algebra _ (space ?IJ) ?f = sigma ?IJ") 

1121 
proof  

1122 
have "finite (I \<union> J)" using assms by auto 

1123 
interpret I: finite_product_sigma_algebra M I by default fact 

1124 
interpret J: finite_product_sigma_algebra M J by default fact 

1125 
interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact 

1126 
interpret pair_sigma_algebra I.P J.P by default 

1127 

1128 
show "vimage_algebra (space ?IJ) ?f = sigma ?IJ" 

1129 
unfolding I.sigma_pair_algebra_sigma_eq 

1130 
proof (rule vimage_algebra_sigma) 

1131 
from M.sets_into_space 

1132 
show "sets (pair_algebra I.G J.G) \<subseteq> Pow (space (pair_algebra I.G J.G))" 

1133 
by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast+ 

1134 
show "?f \<in> space IJ.G \<rightarrow> space (pair_algebra I.G J.G)" 

1135 
by (auto simp: space_pair_algebra product_algebra_def) 

1136 
let ?F = "\<lambda>A. ?f ` A \<inter> (space IJ.G)" 

1137 
let ?s = "\<lambda>I. Pi\<^isub>E I ` (\<Pi> i\<in>I. sets (M i))" 

1138 
{ fix A assume "A \<in> sets IJ.G" 

1139 
then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))" 

1140 
by (auto simp: product_algebra_def) 

1141 
show "A \<in> ?F ` sets (pair_algebra I.G J.G)" 

1142 
using A M.sets_into_space 

1143 
by (auto simp: restrict_Pi_cancel product_algebra_def 

1144 
intro!: image_eqI[where x="Pi\<^isub>E I F \<times> Pi\<^isub>E J F"]) blast+ } 

1145 
{ fix A assume "A \<in> sets (pair_algebra I.G J.G)" 

1146 
then obtain E F where A: "A = Pi\<^isub>E I E \<times> Pi\<^isub>E J F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))" 

1147 
by (auto simp: product_algebra_def sets_pair_algebra) 

1148 
then show "?F A \<in> sets IJ.G" 

1149 
using A M.sets_into_space 

1150 
by (auto simp: restrict_Pi_cancel product_algebra_def 

1151 
intro!: image_eqI[where x="merge I E J F"]) blast+ } 

1152 
qed 

1153 
qed 

1154 

1155 
lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_M_eq: 

1156 
"sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))" 

1157 
proof  

1158 
have "sigma (pair_algebra P (sigma (M i))) = sigma (pair_algebra G (M i))" 

1159 
using M.sets_into_space 

1160 
by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. space (M i)"]) 

1161 
(auto simp: isoton_const product_algebra_def, blast+) 

1162 
then show ?thesis by simp 

1163 
qed 

1164 

1165 
lemma (in product_sigma_algebra) product_singleton_vimage_algebra_eq: 

1166 
assumes [simp]: "i \<notin> I" "finite I" 

1167 
shows "sigma_algebra.vimage_algebra 

1168 
(sigma (pair_algebra (sigma (product_algebra M I)) (M i))) 

1169 
(space (product_algebra M (insert i I))) (\<lambda>x. ((\<lambda>i\<in>I. x i), x i)) = 

1170 
sigma (product_algebra M (insert i I))" 

1171 
(is "sigma_algebra.vimage_algebra _ (space ?I') ?f = sigma ?I'") 

1172 
proof  

1173 
have "finite (insert i I)" using assms by auto 

1174 
interpret I: finite_product_sigma_algebra M I by default fact 

1175 
interpret I': finite_product_sigma_algebra M "insert i I" by default fact 

1176 
interpret pair_sigma_algebra I.P "M i" by default 

1177 
show "vimage_algebra (space ?I') ?f = sigma ?I'" 

1178 
unfolding I.sigma_pair_algebra_sigma_M_eq 

1179 
proof (rule vimage_algebra_sigma) 

1180 
from M.sets_into_space 

1181 
show "sets (pair_algebra I.G (M i)) \<subseteq> Pow (space (pair_algebra I.G (M i)))" 

1182 
by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast 

1183 
show "?f \<in> space I'.G \<rightarrow> space (pair_algebra I.G (M i))" 

1184 
by (auto simp: space_pair_algebra product_algebra_def) 

1185 
let ?F = "\<lambda>A. ?f ` A \<inter> (space I'.G)" 

1186 
{ fix A assume "A \<in> sets I'.G" 

1187 
then obtain F where A: "A = Pi\<^isub>E (insert i I) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F i \<in> sets (M i)" 

1188 
by (auto simp: product_algebra_def) 

1189 
show "A \<in> ?F ` sets (pair_algebra I.G (M i))" 

1190 
using A M.sets_into_space 

1191 
by (auto simp: restrict_Pi_cancel product_algebra_def 

1192 
intro!: image_eqI[where x="Pi\<^isub>E I F \<times> F i"]) blast+ } 

1193 
{ fix A assume "A \<in> sets (pair_algebra I.G (M i))" 

1194 
then obtain E F where A: "A = Pi\<^isub>E I E \<times> F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)" 

1195 
by (auto simp: product_algebra_def sets_pair_algebra) 

1196 
then show "?F A \<in> sets I'.G" 

1197 
using A M.sets_into_space 

1198 
by (auto simp: restrict_Pi_cancel product_algebra_def 

1199 
intro!: image_eqI[where x="E(i:= F)"]) blast+ } 

1200 
qed 

1201 
qed 

38656  1202 

40859  1203 
lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I" 
1204 
by (auto simp: restrict_def intro!: ext) 

1205 

1206 
lemma bij_betw_restrict_I_i: 

1207 
"i \<notin> I \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, x i)) 

1208 
(space (product_algebra M (insert i I))) 

1209 
(space (pair_algebra (sigma (product_algebra M I)) (M i)))" 

1210 
by (intro bij_betwI[where g="(\<lambda>(x,y). x(i:=y))"]) 

1211 
(auto simp: space_pair_algebra extensional_def intro!: ext) 

1212 

1213 
lemma (in product_sigma_algebra) product_singleton_vimage_algebra_inv_eq: 

1214 
assumes [simp]: "i \<notin> I" "finite I" 

1215 
shows "sigma_algebra.vimage_algebra 

1216 
(sigma (product_algebra M (insert i I))) 

1217 
(space (pair_algebra (sigma (product_algebra M I)) (M i))) (\<lambda>(x,y). x(i:=y)) = 

1218 
sigma (pair_algebra (sigma (product_algebra M I)) (M i))" 

1219 
proof  

1220 
have "finite (insert i I)" using `finite I` by auto 

1221 
interpret I: finite_product_sigma_algebra M I by default fact 
