author  hoelzl 
Wed, 02 Feb 2011 12:34:45 +0100  
changeset 41689  3e39b0e730d6 
parent 41661  baf1964bc468 
child 41705  1100512e16d8 
permissions  rwrr 
35833  1 
theory Product_Measure 
38656  2 
imports Lebesgue_Integration 
35833  3 
begin 
4 

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

5 
lemma measurable_cancel_measure2[simp]: 
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

6 
"measurable M1 (M2\<lparr>measure := m\<rparr>) = measurable M1 M2" 
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

7 
unfolding measurable_def by auto 
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

8 

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

9 
lemma measurable_cancel_measure1[simp]: 
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

10 
"measurable (M1\<lparr>measure := m\<rparr>) M2 = measurable M1 M2" 
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

11 
unfolding measurable_def by auto 
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

12 

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

13 
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" 
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

14 
proof 
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

15 
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" 
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

16 
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros) 
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

17 
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

18 

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

21 

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

23 
by auto 

24 

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

26 
by auto 

27 

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

29 
by (cases x) simp 

30 

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

31 
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

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

33 

40859  34 
abbreviation 
35 
"Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A" 

39094  36 

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

37 
syntax 
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

38 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10) 
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 

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 
syntax (xsymbols) 
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

41 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 
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

42 

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

43 
syntax (HTML output) 
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

44 
"_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10) 
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

45 

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

46 
translations 
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

47 
"PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)" 
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

48 

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

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

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

53 

54 
notation (xsymbols) 

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

56 

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

58 
by safe (auto simp add: extensional_def fun_eq_iff) 

59 

60 
lemma extensional_insert[intro, simp]: 

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

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

63 
using assms unfolding extensional_def by auto 

64 

65 
lemma extensional_Int[simp]: 

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

67 
unfolding extensional_def by auto 

38656  68 

35833  69 
definition 
40859  70 
"merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)" 
71 

72 
lemma merge_apply[simp]: 

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

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

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

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

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

78 
unfolding merge_def by auto 

79 

80 
lemma merge_commute: 

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

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

83 

84 
lemma Pi_cancel_merge_range[simp]: 

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

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

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

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

89 
by (auto simp: Pi_def) 

90 

91 
lemma Pi_cancel_merge[simp]: 

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

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

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

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

96 
by (auto simp: Pi_def) 

97 

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

99 
by (auto simp: extensional_def) 

100 

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

102 
by (auto simp: restrict_def Pi_def) 

103 

104 
lemma restrict_merge[simp]: 

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

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

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

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

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

110 

111 
lemma extensional_insert_undefined[intro, simp]: 

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

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

114 
using assms unfolding extensional_def by auto 

115 

116 
lemma extensional_insert_cancel[intro, simp]: 

117 
assumes "a \<in> extensional I" 

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

119 
using assms unfolding extensional_def by auto 

120 

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

123 

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

125 
by auto 

126 

40859  127 
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)" 
128 
by auto 

129 

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

131 
by (auto simp: Pi_def) 

132 

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

134 
by (auto simp: Pi_def) 

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

135 

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

138 

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

140 
by (auto simp: Pi_def) 

141 

41095  142 
lemma restrict_vimage: 
143 
assumes "I \<inter> J = {}" 

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

145 
using assms by (auto simp: restrict_Pi_cancel) 

146 

147 
lemma merge_vimage: 

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

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

150 
using assms by (auto simp: restrict_Pi_cancel) 

151 

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

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

154 

155 
lemma merge_restrict[simp]: 

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

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

158 
unfolding merge_def by (auto intro!: ext) 

159 

160 
lemma merge_x_x_eq_restrict[simp]: 

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

162 
unfolding merge_def by (auto intro!: ext) 

163 

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

165 
apply auto 

166 
apply (drule_tac x=x in Pi_mem) 

167 
apply (simp_all split: split_if_asm) 

168 
apply (drule_tac x=i in Pi_mem) 

169 
apply (auto dest!: Pi_mem) 

170 
done 

171 

172 
lemma Pi_UN: 

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

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

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

176 
proof (intro set_eqI iffI) 

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

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

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

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

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

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

183 
proof (intro Pi_I) 

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

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

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

187 
qed 

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

189 
qed auto 

190 

191 
lemma PiE_cong: 

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

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

194 
using assms by (auto intro!: Pi_cong) 

195 

196 
lemma restrict_upd[simp]: 

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

198 
by (auto simp: fun_eq_iff) 

199 

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

200 
lemma Pi_eq_subset: 
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

201 
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" 
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

202 
assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I" 
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

203 
shows "F i \<subseteq> F' i" 
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

204 
proof 
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

205 
fix x assume "x \<in> F i" 
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

206 
with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto 
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

207 
from choice[OF this] guess f .. note f = this 
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

208 
then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def) 
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

209 
then have "f \<in> Pi\<^isub>E I F'" using assms by simp 
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

210 
then show "x \<in> F' i" using f `i \<in> I` by auto 
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

211 
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

212 

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

213 
lemma Pi_eq_iff_not_empty: 
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

214 
assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}" 
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

215 
shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)" 
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

216 
proof (intro iffI ballI) 
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

217 
fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I" 
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

218 
show "F i = F' i" 
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

219 
using Pi_eq_subset[of I F F', OF ne eq i] 
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

220 
using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i] 
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

221 
by auto 
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

222 
qed auto 
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

223 

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

224 
lemma Pi_eq_empty_iff: 
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

225 
"Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})" 
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

226 
proof 
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

227 
assume "Pi\<^isub>E I F = {}" 
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

228 
show "\<exists>i\<in>I. F i = {}" 
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

229 
proof (rule ccontr) 
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

230 
assume "\<not> ?thesis" 
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

231 
then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto 
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

232 
from choice[OF this] guess f .. 
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

233 
then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def) 
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

234 
with `Pi\<^isub>E I F = {}` show False by auto 
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

235 
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

236 
qed auto 
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

237 

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

238 
lemma Pi_eq_iff: 
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

239 
"Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))" 
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

240 
proof (intro iffI disjCI) 
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

241 
assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'" 
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

242 
assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))" 
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

243 
then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})" 
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

244 
using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto 
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

