author  hoelzl 
Mon, 24 Jan 2011 22:29:50 +0100  
changeset 41661  baf1964bc468 
parent 41659  a5d1b2df5e97 
child 41689  3e39b0e730d6 
permissions  rwrr 
35833  1 
theory Product_Measure 
38656  2 
imports Lebesgue_Integration 
35833  3 
begin 
4 

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

7 

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

9 
by auto 

10 

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

12 
by auto 

13 

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

15 
by (cases x) simp 

16 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

17 
lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

18 
by (auto simp: fun_eq_iff) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

19 

40859  20 
abbreviation 
21 
"Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A" 

39094  22 

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

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

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

27 

28 
notation (xsymbols) 

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

30 

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

32 
by safe (auto simp add: extensional_def fun_eq_iff) 

33 

34 
lemma extensional_insert[intro, simp]: 

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

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

37 
using assms unfolding extensional_def by auto 

38 

39 
lemma extensional_Int[simp]: 

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

41 
unfolding extensional_def by auto 

38656  42 

35833  43 
definition 
40859  44 
"merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)" 
45 

46 
lemma merge_apply[simp]: 

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

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

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

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

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

52 
unfolding merge_def by auto 

53 

54 
lemma merge_commute: 

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

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

57 

58 
lemma Pi_cancel_merge_range[simp]: 

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

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

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

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

63 
by (auto simp: Pi_def) 

64 

65 
lemma Pi_cancel_merge[simp]: 

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

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

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

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

70 
by (auto simp: Pi_def) 

71 

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

73 
by (auto simp: extensional_def) 

74 

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

76 
by (auto simp: restrict_def Pi_def) 

77 

78 
lemma restrict_merge[simp]: 

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

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

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

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

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

84 

85 
lemma extensional_insert_undefined[intro, simp]: 

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

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

88 
using assms unfolding extensional_def by auto 

89 

90 
lemma extensional_insert_cancel[intro, simp]: 

91 
assumes "a \<in> extensional I" 

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

93 
using assms unfolding extensional_def by auto 

94 

41095  95 
lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)" 
96 
unfolding merge_def by (auto simp: fun_eq_iff) 

97 

98 
lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)" 

99 
by auto 

100 

40859  101 
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)" 
102 
by auto 

103 

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

105 
by (auto simp: Pi_def) 

106 

107 
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" 

108 
by (auto simp: Pi_def) 

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

109 

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

112 

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

114 
by (auto simp: Pi_def) 

115 

41095  116 
lemma restrict_vimage: 
117 
assumes "I \<inter> J = {}" 

118 
shows "(\<lambda>x. (restrict x I, restrict x J)) ` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)" 

119 
using assms by (auto simp: restrict_Pi_cancel) 

120 

121 
lemma merge_vimage: 

122 
assumes "I \<inter> J = {}" 

123 
shows "(\<lambda>(x,y). merge I x J y) ` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E" 

124 
using assms by (auto simp: restrict_Pi_cancel) 

125 

126 
lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I" 

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

128 

129 
lemma merge_restrict[simp]: 

130 
"merge I (restrict x I) J y = merge I x J y" 

131 
"merge I x J (restrict y J) = merge I x J y" 

132 
unfolding merge_def by (auto intro!: ext) 

133 

134 
lemma merge_x_x_eq_restrict[simp]: 

135 
"merge I x J x = restrict x (I \<union> J)" 

136 
unfolding merge_def by (auto intro!: ext) 

137 

138 
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" 

139 
apply auto 

140 
apply (drule_tac x=x in Pi_mem) 

141 
apply (simp_all split: split_if_asm) 

142 
apply (drule_tac x=i in Pi_mem) 

143 
apply (auto dest!: Pi_mem) 

144 
done 

145 

146 
lemma Pi_UN: 

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

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

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

150 
proof (intro set_eqI iffI) 

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

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

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

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

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

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

157 
proof (intro Pi_I) 

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

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

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

161 
qed 

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

163 
qed auto 

164 

165 
lemma PiE_cong: 

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

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

168 
using assms by (auto intro!: Pi_cong) 

169 

170 
lemma restrict_upd[simp]: 

171 
"i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)" 

172 
by (auto simp: fun_eq_iff) 

173 

40859  174 
section "Binary products" 
175 

176 
definition 

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

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

179 

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

181 
for M1 M2 

182 

183 
abbreviation (in pair_sigma_algebra) 

184 
"E \<equiv> pair_algebra M1 M2" 

185 

186 
abbreviation (in pair_sigma_algebra) 

187 
"P \<equiv> sigma E" 

188 

189 
sublocale pair_sigma_algebra \<subseteq> sigma_algebra P 

190 
using M1.sets_into_space M2.sets_into_space 

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

192 

193 
lemma pair_algebraI[intro, simp]: 

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

195 
by (auto simp add: pair_algebra_def) 

196 

197 
lemma space_pair_algebra: 

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

199 
by (simp add: pair_algebra_def) 

200 

41095  201 
lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)" 
202 
unfolding pair_algebra_def by auto 

203 

204 
lemma pair_algebra_sets_into_space: 

