author  hoelzl 
Tue, 22 Mar 2011 20:06:10 +0100  
changeset 42067  66c8281349ec 
parent 41981  cdf7693bbe08 
permissions  rwrr 
42067  1 
(* Title: HOL/Probability/Product_Measure.thy 
2 
Author: Johannes Hölzl, TU München 

3 
*) 

4 

5 
header {*Product measure spaces*} 

6 

35833  7 
theory Product_Measure 
38656  8 
imports Lebesgue_Integration 
35833  9 
begin 
10 

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

11 
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

12 
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

13 
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

14 
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

15 
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

16 

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

19 

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

21 
by auto 

22 

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

24 
by auto 

25 

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

27 
by (cases x) simp 

28 

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

29 
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

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

31 

40859  32 
abbreviation 
33 
"Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A" 

39094  34 

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

35 
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

36 
"_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

37 

3e39b0e730d6
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 
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

39 
"_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

40 

3e39b0e730d6
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 
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

42 
"_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

43 

3e39b0e730d6
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 
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

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

46 

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

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

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

51 

52 
notation (xsymbols) 

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

54 

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

56 
by safe (auto simp add: extensional_def fun_eq_iff) 

57 

58 
lemma extensional_insert[intro, simp]: 

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

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

61 
using assms unfolding extensional_def by auto 

62 

63 
lemma extensional_Int[simp]: 

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

65 
unfolding extensional_def by auto 

38656  66 

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

70 
lemma merge_apply[simp]: 

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

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

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

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

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

76 
unfolding merge_def by auto 

77 

78 
lemma merge_commute: 

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

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

81 

82 
lemma Pi_cancel_merge_range[simp]: 

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

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

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

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

87 
by (auto simp: Pi_def) 

88 

89 
lemma Pi_cancel_merge[simp]: 

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

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

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

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

94 
by (auto simp: Pi_def) 

95 

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

97 
by (auto simp: extensional_def) 

98 

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

100 
by (auto simp: restrict_def Pi_def) 

101 

102 
lemma restrict_merge[simp]: 

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

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

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

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

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

108 

109 
lemma extensional_insert_undefined[intro, simp]: 

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

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

112 
using assms unfolding extensional_def by auto 

113 

114 
lemma extensional_insert_cancel[intro, simp]: 

115 
assumes "a \<in> extensional I" 

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

117 
using assms unfolding extensional_def by auto 

118 

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

121 

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

123 
by auto 

124 

40859  125 
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)" 
126 
by auto 

127 

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

129 
by (auto simp: Pi_def) 

130 

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

132 
by (auto simp: Pi_def) 

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

133 

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

136 

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

138 
by (auto simp: Pi_def) 

139 

41095  140 
lemma restrict_vimage: 
141 
assumes "I \<inter> J = {}" 

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

143 
using assms by (auto simp: restrict_Pi_cancel) 

144 

145 
lemma merge_vimage: 

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

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

148 
using assms by (auto simp: restrict_Pi_cancel) 

149 

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

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

152 

153 
lemma merge_restrict[simp]: 

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

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

156 
unfolding merge_def by (auto intro!: ext) 

157 

158 
lemma merge_x_x_eq_restrict[simp]: 

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

160 
unfolding merge_def by (auto intro!: ext) 

161 

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

163 
apply auto 

164 
apply (drule_tac x=x in Pi_mem) 

165 
apply (simp_all split: split_if_asm) 

166 
apply (drule_tac x=i in Pi_mem) 

167 
apply (auto dest!: Pi_mem) 

168 
done 

169 

170 
lemma Pi_UN: 

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

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

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

174 
proof (intro set_eqI iffI) 

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

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

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

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

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

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

181 
proof (intro Pi_I) 

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

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

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

185 
qed 

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

187 
qed auto 

188 

189 
lemma PiE_cong: 

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

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

192 
using assms by (auto intro!: Pi_cong) 

193 

194 
lemma restrict_upd[simp]: 

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

196 
by (auto simp: fun_eq_iff) 

197 

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

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
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

209 
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

210 

3e39b0e730d6
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 
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

212 
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

213 
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

214 
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

215 
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

216 
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

217 
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

218 
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

219 
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

220 
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

221 

3e39b0e730d6
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 
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

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

224 
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

225 
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

226 
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

227 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 

3e39b0e730d6
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 
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

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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
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

244 
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

245 
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

246 
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