245 
with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto 
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

246 
next 
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

247 
assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})" 
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

248 
then show "Pi\<^isub>E I F = Pi\<^isub>E I F'" 
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

249 
using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto 
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

250 
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

251 

40859  252 
section "Binary products" 
253 

254 
definition 

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

255 
"pair_measure_generator A B = 
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

256 
\<lparr> space = space A \<times> space B, 
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

257 
sets = {a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B}, 
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

258 
measure = \<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A \<rparr>" 
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

259 

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

260 
definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where 
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

261 
"A \<Otimes>\<^isub>M B = sigma (pair_measure_generator A B)" 
40859  262 

263 
locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra 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

264 
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
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

265 

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

266 
abbreviation (in pair_sigma_algebra) 
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

267 
"E \<equiv> pair_measure_generator M1 M2" 
40859  268 

269 
abbreviation (in pair_sigma_algebra) 

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

270 
"P \<equiv> M1 \<Otimes>\<^isub>M M2" 
40859  271 

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

272 
lemma sigma_algebra_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

273 
"sets M1 \<subseteq> Pow (space M1) \<Longrightarrow> sets M2 \<subseteq> Pow (space M2) \<Longrightarrow> sigma_algebra (pair_measure M1 M2)" 
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

274 
by (force simp: pair_measure_def pair_measure_generator_def intro!: sigma_algebra_sigma) 
40859  275 

276 
sublocale pair_sigma_algebra \<subseteq> sigma_algebra P 

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

277 
using M1.space_closed M2.space_closed 
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

278 
by (rule sigma_algebra_pair_measure) 
40859  279 

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

280 
lemma pair_measure_generatorI[intro, simp]: 
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

281 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (pair_measure_generator A B)" 
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

282 
by (auto simp add: pair_measure_generator_def) 
40859  283 

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

284 
lemma pair_measureI[intro, simp]: 
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

285 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)" 
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

286 
by (auto simp add: pair_measure_def) 
40859  287 

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

288 
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

289 
"space (A \<Otimes>\<^isub>M B) = space A \<times> space B" 
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

290 
by (simp add: pair_measure_def pair_measure_generator_def) 
41095  291 

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

292 
lemma sets_pair_measure_generator: 
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

293 
"sets (pair_measure_generator N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)" 
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

294 
unfolding pair_measure_generator_def by auto 
41095  295 

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

296 
lemma pair_measure_generator_sets_into_space: 
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

297 
assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)" 
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

298 
shows "sets (pair_measure_generator M N) \<subseteq> Pow (space (pair_measure_generator M N))" 
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

299 
using assms by (auto simp: pair_measure_generator_def) 
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

300 

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

301 
lemma pair_measure_generator_Int_snd: 
40859  302 
assumes "sets S1 \<subseteq> Pow (space S1)" 
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

303 
shows "sets (pair_measure_generator S1 (algebra.restricted_space S2 A)) = 
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

304 
sets (algebra.restricted_space (pair_measure_generator S1 S2) (space S1 \<times> A))" 
40859  305 
(is "?L = ?R") 
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

306 
apply (auto simp: pair_measure_generator_def image_iff) 
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

307 
using assms 
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

308 
apply (rule_tac x="a \<times> xa" in exI) 
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

309 
apply force 
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

310 
using assms 
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

311 
apply (rule_tac x="a" in exI) 
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

312 
apply (rule_tac x="b \<inter> A" in exI) 
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

313 
apply auto 
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

314 
done 
40859  315 

316 
lemma (in pair_sigma_algebra) 

317 
shows measurable_fst[intro!, simp]: 

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

319 
and measurable_snd[intro!, simp]: 

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

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

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

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

323 
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

324 
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

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

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

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

328 
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

329 
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

330 
using M2.sets_into_space by force+ } 
40859  331 
ultimately have "?fst \<and> ?snd" 
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

332 
by (fastsimp simp: measurable_def sets_sigma space_pair_measure 
40859  333 
intro!: sigma_sets.Basic) 
334 
then show ?fst ?snd by auto 

335 
qed 

336 

41095  337 
lemma (in pair_sigma_algebra) measurable_pair_iff: 
40859  338 
assumes "sigma_algebra M" 
339 
shows "f \<in> measurable M P \<longleftrightarrow> 

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

341 
proof  

342 
interpret M: sigma_algebra M by fact 

343 
from assms show ?thesis 

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

345 
assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable 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

346 
show "f \<in> measurable M P" unfolding pair_measure_def 
40859  347 
proof (rule M.measurable_sigma) 
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

348 
show "sets (pair_measure_generator M1 M2) \<subseteq> Pow (space E)" 
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

349 
unfolding pair_measure_generator_def using M1.sets_into_space M2.sets_into_space by auto 
40859  350 
show "f \<in> space M \<rightarrow> space E" 
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

351 
using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma pair_measure_generator_def) 
40859  352 
fix A assume "A \<in> sets E" 
353 
then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C" 

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

354 
unfolding pair_measure_generator_def by auto 
40859  355 
moreover have "(fst \<circ> f) ` B \<inter> space M \<in> sets M" 
356 
using f `B \<in> sets M1` unfolding measurable_def by auto 

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

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

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

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

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

362 
qed 

363 
qed 

364 
qed 

365 

41095  366 
lemma (in pair_sigma_algebra) measurable_pair: 
40859  367 
assumes "sigma_algebra M" 
41095  368 
assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" 
40859  369 
shows "f \<in> measurable M P" 
41095  370 
unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp 
40859  371 

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

372 
lemma pair_measure_generatorE: 
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

373 
assumes "X \<in> sets (pair_measure_generator M1 M2)" 
40859  374 
obtains A B where "X = A \<times> B" "A \<in> sets M1" "B \<in> sets 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

375 
using assms unfolding pair_measure_generator_def by auto 
40859  376 

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

377 
lemma (in pair_sigma_algebra) pair_measure_generator_swap: 
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

378 
"(\<lambda>X. (\<lambda>(x,y). (y,x)) ` X \<inter> space M2 \<times> space M1) ` sets E = sets (pair_measure_generator M2 M1)" 
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