205 
assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)" 

206 
shows "sets (pair_algebra M N) \<subseteq> Pow (space (pair_algebra M N))" 

207 
using assms by (auto simp: pair_algebra_def) 

208 

40859  209 
lemma pair_algebra_Int_snd: 
210 
assumes "sets S1 \<subseteq> Pow (space S1)" 

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

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

213 
(is "?L = ?R") 

214 
proof (intro algebra.equality set_eqI iffI) 

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

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

217 
by (auto simp: pair_algebra_def) 

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

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

220 
next 

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

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

223 
by (auto simp: pair_algebra_def) 

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

225 
using assms by auto 

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

227 
unfolding pair_algebra_def by auto 

228 
qed (auto simp add: pair_algebra_def) 

229 

230 
lemma (in pair_sigma_algebra) 

231 
shows measurable_fst[intro!, simp]: 

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

233 
and measurable_snd[intro!, simp]: 

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

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

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

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

237 
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

238 
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

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

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

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

242 
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

243 
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

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

247 
intro!: sigma_sets.Basic) 

248 
then show ?fst ?snd by auto 

249 
qed 

250 

41095  251 
lemma (in pair_sigma_algebra) measurable_pair_iff: 
40859  252 
assumes "sigma_algebra M" 
253 
shows "f \<in> measurable M P \<longleftrightarrow> 

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

255 
proof  

256 
interpret M: sigma_algebra M by fact 

257 
from assms show ?thesis 

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

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

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

261 
proof (rule M.measurable_sigma) 

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

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

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

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

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

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

268 
unfolding pair_algebra_def by auto 

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

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

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

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

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

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

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

276 
qed 

277 
qed 

278 
qed 

279 

41095  280 
lemma (in pair_sigma_algebra) measurable_pair: 
40859  281 
assumes "sigma_algebra M" 
41095  282 
assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" 
40859  283 
shows "f \<in> measurable M P" 
41095  284 
unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp 
40859  285 

286 
lemma pair_algebraE: 

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

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

289 
using assms unfolding pair_algebra_def by auto 

290 

291 
lemma (in pair_sigma_algebra) pair_algebra_swap: 

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

293 
proof (safe elim!: pair_algebraE) 

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

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

296 
using M1.sets_into_space M2.sets_into_space by auto 

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

298 
by (auto intro: pair_algebraI) 

299 
next 

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

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

302 
using M1.sets_into_space M2.sets_into_space 

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

304 
qed 

305 

306 
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap: 

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

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

309 
proof  

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

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

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

313 
from Q sets_into_space show ?thesis 

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

315 
simp: pair_algebra_swap[symmetric] sets_sigma 

316 
sigma_sets_vimage[OF *] space_pair_algebra) 

317 
qed 

318 

319 
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable: 

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

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

322 
unfolding measurable_def 

323 
proof (intro CollectI conjI Pi_I ballI) 

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

325 
unfolding pair_algebra_def by auto 

326 
next 

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

328 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

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

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

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

333 
qed 

334 

335 
lemma (in pair_sigma_algebra) measurable_cut_fst: 

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

337 
proof  

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

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

340 
interpret Q: sigma_algebra ?Q 

341 
proof qed (auto simp: vimage_UN vimage_Diff space_pair_algebra) 

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

343 
using M1.sets_into_space M2.sets_into_space 

344 
by (auto simp: pair_algebra_def space_pair_algebra) 

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

346 
by (subst pair_algebra_def, intro Q.sets_sigma_subset) 

347 
(simp_all add: pair_algebra_def) 

348 
with assms show ?thesis by auto 

349 
qed 

350 

351 
lemma (in pair_sigma_algebra) measurable_cut_snd: 

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

353 
proof  

354 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

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

357 
show ?thesis by simp 

358 
qed 

359 

360 
lemma (in pair_sigma_algebra) measurable_pair_image_snd: 

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

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

363 
unfolding measurable_def 

364 
proof (intro CollectI conjI Pi_I ballI) 

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

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

367 
next 

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

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

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

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

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

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

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

375 
qed 

376 

377 
lemma (in pair_sigma_algebra) measurable_pair_image_fst: 

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

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

380 
proof  

381 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

383 
OF Q.pair_sigma_algebra_swap_measurable m] 

384 
show ?thesis by simp 

385 
qed 

386 

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

388 
unfolding Int_stable_def 

389 
proof (intro ballI) 

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

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

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

393 
unfolding pair_algebra_def by auto 

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

395 
by (auto simp add: times_Int_times pair_algebra_def) 

396 
qed 

397 

398 
lemma finite_measure_cut_measurable: 

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

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

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

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

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

404 
proof  

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

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

407 
interpret pair_sigma_algebra M1 M2 by default 

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

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

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

411 
note space_pair_algebra[simp] 

412 
interpret dynkin_system ?D 

413 
proof (intro dynkin_systemI) 

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

415 
using sets_into_space by simp 

416 
next 

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

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

419 
next 

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

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

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

423 
by (auto intro!: M2.finite_measure_compl measurable_cut_fst 

424 
simp: vimage_Diff) 

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40873
diff
changeset