247 
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

248 
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

249 

40859  250 
section "Binary products" 
251 

252 
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

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

254 
\<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

255 
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

256 
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

257 

3e39b0e730d6
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 
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

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

261 
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

262 
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

263 

3e39b0e730d6
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 
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

265 
"E \<equiv> pair_measure_generator M1 M2" 
40859  266 

267 
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

268 
"P \<equiv> M1 \<Otimes>\<^isub>M M2" 
40859  269 

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

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

272 
by (force simp: pair_measure_def pair_measure_generator_def intro!: sigma_algebra_sigma) 
40859  273 

274 
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

275 
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

276 
by (rule sigma_algebra_pair_measure) 
40859  277 

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

278 
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

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

280 
by (auto simp add: pair_measure_generator_def) 
40859  281 

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

282 
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

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

284 
by (auto simp add: pair_measure_def) 
40859  285 

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

286 
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

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

288 
by (simp add: pair_measure_def pair_measure_generator_def) 
41095  289 

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

290 
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

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

292 
unfolding pair_measure_generator_def by auto 
41095  293 

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

294 
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

295 
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

296 
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

297 
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

298 

3e39b0e730d6
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 
lemma pair_measure_generator_Int_snd: 
40859  300 
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

301 
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

302 
sets (algebra.restricted_space (pair_measure_generator S1 S2) (space S1 \<times> A))" 
40859  303 
(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

304 
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

305 
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

306 
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

307 
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

308 
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

309 
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

310 
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

311 
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

312 
done 
40859  313 

314 
lemma (in pair_sigma_algebra) 

315 
shows measurable_fst[intro!, simp]: 

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

317 
and measurable_snd[intro!, simp]: 

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

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

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

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

321 
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

322 
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

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

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

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

326 
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

327 
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

328 
using M2.sets_into_space by force+ } 
40859  329 
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

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

333 
qed 

334 

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

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

339 
proof  

340 
interpret M: sigma_algebra M by fact 

341 
from assms show ?thesis 

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

343 
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

344 
show "f \<in> measurable M P" unfolding pair_measure_def 
40859  345 
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

346 
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

347 
unfolding pair_measure_generator_def using M1.sets_into_space M2.sets_into_space by auto 
40859  348 
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

349 
using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma pair_measure_generator_def) 
40859  350 
fix A assume "A \<in> sets E" 
351 
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

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

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

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

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

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

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

360 
qed 

361 
qed 

362 
qed 

363 

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

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

370 
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

371 
assumes "X \<in> sets (pair_measure_generator M1 M2)" 
40859  372 
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

373 
using assms unfolding pair_measure_generator_def by auto 
40859  374 

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

376 
"(\<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

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

380 
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

381 
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

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

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

386 
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

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

390 
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap: 

391 
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

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

394 
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

395 
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

396 
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

397 
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

398 
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

399 
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

400 
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

401 
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

402 
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

403 
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

404 
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

405 
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

406 
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

407 
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

408 
using Q by (subst *) auto 
40859  409 
qed 
410 

411 
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

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

415 
proof (intro CollectI conjI Pi_I ballI) 

416 
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

417 
unfolding pair_measure_generator_def pair_measure_def by auto 
40859  418 
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

419 
fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
40859  420 
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

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

424 

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

425 
lemma (in pair_sigma_algebra) measurable_cut_fst[simp,intro]: 
40859  426 
assumes "Q \<in> sets P" shows "Pair x ` Q \<in> sets M2" 
427 
proof  

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

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

430 
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

431 
proof qed (auto simp: vimage_UN vimage_Diff space_pair_measure) 
40859  432 
have "sets E \<subseteq> sets ?Q" 
433 
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

434 
by (auto simp: pair_measure_generator_def space_pair_measure) 
40859  435 
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

436 
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

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

440 

441 
lemma (in pair_sigma_algebra) measurable_cut_snd: 

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

443 
proof  

444 
interpret Q: pair_sigma_algebra M2 M1 by default 

445 
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

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

449 
lemma (in pair_sigma_algebra) measurable_pair_image_snd: 

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

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

452 
unfolding measurable_def 

453 
proof (intro CollectI conjI Pi_I ballI) 

454 
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

455 
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

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

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

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

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

462 
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

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

466 

467 
lemma (in pair_sigma_algebra) measurable_pair_image_fst: 

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

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

470 
proof  