379 
proof (safe elim!: pair_measure_generatorE) 
40859  380 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 
381 
moreover then have "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 = B \<times> A" 

382 
using M1.sets_into_space M2.sets_into_space by auto 

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

383 
ultimately show "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 \<in> sets (pair_measure_generator M2 M1)" 
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

384 
by (auto intro: pair_measure_generatorI) 
40859  385 
next 
386 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 

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

388 
using M1.sets_into_space M2.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

389 
by (auto intro!: image_eqI[where x="A \<times> B"] pair_measure_generatorI) 
40859  390 
qed 
391 

392 
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap: 

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

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

394 
shows "(\<lambda>(x,y). (y, x)) ` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q") 
40859  395 
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

396 
let "?f Q" = "(\<lambda>(x,y). (y, x)) ` Q \<inter> space M2 \<times> space M1" 
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

397 
have *: "(\<lambda>(x,y). (y, x)) ` Q = ?f Q" 
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

398 
using sets_into_space[OF Q] by (auto simp: 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

399 
have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))" 
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

400 
unfolding pair_measure_def .. 
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

401 
also have "\<dots> = sigma_sets (space M2 \<times> space M1) (?f ` sets E)" 
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

402 
unfolding sigma_def pair_measure_generator_swap[symmetric] 
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

403 
by (simp add: pair_measure_generator_def) 
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

404 
also have "\<dots> = ?f ` sigma_sets (space M1 \<times> space M2) (sets E)" 
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

405 
using M1.sets_into_space M2.sets_into_space 
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

406 
by (intro sigma_sets_vimage) (auto simp: pair_measure_generator_def) 
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

407 
also have "\<dots> = ?f ` sets P" 
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

408 
unfolding pair_measure_def pair_measure_generator_def sigma_def by simp 
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

409 
finally show ?thesis 
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

410 
using Q by (subst *) auto 
40859  411 
qed 
412 

413 
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable: 

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

414 
shows "(\<lambda>(x,y). (y, x)) \<in> measurable P (M2 \<Otimes>\<^isub>M M1)" 
40859  415 
(is "?f \<in> measurable ?P ?Q") 
416 
unfolding measurable_def 

417 
proof (intro CollectI conjI Pi_I ballI) 

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

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

419 
unfolding pair_measure_generator_def pair_measure_def by auto 
40859  420 
next 
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

421 
fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
40859  422 
interpret Q: pair_sigma_algebra M2 M1 by default 
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

423 
with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`] 
40859  424 
show "?f ` A \<inter> space ?P \<in> sets ?P" by simp 
425 
qed 

426 

427 
lemma (in pair_sigma_algebra) measurable_cut_fst: 

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

429 
proof  

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

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

432 
interpret Q: sigma_algebra ?Q 

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

433 
proof qed (auto simp: vimage_UN vimage_Diff space_pair_measure) 
40859  434 
have "sets E \<subseteq> sets ?Q" 
435 
using M1.sets_into_space M2.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

436 
by (auto simp: pair_measure_generator_def space_pair_measure) 
40859  437 
then have "sets P \<subseteq> sets ?Q" 
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

438 
apply (subst pair_measure_def, intro Q.sets_sigma_subset) 
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

439 
by (simp add: pair_measure_def) 
40859  440 
with assms show ?thesis by auto 
441 
qed 

442 

443 
lemma (in pair_sigma_algebra) measurable_cut_snd: 

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

445 
proof  

446 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

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

448 
show ?thesis by (simp add: vimage_compose[symmetric] comp_def) 
40859  449 
qed 
450 

451 
lemma (in pair_sigma_algebra) measurable_pair_image_snd: 

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

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

454 
unfolding measurable_def 

455 
proof (intro CollectI conjI Pi_I ballI) 

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

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

457 
show "f (x, y) \<in> space M" 
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

458 
unfolding measurable_def pair_measure_generator_def pair_measure_def by auto 
40859  459 
next 
460 
fix A assume "A \<in> sets M" 

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

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

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

464 
also have "?C = (\<lambda>y. f (x, y)) ` A \<inter> space 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

465 
using `x \<in> space M1` by (auto simp: pair_measure_generator_def pair_measure_def) 
40859  466 
finally show "(\<lambda>y. f (x, y)) ` A \<inter> space M2 \<in> sets M2" . 
467 
qed 

468 

469 
lemma (in pair_sigma_algebra) measurable_pair_image_fst: 

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

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

472 
proof  

473 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

475 
OF Q.pair_sigma_algebra_swap_measurable m] 

476 
show ?thesis by simp 

477 
qed 

478 

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

479 
lemma (in pair_sigma_algebra) Int_stable_pair_measure_generator: "Int_stable E" 
40859  480 
unfolding Int_stable_def 
481 
proof (intro ballI) 

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

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

484 
"A1 \<in> sets M1" "A2 \<in> sets M2" "B1 \<in> sets M1" "B2 \<in> sets 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

485 
unfolding pair_measure_generator_def by auto 
40859  486 
then show "A \<inter> B \<in> sets E" 
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

487 
by (auto simp add: times_Int_times pair_measure_generator_def) 
40859  488 
qed 
489 

490 
lemma finite_measure_cut_measurable: 

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

491 
fixes M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
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

492 
assumes "sigma_finite_measure M1" "finite_measure M2" 
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

493 
assumes "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" 
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

494 
shows "(\<lambda>x. measure M2 (Pair x ` Q)) \<in> borel_measurable M1" 
40859  495 
(is "?s Q \<in> _") 
496 
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

497 
interpret M1: sigma_finite_measure M1 by fact 
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

498 
interpret M2: finite_measure M2 by fact 
40859  499 
interpret pair_sigma_algebra M1 M2 by default 
500 
have [intro]: "sigma_algebra M1" by fact 

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

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

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

503 
note space_pair_measure[simp] 
40859  504 
interpret dynkin_system ?D 
505 
proof (intro dynkin_systemI) 

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

507 
using sets_into_space by simp 

508 
next 

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

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

511 
next 

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

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

513 
with sets_into_space have "\<And>x. measure M2 (Pair x ` (space M1 \<times> space M2  A)) = 
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