426 
by (auto intro!: Diff M1.measurable_If M1.borel_measurable_pextreal_diff) 
40859  427 
next 
428 
fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> sets ?D" 

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

430 
by (intro M2.measure_countably_additive[symmetric]) 

431 
(auto intro!: measurable_cut_fst simp: disjoint_family_on_def) 

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

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

434 
qed 

435 
have "P = ?D" 

436 
proof (intro dynkin_lemma) 

437 
show "Int_stable E" by (rule Int_stable_pair_algebra) 

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

439 
by auto 

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

441 
by (auto simp: pair_algebra_def sets_sigma if_distrib 

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

443 
qed auto 

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

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

446 
qed 

447 

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

449 

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

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

452 

453 
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 

454 
by default 

455 

456 
lemma (in pair_sigma_finite) measure_cut_measurable_fst: 

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

458 
proof  

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

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

461 

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

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

464 
{ fix i 

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

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

467 
using F M2.sets_into_space by auto 

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

469 
proof (intro finite_measure_cut_measurable[OF M1]) 

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

471 
using F by (intro M2.restricted_to_finite_measure) auto 

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

473 
using M1.top F by blast 

474 
from sigma_sets_Int[symmetric, 

475 
OF this[unfolded pair_sigma_algebra_def sets_sigma]] 

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

477 
using `Q \<in> sets P` 

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

479 
by (auto simp: pair_algebra_def sets_sigma) 

480 
qed 

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

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

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

484 
by simp } 

485 
moreover 

486 
{ fix x 

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

488 
proof (intro M2.measure_countably_additive) 

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

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

491 
have "disjoint_family F" using F by auto 

492 
show "disjoint_family (?C x)" 

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

494 
qed 

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

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

497 
by (auto simp: space_pair_algebra) 

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

499 
by simp } 

500 
ultimately show ?thesis 

501 
by (auto intro!: M1.borel_measurable_psuminf) 

502 
qed 

503 

504 
lemma (in pair_sigma_finite) measure_cut_measurable_snd: 

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

506 
proof  

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

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

509 
by auto 

510 
note sets_pair_sigma_algebra_swap[OF assms] 

511 
from Q.measure_cut_measurable_fst[OF this] 

512 
show ?thesis by simp 

513 
qed 

514 

515 
lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable: 

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

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

518 
proof  

519 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

521 
show ?thesis 

522 
using Q.pair_sigma_algebra_swap_measurable assms 

523 
unfolding * by (rule measurable_comp) 

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

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

525 

40859  526 
definition (in pair_sigma_finite) 
527 
"pair_measure A = M1.positive_integral (\<lambda>x. 

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

529 

530 
lemma (in pair_sigma_finite) pair_measure_alt: 

531 
assumes "A \<in> sets P" 

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

533 
unfolding pair_measure_def 

534 
proof (rule M1.positive_integral_cong) 

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40873
diff
changeset

536 
have *: "\<And>y. indicator A (x, y) = (indicator (Pair x ` A) y :: pextreal)" 
40859  537 
unfolding indicator_def by auto 
538 
show "M2.positive_integral (\<lambda>y. indicator A (x, y)) = \<mu>2 (Pair x ` A)" 

539 
unfolding * 

540 
apply (subst M2.positive_integral_indicator) 

541 
apply (rule measurable_cut_fst[OF assms]) 

542 
by simp 

543 
qed 

544 

545 
lemma (in pair_sigma_finite) pair_measure_times: 

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

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

548 
proof  

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

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

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

552 
with assms show ?thesis 

553 
by (simp add: M1.positive_integral_cmult_indicator ac_simps) 

554 
qed 

555 

556 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra: 

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

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

559 
proof  

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

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

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

563 
using M1.sigma_finite_up M2.sigma_finite_up by auto 

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

565 
unfolding isoton_def by auto 

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

567 
show ?thesis unfolding isoton_def space_pair_algebra 

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

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

570 
by (fastsimp intro!: pair_algebraI) 

571 
next 

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

573 
proof (intro subsetI) 

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

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

576 
by (auto simp: space) 

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

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

579 
by (auto simp: max_def dest: isoton_mono_le) 

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

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

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

583 
qed 

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

585 
using space by (auto simp: space) 

586 
next 

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

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

589 
by auto 

590 
next 

591 
fix i 

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

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

594 
by (simp add: pair_measure_times) 

595 
qed 

596 
qed 

597 

598 
sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P pair_measure 

599 
proof 

600 
show "pair_measure {} = 0" 

601 
unfolding pair_measure_def by auto 

602 

603 
show "countably_additive P pair_measure" 

604 
unfolding countably_additive_def 

605 
proof (intro allI impI) 

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

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

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

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

610 
by (intro measure_cut_measurable_fst) auto 

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

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

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

614 
using F by (auto intro!: measurable_cut_fst) 

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

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

617 
M2.measure_countably_additive 

618 
cong: M1.positive_integral_cong) 

619 
qed 

620 

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

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

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

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

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

626 
using F by (auto simp: space_pair_algebra isoton_def) 

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

