author  hoelzl 
Wed, 10 Oct 2012 12:12:34 +0200  
changeset 49800  a6678da5692c 
parent 49789  e0a4cb91a8a9 
child 49825  bb5db3d1d6dd 
permissions  rwrr 
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

1 
(* Title: HOL/Probability/Binary_Product_Measure.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
*) 

4 

42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

5 
header {*Binary product measures*} 
42067  6 

42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

7 
theory Binary_Product_Measure 
38656  8 
imports Lebesgue_Integration 
35833  9 
begin 
10 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

11 
lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

12 
by auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

13 

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

16 

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

18 
by auto 

19 

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

21 
by auto 

22 

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

24 
by (cases x) simp 

25 

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

26 
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

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

28 

40859  29 
section "Binary products" 
30 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

31 
definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where 
47694  32 
"A \<Otimes>\<^isub>M B = measure_of (space A \<times> space B) 
33 
{a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B} 

34 
(\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)" 

40859  35 

49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

36 
lemma pair_measure_closed: "{a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)" 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

37 
using space_closed[of A] space_closed[of B] by auto 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

38 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

39 
lemma space_pair_measure: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

40 
"space (A \<Otimes>\<^isub>M B) = space A \<times> space B" 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

41 
unfolding pair_measure_def using pair_measure_closed[of A B] 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

42 
by (rule space_measure_of) 
47694  43 

44 
lemma sets_pair_measure: 

45 
"sets (A \<Otimes>\<^isub>M B) = sigma_sets (space A \<times> space B) {a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B}" 

49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

46 
unfolding pair_measure_def using pair_measure_closed[of A B] 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

47 
by (rule sets_measure_of) 
41095  48 

49776  49 
lemma sets_pair_measure_cong[cong]: 
50 
"sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')" 

51 
unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) 

52 

47694  53 
lemma pair_measureI[intro, simp]: 
54 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)" 

55 
by (auto simp: sets_pair_measure) 

41095  56 

47694  57 
lemma measurable_pair_measureI: 
58 
assumes 1: "f \<in> space M \<rightarrow> space M1 \<times> space M2" 

59 
assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f ` (A \<times> B) \<inter> space M \<in> sets M" 

60 
shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)" 

61 
unfolding pair_measure_def using 1 2 

62 
by (intro measurable_measure_of) (auto dest: sets_into_space) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

63 

49776  64 
lemma measurable_Pair: 
65 
assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2" 

66 
shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)" 

67 
proof (rule measurable_pair_measureI) 

68 
show "(\<lambda>x. (f x, g x)) \<in> space M \<rightarrow> space M1 \<times> space M2" 

69 
using f g by (auto simp: measurable_def) 

70 
fix A B assume *: "A \<in> sets M1" "B \<in> sets M2" 

71 
have "(\<lambda>x. (f x, g x)) ` (A \<times> B) \<inter> space M = (f ` A \<inter> space M) \<inter> (g ` B \<inter> space M)" 

72 
by auto 

73 
also have "\<dots> \<in> sets M" 

74 
by (rule Int) (auto intro!: measurable_sets * f g) 

75 
finally show "(\<lambda>x. (f x, g x)) ` (A \<times> B) \<inter> space M \<in> sets M" . 

76 
qed 

77 

78 
lemma measurable_pair: 

79 
assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" 

80 
shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)" 

81 
using measurable_Pair[OF assms] by simp 

82 

47694  83 
lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1" 
49776  84 
by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def) 
40859  85 

47694  86 
lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2" 
49776  87 
by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def) 
47694  88 

89 
lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N" 

90 
using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def) 

91 

92 
lemma measurable_snd': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. snd (f x)) \<in> measurable M P" 

93 
using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def) 

40859  94 

47694  95 
lemma measurable_fst'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N" 
96 
using measurable_comp[OF measurable_fst _] by (auto simp: comp_def) 

97 

98 
lemma measurable_snd'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N" 

99 
using measurable_comp[OF measurable_snd _] by (auto simp: comp_def) 

100 

101 
lemma measurable_pair_iff: 

102 
"f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" 

49776  103 
using measurable_pair[of f M M1 M2] by auto 
40859  104 

49776  105 
lemma measurable_split_conv: 
106 
"(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B" 

107 
by (intro arg_cong2[where f="op \<in>"]) auto 

40859  108 

47694  109 
lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)" 
49776  110 
by (auto intro!: measurable_Pair simp: measurable_split_conv) 
47694  111 

112 
lemma measurable_pair_swap: 

113 
assumes f: "f \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M" 

49776  114 
using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def) 
40859  115 

47694  116 
lemma measurable_pair_swap_iff: 
117 
"f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" 

118 
using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"] 

119 
by (auto intro!: measurable_pair_swap) 

40859  120 

49776  121 
lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M" 
122 
unfolding measurable_def by auto 

123 

47694  124 
lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)" 
49776  125 
by (auto intro!: measurable_Pair) 
40859  126 