514 
(if x \<in> space M1 then measure M2 (space M2)  ?s A x else 0)" 
40859  515 
by (auto intro!: M2.finite_measure_compl measurable_cut_fst 
516 
simp: vimage_Diff) 

517 
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

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

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

521 
moreover then have "\<And>x. measure M2 (\<Union>i. Pair x ` F i) = (\<Sum>\<^isub>\<infinity> i. ?s (F i) x)" 
40859  522 
by (intro M2.measure_countably_additive[symmetric]) 
523 
(auto intro!: measurable_cut_fst simp: disjoint_family_on_def) 

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

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

526 
qed 

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

527 
have "sets P = sets ?D" apply (subst pair_measure_def) 
40859  528 
proof (intro dynkin_lemma) 
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

529 
show "Int_stable E" by (rule Int_stable_pair_measure_generator) 
40859  530 
from M1.sets_into_space have "\<And>A. A \<in> sets M1 \<Longrightarrow> {x \<in> space M1. x \<in> A} = A" 
531 
by auto 

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

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

533 
by (auto simp: pair_measure_generator_def sets_sigma if_distrib 
40859  534 
intro: sigma_sets.Basic intro!: M1.measurable_If) 
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

535 
qed (auto simp: pair_measure_def) 
40859  536 
with `Q \<in> sets P` have "Q \<in> sets ?D" by simp 
537 
then show "?s Q \<in> borel_measurable M1" by simp 

538 
qed 

539 

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

541 

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

542 
locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 
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

543 
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
40859  544 

545 
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 

546 
by default 

547 

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

548 
lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))" 
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

549 
by auto 
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

550 

40859  551 
lemma (in pair_sigma_finite) measure_cut_measurable_fst: 
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

552 
assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x ` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") 
40859  553 
proof  
554 
have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+ 

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

555 
have M1: "sigma_finite_measure M1" by default 
40859  556 
from M2.disjoint_sigma_finite guess F .. note F = this 
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

557 
then have "\<And>i. F i \<in> sets M2" by auto 
40859  558 
let "?C x i" = "F i \<inter> Pair x ` Q" 
559 
{ fix i 

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

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

562 
using F M2.sets_into_space by auto 

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 
let ?R2 = "M2.restricted_space (F i)" 
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

564 
have "(\<lambda>x. measure ?R2 (Pair x ` (space M1 \<times> space ?R2 \<inter> Q))) \<in> borel_measurable M1" 
40859  565 
proof (intro finite_measure_cut_measurable[OF M1]) 
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

566 
show "finite_measure ?R2" 
40859  567 
using F by (intro M2.restricted_to_finite_measure) auto 
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

568 
have "(space M1 \<times> space ?R2) \<inter> Q \<in> (op \<inter> (space M1 \<times> F i)) ` sets P" 
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

569 
using `Q \<in> sets P` by (auto simp: image_iff) 
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

570 
also have "\<dots> = sigma_sets (space M1 \<times> F i) ((op \<inter> (space M1 \<times> F i)) ` sets E)" 
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

571 
unfolding pair_measure_def pair_measure_generator_def sigma_def 
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

572 
using `F i \<in> sets M2` M2.sets_into_space 
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

573 
by (auto intro!: sigma_sets_Int sigma_sets.Basic) 
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

574 
also have "\<dots> \<subseteq> sets (M1 \<Otimes>\<^isub>M ?R2)" 
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

575 
using M1.sets_into_space 
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

576 
apply (auto simp: times_Int_times pair_measure_def pair_measure_generator_def sigma_def 
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

577 
intro!: sigma_sets_subseteq) 
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

578 
apply (rule_tac x="a" in exI) 
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

579 
apply (rule_tac x="b \<inter> F i" in exI) 
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

580 
by auto 
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

581 
finally show "(space M1 \<times> space ?R2) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R2)" . 
40859  582 
qed 
583 
moreover have "\<And>x. Pair x ` (space M1 \<times> F i \<inter> Q) = ?C x i" 

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

584 
using `Q \<in> sets P` sets_into_space by (auto simp: 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

585 
ultimately have "(\<lambda>x. measure M2 (?C x i)) \<in> borel_measurable M1" 
40859  586 
by simp } 
587 
moreover 

588 
{ fix x 

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

589 
have "(\<Sum>\<^isub>\<infinity>i. measure M2 (?C x i)) = measure M2 (\<Union>i. ?C x i)" 
40859  590 
proof (intro M2.measure_countably_additive) 
591 
show "range (?C x) \<subseteq> sets M2" 

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

593 
have "disjoint_family F" using F by auto 

594 
show "disjoint_family (?C x)" 

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

596 
qed 

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

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

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

599 
by (auto simp: 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

600 
finally have "measure M2 (Pair x ` Q) = (\<Sum>\<^isub>\<infinity>i. measure M2 (?C x i))" 
40859  601 
by simp } 
602 
ultimately show ?thesis 

603 
by (auto intro!: M1.borel_measurable_psuminf) 

604 
qed 

605 

606 
lemma (in pair_sigma_finite) measure_cut_measurable_snd: 

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

607 
assumes "Q \<in> sets P" shows "(\<lambda>y. M1.\<mu> ((\<lambda>x. (x, y)) ` Q)) \<in> borel_measurable M2" 
40859  608 
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

609 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  610 
note sets_pair_sigma_algebra_swap[OF assms] 
611 
from Q.measure_cut_measurable_fst[OF this] 

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

612 
show ?thesis by (simp add: vimage_compose[symmetric] comp_def) 
40859  613 
qed 
614 

615 
lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable: 

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

616 
assumes "f \<in> measurable P M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M" 
40859  617 
proof  
618 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

620 
show ?thesis 

621 
using Q.pair_sigma_algebra_swap_measurable assms 

622 
unfolding * by (rule measurable_comp) 

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

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

624 

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

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

627 
shows "measure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+ x. measure M2 (Pair x ` A) \<partial>M1)" 
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

628 
apply (simp add: pair_measure_def pair_measure_generator_def) 
40859  629 
proof (rule M1.positive_integral_cong) 
630 
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

631 
have *: "\<And>y. indicator A (x, y) = (indicator (Pair x ` A) y :: pextreal)" 
40859  632 
unfolding indicator_def by auto 
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

633 
show "(\<integral>\<^isup>+ y. indicator A (x, y) \<partial>M2) = measure M2 (Pair x ` A)" 
40859  634 
unfolding * 
635 
apply (subst M2.positive_integral_indicator) 

636 
apply (rule measurable_cut_fst[OF assms]) 

637 
by simp 

638 
qed 

639 

640 
lemma (in pair_sigma_finite) pair_measure_times: 

641 
assumes A: "A \<in> sets M1" and "B \<in> sets 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

642 
shows "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = M1.\<mu> A * measure M2 B" 
40859  643 
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

644 
have "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = (\<integral>\<^isup>+ x. measure M2 B * indicator A x \<partial>M1)" 
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

645 
using assms by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt) 
40859  646 
with assms show ?thesis 
647 
by (simp add: M1.positive_integral_cmult_indicator ac_simps) 

648 
qed 

649 

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

650 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: 
40859  651 
"\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> F \<up> space E \<and> 
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

652 
(\<forall>i. measure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<omega>)" 
40859  653 
proof  
654 
obtain F1 :: "nat \<Rightarrow> 'a set" and F2 :: "nat \<Rightarrow> 'b set" where 

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

655 
F1: "range F1 \<subseteq> sets M1" "F1 \<up> space M1" "\<And>i. M1.\<mu> (F1 i) \<noteq> \<omega>" and 
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

656 
F2: "range F2 \<subseteq> sets M2" "F2 \<up> space M2" "\<And>i. M2.\<mu> (F2 i) \<noteq> \<omega>" 
40859  657 
using M1.sigma_finite_up M2.sigma_finite_up by auto 
658 
then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" 

659 
unfolding isoton_def by auto 

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

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

661 
show ?thesis unfolding isoton_def space_pair_measure 
40859  662 
proof (intro exI[of _ ?F] conjI allI) 
663 
show "range ?F \<subseteq> sets E" using F1 F2 

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

664 
by (fastsimp intro!: pair_measure_generatorI) 
40859  665 
next 
666 
have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)" 