628 
qed 

629 
qed 

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

630 

41661  631 
lemma (in pair_sigma_algebra) sets_swap: 
632 
assumes "A \<in> sets P" 

633 
shows "(\<lambda>(x, y). (y, x)) ` A \<inter> space (sigma (pair_algebra M2 M1)) \<in> sets (sigma (pair_algebra M2 M1))" 

634 
(is "_ ` A \<inter> space ?Q \<in> sets ?Q") 

635 
proof  

636 
have *: "(\<lambda>(x, y). (y, x)) ` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A" 

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

638 
show ?thesis 

639 
unfolding * using assms by (rule sets_pair_sigma_algebra_swap) 

640 
qed 

641 

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

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

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

646 
proof  

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

648 
show ?thesis 

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

650 
simp_all add: pair_sigma_algebra_def[symmetric]) 

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

652 
using F by auto 

653 
show "measure_space P pair_measure" by default 

41659  654 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 
41661  655 
have P: "sigma_algebra P" by default 
656 
show "measure_space P ?\<nu>" 

657 
apply (rule Q.measure_space_vimage[OF P]) 

658 
apply (rule Q.pair_sigma_algebra_swap_measurable) 

659 
proof  

660 
fix A assume "A \<in> sets P" 

661 
from sets_swap[OF this] 

662 
show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) ` A)) = 

663 
Q.pair_measure ((\<lambda>(x, y). (y, x)) ` A \<inter> space Q.P)" 

664 
using sets_into_space[OF `A \<in> sets P`] 

665 
by (auto simp add: Q.pair_measure_alt space_pair_algebra 

666 
intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1]) 

667 
qed 

40859  668 
fix X assume "X \<in> sets E" 
669 
then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2" 

670 
unfolding pair_algebra_def by auto 

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

672 
proof  

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

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

675 
by (auto intro!: M2.positive_integral_cong) 

676 
with AB show ?thesis 

677 
unfolding pair_measure_times[OF AB] X 

678 
by (simp add: M2.positive_integral_cmult_indicator ac_simps) 

679 
qed 

680 
qed fact 

681 
qed 

682 

683 
section "Fubinis theorem" 

684 

685 
lemma (in pair_sigma_finite) simple_function_cut: 

686 
assumes f: "simple_function f" 

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

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

689 
= positive_integral f" 

690 
proof  

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

692 
using f by (rule borel_measurable_simple_function) 

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

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

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

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

697 
by (auto simp: indicator_def) 

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

699 
by (simp add: space_pair_algebra) 

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

701 
by (intro borel_measurable_vimage measurable_cut_fst) 

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

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

704 
apply (rule simple_function_indicator_representation[OF f]) 

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

706 
note M2_sf = this 

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

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

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

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

711 
unfolding M2.simple_integral_def 

712 
proof (safe intro!: setsum_mono_zero_cong_left) 

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

714 
next 

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

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

717 
next 

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

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

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

721 
by (force simp: space_pair_algebra) 

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

723 
unfolding * by simp 

724 
qed (simp add: vimage_compose[symmetric] comp_def 

725 
space_pair_algebra) } 

726 
note eq = this 

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

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

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

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

731 
ultimately 

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

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

734 
= positive_integral f" 

735 
by (auto simp del: vimage_Int cong: measurable_cong 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40873
diff
changeset

736 
intro!: M1.borel_measurable_pextreal_setsum 
40859  737 
simp add: M1.positive_integral_setsum simple_integral_def 
738 
M1.positive_integral_cmult 

739 
M1.positive_integral_cong[OF eq] 

740 
positive_integral_eq_simple_integral[OF f] 

741 
pair_measure_alt[symmetric]) 

742 
qed 

743 

744 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

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

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

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

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

749 
positive_integral f" 

750 
proof  

751 
from borel_measurable_implies_simple_function_sequence[OF f] 

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

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

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

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

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

756 
unfolding isoton_fun_expand unfolding isoton_def le_fun_def 
40859  757 
by (auto intro: borel_measurable_simple_function) 
758 
note sf = simple_function_cut[OF F(1)] 

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

759 
then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1" 
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

760 
using F(1) by auto 
40859  761 
moreover 
762 
{ fix x assume "x \<in> space M1" 

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

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

765 
by (auto simp: isoton_def) 

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

767 
from M2.positive_integral_isoton[OF isotone this] 

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

769 
by (simp add: isoton_def) } 

770 
note SUPR_C = this 

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

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

772 
by (simp cong: measurable_cong) 
41544  773 
have "positive_integral (\<lambda>x. (SUP i. F i x)) = (SUP i. positive_integral (F i))" 
40859  774 
using F_borel F_mono 
775 
by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric]) 

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

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

778 
unfolding sf(2) by simp 

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

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

781 
M2.positive_integral_mono F_mono) 

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

783 
using F_borel F_mono 

784 
by (auto intro!: M2.positive_integral_monotone_convergence_SUP 

785 
M1.positive_integral_cong measurable_pair_image_snd) 

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

787 
positive_integral f" 

788 
unfolding F_SUPR by simp 

