author | hoelzl |
Thu, 26 Aug 2010 15:20:41 +0200 | |
changeset 39082 | 54dbe0368dc6 |
parent 39080 | cae59dc0a094 |
child 39088 | ca17017c10e6 |
permissions | -rw-r--r-- |
35833 | 1 |
theory Product_Measure |
38656 | 2 |
imports Lebesgue_Integration |
35833 | 3 |
begin |
4 |
||
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
5 |
definition "dynkin M \<longleftrightarrow> |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
6 |
space M \<in> sets M \<and> |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
7 |
(\<forall> A \<in> sets M. A \<subseteq> space M) \<and> |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
8 |
(\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and> |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
9 |
(\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" |
39080 | 10 |
|
11 |
lemma dynkinI: |
|
12 |
assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" |
|
13 |
assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M" |
|
14 |
assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}) |
|
15 |
\<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M" |
|
16 |
shows "dynkin M" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
17 |
using assms unfolding dynkin_def sorry |
39080 | 18 |
|
19 |
lemma dynkin_subset: |
|
20 |
assumes "dynkin M" |
|
21 |
shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" |
|
22 |
using assms unfolding dynkin_def by auto |
|
23 |
||
24 |
lemma dynkin_space: |
|
25 |
assumes "dynkin M" |
|
26 |
shows "space M \<in> sets M" |
|
27 |
using assms unfolding dynkin_def by auto |
|
28 |
||
29 |
lemma dynkin_diff: |
|
30 |
assumes "dynkin M" |
|
31 |
shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M" |
|
32 |
using assms unfolding dynkin_def by auto |
|
33 |
||
34 |
lemma dynkin_UN: |
|
35 |
assumes "dynkin M" |
|
36 |
assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" |
|
37 |
assumes "\<forall> i :: nat. a i \<in> sets M" |
|
38 |
shows "UNION UNIV a \<in> sets M" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
39 |
using assms unfolding dynkin_def sorry |
39080 | 40 |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
41 |
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" |
39080 | 42 |
|
43 |
lemma dynkin_trivial: |
|
44 |
shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>" |
|
45 |
by (rule dynkinI) auto |
|
46 |
||
47 |
lemma |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
48 |
fixes D :: "'a algebra" |
39080 | 49 |
assumes stab: "Int_stable E" |
50 |
and spac: "space E = space D" |
|
51 |
and subsED: "sets E \<subseteq> sets D" |
|
52 |
and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)" |
|
53 |
and dyn: "dynkin D" |
|
54 |
shows "sigma (space E) (sets E) = D" |
|
55 |
proof - |
|
56 |
def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}" |
|
57 |
def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>" |
|
58 |
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}" |
|
59 |
using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp |
|
60 |
hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}" |
|
61 |
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] |
|
62 |
by auto |
|
63 |
||
64 |
have "sets_\<delta>E \<subseteq> sets D" |
|
65 |
unfolding sets_\<delta>E_def using assms by auto |
|
66 |
||
67 |
have \<delta>ynkin: "dynkin \<delta>E" |
|
68 |
proof (rule dynkinI, safe) |
|
69 |
fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A" |
|
70 |
{ fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
71 |
hence "A \<subseteq> space d" using dynkin_subset by auto } |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
72 |
show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
73 |
by simp (metis dynkin_subset in_mono mem_def) |
39080 | 74 |
next |
75 |
show "space \<delta>E \<in> sets \<delta>E" |
|
76 |
unfolding \<delta>E_def sets_\<delta>E_def |
|
77 |
using dynkin_space by fastsimp |
|
78 |
next |
|
79 |
fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" |
|
80 |
thus "b - a \<in> sets \<delta>E" |
|
81 |
unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff) |
|
82 |
next |
|
83 |
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" |
|
84 |
thus "UNION UNIV a \<in> sets \<delta>E" |
|
85 |
unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)]) |
|
86 |
by blast |
|
87 |
qed |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
88 |
|
39080 | 89 |
def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}" |
90 |
{ fix d assume dasm: "d \<in> sets_\<delta>E" |
|
91 |
have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
92 |
proof (rule dynkinI, safe, simp_all) |
39080 | 93 |
fix A x assume "A \<in> Dy d" "x \<in> A" |
94 |
thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
95 |
by simp (metis dynkin_subset in_mono mem_def) |
39080 | 96 |
next |
97 |
show "space E \<in> Dy d" |
|
98 |
unfolding Dy_def \<delta>E_def sets_\<delta>E_def |
|
99 |
proof auto |
|
100 |
fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d" |
|
101 |
hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto |
|
102 |
thus "space E \<in> sets d" using asm by auto |
|
103 |
next |
|
104 |
fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da" |
|
105 |
have d: "d = space E \<inter> d" |
|
106 |
using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin] |
|
107 |
unfolding \<delta>E_def by auto |
|
108 |
hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def |
|
109 |
using dasm by auto |
|
110 |
have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm |
|
111 |
by auto |
|
112 |
thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin] |
|
113 |
unfolding \<delta>E_def by auto |
|
114 |
qed |
|
115 |
next |
|
116 |
fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" |
|
117 |
hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" |
|
118 |
unfolding Dy_def \<delta>E_def by auto |
|
119 |
hence *: "b - a \<in> sets \<delta>E" |
|
120 |
using dynkin_diff[OF \<delta>ynkin] by auto |
|
121 |
have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E" |
|
122 |
using absm unfolding Dy_def \<delta>E_def by auto |
|
123 |
hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E" |
|
124 |
using dynkin_diff[OF \<delta>ynkin] by auto |
|
125 |
hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2) |
|
126 |
thus "b - a \<in> Dy d" |
|
127 |
using * ** unfolding Dy_def \<delta>E_def by auto |
|
128 |
next |
|
129 |
fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d" |
|
130 |
hence "\<forall> i. a i \<in> sets \<delta>E" |
|
131 |
unfolding Dy_def \<delta>E_def by auto |
|
132 |
from dynkin_UN[OF \<delta>ynkin aasm(1) this] |
|
133 |
have *: "UNION UNIV a \<in> sets \<delta>E" by auto |
|
134 |
from aasm |
|
135 |
have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E" |
|
136 |
unfolding Dy_def \<delta>E_def by auto |
|
137 |
from aasm |
|
138 |
have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto |
|
139 |
from dynkin_UN[OF \<delta>ynkin this] |
|
140 |
have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E" |
|
141 |
using aE by auto |
|
142 |
hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto |
|
143 |
from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto |
|
144 |
qed } note Dy_nkin = this |
|
145 |
have E_\<delta>E: "sets E \<subseteq> sets \<delta>E" |
|
146 |
unfolding \<delta>E_def sets_\<delta>E_def by auto |
|
147 |
{ fix d assume dasm: "d \<in> sets \<delta>E" |
|
148 |
{ fix e assume easm: "e \<in> sets E" |
|
149 |
hence deasm: "e \<in> sets \<delta>E" |
|
150 |
unfolding \<delta>E_def sets_\<delta>E_def by auto |
|
151 |
have subset: "Dy e \<subseteq> sets \<delta>E" |
|
152 |
unfolding Dy_def \<delta>E_def by auto |
|
153 |
{ fix e' assume e'asm: "e' \<in> sets E" |
|
154 |
have "e' \<inter> e \<in> sets E" |
|
155 |
using easm e'asm stab unfolding Int_stable_def by auto |
|
156 |
hence "e' \<inter> e \<in> sets \<delta>E" |
|
157 |
unfolding \<delta>E_def sets_\<delta>E_def by auto |
|
158 |
hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto } |
|
159 |
hence E_Dy: "sets E \<subseteq> Dy e" by auto |
|
160 |
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}" |
|
161 |
using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto |
|
162 |
hence "sets_\<delta>E \<subseteq> Dy e" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
163 |
unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac) |
39080 | 164 |
hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto |
165 |
hence "d \<inter> e \<in> sets \<delta>E" |
|
166 |
using dasm easm deasm unfolding Dy_def \<delta>E_def by auto |
|
167 |
hence "e \<in> Dy d" using deasm |
|
168 |
unfolding Dy_def \<delta>E_def |
|
169 |
by (auto simp add:Int_commute) } |
|
170 |
hence "sets E \<subseteq> Dy d" by auto |
|
171 |
hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]] |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
172 |
unfolding \<delta>E_def sets_\<delta>E_def |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
173 |
by auto (metis `sets E <= Dy d` simps(1) simps(2) spac) |
39080 | 174 |
hence *: "sets \<delta>E = Dy d" |
175 |
unfolding Dy_def \<delta>E_def by auto |
|
176 |
fix a assume aasm: "a \<in> sets \<delta>E" |
|
177 |
hence "a \<inter> d \<in> sets \<delta>E" |
|
178 |
using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this |
|
179 |
have "sigma_algebra D" |
|
180 |
apply unfold_locales |
|
181 |
using dynkin_subset[OF dyn] |
|
182 |
using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]] |
|
183 |
using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]] |
|
184 |
using dynkin_space[OF dyn] |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
185 |
sorry |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
186 |
(* |
39080 | 187 |
proof auto |
188 |
fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D" |
|
189 |
"\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D" |
|
190 |
"{} \<in> sets D" "space D \<in> sets D" |
|
191 |
let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)" |
|
192 |
{ fix i :: nat assume "i > 0" |
|
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
193 |
have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E" sorry } |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
194 |
oops |
39080 | 195 |
qed |
39082
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
196 |
*) |
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
197 |
|
54dbe0368dc6
changed definition of dynkin; replaces proofs by metis calles
hoelzl
parents:
39080
diff
changeset
|
198 |
show ?thesis sorry |
39080 | 199 |
qed |
200 |
||
38656 | 201 |
definition prod_sets where |
202 |
"prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}" |
|
203 |
||
35833 | 204 |
definition |
38656 | 205 |
"prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))" |
35833 | 206 |
|
207 |
definition |
|
38656 | 208 |
"prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))" |
209 |
||
210 |
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B" |
|
211 |
by (auto simp add: prod_sets_def) |
|
35833 | 212 |
|
38656 | 213 |
lemma sigma_prod_sets_finite: |
214 |
assumes "finite A" and "finite B" |
|
215 |
shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)" |
|
216 |
proof safe |
|
217 |
have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product) |
|
35833 | 218 |
|
38656 | 219 |
fix x assume subset: "x \<subseteq> A \<times> B" |
220 |
hence "finite x" using fin by (rule finite_subset) |
|
221 |
from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" |
|
222 |
(is "x \<in> sigma_sets ?prod ?sets") |
|
223 |
proof (induct x) |
|
224 |
case empty show ?case by (rule sigma_sets.Empty) |
|
225 |
next |
|
226 |
case (insert a x) |
|
227 |
hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic) |
|
228 |
moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto |
|
229 |
ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) |
|
230 |
qed |
|
231 |
next |
|
232 |
fix x a b |
|
233 |
assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x" |
|
234 |
from sigma_sets_into_sp[OF _ this(1)] this(2) |
|
235 |
show "a \<in> A" and "b \<in> B" |
|
236 |
by (auto simp: prod_sets_def) |
|
35833 | 237 |
qed |
238 |
||
38656 | 239 |
lemma (in sigma_algebra) measurable_prod_sigma: |
240 |
assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2" |
|
241 |
assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2" |
|
242 |
shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2)) |
|
243 |
(prod_sets (sets a1) (sets a2)))" |
|
35977 | 244 |
proof - |
38656 | 245 |
from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1" |
246 |
and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M" |
|
247 |
by (auto simp add: measurable_def) |
|
248 |
from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2" |
|
249 |
and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M" |
|
250 |
by (auto simp add: measurable_def) |
|
251 |
show ?thesis |
|
252 |
proof (rule measurable_sigma) |
|
253 |
show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2 |
|
254 |
by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed) |
|
255 |
next |
|
256 |
show "f \<in> space M \<rightarrow> space a1 \<times> space a2" |
|
257 |
by (rule prod_final [OF fn1 fn2]) |
|
258 |
next |
|
259 |
fix z |
|
260 |
assume z: "z \<in> prod_sets (sets a1) (sets a2)" |
|
261 |
thus "f -` z \<inter> space M \<in> sets M" |
|
262 |
proof (auto simp add: prod_sets_def vimage_Times) |
|
263 |
fix x y |
|
264 |
assume x: "x \<in> sets a1" and y: "y \<in> sets a2" |
|
265 |
have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M = |
|
266 |
((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)" |
|
267 |
by blast |
|
268 |
also have "... \<in> sets M" using x y q1 q2 |
|
269 |
by blast |
|
270 |
finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" . |
|
271 |
qed |
|
272 |
qed |
|
35977 | 273 |
qed |
35833 | 274 |
|
38656 | 275 |
lemma (in sigma_finite_measure) prod_measure_times: |
276 |
assumes "sigma_finite_measure N \<nu>" |
|
277 |
and "A1 \<in> sets M" "A2 \<in> sets N" |
|
278 |
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2" |
|
279 |
oops |
|
35833 | 280 |
|
38656 | 281 |
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space: |
282 |
assumes "sigma_finite_measure N \<nu>" |
|
283 |
shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)" |
|
284 |
oops |
|
285 |
||
286 |
lemma (in finite_measure_space) finite_prod_measure_times: |
|
287 |
assumes "finite_measure_space N \<nu>" |
|
288 |
and "A1 \<in> sets M" "A2 \<in> sets N" |
|
289 |
shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2" |
|
290 |
proof - |
|
291 |
interpret N: finite_measure_space N \<nu> by fact |
|
292 |
have *: "\<And>x. \<nu> (Pair x -` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)" |
|
293 |
by (auto simp: vimage_Times comp_def) |
|
294 |
have "finite A1" |
|
295 |
using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset) |
|
296 |
then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M` |
|
297 |
by (auto intro!: measure_finite_singleton simp: sets_eq_Pow) |
|
298 |
then show ?thesis using `A1 \<in> sets M` |
|
299 |
unfolding prod_measure_def positive_integral_finite_eq_setsum * |
|
300 |
by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space]) |
|
35833 | 301 |
qed |
302 |
||
38656 | 303 |
lemma (in finite_measure_space) finite_prod_measure_space: |
304 |
assumes "finite_measure_space N \<nu>" |
|
305 |
shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>" |
|
35977 | 306 |
proof - |
38656 | 307 |
interpret N: finite_measure_space N \<nu> by fact |
308 |
show ?thesis using finite_space N.finite_space |
|
309 |
by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow) |
|
35833 | 310 |
qed |
311 |
||
38656 | 312 |
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure: |
313 |
assumes "finite_measure_space N \<nu>" |
|
314 |
shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)" |
|
315 |
unfolding finite_prod_measure_space[OF assms] |
|
316 |
proof (rule finite_measure_spaceI) |
|
317 |
interpret N: finite_measure_space N \<nu> by fact |
|
318 |
||
319 |
let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>" |
|
320 |
show "measure_space ?P (prod_measure M \<mu> N \<nu>)" |
|
321 |
proof (rule sigma_algebra.finite_additivity_sufficient) |
|
322 |
show "sigma_algebra ?P" by (rule sigma_algebra_Pow) |
|
323 |
show "finite (space ?P)" using finite_space N.finite_space by auto |
|
324 |
from finite_prod_measure_times[OF assms, of "{}" "{}"] |
|
325 |
show "positive (prod_measure M \<mu> N \<nu>)" |
|
326 |
unfolding positive_def by simp |
|
327 |
||
328 |
show "additive ?P (prod_measure M \<mu> N \<nu>)" |
|
329 |
unfolding additive_def |
|
330 |
apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric] |
|
331 |
intro!: positive_integral_cong) |
|
332 |
apply (subst N.measure_additive[symmetric]) |
|
333 |
by (auto simp: N.sets_eq_Pow sets_eq_Pow) |
|
334 |
qed |
|
335 |
show "finite (space ?P)" using finite_space N.finite_space by auto |
|
336 |
show "sets ?P = Pow (space ?P)" by simp |
|
337 |
||
338 |
fix x assume "x \<in> space ?P" |
|
339 |
with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"] |
|
340 |
finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"] |
|
341 |
show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>" |
|
342 |
by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE) |
|
343 |
qed |
|
344 |
||
345 |
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive: |
|
346 |
assumes N: "finite_measure_space N \<nu>" |
|
347 |
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>)" |
|
348 |
(is "finite_measure_space ?M ?m") |
|
349 |
unfolding finite_prod_measure_space[OF N, symmetric] |
|
350 |
using finite_measure_space_finite_prod_measure[OF N] . |
|
351 |
||
35833 | 352 |
end |