47694  127 
lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x ` A \<in> sets M2" 
40859  128 
proof  
47694  129 
have "Pair x ` A = (if x \<in> space M1 then Pair x ` A \<inter> space M2 else {})" 
130 
using A[THEN sets_into_space] by (auto simp: space_pair_measure) 

131 
also have "\<dots> \<in> sets M2" 

132 
using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm) 

133 
finally show ?thesis . 

40859  134 
qed 
135 

47694  136 
lemma measurable_Pair2': "y \<in> space M2 \<Longrightarrow> (\<lambda>x. (x, y)) \<in> measurable M1 (M1 \<Otimes>\<^isub>M M2)" 
49776  137 
by (auto intro!: measurable_Pair) 
40859  138 

47694  139 
lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) ` A \<in> sets M1" 
140 
proof  

141 
have "(\<lambda>x. (x, y)) ` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) ` A \<inter> space M1 else {})" 

142 
using A[THEN sets_into_space] by (auto simp: space_pair_measure) 

143 
also have "\<dots> \<in> sets M1" 

144 
using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm) 

145 
finally show ?thesis . 

40859  146 
qed 
147 

47694  148 
lemma measurable_Pair2: 
149 
assumes f: "f \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" and x: "x \<in> space M1" 

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

151 
using measurable_comp[OF measurable_Pair1' f, OF x] 

152 
by (simp add: comp_def) 

153 

154 
lemma measurable_Pair1: 

155 
assumes f: "f \<in> measurable (M1 \<Otimes>\<^isub>M M2) M" and y: "y \<in> space M2" 

40859  156 
shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M" 
47694  157 
using measurable_comp[OF measurable_Pair2' f, OF y] 
158 
by (simp add: comp_def) 

40859  159 

47694  160 
lemma Int_stable_pair_measure_generator: "Int_stable {a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B}" 
40859  161 
unfolding Int_stable_def 
47694  162 
by safe (auto simp add: times_Int_times) 
40859  163 

49776  164 
lemma (in finite_measure) finite_measure_cut_measurable: 
165 
assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)" 

166 
shows "(\<lambda>x. emeasure M (Pair x ` Q)) \<in> borel_measurable N" 

40859  167 
(is "?s Q \<in> _") 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

168 
using Int_stable_pair_measure_generator pair_measure_closed assms 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

169 
unfolding sets_pair_measure 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

170 
proof (induct rule: sigma_sets_induct_disjoint) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

171 
case (compl A) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

172 
with sets_into_space have "\<And>x. emeasure M (Pair x ` ((space N \<times> space M)  A)) = 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

173 
(if x \<in> space N then emeasure M (space M)  ?s A x else 0)" 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

174 
unfolding sets_pair_measure[symmetric] 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

175 
by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

176 
with compl top show ?case 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

177 
by (auto intro!: measurable_If simp: space_pair_measure) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

178 
next 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

179 
case (union F) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

180 
moreover then have "\<And>x. emeasure M (\<Union>i. Pair x ` F i) = (\<Sum>i. ?s (F i) x)" 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

181 
unfolding sets_pair_measure[symmetric] 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

182 
by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

183 
ultimately show ?case 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

184 
by (auto simp: vimage_UN) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

185 
qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If) 
49776  186 

187 
lemma (in sigma_finite_measure) measurable_emeasure_Pair: 

188 
assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x ` Q)) \<in> borel_measurable N" (is "?s Q \<in> _") 

189 
proof  

190 
from sigma_finite_disjoint guess F . note F = this 

191 
then have F_sets: "\<And>i. F i \<in> sets M" by auto 

192 
let ?C = "\<lambda>x i. F i \<inter> Pair x ` Q" 

193 
{ fix i 

194 
have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i" 

195 
using F sets_into_space by auto 

196 
let ?R = "density M (indicator (F i))" 

197 
have "finite_measure ?R" 

198 
using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq) 

199 
then have "(\<lambda>x. emeasure ?R (Pair x ` (space N \<times> space ?R \<inter> Q))) \<in> borel_measurable N" 

200 
by (rule finite_measure.finite_measure_cut_measurable) (auto intro: Q) 

201 
moreover have "\<And>x. emeasure ?R (Pair x ` (space N \<times> space ?R \<inter> Q)) 

202 
= emeasure M (F i \<inter> Pair x ` (space N \<times> space ?R \<inter> Q))" 

203 
using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1) 

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

205 
using sets_into_space[OF Q] by (auto simp: space_pair_measure) 

206 
ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N" 

207 
by simp } 

208 
moreover 

209 
{ fix x 

210 
have "(\<Sum>i. emeasure M (?C x i)) = emeasure M (\<Union>i. ?C x i)" 

211 
proof (intro suminf_emeasure) 

212 
show "range (?C x) \<subseteq> sets M" 

213 
using F `Q \<in> sets (N \<Otimes>\<^isub>M M)` by (auto intro!: sets_Pair1) 

214 
have "disjoint_family F" using F by auto 

215 
show "disjoint_family (?C x)" 

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

217 
qed 

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

219 
using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`] 

220 
by (auto simp: space_pair_measure) 

221 
finally have "emeasure M (Pair x ` Q) = (\<Sum>i. emeasure M (?C x i))" 

222 
by simp } 

223 
ultimately show ?thesis using `Q \<in> sets (N \<Otimes>\<^isub>M M)` F_sets 

224 
by auto 

225 
qed 

226 

227 
lemma (in sigma_finite_measure) emeasure_pair_measure: 

228 
assumes "X \<in> sets (N \<Otimes>\<^isub>M M)" 

229 
shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X") 

230 
proof (rule emeasure_measure_of[OF pair_measure_def]) 

231 
show "positive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>" 