667 
proof (intro subsetI) 

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

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

670 
by (auto simp: space) 

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

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

673 
by (auto simp: max_def dest: isoton_mono_le) 

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

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

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

677 
qed 

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

678 
then show "(\<Union>i. ?F i) = space E" 
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 
using space by (auto simp: space pair_measure_generator_def) 
40859  680 
next 
681 
fix i show "F1 i \<times> F2 i \<subseteq> F1 (Suc i) \<times> F2 (Suc i)" 

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

683 
by auto 

684 
next 

685 
fix i 

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

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

687 
with F1 F2 show "measure P (F1 i \<times> F2 i) \<noteq> \<omega>" 
40859  688 
by (simp add: pair_measure_times) 
689 
qed 

690 
qed 

691 

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

692 
sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P 
40859  693 
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

694 
show "measure P {} = 0" 
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

695 
unfolding pair_measure_def pair_measure_generator_def sigma_def by auto 
40859  696 

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

697 
show "countably_additive P (measure P)" 
40859  698 
unfolding countably_additive_def 
699 
proof (intro allI impI) 

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

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

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

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

703 
moreover from F have "\<And>i. (\<lambda>x. measure M2 (Pair x ` F i)) \<in> borel_measurable M1" 
40859  704 
by (intro measure_cut_measurable_fst) auto 
705 
moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x ` F i)" 

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

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

708 
using F by (auto intro!: measurable_cut_fst) 

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

709 
ultimately show "(\<Sum>\<^isub>\<infinity>n. measure P (F n)) = measure P (\<Union>i. F i)" 
40859  710 
by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric] 
711 
M2.measure_countably_additive 

712 
cong: M1.positive_integral_cong) 

713 
qed 

714 

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

715 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
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

716 
show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets P \<and> (\<Union>i. F i) = space P \<and> (\<forall>i. measure P (F i) \<noteq> \<omega>)" 
40859  717 
proof (rule exI[of _ F], intro conjI) 
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

718 
show "range F \<subseteq> sets P" using F by (auto simp: pair_measure_def) 
40859  719 
show "(\<Union>i. F i) = space P" 
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

720 
using F by (auto simp: pair_measure_def pair_measure_generator_def isoton_def) 
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

721 
show "\<forall>i. measure P (F i) \<noteq> \<omega>" using F by auto 
40859  722 
qed 
723 
qed 

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

724 

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

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

727 
shows "(\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
41661  728 
(is "_ ` A \<inter> space ?Q \<in> sets ?Q") 
729 
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

730 
have *: "(\<lambda>(x, y). (y, x)) ` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A" 
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

731 
using `A \<in> sets P` sets_into_space by (auto simp: space_pair_measure) 
41661  732 
show ?thesis 
733 
unfolding * using assms by (rule sets_pair_sigma_algebra_swap) 

734 
qed 

735 

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

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

738 
shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) ` A) \<partial>M2)" 
40859  739 
(is "_ = ?\<nu> A") 
740 
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

741 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
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

742 
have [simp]: "\<And>m. \<lparr> space = space E, sets = sets (sigma E), measure = m \<rparr> = P\<lparr> measure := m \<rparr>" 
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

743 
unfolding pair_measure_def by simp 
40859  744 
show ?thesis 
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

745 
proof (rule measure_unique_Int_stable[where \<nu>="?\<nu>", OF Int_stable_pair_measure_generator], simp_all) 
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

746 
show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. \<mu> (F i) \<noteq> \<omega>" "A \<in> sets (sigma E)" 
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

747 
using F `A \<in> sets P` by (auto simp: pair_measure_def) 
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

748 
show "measure_space P" by default 
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

749 
interpret Q: pair_sigma_finite M2 M1 by default 
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

750 
have P: "sigma_algebra (P\<lparr> measure := ?\<nu>\<rparr>)" 
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

751 
by (intro sigma_algebra_cong) auto 
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

752 
show "measure_space (P\<lparr> measure := ?\<nu>\<rparr>)" 
41661  753 
apply (rule Q.measure_space_vimage[OF P]) 
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

754 
apply (simp_all) 
41661  755 
apply (rule Q.pair_sigma_algebra_swap_measurable) 
756 
proof  

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

758 
from sets_swap[OF this] 

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

759 
show "(\<integral>\<^isup>+ y. M1.\<mu> ((\<lambda>x. (x, y)) ` A) \<partial>M2) = Q.\<mu> ((\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1))" 
41661  760 
using sets_into_space[OF `A \<in> sets P`] 
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