789 
qed 

790 

41661  791 
lemma (in pair_sigma_finite) positive_integral_product_swap: 
792 
assumes f: "f \<in> borel_measurable P" 

793 
shows "measure_space.positive_integral 

794 
(sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x))) = 

795 
positive_integral f" 

796 
proof  

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

798 
have P: "sigma_algebra P" by default 

799 
show ?thesis 

800 
unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric] 

801 
proof (rule positive_integral_cong_measure) 

802 
fix A 

803 
assume A: "A \<in> sets P" 

804 
from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this] 

805 
show "Q.pair_measure ((\<lambda>(x, y). (y, x)) ` A \<inter> space Q.P) = pair_measure A" 

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

807 
simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra) 

808 
qed 

809 
qed 

810 

40859  811 
lemma (in pair_sigma_finite) positive_integral_snd_measurable: 
812 
assumes f: "f \<in> borel_measurable P" 

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

814 
positive_integral f" 

815 
proof  

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

817 
note pair_sigma_algebra_measurable[OF f] 

818 
from Q.positive_integral_fst_measurable[OF this] 

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

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

821 
by simp 

41661  822 
also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f" 
823 
unfolding positive_integral_product_swap[OF f, symmetric] 

824 
by (auto intro!: Q.positive_integral_cong) 

40859  825 
finally show ?thesis . 
826 
qed 

827 

828 
lemma (in pair_sigma_finite) Fubini: 

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

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

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

832 
unfolding positive_integral_snd_measurable[OF assms] 

833 
unfolding positive_integral_fst_measurable[OF assms] .. 

834 

835 
lemma (in pair_sigma_finite) AE_pair: 

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

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

838 
proof  

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

840 
using assms unfolding almost_everywhere_def by auto 

841 
show ?thesis 

842 
proof (rule M1.AE_I) 

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

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

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

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40873
diff
changeset

847 
by (intro M1.borel_measurable_pextreal_neq_const measure_cut_measurable_fst N) 
40859  848 
{ fix x assume "x \<in> space M1" "\<mu>2 (Pair x ` N) = 0" 
849 
have "M2.almost_everywhere (\<lambda>y. Q (x, y))" 

850 
proof (rule M2.AE_I) 

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

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

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

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

855 
qed } 

856 
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}" 

857 
by auto 

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

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

859 
qed 
35833  860 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

861 
lemma (in pair_sigma_algebra) measurable_product_swap: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

862 
"f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

863 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

864 
interpret Q: pair_sigma_algebra M2 M1 by default 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

865 
show ?thesis 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

866 
using pair_sigma_algebra_measurable[of "\<lambda>(x,y). f (y, x)"] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

867 
by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

868 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

869 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

870 
lemma (in pair_sigma_finite) integrable_product_swap: 
41661  871 
assumes "integrable f" 
872 
shows "measure_space.integrable 

873 
(sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))" 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

874 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

875 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 
41661  876 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
877 
show ?thesis unfolding * 

878 
using assms unfolding Q.integrable_def integrable_def 

879 
apply (subst (1 2) positive_integral_product_swap) 

880 
using `integrable f` unfolding integrable_def 

881 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 

882 
qed 

883 

884 
lemma (in pair_sigma_finite) integrable_product_swap_iff: 

885 
"measure_space.integrable 

886 
(sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> 

887 
integrable f" 

888 
proof  

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

890 
from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f] 

891 
show ?thesis by auto 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

892 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

893 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

894 
lemma (in pair_sigma_finite) integral_product_swap: 
41661  895 
assumes "integrable f" 
896 
shows "measure_space.integral 

897 
(sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) = 

898 
integral f" 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

899 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

900 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 
41661  901 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

902 
show ?thesis 
41661  903 
unfolding integral_def Q.integral_def * 
904 
apply (subst (1 2) positive_integral_product_swap) 

905 
using `integrable f` unfolding integrable_def 

906 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

907 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

908 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

909 
lemma (in pair_sigma_finite) integrable_fst_measurable: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

910 
assumes f: "integrable f" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

911 
shows "M1.almost_everywhere (\<lambda>x. M2.integrable (\<lambda> y. f (x, y)))" (is "?AE") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

912 
and "M1.integral (\<lambda> x. M2.integral (\<lambda> y. f (x, y))) = integral f" (is "?INT") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

913 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

914 
let "?pf x" = "Real (f x)" and "?nf x" = "Real ( f x)" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

915 
have 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

916 
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

917 
int: "positive_integral ?nf \<noteq> \<omega>" "positive_integral ?pf \<noteq> \<omega>" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

918 
using assms by auto 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

919 
have "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. Real (f (x, y)))) \<noteq> \<omega>" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

920 
"M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. Real ( f (x, y)))) \<noteq> \<omega>" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

921 
using borel[THEN positive_integral_fst_measurable(1)] int 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

922 
unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

923 
with borel[THEN positive_integral_fst_measurable(1)] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

924 
have AE: "M1.almost_everywhere (\<lambda>x. M2.positive_integral (\<lambda>y. Real (f (x, y))) \<noteq> \<omega>)" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