232 
by (auto simp: positive_def positive_integral_positive) 

233 
have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x ` A) y" 

234 
by (auto simp: indicator_def) 

235 
show "countably_additive (sets (N \<Otimes>\<^isub>M M)) ?\<mu>" 

236 
proof (rule countably_additiveI) 

237 
fix F :: "nat \<Rightarrow> ('b \<times> 'a) set" assume F: "range F \<subseteq> sets (N \<Otimes>\<^isub>M M)" "disjoint_family F" 

238 
from F have *: "\<And>i. F i \<in> sets (N \<Otimes>\<^isub>M M)" "(\<Union>i. F i) \<in> sets (N \<Otimes>\<^isub>M M)" by auto 

239 
moreover from F have "\<And>i. (\<lambda>x. emeasure M (Pair x ` F i)) \<in> borel_measurable N" 

240 
by (intro measurable_emeasure_Pair) auto 

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

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

243 
moreover have "\<And>x. range (\<lambda>i. Pair x ` F i) \<subseteq> sets M" 

244 
using F by (auto simp: sets_Pair1) 

245 
ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)" 

246 
by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1 

247 
intro!: positive_integral_cong positive_integral_indicator[symmetric]) 

248 
qed 

249 
show "{a \<times> b a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)" 

250 
using space_closed[of N] space_closed[of M] by auto 

251 
qed fact 

252 

253 
lemma (in sigma_finite_measure) emeasure_pair_measure_alt: 

254 
assumes X: "X \<in> sets (N \<Otimes>\<^isub>M M)" 

255 
shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+x. emeasure M (Pair x ` X) \<partial>N)" 

256 
proof  

257 
have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x ` X) y" 

258 
by (auto simp: indicator_def) 

259 
show ?thesis 

260 
using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1) 

261 
qed 

262 

263 
lemma (in sigma_finite_measure) emeasure_pair_measure_Times: 

264 
assumes A: "A \<in> sets N" and B: "B \<in> sets M" 

265 
shows "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = emeasure N A * emeasure M B" 

266 
proof  

267 
have "emeasure (N \<Otimes>\<^isub>M M) (A \<times> B) = (\<integral>\<^isup>+x. emeasure M B * indicator A x \<partial>N)" 

268 
using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt) 

269 
also have "\<dots> = emeasure M B * emeasure N A" 

270 
using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator) 

271 
finally show ?thesis 

272 
by (simp add: ac_simps) 

40859  273 
qed 
274 

47694  275 
subsection {* Binary products of $\sigma$finite emeasure spaces *} 
40859  276 

47694  277 
locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 
278 
for M1 :: "'a measure" and M2 :: "'b measure" 

40859  279 

47694  280 
lemma (in pair_sigma_finite) measurable_emeasure_Pair1: 
49776  281 
"Q \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. emeasure M2 (Pair x ` Q)) \<in> borel_measurable M1" 
282 
using M2.measurable_emeasure_Pair . 

40859  283 

47694  284 
lemma (in pair_sigma_finite) measurable_emeasure_Pair2: 
285 
assumes Q: "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>y. emeasure M1 ((\<lambda>x. (x, y)) ` Q)) \<in> borel_measurable M2" 

40859  286 
proof  
47694  287 
have "(\<lambda>(x, y). (y, x)) ` Q \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
288 
using Q measurable_pair_swap' by (auto intro: measurable_sets) 

49776  289 
note M1.measurable_emeasure_Pair[OF this] 
47694  290 
moreover have "\<And>y. Pair y ` ((\<lambda>(x, y). (y, x)) ` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) ` Q" 
291 
using Q[THEN sets_into_space] by (auto simp: space_pair_measure) 

292 
ultimately show ?thesis by simp 

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

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

294 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

295 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: 
47694  296 
defines "E \<equiv> {A \<times> B  A B. A \<in> sets M1 \<and> B \<in> sets M2}" 
297 
shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and> 

298 
(\<forall>i. emeasure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>)" 

40859  299 
proof  
47694  300 
from M1.sigma_finite_incseq guess F1 . note F1 = this 
301 
from M2.sigma_finite_incseq guess F2 . note F2 = this 

302 
from F1 F2 have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto 

40859  303 
let ?F = "\<lambda>i. F1 i \<times> F2 i" 
47694  304 
show ?thesis 
40859  305 
proof (intro exI[of _ ?F] conjI allI) 
47694  306 
show "range ?F \<subseteq> E" using F1 F2 by (auto simp: E_def) (metis range_subsetD) 
40859  307 
next 
308 
have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)" 

309 
proof (intro subsetI) 

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

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

312 
by (auto simp: space) 

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

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

314 
using `incseq F1` `incseq F2` unfolding incseq_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

315 
by (force split: split_max)+ 
40859  316 
then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)" 
317 
by (intro SigmaI) (auto simp add: min_max.sup_commute) 

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

319 
qed 

47694  320 
then show "(\<Union>i. ?F i) = space M1 \<times> space M2" 
321 
using space by (auto simp: space) 

40859  322 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

323 
fix i show "incseq (\<lambda>i. F1 i \<times> F2 i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

324 
using `incseq F1` `incseq F2` unfolding incseq_Suc_iff by auto 
40859  325 
next 
326 
fix i 

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