761 
by (auto simp add: Q.pair_measure_alt 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

762 
intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"]) 
41661  763 
qed 
40859  764 
fix X assume "X \<in> sets E" 
765 
then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets 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

766 
unfolding pair_measure_def pair_measure_generator_def by auto 
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

767 
show "\<mu> X = ?\<nu> X" 
40859  768 
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

769 
from AB have "?\<nu> (A \<times> B) = (\<integral>\<^isup>+y. M1.\<mu> A * indicator B y \<partial>M2)" 
40859  770 
by (auto intro!: M2.positive_integral_cong) 
771 
with AB show ?thesis 

772 
unfolding pair_measure_times[OF AB] X 

773 
by (simp add: M2.positive_integral_cmult_indicator ac_simps) 

774 
qed 

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

775 
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

776 
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

777 

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

778 

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

779 
lemma pair_sigma_algebra_sigma: 
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

780 
assumes 1: "S1 \<up> (space E1)" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)" 
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

781 
assumes 2: "S2 \<up> (space E2)" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)" 
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

782 
shows "sets (sigma (pair_measure_generator (sigma E1) (sigma E2))) = sets (sigma (pair_measure_generator E1 E2))" 
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

783 
(is "sets ?S = sets ?E") 
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

784 
proof  
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

785 
interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma) 
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

786 
interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma) 
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

787 
have P: "sets (pair_measure_generator E1 E2) \<subseteq> Pow (space E1 \<times> space E2)" 
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

788 
using E1 E2 by (auto simp add: pair_measure_generator_def) 
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

789 
interpret E: sigma_algebra ?E unfolding pair_measure_generator_def 
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

790 
using E1 E2 by (intro sigma_algebra_sigma) auto 
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

791 
{ fix A assume "A \<in> sets E1" 
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

792 
then have "fst ` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)" 
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

793 
using E1 2 unfolding isoton_def pair_measure_generator_def by auto 
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

794 
also have "\<dots> = (\<Union>i. A \<times> S2 i)" by auto 
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

795 
also have "\<dots> \<in> sets ?E" unfolding pair_measure_generator_def sets_sigma 
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

796 
using 2 `A \<in> sets E1` 
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

797 
by (intro sigma_sets.Union) 
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

798 
(auto simp: image_subset_iff intro!: sigma_sets.Basic) 
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

799 
finally have "fst ` A \<inter> space ?E \<in> sets ?E" . } 
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

800 
moreover 
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

801 
{ fix B assume "B \<in> sets E2" 
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

802 
then have "snd ` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B" 
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

803 
using E2 1 unfolding isoton_def pair_measure_generator_def by auto 
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

804 
also have "\<dots> = (\<Union>i. S1 i \<times> B)" by auto 
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

805 
also have "\<dots> \<in> sets ?E" 
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

806 
using 1 `B \<in> sets E2` unfolding pair_measure_generator_def sets_sigma 
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

807 
by (intro sigma_sets.Union) 
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

808 
(auto simp: image_subset_iff intro!: sigma_sets.Basic) 
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

809 
finally have "snd ` B \<inter> space ?E \<in> sets ?E" . } 
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

810 
ultimately have proj: 
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

811 
"fst \<in> measurable ?E (sigma E1) \<and> snd \<in> measurable ?E (sigma E2)" 
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

812 
using E1 E2 by (subst (1 2) E.measurable_iff_sigma) 
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

813 
(auto simp: pair_measure_generator_def sets_sigma) 
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

814 
{ fix A B assume A: "A \<in> sets (sigma E1)" and B: "B \<in> sets (sigma E2)" 
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

815 
with proj have "fst ` A \<inter> space ?E \<in> sets ?E" "snd ` B \<inter> space ?E \<in> sets ?E" 
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

816 
unfolding measurable_def by simp_all 
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

817 
moreover have "A \<times> B = (fst ` A \<inter> space ?E) \<inter> (snd ` B \<inter> space ?E)" 
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

818 
using A B M1.sets_into_space M2.sets_into_space 
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

819 
by (auto simp: pair_measure_generator_def) 
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

820 
ultimately have "A \<times> B \<in> sets ?E" by auto } 
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

821 
then have "sigma_sets (space ?E) (sets (pair_measure_generator (sigma E1) (sigma E2))) \<subseteq> sets ?E" 
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

822 
by (intro E.sigma_sets_subset) (auto simp add: pair_measure_generator_def sets_sigma) 
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

823 
then have subset: "sets ?S \<subseteq> sets ?E" 
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

824 
by (simp add: sets_sigma pair_measure_generator_def) 
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

825 
show "sets ?S = sets ?E" 
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

826 
proof (intro set_eqI iffI) 
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

827 
fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S" 
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

828 
unfolding sets_sigma 
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

829 
proof induct 
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

830 
case (Basic A) then show ?case 
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

831 
by (auto simp: pair_measure_generator_def sets_sigma intro: sigma_sets.Basic) 
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

832 
qed (auto intro: sigma_sets.intros simp: pair_measure_generator_def) 
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

833 
next 
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

834 
fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto 
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

835 
qed 
40859  836 
qed 
837 

838 
section "Fubinis theorem" 

839 

840 
lemma (in pair_sigma_finite) simple_function_cut: 

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

841 
assumes f: "simple_function P f" 
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

842 
shows "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
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

843 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  844 
proof  
845 
have f_borel: "f \<in> borel_measurable P" 

846 
using f by (rule borel_measurable_simple_function) 

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

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

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

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

851 
by (auto simp: indicator_def) 

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

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

853 
by (simp add: space_pair_measure) 
40859  854 
moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel 
855 
by (intro borel_measurable_vimage measurable_cut_fst) 

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

856 
ultimately have "simple_function M2 (\<lambda> y. f (x, y))" 
40859  857 
apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _]) 
858 
apply (rule simple_function_indicator_representation[OF f]) 

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