925 
"M1.almost_everywhere (\<lambda>x. M2.positive_integral (\<lambda>y. Real ( f (x, y))) \<noteq> \<omega>)" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

926 
by (auto intro!: M1.positive_integral_omega_AE) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

927 
then show ?AE 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

928 
apply (rule M1.AE_mp[OF _ M1.AE_mp]) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

929 
apply (rule M1.AE_cong) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

930 
using assms unfolding M2.integrable_def 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

931 
by (auto intro!: measurable_pair_image_snd) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

932 
have "M1.integrable 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

933 
(\<lambda>x. real (M2.positive_integral (\<lambda>xa. Real (f (x, xa)))))" (is "M1.integrable ?f") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

934 
proof (unfold M1.integrable_def, intro conjI) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

935 
show "?f \<in> borel_measurable M1" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

936 
using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

937 
have "M1.positive_integral (\<lambda>x. Real (?f x)) = 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

938 
M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>xa. Real (f (x, xa))))" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

939 
apply (rule M1.positive_integral_cong_AE) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

940 
apply (rule M1.AE_mp[OF AE(1)]) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

941 
apply (rule M1.AE_cong) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

942 
by (auto simp: Real_real) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

943 
then show "M1.positive_integral (\<lambda>x. Real (?f x)) \<noteq> \<omega>" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

944 
using positive_integral_fst_measurable[OF borel(2)] int by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

945 
have "M1.positive_integral (\<lambda>x. Real ( ?f x)) = M1.positive_integral (\<lambda>x. 0)" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

946 
by (intro M1.positive_integral_cong) simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

947 
then show "M1.positive_integral (\<lambda>x. Real ( ?f x)) \<noteq> \<omega>" by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

948 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

949 
moreover have "M1.integrable 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

950 
(\<lambda>x. real (M2.positive_integral (\<lambda>xa. Real ( f (x, xa)))))" (is "M1.integrable ?f") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

951 
proof (unfold M1.integrable_def, intro conjI) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

952 
show "?f \<in> borel_measurable M1" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

953 
using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

954 
have "M1.positive_integral (\<lambda>x. Real (?f x)) = 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

955 
M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>xa. Real ( f (x, xa))))" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

956 
apply (rule M1.positive_integral_cong_AE) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

957 
apply (rule M1.AE_mp[OF AE(2)]) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

958 
apply (rule M1.AE_cong) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

959 
by (auto simp: Real_real) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

960 
then show "M1.positive_integral (\<lambda>x. Real (?f x)) \<noteq> \<omega>" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

961 
using positive_integral_fst_measurable[OF borel(1)] int by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

962 
have "M1.positive_integral (\<lambda>x. Real ( ?f x)) = M1.positive_integral (\<lambda>x. 0)" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

963 
by (intro M1.positive_integral_cong) simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

964 
then show "M1.positive_integral (\<lambda>x. Real ( ?f x)) \<noteq> \<omega>" by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

965 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

966 
ultimately show ?INT 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

967 
unfolding M2.integral_def integral_def 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

968 
borel[THEN positive_integral_fst_measurable(2), symmetric] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

969 
by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)]) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

970 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

971 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

972 
lemma (in pair_sigma_finite) integrable_snd_measurable: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

973 
assumes f: "integrable f" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

974 
shows "M2.almost_everywhere (\<lambda>y. M1.integrable (\<lambda>x. f (x, y)))" (is "?AE") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

975 
and "M2.integral (\<lambda>y. M1.integral (\<lambda>x. f (x, y))) = integral f" (is "?INT") 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

976 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

977 
interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

978 
have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))" 
41661  979 
using f unfolding integrable_product_swap_iff . 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

980 
show ?INT 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

981 
using Q.integrable_fst_measurable(2)[OF Q_int] 
41661  982 
using integral_product_swap[OF f] by simp 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

983 
show ?AE 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

984 
using Q.integrable_fst_measurable(1)[OF Q_int] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

985 
by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

986 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

987 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

988 
lemma (in pair_sigma_finite) Fubini_integral: 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

989 
assumes f: "integrable f" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

990 
shows "M2.integral (\<lambda>y. M1.integral (\<lambda>x. f (x, y))) = 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

991 
M1.integral (\<lambda>x. M2.integral (\<lambda>y. f (x, y)))" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

992 
unfolding integrable_snd_measurable[OF assms] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

993 
unfolding integrable_fst_measurable[OF assms] .. 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

994 

40859  995 
section "Finite product spaces" 
996 

997 
section "Products" 

998 

999 
locale product_sigma_algebra = 

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

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

1002 

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

1004 
fixes I :: "'i set" 

1005 
assumes finite_index: "finite I" 

1006 

1007 
syntax 

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

1009 

1010 
syntax (xsymbols) 

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

1012 

1013 
syntax (HTML output) 

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

1015 

1016 
translations 

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

1018 

35833  1019 
definition 
40859  1020 
"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>" 
1021 

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

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

1024 

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

1026 

1027 
lemma (in finite_product_sigma_algebra) product_algebra_into_space: 

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