47694  328 
with F1 F2 emeasure_nonneg[of M1 "F1 i"] emeasure_nonneg[of M2 "F2 i"] 
329 
show "emeasure (M1 \<Otimes>\<^isub>M M2) (F1 i \<times> F2 i) \<noteq> \<infinity>" 

330 
by (auto simp add: emeasure_pair_measure_Times) 

331 
qed 

332 
qed 

333 

49800  334 
sublocale pair_sigma_finite \<subseteq> P: sigma_finite_measure "M1 \<Otimes>\<^isub>M M2" 
47694  335 
proof 
336 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 

337 
show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets (M1 \<Otimes>\<^isub>M M2) \<and> (\<Union>i. F i) = space (M1 \<Otimes>\<^isub>M M2) \<and> (\<forall>i. emeasure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>)" 

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

339 
show "range F \<subseteq> sets (M1 \<Otimes>\<^isub>M M2)" using F by (auto simp: pair_measure_def) 

340 
show "(\<Union>i. F i) = space (M1 \<Otimes>\<^isub>M M2)" 

341 
using F by (auto simp: space_pair_measure) 

342 
show "\<forall>i. emeasure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>" using F by auto 

40859  343 
qed 
344 
qed 

345 

47694  346 
lemma sigma_finite_pair_measure: 
347 
assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B" 

348 
shows "sigma_finite_measure (A \<Otimes>\<^isub>M B)" 

349 
proof  

350 
interpret A: sigma_finite_measure A by fact 

351 
interpret B: sigma_finite_measure B by fact 

352 
interpret AB: pair_sigma_finite A B .. 

353 
show ?thesis .. 

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

355 

47694  356 
lemma sets_pair_swap: 
357 
assumes "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

358 
shows "(\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
47694  359 
using measurable_pair_swap' assms by (rule measurable_sets) 
41661  360 

47694  361 
lemma (in pair_sigma_finite) distr_pair_swap: 
362 
"M1 \<Otimes>\<^isub>M M2 = distr (M2 \<Otimes>\<^isub>M M1) (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D") 

40859  363 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

364 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
47694  365 
let ?E = "{a \<times> b a b. a \<in> sets M1 \<and> b \<in> sets M2}" 
366 
show ?thesis 

367 
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) 

368 
show "?E \<subseteq> Pow (space ?P)" 

369 
using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) 

370 
show "sets ?P = sigma_sets (space ?P) ?E" 

371 
by (simp add: sets_pair_measure space_pair_measure) 

372 
then show "sets ?D = sigma_sets (space ?P) ?E" 

373 
by simp 

374 
next 

49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49776
diff
changeset

375 
show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>" 
47694  376 
using F by (auto simp: space_pair_measure) 
377 
next 

378 
fix X assume "X \<in> ?E" 

379 
then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto 

380 
have "(\<lambda>(y, x). (x, y)) ` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A" 

381 
using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure) 

382 
with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X" 

49776  383 
by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr 
47694  384 
measurable_pair_swap' ac_simps) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

385 
qed 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

386 
qed 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

387 

47694  388 
lemma (in pair_sigma_finite) emeasure_pair_measure_alt2: 
389 
assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" 

390 
shows "emeasure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+y. emeasure M1 ((\<lambda>x. (x, y)) ` A) \<partial>M2)" 

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

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

392 
proof  
47694  393 
have [simp]: "\<And>y. (Pair y ` ((\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) ` A" 
394 
using sets_into_space[OF A] by (auto simp: space_pair_measure) 

395 
show ?thesis using A 

396 
by (subst distr_pair_swap) 

397 
(simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap'] 

49776  398 
M1.emeasure_pair_measure_alt emeasure_distr[OF measurable_pair_swap' A]) 
399 
qed 

400 

401 
lemma (in pair_sigma_finite) AE_pair: 

402 
assumes "AE x in (M1 \<Otimes>\<^isub>M M2). Q x" 

403 
shows "AE x in M1. (AE y in M2. Q (x, y))" 

404 
proof  

405 
obtain N where N: "N \<in> sets (M1 \<Otimes>\<^isub>M M2)" "emeasure (M1 \<Otimes>\<^isub>M M2) N = 0" "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> Q x} \<subseteq> N" 

406 
using assms unfolding eventually_ae_filter by auto 

407 
show ?thesis 

408 
proof (rule AE_I) 

409 
from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^isub>M M2)`] 

410 
show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x ` N) \<noteq> 0} = 0" 

411 
by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg) 

412 
show "{x \<in> space M1. emeasure M2 (Pair x ` N) \<noteq> 0} \<in> sets M1" 

413 
by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N) 

414 
{ fix x assume "x \<in> space M1" "emeasure M2 (Pair x ` N) = 0" 

415 
have "AE y in M2. Q (x, y)" 

416 
proof (rule AE_I) 

417 
show "emeasure M2 (Pair x ` N) = 0" by fact 

418 
show "Pair x ` N \<in> sets M2" using N(1) by (rule sets_Pair1) 

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

420 
using N `x \<in> space M1` unfolding space_pair_measure by auto 

421 
qed } 

422 
then show "{x \<in> space M1. \<not> (AE y in M2. Q (x, y))} \<subseteq> {x \<in> space M1. emeasure M2 (Pair x ` N) \<noteq> 0}" 

423 
by auto 

424 
qed 

425 
qed 

426 

427 
lemma (in pair_sigma_finite) AE_pair_measure: 

