35833
|
1 |
theory Product_Measure
|
38656
|
2 |
imports Lebesgue_Integration
|
35833
|
3 |
begin
|
|
4 |
|
39080
|
5 |
definition dynkin
|
|
6 |
where "dynkin M =
|
|
7 |
((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
|
39094
|
8 |
space M \<in> sets M \<and> (\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
|
39080
|
9 |
(\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
|
|
10 |
(\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
|
|
11 |
|
|
12 |
lemma dynkinI:
|
|
13 |
assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
|
39094
|
14 |
assumes "space M \<in> sets M" and "\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M"
|
39080
|
15 |
assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
|
|
16 |
\<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
|
|
17 |
shows "dynkin M"
|
|
18 |
using assms unfolding dynkin_def by auto
|
|
19 |
|
|
20 |
lemma dynkin_subset:
|
|
21 |
assumes "dynkin M"
|
|
22 |
shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
|
|
23 |
using assms unfolding dynkin_def by auto
|
|
24 |
|
|
25 |
lemma dynkin_space:
|
|
26 |
assumes "dynkin M"
|
|
27 |
shows "space M \<in> sets M"
|
|
28 |
using assms unfolding dynkin_def by auto
|
|
29 |
|
|
30 |
lemma dynkin_diff:
|
|
31 |
assumes "dynkin M"
|
39094
|
32 |
shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M ; a \<subseteq> b \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
|
39080
|
33 |
using assms unfolding dynkin_def by auto
|
|
34 |
|
39094
|
35 |
lemma dynkin_empty:
|
|
36 |
assumes "dynkin M"
|
|
37 |
shows "{} \<in> sets M"
|
|
38 |
using dynkin_diff[OF assms dynkin_space[OF assms] dynkin_space[OF assms]] by auto
|
|
39 |
|
39080
|
40 |
lemma dynkin_UN:
|
|
41 |
assumes "dynkin M"
|
|
42 |
assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
|
39094
|
43 |
assumes "\<And> i :: nat. a i \<in> sets M"
|
39080
|
44 |
shows "UNION UNIV a \<in> sets M"
|
|
45 |
using assms unfolding dynkin_def by auto
|
|
46 |
|
|
47 |
definition Int_stable
|
|
48 |
where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
|
|
49 |
|
|
50 |
lemma dynkin_trivial:
|
|
51 |
shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
|
|
52 |
by (rule dynkinI) auto
|
|
53 |
|
39094
|
54 |
lemma dynkin_lemma:
|
39080
|
55 |
assumes stab: "Int_stable E"
|
|
56 |
and spac: "space E = space D"
|
|
57 |
and subsED: "sets E \<subseteq> sets D"
|
|
58 |
and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)"
|
|
59 |
and dyn: "dynkin D"
|
|
60 |
shows "sigma (space E) (sets E) = D"
|
|
61 |
proof -
|
|
62 |
def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
|
|
63 |
def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>"
|
|
64 |
have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
|
|
65 |
using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp
|
|
66 |
hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
|
|
67 |
using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
|
|
68 |
by auto
|
39094
|
69 |
have \<delta>E_D: "sets_\<delta>E \<subseteq> sets D"
|
39080
|
70 |
unfolding sets_\<delta>E_def using assms by auto
|
|
71 |
have \<delta>ynkin: "dynkin \<delta>E"
|
|
72 |
proof (rule dynkinI, safe)
|
|
73 |
fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
|
|
74 |
{ fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
|
|
75 |
hence "A \<subseteq> space d"
|
|
76 |
using dynkin_subset by auto }
|
|
77 |
show "x \<in> space \<delta>E" using asm
|
|
78 |
unfolding \<delta>E_def sets_\<delta>E_def using not_empty
|
|
79 |
proof auto
|
|
80 |
fix x A fix d :: "'a algebra"
|
|
81 |
assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
|
|
82 |
dynkin d \<and>
|
|
83 |
space d = space E \<and>
|
|
84 |
sets E \<subseteq> sets d) \<longrightarrow>
|
|
85 |
A \<in> x" "x \<in> A"
|
|
86 |
and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
|
|
87 |
have "A \<in> sets d"
|
|
88 |
apply (rule impE[OF spec[OF asm(1), of "sets d"]])
|
|
89 |
using exI[of _ d] asm' by auto
|
|
90 |
thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
|
|
91 |
qed
|
|
92 |
next
|
|
93 |
show "space \<delta>E \<in> sets \<delta>E"
|
|
94 |
unfolding \<delta>E_def sets_\<delta>E_def
|
|
95 |
using dynkin_space by fastsimp
|
|
96 |
next
|
39094
|
97 |
fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" "a \<subseteq> b"
|
39080
|
98 |
thus "b - a \<in> sets \<delta>E"
|
|
99 |
unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
|
|
100 |
next
|
|
101 |
fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E"
|
|
102 |
thus "UNION UNIV a \<in> sets \<delta>E"
|
|
103 |
unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
|
|
104 |
by blast
|
|
105 |
qed
|
|
106 |
def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
|
|
107 |
{ fix d assume dasm: "d \<in> sets_\<delta>E"
|
|
108 |
have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
|
|
109 |
proof (rule dynkinI, auto)
|
|
110 |
fix A x assume "A \<in> Dy d" "x \<in> A"
|
|
111 |
thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
|
|
112 |
proof auto fix x A fix da :: "'a algebra"
|
|
113 |
assume asm: "x \<in> A"
|
|
114 |
"\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
|
|
115 |
dynkin d \<and> space d = space E \<and>
|
|
116 |
sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
|
|
117 |
"\<forall>x. (\<exists>d. x = sets d \<and>
|
|
118 |
dynkin d \<and> space d = space E \<and>
|
|
119 |
sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
|
|
120 |
"space da = space E" "dynkin da"
|
|
121 |
"sets E \<subseteq> sets da"
|
|
122 |
have "A \<in> sets da"
|
|
123 |
apply (rule impE[OF spec[OF asm(2)], of "sets da"])
|
|
124 |
apply (rule exI[of _ da])
|
|
125 |
using exI[of _ da] asm(4,5,6) by auto
|
|
126 |
thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
|
|
127 |
qed
|
|
128 |
next
|
|
129 |
show "space E \<in> Dy d"
|
|
130 |
unfolding Dy_def \<delta>E_def sets_\<delta>E_def
|
|
131 |
proof auto
|
|
132 |
fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d"
|
|
133 |
hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto
|
|
134 |
thus "space E \<in> sets d" using asm by auto
|
|
135 |
next
|
|
136 |
fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da"
|
|
137 |
have d: "d = space E \<inter> d"
|
|
138 |
using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin]
|
|
139 |
unfolding \<delta>E_def by auto
|
|
140 |
hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def
|
|
141 |
using dasm by auto
|
|
142 |
have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm
|
|
143 |
by auto
|
|
144 |
thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin]
|
|
145 |
unfolding \<delta>E_def by auto
|
|
146 |
qed
|
|
147 |
next
|
39094
|
148 |
fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" "a \<subseteq> b"
|
39080
|
149 |
hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
|
|
150 |
unfolding Dy_def \<delta>E_def by auto
|
|
151 |
hence *: "b - a \<in> sets \<delta>E"
|
39094
|
152 |
using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
|
39080
|
153 |
have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
|
|
154 |
using absm unfolding Dy_def \<delta>E_def by auto
|
|
155 |
hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
|
39094
|
156 |
using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
|
39080
|
157 |
hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
|
|
158 |
thus "b - a \<in> Dy d"
|
|
159 |
using * ** unfolding Dy_def \<delta>E_def by auto
|
|
160 |
next
|
|
161 |
fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
|
39094
|
162 |
hence "\<And> i. a i \<in> sets \<delta>E"
|
39080
|
163 |
unfolding Dy_def \<delta>E_def by auto
|
|
164 |
from dynkin_UN[OF \<delta>ynkin aasm(1) this]
|
|
165 |
have *: "UNION UNIV a \<in> sets \<delta>E" by auto
|
|
166 |
from aasm
|
|
167 |
have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E"
|
|
168 |
unfolding Dy_def \<delta>E_def by auto
|
|
169 |
from aasm
|
|
170 |
have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto
|
|
171 |
from dynkin_UN[OF \<delta>ynkin this]
|
|
172 |
have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E"
|
|
173 |
using aE by auto
|
|
174 |
hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto
|
|
175 |
from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto
|
|
176 |
qed } note Dy_nkin = this
|
|
177 |
have E_\<delta>E: "sets E \<subseteq> sets \<delta>E"
|
|
178 |
unfolding \<delta>E_def sets_\<delta>E_def by auto
|
|
179 |
{ fix d assume dasm: "d \<in> sets \<delta>E"
|
|
180 |
{ fix e assume easm: "e \<in> sets E"
|
|
181 |
hence deasm: "e \<in> sets \<delta>E"
|
|
182 |
unfolding \<delta>E_def sets_\<delta>E_def by auto
|
|
183 |
have subset: "Dy e \<subseteq> sets \<delta>E"
|
|
184 |
unfolding Dy_def \<delta>E_def by auto
|
|
185 |
{ fix e' assume e'asm: "e' \<in> sets E"
|
|
186 |
have "e' \<inter> e \<in> sets E"
|
|
187 |
using easm e'asm stab unfolding Int_stable_def by auto
|
|
188 |
hence "e' \<inter> e \<in> sets \<delta>E"
|
|
189 |
unfolding \<delta>E_def sets_\<delta>E_def by auto
|
|
190 |
hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto }
|
|
191 |
hence E_Dy: "sets E \<subseteq> Dy e" by auto
|
|
192 |
have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
|
|
193 |
using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
|
|
194 |
hence "sets_\<delta>E \<subseteq> Dy e"
|
|
195 |
unfolding sets_\<delta>E_def
|
|
196 |
proof auto fix x
|
|
197 |
assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
|
|
198 |
dynkin d \<and>
|
|
199 |
space d = space E \<and>
|
|
200 |
sets E \<subseteq> sets d) \<longrightarrow>
|
|
201 |
x \<in> xa"
|
|
202 |
"dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
|
|
203 |
"sets E \<subseteq> Dy e"
|
|
204 |
show "x \<in> Dy e"
|
|
205 |
apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
|
|
206 |
apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
|
|
207 |
using asm by auto
|
|
208 |
qed
|
|
209 |
hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
|
|
210 |
hence "d \<inter> e \<in> sets \<delta>E"
|
|
211 |
using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
|
|
212 |
hence "e \<in> Dy d" using deasm
|
|
213 |
unfolding Dy_def \<delta>E_def
|
|
214 |
by (auto simp add:Int_commute) }
|
|
215 |
hence "sets E \<subseteq> Dy d" by auto
|
|
216 |
hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
|
|
217 |
unfolding \<delta>E_def sets_\<delta>E_def
|
|
218 |
proof auto
|
|
219 |
fix x
|
|
220 |
assume asm: "sets E \<subseteq> Dy d"
|
|
221 |
"dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
|
|
222 |
"\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
|
|
223 |
space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
|
|
224 |
show "x \<in> Dy d"
|
|
225 |
apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
|
|
226 |
apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
|
|
227 |
using asm by auto
|
|
228 |
qed
|
|
229 |
hence *: "sets \<delta>E = Dy d"
|
|
230 |
unfolding Dy_def \<delta>E_def by auto
|
|
231 |
fix a assume aasm: "a \<in> sets \<delta>E"
|
|
232 |
hence "a \<inter> d \<in> sets \<delta>E"
|
|
233 |
using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
|
39094
|
234 |
{ fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets \<delta>E" "\<And>A. A \<in> sets \<delta>E \<Longrightarrow> A \<subseteq> space \<delta>E"
|
|
235 |
"\<And>a. a \<in> sets \<delta>E \<Longrightarrow> space \<delta>E - a \<in> sets \<delta>E"
|
|
236 |
"{} \<in> sets \<delta>E" "space \<delta>E \<in> sets \<delta>E"
|
|
237 |
let "?A i" = "A i \<inter> (\<Inter> j \<in> {..< i}. space \<delta>E - A j)"
|
|
238 |
{ fix i :: nat
|
|
239 |
have *: "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<inter> space \<delta>E \<in> sets \<delta>E"
|
|
240 |
apply (induct i)
|
|
241 |
using lessThan_Suc Asm \<delta>E_stab apply fastsimp
|
|
242 |
apply (subst lessThan_Suc)
|
|
243 |
apply (subst INT_insert)
|
|
244 |
apply (subst Int_assoc)
|
|
245 |
apply (subst \<delta>E_stab)
|
|
246 |
using lessThan_Suc Asm \<delta>E_stab Asm
|
|
247 |
apply (fastsimp simp add:Int_assoc dynkin_diff[OF \<delta>ynkin])
|
|
248 |
prefer 2 apply simp
|
|
249 |
apply (rule dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]])
|
|
250 |
using Asm by auto
|
|
251 |
have **: "\<And> i. A i \<subseteq> space \<delta>E" using Asm by auto
|
|
252 |
have "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<subseteq> space \<delta>E \<or> (\<Inter> j \<in> {..< i}. A j) = UNIV \<and> i = 0"
|
|
253 |
apply (cases i)
|
|
254 |
using Asm ** dynkin_subset[OF \<delta>ynkin, of "A (i - 1)"]
|
|
255 |
by auto
|
|
256 |
hence Aisets: "?A i \<in> sets \<delta>E"
|
|
257 |
apply (cases i)
|
|
258 |
using Asm * apply fastsimp
|
|
259 |
apply (rule \<delta>E_stab)
|
|
260 |
using Asm * **
|
|
261 |
by (auto simp add:Int_absorb2)
|
|
262 |
have "?A i = disjointed A i" unfolding disjointed_def
|
|
263 |
atLeast0LessThan using Asm by auto
|
|
264 |
hence "?A i = disjointed A i" "?A i \<in> sets \<delta>E"
|
|
265 |
using Aisets by auto
|
|
266 |
} note Ai = this
|
|
267 |
from dynkin_UN[OF \<delta>ynkin _ this(2)] this disjoint_family_disjointed[of A]
|
|
268 |
have "(\<Union> i. ?A i) \<in> sets \<delta>E"
|
|
269 |
by (auto simp add:disjoint_family_on_def disjointed_def)
|
|
270 |
hence "(\<Union> i. A i) \<in> sets \<delta>E"
|
|
271 |
using Ai(1) UN_disjointed_eq[of A] by auto } note \<delta>E_UN = this
|
|
272 |
{ fix a b assume asm: "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
|
|
273 |
let ?ab = "\<lambda> i. if (i::nat) = 0 then a else if i = 1 then b else {}"
|
|
274 |
have *: "(\<Union> i. ?ab i) \<in> sets \<delta>E"
|
|
275 |
apply (rule \<delta>E_UN)
|
|
276 |
using asm \<delta>E_UN dynkin_empty[OF \<delta>ynkin]
|
|
277 |
dynkin_subset[OF \<delta>ynkin]
|
|
278 |
dynkin_space[OF \<delta>ynkin]
|
|
279 |
dynkin_diff[OF \<delta>ynkin] by auto
|
|
280 |
have "(\<Union> i. ?ab i) = a \<union> b" apply auto
|
|
281 |
apply (case_tac "i = 0")
|
|
282 |
apply auto
|
|
283 |
apply (case_tac "i = 1")
|
|
284 |
by auto
|
|
285 |
hence "a \<union> b \<in> sets \<delta>E" using * by auto} note \<delta>E_Un = this
|
|
286 |
have "sigma_algebra \<delta>E"
|
39080
|
287 |
apply unfold_locales
|
39094
|
288 |
using dynkin_subset[OF \<delta>ynkin]
|
|
289 |
using dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]]
|
|
290 |
using dynkin_diff[OF \<delta>ynkin, of "space \<delta>E" "space \<delta>E", OF dynkin_space[OF \<delta>ynkin] dynkin_space[OF \<delta>ynkin]]
|
|
291 |
using dynkin_space[OF \<delta>ynkin]
|
|
292 |
using \<delta>E_UN \<delta>E_Un
|
|
293 |
by auto
|
|
294 |
from sigma_algebra.sigma_subset[OF this E_\<delta>E] \<delta>E_D subsDE spac
|
|
295 |
show ?thesis by (auto simp add:\<delta>E_def sigma_def)
|
|
296 |
qed
|
|
297 |
|
|
298 |
lemma measure_eq:
|
|
299 |
assumes fin: "\<mu> (space M) = \<nu> (space M)" "\<nu> (space M) < \<omega>"
|
|
300 |
assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
|
|
301 |
assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
|
|
302 |
assumes ms: "measure_space M \<mu>" "measure_space M \<nu>"
|
|
303 |
assumes A: "A \<in> sets M"
|
|
304 |
shows "\<mu> A = \<nu> A"
|
|
305 |
proof -
|
|
306 |
interpret M: measure_space M \<mu>
|
|
307 |
using ms by simp
|
|
308 |
interpret M': measure_space M \<nu>
|
|
309 |
using ms by simp
|
|
310 |
|
|
311 |
let ?D_sets = "{A. A \<in> sets M \<and> \<mu> A = \<nu> A}"
|
|
312 |
have \<delta>: "dynkin \<lparr> space = space M , sets = ?D_sets \<rparr>"
|
|
313 |
proof (rule dynkinI, safe, simp_all)
|
|
314 |
fix A x assume "A \<in> sets M \<and> \<mu> A = \<nu> A" "x \<in> A"
|
|
315 |
thus "x \<in> space M" using assms M.sets_into_space by auto
|
|
316 |
next
|
|
317 |
show "\<mu> (space M) = \<nu> (space M)"
|
|
318 |
using fin by auto
|
|
319 |
next
|
|
320 |
fix a b
|
|
321 |
assume asm: "a \<in> sets M \<and> \<mu> a = \<nu> a"
|
|
322 |
"b \<in> sets M \<and> \<mu> b = \<nu> b" "a \<subseteq> b"
|
|
323 |
hence "a \<subseteq> space M"
|
|
324 |
using M.sets_into_space by auto
|
|
325 |
from M.measure_mono[OF this]
|
|
326 |
have "\<mu> a \<le> \<mu> (space M)"
|
|
327 |
using asm by auto
|
|
328 |
hence afin: "\<mu> a < \<omega>"
|
|
329 |
using fin by auto
|
|
330 |
have *: "b = b - a \<union> a" using asm by auto
|
|
331 |
have **: "(b - a) \<inter> a = {}" using asm by auto
|
|
332 |
have iv: "\<mu> (b - a) + \<mu> a = \<mu> b"
|
|
333 |
using M.measure_additive[of "b - a" a]
|
|
334 |
conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
|
|
335 |
by auto
|
|
336 |
have v: "\<nu> (b - a) + \<nu> a = \<nu> b"
|
|
337 |
using M'.measure_additive[of "b - a" a]
|
|
338 |
conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
|
|
339 |
by auto
|
|
340 |
from iv v have "\<mu> (b - a) = \<nu> (b - a)" using asm afin
|
|
341 |
pinfreal_add_cancel_right[of "\<mu> (b - a)" "\<nu> a" "\<nu> (b - a)"]
|
|
342 |
by auto
|
|
343 |
thus "b - a \<in> sets M \<and> \<mu> (b - a) = \<nu> (b - a)"
|
|
344 |
using asm by auto
|
|
345 |
next
|
|
346 |
fix a assume "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
|
|
347 |
"\<And>i. a i \<in> sets M \<and> \<mu> (a i) = \<nu> (a i)"
|
|
348 |
thus "(\<Union>x. a x) \<in> sets M \<and> \<mu> (\<Union>x. a x) = \<nu> (\<Union>x. a x)"
|
|
349 |
using M.measure_countably_additive
|
|
350 |
M'.measure_countably_additive
|
|
351 |
M.countable_UN
|
|
352 |
apply (auto simp add:disjoint_family_on_def image_def)
|
|
353 |
apply (subst M.measure_countably_additive[symmetric])
|
|
354 |
apply (auto simp add:disjoint_family_on_def)
|
|
355 |
apply (subst M'.measure_countably_additive[symmetric])
|
|
356 |
by (auto simp add:disjoint_family_on_def)
|
39080
|
357 |
qed
|
39094
|
358 |
have *: "sets E \<subseteq> ?D_sets"
|
|
359 |
using eq E sigma_sets.Basic[of _ "sets E"]
|
|
360 |
by (auto simp add:sigma_def)
|
|
361 |
have **: "?D_sets \<subseteq> sets M" by auto
|
|
362 |
have "M = \<lparr> space = space M , sets = ?D_sets \<rparr>"
|
|
363 |
unfolding E(1)
|
|
364 |
apply (rule dynkin_lemma[OF E(2)])
|
|
365 |
using eq E space_sigma \<delta> sigma_sets.Basic
|
|
366 |
by (auto simp add:sigma_def)
|
|
367 |
from subst[OF this, of "\<lambda> M. A \<in> sets M", OF A]
|
|
368 |
show ?thesis by auto
|
|
369 |
qed
|
|
370 |
|
|
371 |
lemma
|
|
372 |
assumes sfin: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And> i :: nat. \<nu> (A i) < \<omega>"
|
|
373 |
assumes A: "\<And> i. \<mu> (A i) = \<nu> (A i)" "\<And> i. A i \<subseteq> A (Suc i)"
|
|
374 |
assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
|
|
375 |
assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
|
|
376 |
assumes ms: "measure_space (M :: 'a algebra) \<mu>" "measure_space M \<nu>"
|
|
377 |
assumes B: "B \<in> sets M"
|
|
378 |
shows "\<mu> B = \<nu> B"
|
|
379 |
proof -
|
|
380 |
interpret M: measure_space M \<mu> by (rule ms)
|
|
381 |
interpret M': measure_space M \<nu> by (rule ms)
|
|
382 |
have *: "M = \<lparr> space = space M, sets = sets M \<rparr>" by auto
|
|
383 |
{ fix i :: nat
|
|
384 |
have **: "M\<lparr> space := A i, sets := op \<inter> (A i) ` sets M \<rparr> =
|
|
385 |
\<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
|
|
386 |
by auto
|
|
387 |
have mu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<mu>"
|
|
388 |
using M.restricted_measure_space[of "A i", simplified **]
|
|
389 |
sfin by auto
|
|
390 |
have nu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<nu>"
|
|
391 |
using M'.restricted_measure_space[of "A i", simplified **]
|
|
392 |
sfin by auto
|
|
393 |
let ?M = "\<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
|
|
394 |
have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
|
|
395 |
apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
|
|
396 |
using assms nu_i mu_i
|
|
397 |
apply (auto simp add:image_def) (* TODO *)
|
39080
|
398 |
qed
|
|
399 |
|
|
400 |
lemma
|
|
401 |
(*
|
38656
|
402 |
definition prod_sets where
|
|
403 |
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
|
|
404 |
|
35833
|
405 |
definition
|
38656
|
406 |
"prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
|
35833
|
407 |
|
|
408 |
definition
|
38656
|
409 |
"prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
|
|
410 |
|
|
411 |
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
|
|
412 |
by (auto simp add: prod_sets_def)
|
35833
|
413 |
|
38656
|
414 |
lemma sigma_prod_sets_finite:
|
|
415 |
assumes "finite A" and "finite B"
|
|
416 |
shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)"
|
|
417 |
proof safe
|
|
418 |
have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
|
35833
|
419 |
|
38656
|
420 |
fix x assume subset: "x \<subseteq> A \<times> B"
|
|
421 |
hence "finite x" using fin by (rule finite_subset)
|
|
422 |
from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
|
|
423 |
(is "x \<in> sigma_sets ?prod ?sets")
|
|
424 |
proof (induct x)
|
|
425 |
case empty show ?case by (rule sigma_sets.Empty)
|
|
426 |
next
|
|
427 |
case (insert a x)
|
|
428 |
hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
|
|
429 |
moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
|
|
430 |
ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
|
|
431 |
qed
|
|
432 |
next
|
|
433 |
fix x a b
|
|
434 |
assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
|
|
435 |
from sigma_sets_into_sp[OF _ this(1)] this(2)
|
|
436 |
show "a \<in> A" and "b \<in> B"
|
|
437 |
by (auto simp: prod_sets_def)
|
35833
|
438 |
qed
|
|
439 |
|
38656
|
440 |
lemma (in sigma_algebra) measurable_prod_sigma:
|
|
441 |
assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2"
|
|
442 |
assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
|
|
443 |
shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
|
|
444 |
(prod_sets (sets a1) (sets a2)))"
|
35977
|
445 |
proof -
|
38656
|
446 |
from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
|
|
447 |
and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
|
|
448 |
by (auto simp add: measurable_def)
|
|
449 |
from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
|
|
450 |
and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
|
|
451 |
by (auto simp add: measurable_def)
|
|
452 |
show ?thesis
|
|
453 |
proof (rule measurable_sigma)
|
|
454 |
show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
|
|
455 |
by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)
|
|
456 |
next
|
|
457 |
show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
|
|
458 |
by (rule prod_final [OF fn1 fn2])
|
|
459 |
next
|
|
460 |
fix z
|
|
461 |
assume z: "z \<in> prod_sets (sets a1) (sets a2)"
|
|
462 |
thus "f -` z \<inter> space M \<in> sets M"
|
|
463 |
proof (auto simp add: prod_sets_def vimage_Times)
|
|
464 |
fix x y
|
|
465 |
assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
|
|
466 |
have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
|
|
467 |
((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
|
|
468 |
by blast
|
|
469 |
also have "... \<in> sets M" using x y q1 q2
|
|
470 |
by blast
|
|
471 |
finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
|
|
472 |
qed
|
|
473 |
qed
|
35977
|
474 |
qed
|
35833
|
475 |
|
38656
|
476 |
lemma (in sigma_finite_measure) prod_measure_times:
|
|
477 |
assumes "sigma_finite_measure N \<nu>"
|
|
478 |
and "A1 \<in> sets M" "A2 \<in> sets N"
|
|
479 |
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
|
|
480 |
oops
|
35833
|
481 |
|
38656
|
482 |
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space:
|
|
483 |
assumes "sigma_finite_measure N \<nu>"
|
|
484 |
shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
|
|
485 |
oops
|
|
486 |
|
|
487 |
lemma (in finite_measure_space) finite_prod_measure_times:
|
|
488 |
assumes "finite_measure_space N \<nu>"
|
|
489 |
and "A1 \<in> sets M" "A2 \<in> sets N"
|
|
490 |
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
|
|
491 |
proof -
|
|
492 |
interpret N: finite_measure_space N \<nu> by fact
|
|
493 |
have *: "\<And>x. \<nu> (Pair x -` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)"
|
|
494 |
by (auto simp: vimage_Times comp_def)
|
|
495 |
have "finite A1"
|
|
496 |
using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset)
|
|
497 |
then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M`
|
|
498 |
by (auto intro!: measure_finite_singleton simp: sets_eq_Pow)
|
|
499 |
then show ?thesis using `A1 \<in> sets M`
|
|
500 |
unfolding prod_measure_def positive_integral_finite_eq_setsum *
|
|
501 |
by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space])
|
35833
|
502 |
qed
|
|
503 |
|
38656
|
504 |
lemma (in finite_measure_space) finite_prod_measure_space:
|
|
505 |
assumes "finite_measure_space N \<nu>"
|
|
506 |
shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>"
|
35977
|
507 |
proof -
|
38656
|
508 |
interpret N: finite_measure_space N \<nu> by fact
|
|
509 |
show ?thesis using finite_space N.finite_space
|
|
510 |
by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow)
|
35833
|
511 |
qed
|
|
512 |
|
38656
|
513 |
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure:
|
|
514 |
assumes "finite_measure_space N \<nu>"
|
|
515 |
shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
|
|
516 |
unfolding finite_prod_measure_space[OF assms]
|
|
517 |
proof (rule finite_measure_spaceI)
|
|
518 |
interpret N: finite_measure_space N \<nu> by fact
|
|
519 |
|
|
520 |
let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>"
|
|
521 |
show "measure_space ?P (prod_measure M \<mu> N \<nu>)"
|
|
522 |
proof (rule sigma_algebra.finite_additivity_sufficient)
|
|
523 |
show "sigma_algebra ?P" by (rule sigma_algebra_Pow)
|
|
524 |
show "finite (space ?P)" using finite_space N.finite_space by auto
|
|
525 |
from finite_prod_measure_times[OF assms, of "{}" "{}"]
|
|
526 |
show "positive (prod_measure M \<mu> N \<nu>)"
|
|
527 |
unfolding positive_def by simp
|
|
528 |
|
|
529 |
show "additive ?P (prod_measure M \<mu> N \<nu>)"
|
|
530 |
unfolding additive_def
|
|
531 |
apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric]
|
|
532 |
intro!: positive_integral_cong)
|
|
533 |
apply (subst N.measure_additive[symmetric])
|
|
534 |
by (auto simp: N.sets_eq_Pow sets_eq_Pow)
|
|
535 |
qed
|
|
536 |
show "finite (space ?P)" using finite_space N.finite_space by auto
|
|
537 |
show "sets ?P = Pow (space ?P)" by simp
|
|
538 |
|
|
539 |
fix x assume "x \<in> space ?P"
|
|
540 |
with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"]
|
|
541 |
finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"]
|
|
542 |
show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>"
|
|
543 |
by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE)
|
|
544 |
qed
|
|
545 |
|
|
546 |
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive:
|
|
547 |
assumes N: "finite_measure_space N \<nu>"
|
|
548 |
shows "finite_measure_space \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr> (prod_measure M \<mu> N \<nu>)"
|
|
549 |
(is "finite_measure_space ?M ?m")
|
|
550 |
unfolding finite_prod_measure_space[OF N, symmetric]
|
|
551 |
using finite_measure_space_finite_prod_measure[OF N] .
|
|
552 |
|
39080
|
553 |
*)
|
35833
|
554 |
end |