1029 
using M.sets_into_space unfolding product_algebra_def 

1030 
by auto blast 

1031 

1032 
sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P 

1033 
using product_algebra_into_space by (rule sigma_algebra_sigma) 

1034 

41095  1035 
lemma product_algebraE: 
1036 
assumes "A \<in> sets (product_algebra M I)" 

1037 
obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))" 

1038 
using assms unfolding product_algebra_def by auto 

1039 

1040 
lemma product_algebraI[intro]: 

1041 
assumes "E \<in> (\<Pi> i\<in>I. sets (M i))" 

1042 
shows "Pi\<^isub>E I E \<in> sets (product_algebra M I)" 

1043 
using assms unfolding product_algebra_def by auto 

1044 

40859  1045 
lemma space_product_algebra[simp]: 
1046 
"space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))" 

1047 
unfolding product_algebra_def by simp 

1048 

41095  1049 
lemma product_algebra_sets_into_space: 
1050 
assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))" 

1051 
shows "sets (product_algebra M I) \<subseteq> Pow (space (product_algebra M I))" 

1052 
using assms by (auto simp: product_algebra_def) blast 

1053 

40859  1054 
lemma (in finite_product_sigma_algebra) P_empty: 
1055 
"I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>" 

40872  1056 
unfolding product_algebra_def by (simp add: sigma_def image_constant) 
40859  1057 

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

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

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

1061 

41095  1062 
lemma (in product_sigma_algebra) bij_inv_restrict_merge: 
1063 
assumes [simp]: "I \<inter> J = {}" 

1064 
shows "bij_inv 

1065 
(space (sigma (product_algebra M (I \<union> J)))) 

1066 
(space (sigma (pair_algebra (product_algebra M I) (product_algebra M J)))) 

1067 
(\<lambda>x. (restrict x I, restrict x J)) (\<lambda>(x, y). merge I x J y)" 

1068 
by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict) 

1069 

1070 
lemma (in product_sigma_algebra) bij_inv_singleton: 

1071 
"bij_inv (space (sigma (product_algebra M {i}))) (space (M i)) 

1072 
(\<lambda>x. x i) (\<lambda>x. (\<lambda>j\<in>{i}. x))" 

1073 
by (rule bij_invI) (auto simp: restrict_def extensional_def fun_eq_iff) 

1074 

1075 
lemma (in product_sigma_algebra) bij_inv_restrict_insert: 

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

1077 
shows "bij_inv 

1078 
(space (sigma (product_algebra M (insert i I)))) 

1079 
(space (sigma (pair_algebra (product_algebra M I) (M i)))) 

1080 
(\<lambda>x. (restrict x I, x i)) (\<lambda>(x, y). x(i := y))" 

1081 
by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict) 

1082 

1083 
lemma (in product_sigma_algebra) measurable_restrict_on_generating: 

1084 
assumes [simp]: "I \<inter> J = {}" 

1085 
shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable 

1086 
(product_algebra M (I \<union> J)) 

1087 
(pair_algebra (product_algebra M I) (product_algebra M J))" 

1088 
(is "?R \<in> measurable ?IJ ?P") 

1089 
proof (unfold measurable_def, intro CollectI conjI ballI) 

1090 
show "?R \<in> space ?IJ \<rightarrow> space ?P" by (auto simp: space_pair_algebra) 

1091 
{ fix F E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))" 

1092 
then have "Pi (I \<union> J) (merge I E J F) \<inter> (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) = 

1093 
Pi\<^isub>E (I \<union> J) (merge I E J F)" 

1094 
using M.sets_into_space by auto blast+ } 

1095 
note this[simp] 

1096 
show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R ` A \<inter> space ?IJ \<in> sets ?IJ" 

1097 
by (force elim!: pair_algebraE product_algebraE 

1098 
simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra) 

1099 
qed 

1100 

1101 
lemma (in product_sigma_algebra) measurable_merge_on_generating: 

1102 
assumes [simp]: "I \<inter> J = {}" 

1103 
shows "(\<lambda>(x, y). merge I x J y) \<in> measurable 

1104 
(pair_algebra (product_algebra M I) (product_algebra M J)) 

1105 
(product_algebra M (I \<union> J))" 

1106 
(is "?M \<in> measurable ?P ?IJ") 

1107 
proof (unfold measurable_def, intro CollectI conjI ballI) 

1108 
show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra) 

1109 
{ fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E \<in> (\<Pi> i\<in>J. sets (M i))" 

1110 
then have "Pi I E \<times> Pi J E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> (\<Pi>\<^isub>E i\<in>J. space (M i)) = 

1111 
Pi\<^isub>E I E \<times> Pi\<^isub>E J E" 

1112 
using M.sets_into_space by auto blast+ } 

1113 
note this[simp] 

1114 
show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M ` A \<inter> space ?P \<in> sets ?P" 

1115 
by (force elim!: pair_algebraE product_algebraE 

1116 
simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra) 

40859  1117 
qed 
41095  1118 

1119 
lemma (in product_sigma_algebra) measurable_singleton_on_generator: 

