author | hoelzl |
Tue, 04 May 2010 18:19:24 +0200 | |
changeset 36649 | bfd8c550faa6 |
parent 35977 | 30d42bfd0174 |
child 38656 | d5d342611edb |
permissions | -rw-r--r-- |
35833 | 1 |
theory Product_Measure |
36649
bfd8c550faa6
Corrected imports; better approximation of dependencies.
hoelzl
parents:
35977
diff
changeset
|
2 |
imports Lebesgue |
35833 | 3 |
begin |
4 |
||
5 |
definition |
|
6 |
"prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) -` a)))" |
|
7 |
||
8 |
definition |
|
9 |
"prod_measure_space M M' \<equiv> |
|
10 |
\<lparr> space = space M \<times> space M', |
|
11 |
sets = sets (sigma (space M \<times> space M') (prod_sets (sets M) (sets M'))), |
|
12 |
measure = prod_measure M M' \<rparr>" |
|
13 |
||
14 |
lemma prod_measure_times: |
|
15 |
assumes "measure_space M" and "measure_space M'" and a: "a \<in> sets M" |
|
16 |
shows "prod_measure M M' (a \<times> a') = measure M a * measure M' a'" |
|
17 |
proof - |
|
18 |
interpret M: measure_space M by fact |
|
19 |
interpret M': measure_space M' by fact |
|
20 |
||
21 |
{ fix \<omega> |
|
22 |
have "(\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a') = (if \<omega> \<in> a then a' else {})" |
|
23 |
by auto |
|
24 |
hence "measure M' ((\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a')) = |
|
25 |
measure M' a' * indicator_fn a \<omega>" |
|
26 |
unfolding indicator_fn_def by auto } |
|
27 |
note vimage_eq_indicator = this |
|
28 |
||
29 |
show ?thesis |
|
30 |
unfolding prod_measure_def vimage_eq_indicator |
|
31 |
M.integral_cmul_indicator(1)[OF `a \<in> sets M`] |
|
32 |
by simp |
|
33 |
qed |
|
34 |
||
35977 | 35 |
lemma finite_prod_measure_space: |
36 |
assumes "finite_measure_space M" and "finite_measure_space M'" |
|
37 |
shows "prod_measure_space M M' = |
|
38 |
\<lparr> space = space M \<times> space M', |
|
39 |
sets = Pow (space M \<times> space M'), |
|
40 |
measure = prod_measure M M' \<rparr>" |
|
41 |
proof - |
|
42 |
interpret M: finite_measure_space M by fact |
|
43 |
interpret M': finite_measure_space M' by fact |
|
44 |
show ?thesis using M.finite_space M'.finite_space |
|
45 |
by (simp add: sigma_prod_sets_finite M.sets_eq_Pow M'.sets_eq_Pow |
|
46 |
prod_measure_space_def) |
|
47 |
qed |
|
35833 | 48 |
|
35977 | 49 |
lemma finite_measure_space_finite_prod_measure: |
50 |
assumes "finite_measure_space M" and "finite_measure_space M'" |
|
51 |
shows "finite_measure_space (prod_measure_space M M')" |
|
52 |
proof (rule finite_Pow_additivity_sufficient) |
|
53 |
interpret M: finite_measure_space M by fact |
|
54 |
interpret M': finite_measure_space M' by fact |
|
35833 | 55 |
|
35977 | 56 |
from M.finite_space M'.finite_space |
57 |
show "finite (space (prod_measure_space M M'))" and |
|
58 |
"sets (prod_measure_space M M') = Pow (space (prod_measure_space M M'))" |
|
59 |
by (simp_all add: finite_prod_measure_space[OF assms]) |
|
35833 | 60 |
|
61 |
show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))" |
|
35977 | 62 |
unfolding additive_def finite_prod_measure_space[OF assms] |
63 |
proof (simp, safe) |
|
64 |
fix x y assume subs: "x \<subseteq> space M \<times> space M'" "y \<subseteq> space M \<times> space M'" |
|
35833 | 65 |
and disj_x_y: "x \<inter> y = {}" |
35977 | 66 |
have "\<And>z. measure M' (Pair z -` x \<union> Pair z -` y) = |
67 |
measure M' (Pair z -` x) + measure M' (Pair z -` y)" |
|
68 |
using disj_x_y subs by (subst M'.measure_additive) (auto simp: M'.sets_eq_Pow) |
|
69 |
thus "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y" |
|
70 |
unfolding prod_measure_def M.integral_finite_singleton |
|
35833 | 71 |
by (simp_all add: setsum_addf[symmetric] field_simps) |
72 |
qed |
|
73 |
||
74 |
show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))" |
|
75 |
unfolding positive_def |
|
35977 | 76 |
by (auto intro!: setsum_nonneg mult_nonneg_nonneg M'.positive M.positive |
77 |
simp add: M.integral_zero finite_prod_measure_space[OF assms] |
|
78 |
prod_measure_def M.integral_finite_singleton |
|
79 |
M.sets_eq_Pow M'.sets_eq_Pow) |
|
35833 | 80 |
qed |
81 |
||
35977 | 82 |
lemma finite_measure_space_finite_prod_measure_alterantive: |
83 |
assumes M: "finite_measure_space M" and M': "finite_measure_space M'" |
|
84 |
shows "finite_measure_space \<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M'), measure = prod_measure M M' \<rparr>" |
|
85 |
(is "finite_measure_space ?M") |
|
86 |
proof - |
|
87 |
interpret M: finite_measure_space M by fact |
|
88 |
interpret M': finite_measure_space M' by fact |
|
35833 | 89 |
|
35977 | 90 |
show ?thesis |
91 |
using finite_measure_space_finite_prod_measure[OF assms] |
|
92 |
unfolding prod_measure_space_def M.sets_eq_Pow M'.sets_eq_Pow |
|
93 |
using M.finite_space M'.finite_space |
|
94 |
by (simp add: sigma_prod_sets_finite) |
|
35833 | 95 |
qed |
96 |
||
97 |
end |