471 
interpret Q: pair_sigma_algebra M2 M1 by default 

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

473 
OF Q.pair_sigma_algebra_swap_measurable m] 

474 
show ?thesis by simp 

475 
qed 

476 

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

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

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

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

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

483 
unfolding pair_measure_generator_def by auto 
40859  484 
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

485 
by (auto simp add: times_Int_times pair_measure_generator_def) 
40859  486 
qed 
487 

488 
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

489 
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

490 
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

491 
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

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

495 
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

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

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

500 
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

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

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

505 
using sets_into_space by simp 

506 
next 

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

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

509 
next 

510 
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

511 
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

512 
(if x \<in> space M1 then measure M2 (space M2)  ?s A x else 0)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

513 
by (auto intro!: M2.measure_compl simp: vimage_Diff) 
40859  514 
with `A \<in> sets ?D` top show "space ?D  A \<in> sets ?D" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

518 
moreover then have "\<And>x. measure M2 (\<Union>i. Pair x ` F i) = (\<Sum>i. ?s (F i) x)" 
40859  519 
by (intro M2.measure_countably_additive[symmetric]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

520 
(auto simp: disjoint_family_on_def) 
40859  521 
ultimately show "(\<Union>i. F i) \<in> sets ?D" 
522 
by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf) 

523 
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

524 
have "sets P = sets ?D" apply (subst pair_measure_def) 
40859  525 
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

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

529 
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

530 
by (auto simp: pair_measure_generator_def sets_sigma if_distrib 
40859  531 
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

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

535 
qed 

536 

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

538 

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

539 
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

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

542 
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 

543 
by default 

544 

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

545 
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

546 
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

547 

40859  548 
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

549 
assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x ` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") 
40859  550 
proof  
551 
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

552 
have M1: "sigma_finite_measure M1" by default 
40859  553 
from M2.disjoint_sigma_finite guess F .. note F = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

554 
then have F_sets: "\<And>i. F i \<in> sets M2" by auto 
40859  555 
let "?C x i" = "F i \<inter> Pair x ` Q" 
556 
{ fix i 

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

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

559 
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

560 
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

561 
have "(\<lambda>x. measure ?R2 (Pair x ` (space M1 \<times> space ?R2 \<inter> Q))) \<in> borel_measurable M1" 
40859  562 
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

563 
show "finite_measure ?R2" 
40859  564 
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

565 
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

566 
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

567 
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

568 
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

569 
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

570 
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

571 
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

572 
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

573 
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

574 
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

575 
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

576 
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

577 
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

578 
finally show "(space M1 \<times> space ?R2) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R2)" . 
40859  579 
qed 
580 
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

581 
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

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

585 
{ fix x 

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

586 
have "(\<Sum>i. measure M2 (?C x i)) = measure M2 (\<Union>i. ?C x i)" 
40859  587 
proof (intro M2.measure_countably_additive) 
588 
show "range (?C x) \<subseteq> sets M2" 

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

589 
using F `Q \<in> sets P` by (auto intro!: M2.Int) 
40859  590 
have "disjoint_family F" using F by auto 
591 
show "disjoint_family (?C x)" 

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

593 
qed 

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

595 
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

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

597 
finally have "measure M2 (Pair x ` Q) = (\<Sum>i. measure M2 (?C x i))" 
40859  598 
by simp } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

599 
ultimately show ?thesis using `Q \<in> sets P` F_sets 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

600 
by (auto intro!: M1.borel_measurable_psuminf M2.Int) 
40859  601 
qed 
602 

603 
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

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

606 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  607 
note sets_pair_sigma_algebra_swap[OF assms] 
608 
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

609 
show ?thesis by (simp add: vimage_compose[symmetric] comp_def) 
40859  610 
qed 
611 

612 
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

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

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

617 
show ?thesis 

618 
using Q.pair_sigma_algebra_swap_measurable assms 

619 
unfolding * by (rule measurable_comp) 

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

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

621 

40859  622 
lemma (in pair_sigma_finite) pair_measure_alt: 
623 
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

624 
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

625 
apply (simp add: pair_measure_def pair_measure_generator_def) 
40859  626 
proof (rule M1.positive_integral_cong) 
627 
fix x assume "x \<in> space M1" 

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

628 
have *: "\<And>y. indicator A (x, y) = (indicator (Pair x ` A) y :: extreal)" 
40859  629 
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

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

633 
apply (rule measurable_cut_fst[OF assms]) 

634 
by simp 

635 
qed 

636 

637 
lemma (in pair_sigma_finite) pair_measure_times: 

638 
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

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

641 
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

642 
using assms by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt) 
40859  643 
with assms show ?thesis 
644 
by (simp add: M1.positive_integral_cmult_indicator ac_simps) 

645 
qed 

646 

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

647 
lemma (in measure_space) measure_not_negative[simp,intro]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

648 
assumes A: "A \<in> sets M" shows "\<mu> A \<noteq>  \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

649 
using positive_measure[OF A] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

650 

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

651 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

652 
"\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> incseq F \<and> (\<Union>i. F i) = space E \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

656 
F1: "range F1 \<subseteq> sets M1" "incseq F1" "(\<Union>i. F1 i) = space M1" "\<And>i. M1.\<mu> (F1 i) \<noteq> \<infinity>" and 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

657 
F2: "range F2 \<subseteq> sets M2" "incseq F2" "(\<Union>i. F2 i) = space M2" "\<And>i. M2.\<mu> (F2 i) \<noteq> \<infinity>" 
40859  658 
using M1.sigma_finite_up M2.sigma_finite_up by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

659 
then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto 
40859  660 
let ?F = "\<lambda>i. F1 i \<times> F2 i" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

661 
show ?thesis unfolding 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)" 

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

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