428 
assumes "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)" 

429 
assumes ae: "AE x in M1. AE y in M2. P (x, y)" 

430 
shows "AE x in M1 \<Otimes>\<^isub>M M2. P x" 

431 
proof (subst AE_iff_measurable[OF _ refl]) 

432 
show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)" 

433 
by (rule sets_Collect) fact 

434 
then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 

435 
(\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)" 

436 
by (simp add: M2.emeasure_pair_measure) 

437 
also have "\<dots> = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. 0 \<partial>M2 \<partial>M1)" 

438 
using ae 

439 
apply (safe intro!: positive_integral_cong_AE) 

440 
apply (intro AE_I2) 

441 
apply (safe intro!: positive_integral_cong_AE) 

442 
apply auto 

443 
done 

444 
finally show "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} = 0" by simp 

445 
qed 

446 

447 
lemma (in pair_sigma_finite) AE_pair_iff: 

448 
"{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> 

449 
(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE x in (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x))" 

450 
using AE_pair[of "\<lambda>x. P (fst x) (snd x)"] AE_pair_measure[of "\<lambda>x. P (fst x) (snd x)"] by auto 

451 

452 
lemma (in pair_sigma_finite) AE_commute: 

453 
assumes P: "{x\<in>space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<in> sets (M1 \<Otimes>\<^isub>M M2)" 

454 
shows "(AE x in M1. AE y in M2. P x y) \<longleftrightarrow> (AE y in M2. AE x in M1. P x y)" 

455 
proof  

456 
interpret Q: pair_sigma_finite M2 M1 .. 

457 
have [simp]: "\<And>x. (fst (case x of (x, y) \<Rightarrow> (y, x))) = snd x" "\<And>x. (snd (case x of (x, y) \<Rightarrow> (y, x))) = fst x" 

458 
by auto 

459 
have "{x \<in> space (M2 \<Otimes>\<^isub>M M1). P (snd x) (fst x)} = 

460 
(\<lambda>(x, y). (y, x)) ` {x \<in> space (M1 \<Otimes>\<^isub>M M2). P (fst x) (snd x)} \<inter> space (M2 \<Otimes>\<^isub>M M1)" 

461 
by (auto simp: space_pair_measure) 

462 
also have "\<dots> \<in> sets (M2 \<Otimes>\<^isub>M M1)" 

463 
by (intro sets_pair_swap P) 

464 
finally show ?thesis 

465 
apply (subst AE_pair_iff[OF P]) 

466 
apply (subst distr_pair_swap) 

467 
apply (subst AE_distr_iff[OF measurable_pair_swap' P]) 

468 
apply (subst Q.AE_pair_iff) 

469 
apply simp_all 

470 
done 

40859  471 
qed 
472 

473 
section "Fubinis theorem" 

474 

49800  475 
lemma measurable_compose_Pair1: 
476 
"x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L" 

477 
by (rule measurable_compose[OF measurable_Pair]) auto 

478 

479 
lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: 

480 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x" 

481 
shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 

482 
using f proof induct 

483 
case (cong u v) 

484 
then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M2 \<Longrightarrow> u (w, x) = v (w, x)" 

485 
by (auto simp: space_pair_measure) 

486 
show ?case 

487 
apply (subst measurable_cong) 

488 
apply (rule positive_integral_cong) 

489 
apply fact+ 

490 
done 

491 
next 

492 
case (set Q) 

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

494 
by (auto simp: indicator_def) 

495 
have "\<And>x. x \<in> space M1 \<Longrightarrow> emeasure M2 (Pair x ` Q) = \<integral>\<^isup>+ y. indicator Q (x, y) \<partial>M2" 

496 
by (simp add: sets_Pair1[OF set]) 

497 
from this M2.measurable_emeasure_Pair[OF set] show ?case 

498 
by (rule measurable_cong[THEN iffD1]) 

499 
qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1 

500 
positive_integral_monotone_convergence_SUP incseq_def le_fun_def 

501 
cong: measurable_cong) 

502 

503 
lemma (in pair_sigma_finite) positive_integral_fst: 

504 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x" 

505 
shows "(\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2 \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" (is "?I f = _") 

506 
using f proof induct 

507 
case (cong u v) 

508 
moreover then have "?I u = ?I v" 

509 
by (intro positive_integral_cong) (auto simp: space_pair_measure) 

510 
ultimately show ?case 

511 
by (simp cong: positive_integral_cong) 

512 
qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add 

513 
positive_integral_monotone_convergence_SUP 

514 
measurable_compose_Pair1 positive_integral_positive 

515 
borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def 

516 
cong: positive_integral_cong) 

40859  517 

518 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

47694  519 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

520 
shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
40859  521 
(is "?C f \<in> borel_measurable M1") 
47694  522 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" 
49800  523 
using f 
524 
borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"] 

525 
positive_integral_fst[of "\<lambda>x. max 0 (f x)"] 

526 
unfolding positive_integral_max_0 by auto 

40859  527 

47694  528 
lemma (in pair_sigma_finite) positive_integral_snd_measurable: 
529 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 

530 
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" 

41661  531 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

532 
interpret Q: pair_sigma_finite M2 M1 by default 
47694  533 
note measurable_pair_swap[OF f] 
40859  534 
from Q.positive_integral_fst_measurable[OF this] 
47694  535 
have "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^isub>M M1))" 
40859  536 
by simp 
47694  537 
also have "(\<integral>\<^isup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" 
538 
by (subst distr_pair_swap) 