1120 
"(\<lambda>x. \<lambda>j\<in>{i}. x) \<in> measurable (M i) (product_algebra M {i})" 

1121 
(is "?f \<in> measurable _ ?P") 

1122 
proof (unfold measurable_def, intro CollectI conjI) 

1123 
show "?f \<in> space (M i) \<rightarrow> space ?P" by auto 

1124 
have "\<And>E. E i \<in> sets (M i) \<Longrightarrow> ?f ` Pi\<^isub>E {i} E \<inter> space (M i) = E i" 

1125 
using M.sets_into_space by auto 

1126 
then show "\<forall>A \<in> sets ?P. ?f ` A \<inter> space (M i) \<in> sets (M i)" 

1127 
by (auto elim!: product_algebraE) 

1128 
qed 

1129 

1130 
lemma (in product_sigma_algebra) measurable_component_on_generator: 

1131 
assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (product_algebra M I) (M i)" 

1132 
(is "?f \<in> measurable ?P _") 

1133 
proof (unfold measurable_def, intro CollectI conjI ballI) 

1134 
show "?f \<in> space ?P \<rightarrow> space (M i)" using `i \<in> I` by auto 

1135 
fix A assume "A \<in> sets (M i)" 

1136 
moreover then have "(\<lambda>x. x i) ` A \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) = 

1137 
(\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))" 

1138 
using M.sets_into_space `i \<in> I` 

1139 
by (fastsimp dest: Pi_mem split: split_if_asm) 

1140 
ultimately show "?f ` A \<inter> space ?P \<in> sets ?P" 

1141 
by (auto intro!: product_algebraI) 

1142 
qed 

40859  1143 

41095  1144 
lemma (in product_sigma_algebra) measurable_restrict_singleton_on_generating: 
1145 
assumes [simp]: "i \<notin> I" 

1146 
shows "(\<lambda>x. (restrict x I, x i)) \<in> measurable 

1147 
(product_algebra M (insert i I)) 

1148 
(pair_algebra (product_algebra M I) (M i))" 

1149 
(is "?R \<in> measurable ?I ?P") 

1150 
proof (unfold measurable_def, intro CollectI conjI ballI) 

1151 
show "?R \<in> space ?I \<rightarrow> space ?P" by (auto simp: space_pair_algebra) 

1152 
{ fix E F assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)" 

1153 
then have "(\<lambda>x. (restrict x I, x i)) ` (Pi\<^isub>E I E \<times> F) \<inter> (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) = 

1154 
Pi\<^isub>E (insert i I) (E(i := F))" 

1155 
using M.sets_into_space using `i\<notin>I` by (auto simp: restrict_Pi_cancel) blast+ } 

1156 
note this[simp] 

1157 
show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R ` A \<inter> space ?I \<in> sets ?I" 

1158 
by (force elim!: pair_algebraE product_algebraE 

1159 
simp del: vimage_Int simp: space_pair_algebra) 

1160 
qed 

1161 

1162 
lemma (in product_sigma_algebra) measurable_merge_singleton_on_generating: 

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

1164 
shows "(\<lambda>(x, y). x(i := y)) \<in> measurable 

1165 
(pair_algebra (product_algebra M I) (M i)) 

1166 
(product_algebra M (insert i I))" 

1167 
(is "?M \<in> measurable ?P ?IJ") 

1168 
proof (unfold measurable_def, intro CollectI conjI ballI) 

1169 
show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra) 

1170 
{ fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E i \<in> sets (M i)" 

1171 
then have "(\<lambda>(x, y). x(i := y)) ` Pi\<^isub>E (insert i I) E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> space (M i) = 

1172 
Pi\<^isub>E I E \<times> E i" 

1173 
using M.sets_into_space by auto blast+ } 

1174 
note this[simp] 

1175 
show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M ` A \<inter> space ?P \<in> sets ?P" 

1176 
by (force elim!: pair_algebraE product_algebraE 

1177 
simp del: vimage_Int simp: space_pair_algebra) 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1178 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1179 

40859  1180 
section "Generating set generates also product algebra" 
1181 

1182 
lemma pair_sigma_algebra_sigma: 

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

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

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

1186 
(is "?S = ?E") 

1187 
proof  

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

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

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

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

1192 
interpret E: sigma_algebra ?E unfolding pair_algebra_def 

1193 
using E1 E2 by (intro sigma_algebra_sigma) auto 

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

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

1196 
using E1 2 unfolding isoton_def pair_algebra_def by auto 

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

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

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

1200 
by (intro sigma_sets.Union) 

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

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

1203 
moreover 

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

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

1206 
using E2 1 unfolding isoton_def pair_algebra_def by auto 

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

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

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

1210 
by (intro sigma_sets.Union) 

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

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

1213 
ultimately have proj: 

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

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

1216 
(auto simp: pair_algebra_def sets_sigma) 

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

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

1219 
unfolding measurable_def by simp_all 

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

1221 
using A B M1.sets_into_space M2.sets_into_space 

1222 
by (auto simp: pair_algebra_def) 

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

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

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

1226 
then have subset: "sets ?S \<subseteq> sets ?E&q 