673 
by (force split: split_max)+ 
40859  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 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

682 
using `incseq F1` `incseq F2` unfolding incseq_Suc_iff by auto 
40859  683 
next 
684 
fix i 

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

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

686 
with F1 F2 M1.positive_measure[OF this(1)] M2.positive_measure[OF this(2)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

687 
show "measure P (F1 i \<times> F2 i) \<noteq> \<infinity>" 
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 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

694 
show "positive P (measure P)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

695 
unfolding pair_measure_def pair_measure_generator_def sigma_def positive_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

696 
by (auto intro: M1.positive_integral_positive M2.positive_integral_positive) 
40859  697 

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

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

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

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

703 
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

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

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

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

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

709 
using F by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

710 
ultimately show "(\<Sum>n. measure P (F n)) = measure P (\<Union>i. F i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

711 
by (simp add: pair_measure_alt vimage_UN M1.positive_integral_suminf[symmetric] 
40859  712 
M2.measure_countably_additive 
713 
cong: M1.positive_integral_cong) 

714 
qed 

715 

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

716 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

717 
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> \<infinity>)" 
40859  718 
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

719 
show "range F \<subseteq> sets P" using F by (auto simp: pair_measure_def) 
40859  720 
show "(\<Union>i. F i) = space P" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

721 
using F by (auto simp: pair_measure_def pair_measure_generator_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

725 

41661  726 
lemma (in pair_sigma_algebra) sets_swap: 
727 
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

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

731 
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

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

735 
qed 

736 

40859  737 
lemma (in pair_sigma_finite) pair_measure_alt2: 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

738 
assumes A: "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

739 
shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) ` A) \<partial>M2)" 
40859  740 
(is "_ = ?\<nu> A") 
741 
proof  

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

742 
interpret Q: pair_sigma_finite 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

743 
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

744 
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

745 
unfolding pair_measure_def by simp 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

746 

a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

747 
have "\<mu> A = Q.\<mu> ((\<lambda>(y, x). (x, y)) ` A \<inter> space Q.P)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

748 
proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator]) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

749 
show "measure_space P" "measure_space Q.P" by default 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

750 
show "(\<lambda>(y, x). (x, y)) \<in> measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

751 
show "sets (sigma E) = sets P" "space E = space P" "A \<in> sets (sigma E)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

752 
using assms unfolding pair_measure_def by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

753 
show "range F \<subseteq> sets E" "incseq F" "(\<Union>i. F i) = space E" "\<And>i. \<mu> (F i) \<noteq> \<infinity>" 
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 
using F `A \<in> sets P` by (auto simp: pair_measure_def) 
40859  755 
fix X assume "X \<in> sets E" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

756 
then obtain A B where X[simp]: "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

757 
unfolding pair_measure_def pair_measure_generator_def by auto 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

758 
then have "(\<lambda>(y, x). (x, y)) ` X \<inter> space Q.P = B \<times> A" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

759 
using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

760 
then show "\<mu> X = Q.\<mu> ((\<lambda>(y, x). (x, y)) ` X \<inter> space Q.P)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