539 
(auto simp: positive_integral_distr[OF measurable_pair_swap' f] intro!: positive_integral_cong) 

40859  540 
finally show ?thesis . 
541 
qed 

542 

543 
lemma (in pair_sigma_finite) Fubini: 

47694  544 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

545 
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1)" 
40859  546 
unfolding positive_integral_snd_measurable[OF assms] 
547 
unfolding positive_integral_fst_measurable[OF assms] .. 

548 

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

549 
lemma (in pair_sigma_finite) integrable_product_swap: 
47694  550 
assumes "integrable (M1 \<Otimes>\<^isub>M M2) f" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

551 
shows "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x))" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

552 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

553 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  554 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
555 
show ?thesis unfolding * 

47694  556 
by (rule integrable_distr[OF measurable_pair_swap']) 
557 
(simp add: distr_pair_swap[symmetric] assms) 

41661  558 
qed 
559 

560 
lemma (in pair_sigma_finite) integrable_product_swap_iff: 

47694  561 
"integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^isub>M M2) f" 
41661  562 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

563 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  564 
from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f] 
565 
show ?thesis by auto 

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

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

567 

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

568 
lemma (in pair_sigma_finite) integral_product_swap: 
47694  569 
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 
570 
shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>L (M1 \<Otimes>\<^isub>M M2) f" 

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

571 
proof  
41661  572 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
47694  573 
show ?thesis unfolding * 
574 
by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric]) 

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

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

576 

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

577 
lemma (in pair_sigma_finite) integrable_fst_measurable: 
47694  578 
assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f" 
579 
shows "AE x in M1. integrable M2 (\<lambda> y. f (x, y))" (is "?AE") 

580 
and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L (M1 \<Otimes>\<^isub>M M2) f" (is "?INT") 

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

581 
proof  
47694  582 
have f_borel: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 
583 
using f by auto 

46731  584 
let ?pf = "\<lambda>x. ereal (f x)" and ?nf = "\<lambda>x. ereal ( f x)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

585 
have 
47694  586 
borel: "?nf \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)""?pf \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" and 
587 
int: "integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) ?nf \<noteq> \<infinity>" "integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) ?pf \<noteq> \<infinity>" 

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

588 
using assms by auto 
43920  589 
have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>" 
590 
"(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>" 

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

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

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

593 
with borel[THEN positive_integral_fst_measurable(1)] 
43920  594 
have AE_pos: "AE x in M1. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<noteq> \<infinity>" 
595 
"AE x in M1. (\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2) \<noteq> \<infinity>" 

47694  596 
by (auto intro!: positive_integral_PInf_AE ) 
43920  597 
then have AE: "AE x in M1. \<bar>\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 
598 
"AE x in M1. \<bar>\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 

47694  599 
by (auto simp: positive_integral_positive) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

600 
from AE_pos show ?AE using assms 
47694  601 
by (simp add: measurable_Pair2[OF f_borel] integrable_def) 
43920  602 
{ fix f have "(\<integral>\<^isup>+ x.  \<integral>\<^isup>+ y. ereal (f x y) \<partial>M2 \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
47694  603 
using positive_integral_positive 
604 
by (intro positive_integral_cong_pos) (auto simp: ereal_uminus_le_reorder) 

43920  605 
then have "(\<integral>\<^isup>+ x.  \<integral>\<^isup>+ y. ereal (f x y) \<partial>M2 \<partial>M1) = 0" by simp } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

606 
note this[simp] 
47694  607 
{ fix f assume borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 
608 
and int: "integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. ereal (f x)) \<noteq> \<infinity>" 

609 
and AE: "AE x in M1. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<noteq> \<infinity>" 

43920  610 
have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2))" (is "integrable M1 ?f") 
41705  611 
proof (intro integrable_def[THEN iffD2] conjI) 
612 
show "?f \<in> borel_measurable M1" 

47694  613 
using borel by (auto intro!: positive_integral_fst_measurable) 
43920  614 
have "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<partial>M1)" 
47694  615 
using AE positive_integral_positive[of M2] 
616 
by (auto intro!: positive_integral_cong_AE simp: ereal_real) 

43920  617 
then show "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) \<noteq> \<infinity>" 
41705  618 
using positive_integral_fst_measurable[OF borel] int by simp 
43920  619 
have "(\<integral>\<^isup>+x. ereal ( ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
47694  620 
by (intro positive_integral_cong_pos) 
621 
(simp add: positive_integral_positive real_of_ereal_pos) 

43920  622 
then show "(\<integral>\<^isup>+x. ereal ( ?f x) \<partial>M1) \<noteq> \<infinity>" by simp 
41705  623 
qed } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

624 
with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)] 
41705  625 
show ?INT 
47694  626 
unfolding lebesgue_integral_def[of "M1 \<Otimes>\<^isub>M M2"] lebesgue_integral_def[of M2] 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

627 
borel[THEN positive_integral_fst_measurable(2), symmetric] 
47694  628 
using AE[THEN integral_real] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

631 

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

632 
lemma (in pair_sigma_finite) integrable_snd_measurable: 
47694  633 
assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f" 
634 
shows "AE y in M2. integrable M1 (\<lambda>x. f (x, y))" (is "?AE") 