860 
note M2_sf = this 

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

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

862 
then have "(\<integral>\<^isup>+y. f (x, y) \<partial>M2) = (\<Sum>z\<in>f ` space P. z * M2.\<mu> (?F' x z))" 
40859  863 
unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]] 
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

864 
unfolding simple_integral_def 
40859  865 
proof (safe intro!: setsum_mono_zero_cong_left) 
866 
from f show "finite (f ` space P)" by (rule simple_functionD) 

867 
next 

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

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

869 
using `x \<in> space M1` by (auto simp: space_pair_measure) 
40859  870 
next 
871 
fix x' y assume "(x', y) \<in> space P" 

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

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

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

874 
by (force simp: 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

875 
show "f (x', y) * M2.\<mu> (?F' x (f (x', y))) = 0" 
40859  876 
unfolding * by simp 
877 
qed (simp add: vimage_compose[symmetric] comp_def 

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

878 
space_pair_measure) } 
40859  879 
note eq = this 
880 
moreover have "\<And>z. ?F z \<in> sets P" 

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

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

882 
moreover then have "\<And>z. (\<lambda>x. M2.\<mu> (?F' x z)) \<in> borel_measurable M1" 
40859  883 
by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int) 
884 
ultimately 

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

885 
show "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
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

886 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  887 
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

888 
intro!: M1.borel_measurable_pextreal_setsum 
40859  889 
simp add: M1.positive_integral_setsum simple_integral_def 
890 
M1.positive_integral_cmult 

891 
M1.positive_integral_cong[OF eq] 

892 
positive_integral_eq_simple_integral[OF f] 

893 
pair_measure_alt[symmetric]) 

894 
qed 

895 

896 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

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

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

898 
shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
40859  899 
(is "?C f \<in> borel_measurable M1") 
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

900 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  901 
proof  
902 
from borel_measurable_implies_simple_function_sequence[OF 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

903 
obtain F where F: "\<And>i. simple_function P (F i)" "F \<up> f" by auto 
40859  904 
then have F_borel: "\<And>i. F i \<in> borel_measurable P" 
905 
and F_mono: "\<And>i x. F i x \<le> F (Suc i) x" 

906 
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

907 
unfolding isoton_fun_expand unfolding isoton_def le_fun_def 
40859  908 
by (auto intro: borel_measurable_simple_function) 
909 
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

910 
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

911 
using F(1) by auto 
40859  912 
moreover 
913 
{ fix x assume "x \<in> space M1" 

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

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

916 
by (auto simp: isoton_def) 

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

918 
from M2.positive_integral_isoton[OF isotone this] 

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

920 
by (simp add: isoton_def) } 

921 
note SUPR_C = this 

922 
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

923 
by (simp cong: measurable_cong) 
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

924 
have "(\<integral>\<^isup>+x. (SUP i. F i x) \<partial>P) = (SUP i. integral\<^isup>P P (F i))" 
40859  925 
using F_borel F_mono 
926 
by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric]) 

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

927 
also have "(SUP i. integral\<^isup>P P (F i)) = (SUP i. \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1)" 
40859  928 
unfolding sf(2) by simp 
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

929 
also have "\<dots> = \<integral>\<^isup>+ x. (SUP i. \<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1" 
40859  930 
by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)] 
931 
M2.positive_integral_mono F_mono) 

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

932 
also have "\<dots> = \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. (SUP i. F i (x, y)) \<partial>M2) \<partial>M1" 
40859  933 
using F_borel F_mono 
934 
by (auto intro!: M2.positive_integral_monotone_convergence_SUP 

935 
M1.positive_integral_cong measurable_pair_image_snd) 

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

936 
finally show "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  937 
unfolding F_SUPR by simp 
938 
qed 

939 

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

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

942 
shows "(\<integral>\<^isup>+x. f (case x of (x,y)\<Rightarrow>(y,x)) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P P f" 
41661  943 
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

944 
interpret Q: pair_sigma_finite M2 M1 by default 
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

945 
have "sigma_algebra P" by default 
41661  946 
show ?thesis 
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

947 
proof (intro Q.positive_integral_vimage[symmetric] Q.pair_sigma_algebra_swap_measurable) 
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

948 
fix A assume "A \<in> sets P" 
41661  949 
from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this] 
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

950 
show "\<mu> A = Q.\<mu> ((\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1))" 
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

951 
by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"] 
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

952 
simp: pair_measure_alt Q.pair_measure_alt2 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

953 
qed fact+ 
41661  954 
qed 
955 

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

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

958 
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P P f" 
40859  959 
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

960 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  961 
note pair_sigma_algebra_measurable[OF f] 
962 
from Q.positive_integral_fst_measurable[OF this] 

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

963 
have "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P)" 
40859  964 
by simp 
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

965 
also have "(\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P) = integral\<^isup>P P f" 
41661  966 
unfolding positive_integral_product_swap[OF f, symmetric] 
967 
by (auto intro!: Q.positive_integral_cong) 

40859  968 
finally show ?thesis . 
969 
qed 

970 

971 
lemma (in pair_sigma_finite) Fubini: 

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

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

973 
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  974 
unfolding positive_integral_snd_measurable[OF assms] 
975 
unfolding positive_integral_fst_measurable[OF assms] .. 

976 

977 
lemma (in pair_sigma_finite) AE_pair: 

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

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

980 
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

981 
obtain N where N: "N \<in> sets P" "\<mu> N = 0" "{x\<in>space P. \<not> Q x} \<subseteq> N" 
40859  982 
using assms unfolding almost_everywhere_def by auto 
983 
show ?thesis 

984 
proof (rule M1.AE_I) 

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

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

986 
show "M1.\<mu> {x\<in>space M1. M2.\<mu> (Pair x ` N) \<noteq> 0} = 0" 
40859  987 
by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def) 
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

988 
show "{x \<in> space M1. M2.\<mu> (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

989 
by (intro M1.borel_measurable_pextreal_neq_const measure_cut_measurable_fst N) 
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