761 
using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

762 
qed 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

763 
then show ?thesis 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

764 
using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]] 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

765 
by (auto simp add: Q.pair_measure_alt space_pair_measure 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

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

767 
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

768 

3e39b0e730d6
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 
lemma pair_sigma_algebra_sigma: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

770 
assumes 1: "incseq S1" "(\<Union>i. S1 i) = space E1" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

771 
assumes 2: "decseq S2" "(\<Union>i. S2 i) = space E2" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)" 
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

772 
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

773 
(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

774 
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

775 
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

776 
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

777 
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

778 
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

779 
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

780 
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

781 
{ 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

782 
then have "fst ` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

783 
using E1 2 unfolding pair_measure_generator_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

784 
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

785 
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

786 
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

787 
by (intro sigma_sets.Union) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

789 
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

790 
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

791 
{ 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

792 
then have "snd ` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

793 
using E2 1 unfolding pair_measure_generator_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

794 
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

795 
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

796 
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

797 
by (intro sigma_sets.Union) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

799 
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

800 
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

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

802 
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

803 
(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

804 
{ 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

805 
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

806 
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

807 
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

808 
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

809 
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

810 
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

811 
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

812 
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

813 
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

814 
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

815 
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

816 
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

817 
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

818 
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

819 
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

820 
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

821 
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

822 
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

823 
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

824 
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

825 
qed 
40859  826 
qed 
827 

828 
section "Fubinis theorem" 

829 

830 
lemma (in pair_sigma_finite) simple_function_cut: 

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

831 
assumes f: "simple_function P f" "\<And>x. 0 \<le> f 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

832 
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

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

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

836 
using f(1) by (rule borel_measurable_simple_function) 
40859  837 
let "?F z" = "f ` {z} \<inter> space P" 
838 
let "?F' x z" = "Pair x ` ?F z" 

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

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

841 
by (auto simp: indicator_def) 

842 
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

843 
by (simp add: space_pair_measure) 
40859  844 
moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel 
845 
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

846 
ultimately have "simple_function M2 (\<lambda> y. f (x, y))" 
40859  847 
apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

848 
apply (rule simple_function_indicator_representation[OF f(1)]) 
40859  849 
using `x \<in> space M1` by (auto simp del: space_sigma) } 
850 
note M2_sf = this 

851 
{ 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

852 
then have "(\<integral>\<^isup>+y. f (x, y) \<partial>M2) = (\<Sum>z\<in>f ` space P. z * M2.\<mu> (?F' x z))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

853 
unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)] 
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

854 
unfolding simple_integral_def 
40859  855 
proof (safe intro!: setsum_mono_zero_cong_left) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

856 
from f(1) show "finite (f ` space P)" by (rule simple_functionD) 
40859  857 
next 
858 
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

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

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

863 
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

864 
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

865 
show "f (x', y) * M2.\<mu> (?F' x (f (x', y))) = 0" 
40859  866 
unfolding * by simp 
867 
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

868 
space_pair_measure) } 
40859  869 
note eq = this 
870 
moreover have "\<And>z. ?F z \<in> sets P" 

871 
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

872 
moreover then have "\<And>z. (\<lambda>x. M2.\<mu> (?F' x z)) \<in> borel_measurable M1" 
40859  873 
by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

874 
moreover have *: "\<And>i x. 0 \<le> M2.\<mu> (Pair x ` (f ` {i} \<inter> space P))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

875 
using f(1)[THEN simple_functionD(2)] f(2) by (intro M2.positive_measure measurable_cut_fst) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

876 
moreover { fix i assume "i \<in> f`space P" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

877 
with * have "\<And>x. 0 \<le> i * M2.\<mu> (Pair x ` (f ` {i} \<inter> space P))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

878 
using f(2) by auto } 
40859  879 
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

880 
show "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

881 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" using f(2) 
40859  882 
by (auto simp del: vimage_Int cong: measurable_cong 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

883 
intro!: M1.borel_measurable_extreal_setsum setsum_cong 
40859  884 
simp add: M1.positive_integral_setsum simple_integral_def 
885 
M1.positive_integral_cmult 

886 
M1.positive_integral_cong[OF eq] 

887 
positive_integral_eq_simple_integral[OF f] 

888 
pair_measure_alt[symmetric]) 

889 
qed 

890 

891 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

892 
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

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

895 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  896 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

897 
from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this 
40859  898 
then have F_borel: "\<And>i. F i \<in> borel_measurable P" 
899 
by (auto intro: borel_measurable_simple_function) 

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

900 
note sf = simple_function_cut[OF F(1,5)] 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

901 
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

902 
using F(1) by auto 
40859  903 
moreover 
904 
{ fix x assume "x \<in> space M1" 

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

905 
from F measurable_pair_image_snd[OF F_borel`x \<in> space M1`] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

906 
have "(\<integral>\<^isup>+y. (SUP i. F i (x, y)) \<partial>M2) = (SUP i. ?C (F i) x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

907 
by (intro M2.positive_integral_monotone_convergence_SUP) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

908 
(auto simp: incseq_Suc_iff le_fun_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

909 
then have "(SUP i. ?C (F i) x) = ?C f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

910 
unfolding F(4) positive_integral_max_0 by simp } 
40859  911 
note SUPR_C = this 
912 
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

913 
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

914 
have "(\<integral>\<^isup>+x. (SUP i. F i x) \<partial>P) = (SUP i. integral\<^isup>P P (F i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

915 
using F_borel F 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

916 
by (intro positive_integral_monotone_convergence_SUP) 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

917 
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  918 
unfolding sf(2) by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

919 
also have "\<dots> = \<integral>\<^isup>+ x. (SUP i. \<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1" using F sf(1) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

920 
by (intro M1.positive_integral_monotone_convergence_SUP[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

921 
(auto intro!: M2.positive_integral_mono M2.positive_integral_positive 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

922 
simp: incseq_Suc_iff le_fun_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

923 
also have "\<dots> = \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. (SUP i. F i (x, y)) \<partial>M2) \<partial>M1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

924 
using F_borel F(2,5) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

925 
by (auto intro!: M1.positive_integral_cong M2.positive_integral_monotone_convergence_SUP[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

926 
simp: incseq_Suc_iff le_fun_def 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

927 
finally show "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

928 
using F by (simp add: positive_integral_max_0) 
40859  929 
qed 
930 

41831  931 
lemma (in pair_sigma_finite) measure_preserving_swap: 
932 
"(\<lambda>(x,y). (y, x)) \<in> measure_preserving (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)" 

933 
proof 

934 
interpret Q: pair_sigma_finite M2 M1 by default 

935 
show *: "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)" 

936 
using pair_sigma_algebra_swap_measurable . 

937 
fix X assume "X \<in> sets (M2 \<Otimes>\<^isub>M M1)" 

938 
from measurable_sets[OF * this] this Q.sets_into_space[OF this] 

939 
show "measure (M1 \<Otimes>\<^isub>M M2) ((\<lambda>(x, y). (y, x)) ` X \<inter> space P) = measure (M2 \<Otimes>\<^isub>M M1) X" 

940 
by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"] 

941 
simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure) 

942 
qed 

943 

41661  944 
lemma (in pair_sigma_finite) positive_integral_product_swap: 
945 
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

946 
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  947 
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

948 
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

949 
have "sigma_algebra P" by default 
41831  950 
with f show ?thesis 
951 
by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto 

41661  952 
qed 
953 

40859  954 
lemma (in pair_sigma_finite) positive_integral_snd_measurable: 
955 
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

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

958 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  959 
note pair_sigma_algebra_measurable[OF f] 
960 
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

961 
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  962 
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

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

40859  966 
finally show ?thesis . 
967 
qed 

968 

969 
lemma (in pair_sigma_finite) Fubini: 

970 
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

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

974 

975 
lemma (in pair_sigma_finite) AE_pair: 

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

976 
assumes "AE x in P. Q x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

977 
shows "AE x in M1. (AE y in M2. Q (x, y))" 
40859  978 
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

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

982 
proof (rule M1.AE_I) 

983 
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

984 
show "M1.\<mu> {x\<in>space M1. M2.\<mu> (Pair x ` N) \<noteq> 0} = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

985 
by (auto simp: pair_measure_alt M1.positive_integral_0_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

986 
show "{x \<in> space M1. M2.\<mu> (Pair x ` N) \<noteq> 0} \<in> sets M1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

987 
by (intro M1.borel_measurable_extreal_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

988 
{ fix x assume "x \<in> space M1" "M2.\<mu> (Pair x ` N) = 0" 
40859  989 
have "M2.almost_everywhere (\<lambda>y. Q (x, y))" 
990 
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

991 
show "M2.\<mu> (Pair x ` N) = 0" by fact 
40859  992 
show "Pair x ` N \<in> sets M2" by (intro measurable_cut_fst N) 
993 
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

994 
using N `x \<in> space M1` unfolding space_sigma space_pair_measure by auto 
40859  995 
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

996 
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  997 
by auto 
39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

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

999 
qed 
35833  1000 

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

1001 
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

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

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

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

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

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

1007 
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

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

1009 

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

1010 
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

1011 
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

1012 
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

1013 
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

1014 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  1015 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
1016 
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

1017 
using assms unfolding integrable_def 
41661  1018 
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

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

1022 

1023 
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

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

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

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

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

1030 

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

1031 
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

1032 
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

1033 
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

1034 
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

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

1037 
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

1038 
unfolding lebesgue_integral_def * 
41661  1039 
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

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

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

1043 

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

1044 
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

1045 
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

1046 
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

1047 
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

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

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

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

1051 
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1054 
have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

1058 
with borel[THEN positive_integral_fst_measurable(1)] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1059 
have AE_pos: "AE x in M1. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1060 
"AE x in M1. (\<integral>\<^isup>+y. extreal ( f (x, y)) \<partial>M2) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1061 
by (auto intro!: M1.positive_integral_PInf_AE ) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1062 
then have AE: "AE x in M1. \<bar>\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1063 
"AE x in M1. \<bar>\<integral>\<^isup>+y. extreal ( f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1065 
from AE_pos show ?AE using assms 
41705  1066 
by (simp add: measurable_pair_image_snd integrable_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1067 
{ fix f have "(\<integral>\<^isup>+ x.  \<integral>\<^isup>+ y. extreal (f x y) \<partial>M2 \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1068 
using M2.positive_integral_positive 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1069 
by (intro M1.positive_integral_cong_pos) (auto simp: extreal_uminus_le_reorder) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1071 
note this[simp] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1072 
{ fix f assume borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable P" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1073 
and int: "integral\<^isup>P P (\<lambda>x. extreal (f x)) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1074 
and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<noteq> \<infinity>)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1078 
using borel by (auto intro!: M1.borel_measurable_real_of_extreal positive_integral_fst_measurable) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1079 
have "(\<integral>\<^isup>+x. extreal (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. extreal (f (x, y)) \<partial>M2) \<partial>M1)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1080 
using AE M2.positive_integral_positive 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1081 
by (auto intro!: M1.positive_integral_cong_AE simp: extreal_real) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1082 
then show "(\<integral>\<^isup>+x. extreal (?f x) \<partial>M1) \<noteq> \<infinity>" 
41705  1083 
using positive_integral_fst_measurable[OF borel] int by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1084 
have "(\<integral>\<^isup>+x. extreal ( ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1085 
by (intro M1.positive_integral_cong_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1086 
(simp add: M2.positive_integral_positive real_of_extreal_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1089 
with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)] 
41705  1090 
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

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

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

1093 
using AE[THEN M1.integral_real] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1096 

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

1097 
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

1098 
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

1099 
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

1100 
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

1101 
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

1102 
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

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

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

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

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

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

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

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

1112 

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

1113 
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

1114 
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

1115 
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

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

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

1118 

40859  1119 
section "Finite product spaces" 
1120 

1121 
section "Products" 

1122 

1123 
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

1124 
fixes M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" 
40859  1125 
assumes sigma_algebras: "\<And>i. sigma_algebra (M i)" 
1126 

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

1127 
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

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

1131 

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

1132 
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

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

1134 
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

1135 
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

1136 

3e39b0e730d6
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 
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

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

1139 
\<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

1140 
(\<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

1141 

40859  1142 
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

1143 
"_PiM" :: "[pttrn, 'i set, ('a, 'b) 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

1144 
('i => 'a, 'b) measure_space_scheme" ("(3PIM _:_./ _)" 10) 
40859  1145 

1146 
syntax (xsymbols) 

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

1147 
"_PiM" :: "[pttrn, 'i set, ('a, 'b) 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

1148 
('i => 'a, 'b) measure_space_scheme" ("(3\<Pi>\<^isub>M _\<in>_./ _)" 10) 
40859  1149 

1150 
syntax (HTML output) 

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

1151 
"_PiM" :: "[pttrn, 'i set, ('a, 'b) measure_space_scheme] => 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
h 