635 
and "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>L (M1 \<Otimes>\<^isub>M M2) f" (is "?INT") 

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

636 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

637 
interpret Q: pair_sigma_finite M2 M1 by default 
47694  638 
have Q_int: "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x, y). f (y, x))" 
41661  639 
using f unfolding integrable_product_swap_iff . 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

641 
using Q.integrable_fst_measurable(2)[OF Q_int] 
47694  642 
using integral_product_swap[of f] f by auto 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

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

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

647 

47694  648 
lemma (in pair_sigma_finite) positive_integral_fst_measurable': 
649 
assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 

650 
shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1" 

651 
using positive_integral_fst_measurable(1)[OF f] by simp 

652 

653 
lemma (in pair_sigma_finite) integral_fst_measurable: 

654 
"(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M2) \<in> borel_measurable M1" 

655 
by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable') 

656 

657 
lemma (in pair_sigma_finite) positive_integral_snd_measurable': 

658 
assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 

659 
shows "(\<lambda>y. \<integral>\<^isup>+ x. f x y \<partial>M1) \<in> borel_measurable M2" 

660 
proof  

661 
interpret Q: pair_sigma_finite M2 M1 .. 

662 
show ?thesis 

663 
using measurable_pair_swap[OF f] 

664 
by (intro Q.positive_integral_fst_measurable') (simp add: split_beta') 

665 
qed 

666 

667 
lemma (in pair_sigma_finite) integral_snd_measurable: 

668 
"(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>y. \<integral> x. f x y \<partial>M1) \<in> borel_measurable M2" 

669 
by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable') 

670 

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

671 
lemma (in pair_sigma_finite) Fubini_integral: 
47694  672 
assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

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

676 

47694  677 
section {* Products on counting spaces, densities and distributions *} 
40859  678 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

679 
lemma sigma_sets_pair_measure_generator_finite: 
38656  680 
assumes "finite A" and "finite B" 
47694  681 
shows "sigma_sets (A \<times> B) { a \<times> b  a b. a \<subseteq> A \<and> b \<subseteq> B} = Pow (A \<times> B)" 
40859  682 
(is "sigma_sets ?prod ?sets = _") 
38656  683 
proof safe 
684 
have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product) 

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

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

40859  687 
from this subset show "x \<in> sigma_sets ?prod ?sets" 
38656  688 
proof (induct x) 
689 
case empty show ?case by (rule sigma_sets.Empty) 

690 
next 

691 
case (insert a x) 

47694  692 
hence "{a} \<in> sigma_sets ?prod ?sets" by auto 
38656  693 
moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto 
694 
ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) 

695 
qed 

696 
next 

697 
fix x a b 

40859  698 
assume "x \<in> sigma_sets ?prod ?sets" and "(a, b) \<in> x" 
38656  699 
from sigma_sets_into_sp[OF _ this(1)] this(2) 
40859  700 
show "a \<in> A" and "b \<in> B" by auto 
35833  701 
qed 
702 

47694  703 
lemma pair_measure_count_space: 
704 
assumes A: "finite A" and B: "finite B" 

705 
shows "count_space A \<Otimes>\<^isub>M count_space B = count_space (A \<times> B)" (is "?P = ?C") 

706 
proof (rule measure_eqI) 

707 
interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact 

708 
interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact 

709 
interpret P: pair_sigma_finite "count_space A" "count_space B" by default 

710 
show eq: "sets ?P = sets ?C" 

711 
by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B) 

712 
fix X assume X: "X \<in> sets ?P" 

713 
with eq have X_subset: "X \<subseteq> A \<times> B" by simp 

714 
with A B have fin_Pair: "\<And>x. finite (Pair x ` X)" 

715 
by (intro finite_subset[OF _ B]) auto 

716 
have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B) 

717 
show "emeasure ?P X = emeasure ?C X" 

49776  718 
apply (subst B.emeasure_pair_measure_alt[OF X]) 
47694  719 
apply (subst emeasure_count_space) 
720 
using X_subset apply auto [] 

721 
apply (simp add: fin_Pair emeasure_count_space X_subset fin_X) 

722 
apply (subst positive_integral_count_space) 

723 
using A apply simp 

724 
apply (simp del: real_of_nat_setsum add: real_of_nat_setsum[symmetric]) 

725 
apply (subst card_gt_0_iff) 

726 
apply (simp add: fin_Pair) 

727 
apply (subst card_SigmaI[symmetric]) 

728 
using A apply simp 

729 
using fin_Pair apply simp 

730 
using X_subset apply (auto intro!: arg_cong[where f=card]) 

731 
done 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
44890
diff
changeset

732 
qed 
35833  733 

47694  734 
lemma pair_measure_density: 
735 
assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x" 

736 
assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x" 

737 
assumes "sigma_finite_measure M1" "sigma_finite_measure M2" 

738 
assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)" 

739 
shows "density M1 f \<Otimes>\<^isub>M density M2 g = density (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R") 

740 
proof (rule measure_eqI) 

741 
interpret M1: sigma_finite_measure M1 by fact 

742 
interpret M2: sigma_finite_measure M2 by fact 

743 
interpret D1: sigma_finite_measure "density M1 f" by fact 

744 
interpret D2: sigma_finite_measure "density M2 g" by fact 