990 
{ fix x assume "x \<in> space M1" "M2.\<mu> (Pair x ` N) = 0" 
40859  991 
have "M2.almost_everywhere (\<lambda>y. Q (x, y))" 
992 
proof (rule M2.AE_I) 

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

993 
show "M2.\<mu> (Pair x ` N) = 0" by fact 
40859  994 
show "Pair x ` N \<in> sets M2" by (intro measurable_cut_fst N) 
995 
show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x ` N" 

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

996 
using N `x \<in> space M1` unfolding space_sigma space_pair_measure by auto 
40859  997 
qed } 
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

998 
then show "{x \<in> space M1. \<not> M2.almost_everywhere (\<lambda>y. Q (x, y))} \<subseteq> {x \<in> space M1. M2.\<mu> (Pair x ` N) \<noteq> 0}" 
40859  999 
by auto 
39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

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

1001 
qed 
35833  1002 

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

1003 
lemma (in pair_sigma_algebra) measurable_product_swap: 
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

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

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

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

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

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

1009 
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

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

1011 

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

1012 
lemma (in pair_sigma_finite) integrable_product_swap: 
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

1013 
assumes "integrable P f" 
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

1014 
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

1015 
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

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

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

1019 
using assms unfolding integrable_def 
41661  1020 
apply (subst (1 2) positive_integral_product_swap) 
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

1021 
using `integrable P f` unfolding integrable_def 
41661  1022 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 
1023 
qed 

1024 

1025 
lemma (in pair_sigma_finite) integrable_product_swap_iff: 

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

1026 
"integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable P f" 
41661  1027 
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

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

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

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

1032 

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

1033 
lemma (in pair_sigma_finite) integral_product_swap: 
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

1034 
assumes "integrable P f" 
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

1035 
shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>L P f" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1036 
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

1037 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  1038 
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

1039 
show ?thesis 
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

1040 
unfolding lebesgue_integral_def * 
41661  1041 
apply (subst (1 2) positive_integral_product_swap) 
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

1042 
using `integrable P f` unfolding integrable_def 
41661  1043 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

1045 

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

1046 
lemma (in pair_sigma_finite) integrable_fst_measurable: 
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

1047 
assumes f: "integrable P f" 
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

1048 
shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE") 
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

1049 
and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT") 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

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

1053 
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and 
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

1054 
int: "integral\<^isup>P P ?nf \<noteq> \<omega>" "integral\<^isup>P P ?pf \<noteq> \<omega>" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1055 
using assms by auto 
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

1056 
have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<omega>" 
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

1057 
"(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real ( f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<omega>" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

1060 
with borel[THEN positive_integral_fst_measurable(1)] 
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

1061 
have AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)" 
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

1062 
"M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real ( f (x, y)) \<partial>M2) \<noteq> \<omega>)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

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

1066 
apply (rule M1.AE_cong) 
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

1067 
using assms unfolding integrable_def 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1068 
by (auto intro!: measurable_pair_image_snd) 
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

1069 
have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f") 
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

1070 
proof (intro integrable_def[THEN iffD2] conjI) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

1072 
using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable) 
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

1073 
have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

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

1077 
by (auto simp: Real_real) 
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

1078 
then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1079 
using positive_integral_fst_measurable[OF borel(2)] int by simp 
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

1080 
have "(\<integral>\<^isup>+x. Real ( ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1081 
by (intro M1.positive_integral_cong) simp 
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

1082 
then show "(\<integral>\<^isup>+x. Real ( ?f x) \<partial>M1) \<noteq> \<omega>" by simp 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1083 
qed 
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

1084 
moreover have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+ y. Real ( f (x, y)) \<partial>M2))" 
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

1085 
(is "integrable M1 ?f") 
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

1086 
proof (intro integrable_def[THEN iffD2] conjI) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

1088 
using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable) 
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

1089 
have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real ( f (x, y)) \<partial>M2) \<partial>M1)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

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

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

1093 
by (auto simp: Real_real) 
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

1094 
then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1095 
using positive_integral_fst_measurable[OF borel(1)] int by simp 
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

1096 
have "(\<integral>\<^isup>+x. Real ( ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1097 
by (intro M1.positive_integral_cong) simp 
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

1098 
then show "(\<integral>\<^isup>+x. Real ( ?f x) \<partial>M1) \<noteq> \<omega>" by simp 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

1100 
ultimately show ?INT 
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

1101 
unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2] 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

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

1103 
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

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

1105 

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

1106 
lemma (in pair_sigma_finite) integrable_snd_measurable: 
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

1107 
assumes f: "integrable P f" 
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

1108 
shows "M2.almost_everywhere (\<lambda>y. integrable M1 (\<lambda>x. f (x, y)))" (is "?AE") 
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

1109 
and "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>L P f" (is "?INT") 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

1110 
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

1111 
interpret Q: pair_sigma_finite M2 M1 by default 
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

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

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

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

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

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

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

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

1121 

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

1122 
lemma (in pair_sigma_finite) Fubini_integral: 
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

1123 
assumes f: "integrable P f" 
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

1124 
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

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

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

1127 

40859  1128 
section "Finite product spaces" 
1129 

1130 
section "Products" 

1131 

1132 
locale product_sigma_algebra = 

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

1133 
fixes M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" 
40859  1134 
assumes sigma_algebras: "\<And>i. sigma_algebra (M i)" 
1135 

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

1136 
locale finite_product_sigma_algebra = product_sigma_algebra M 
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

1137 
for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" + 
40859  1138 
fixes I :: "'i set" 
1139 
assumes finite_index: "finite I" 

1140 

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

1141 
definition 
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

1142 
"product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)), 
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

1143 
sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)), 
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

1144 
measure = \<lambda>A. (\<Prod>i\<in>I. measure (M i) ((SOME F. A = Pi\<^isub>E I F) i)) \<rparr>" 
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

1145 

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

1146 
definition product_algebra_def: 
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

1147 
"Pi\<^isub>M I M = sigma (product_algebra_generator I M) 
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

1148 
\<lparr> measure := (SOME \<mu>. sigma_finite_measure (sigma (product_algebra_generator I M) \<lparr> measure := \<mu> \<rparr>) \<and> 
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

1149 
(\<forall>A\<in>\<Pi> i\<in>I. sets (M i). \<mu> (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))))\<rparr>" 
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

1150 

40859  1151 
syntax 
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