745 
interpret L: pair_sigma_finite "density M1 f" "density M2 g" .. 

746 
interpret R: pair_sigma_finite M1 M2 .. 

747 

748 
fix A assume A: "A \<in> sets ?L" 

749 
then have indicator_eq: "\<And>x y. indicator A (x, y) = indicator (Pair x ` A) y" 

750 
and Pair_A: "\<And>x. Pair x ` A \<in> sets M2" 

751 
by (auto simp: indicator_def sets_Pair1) 

752 
have f_fst: "(\<lambda>p. f (fst p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 

753 
using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def) 

754 
have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" 

755 
using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def) 

756 
have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1" 

757 
using g_snd Pair_A A by (intro R.positive_integral_fst_measurable) auto 

758 
then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1" 

759 
by simp 

38656  760 

47694  761 
show "emeasure ?L A = emeasure ?R A" 
49776  762 
apply (subst D2.emeasure_pair_measure[OF A]) 
47694  763 
apply (subst emeasure_density) 
764 
using f_fst g_snd apply (simp add: split_beta') 

765 
using A apply simp 

766 
apply (subst positive_integral_density[OF g]) 

767 
apply (simp add: indicator_eq Pair_A) 

768 
apply (subst positive_integral_density[OF f]) 

769 
apply (rule int_g) 

770 
apply (subst R.positive_integral_fst_measurable(2)[symmetric]) 

771 
using f g A Pair_A f_fst g_snd 

772 
apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1 

773 
simp: positive_integral_cmult indicator_eq split_beta') 

774 
apply (intro AE_I2 impI) 

775 
apply (subst mult_assoc) 

776 
apply (subst positive_integral_cmult) 

777 
apply auto 

778 
done 

779 
qed simp 

780 

781 
lemma sigma_finite_measure_distr: 

782 
assumes "sigma_finite_measure (distr M N f)" and f: "f \<in> measurable M N" 

783 
shows "sigma_finite_measure M" 

40859  784 
proof  
47694  785 
interpret sigma_finite_measure "distr M N f" by fact 
786 
from sigma_finite_disjoint guess A . note A = this 

787 
show ?thesis 

788 
proof (unfold_locales, intro conjI exI allI) 

789 
show "range (\<lambda>i. f ` A i \<inter> space M) \<subseteq> sets M" 

790 
using A f by (auto intro!: measurable_sets) 

791 
show "(\<Union>i. f ` A i \<inter> space M) = space M" 

792 
using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def) 

793 
fix i show "emeasure M (f ` A i \<inter> space M) \<noteq> \<infinity>" 

794 
using f A(1,2) A(3)[of i] by (simp add: emeasure_distr subset_eq) 

795 
qed 

38656  796 
qed 
797 

47694  798 
lemma measurable_cong': 
799 
assumes sets: "sets M = sets M'" "sets N = sets N'" 

800 
shows "measurable M N = measurable M' N'" 

801 
using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def) 

38656  802 

47694  803 
lemma pair_measure_distr: 
804 
assumes f: "f \<in> measurable M S" and g: "g \<in> measurable N T" 

805 
assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)" 

806 
shows "distr M S f \<Otimes>\<^isub>M distr N T g = distr (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). (f x, g y))" (is "?P = ?D") 

807 
proof (rule measure_eqI) 

808 
show "sets ?P = sets ?D" 

809 
by simp 

810 
interpret S: sigma_finite_measure "distr M S f" by fact 

811 
interpret T: sigma_finite_measure "distr N T g" by fact 

812 
interpret ST: pair_sigma_finite "distr M S f" "distr N T g" .. 

813 
interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+ 

814 
interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+ 

815 
interpret MN: pair_sigma_finite M N .. 

816 
interpret SN: pair_sigma_finite "distr M S f" N .. 

817 
have [simp]: 

818 
"\<And>f g. fst \<circ> (\<lambda>(x, y). (f x, g y)) = f \<circ> fst" "\<And>f g. snd \<circ> (\<lambda>(x, y). (f x, g y)) = g \<circ> snd" 

819 
by auto 

820 
then have fg: "(\<lambda>(x, y). (f x, g y)) \<in> measurable (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T)" 

821 
using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g] 

822 
by (auto simp: measurable_pair_iff) 

823 
fix A assume A: "A \<in> sets ?P" 

824 
then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x ` A) \<partial>distr M S f)" 

49776  825 
by (rule T.emeasure_pair_measure_alt) 
47694  826 
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g ` (Pair x ` A) \<inter> space N) \<partial>distr M S f)" 
827 
using g A by (simp add: sets_Pair1 emeasure_distr) 

828 
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g ` (Pair (f x) ` A) \<inter> space N) \<partial>M)" 

829 
using f g A ST.measurable_emeasure_Pair1[OF A] 

830 
by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr) 

831 
also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x ` ((\<lambda>(x, y). (f x, g y)) ` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)" 

832 
by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure) 

833 
also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) ` A \<inter> space (M \<Otimes>\<^isub>M N))" 

49776  834 
using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A]) 
47694  835 
(auto cong: measurable_cong') 
836 
also have "\<dots> = emeasure ?D A" 

837 
using fg A by (subst emeasure_distr) auto 

838 
finally show "emeasure ?P A = emeasure ?D A" . 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
44890
diff
changeset

839 
qed 
39097  840 

40859  841 
end 