1 (* Title: HOL/Analysis/Binary_Product_Measure.thy |
1 (* Title: HOL/Analysis/Binary_Product_Measure.thy |
2 Author: Johannes Hölzl, TU München |
2 Author: Johannes Hölzl, TU München |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Binary product measures\<close> |
5 section%important \<open>Binary product measures\<close> |
6 |
6 |
7 theory Binary_Product_Measure |
7 theory Binary_Product_Measure |
8 imports Nonnegative_Lebesgue_Integration |
8 imports Nonnegative_Lebesgue_Integration |
9 begin |
9 begin |
10 |
10 |
11 lemma Pair_vimage_times[simp]: "Pair x -` (A \<times> B) = (if x \<in> A then B else {})" |
11 lemma%unimportant Pair_vimage_times[simp]: "Pair x -` (A \<times> B) = (if x \<in> A then B else {})" |
12 by auto |
12 by auto |
13 |
13 |
14 lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})" |
14 lemma%unimportant rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})" |
15 by auto |
15 by auto |
16 |
16 |
17 subsection "Binary products" |
17 subsection%important "Binary products" |
18 |
18 |
19 definition pair_measure (infixr "\<Otimes>\<^sub>M" 80) where |
19 definition%important pair_measure (infixr "\<Otimes>\<^sub>M" 80) where |
20 "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B) |
20 "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B) |
21 {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} |
21 {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} |
22 (\<lambda>X. \<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator X (x,y) \<partial>B) \<partial>A)" |
22 (\<lambda>X. \<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator X (x,y) \<partial>B) \<partial>A)" |
23 |
23 |
24 lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)" |
24 lemma%important pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)" |
25 using sets.space_closed[of A] sets.space_closed[of B] by auto |
25 using%unimportant sets.space_closed[of A] sets.space_closed[of B] by auto |
26 |
26 |
27 lemma space_pair_measure: |
27 lemma%important space_pair_measure: |
28 "space (A \<Otimes>\<^sub>M B) = space A \<times> space B" |
28 "space (A \<Otimes>\<^sub>M B) = space A \<times> space B" |
29 unfolding pair_measure_def using pair_measure_closed[of A B] |
29 unfolding pair_measure_def using pair_measure_closed[of A B] |
30 by (rule space_measure_of) |
30 by%unimportant (rule space_measure_of) |
31 |
31 |
32 lemma SIGMA_Collect_eq: "(SIGMA x:space M. {y\<in>space N. P x y}) = {x\<in>space (M \<Otimes>\<^sub>M N). P (fst x) (snd x)}" |
32 lemma%unimportant SIGMA_Collect_eq: "(SIGMA x:space M. {y\<in>space N. P x y}) = {x\<in>space (M \<Otimes>\<^sub>M N). P (fst x) (snd x)}" |
33 by (auto simp: space_pair_measure) |
33 by (auto simp: space_pair_measure) |
34 |
34 |
35 lemma sets_pair_measure: |
35 lemma%unimportant sets_pair_measure: |
36 "sets (A \<Otimes>\<^sub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}" |
36 "sets (A \<Otimes>\<^sub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}" |
37 unfolding pair_measure_def using pair_measure_closed[of A B] |
37 unfolding pair_measure_def using pair_measure_closed[of A B] |
38 by (rule sets_measure_of) |
38 by (rule sets_measure_of) |
39 |
39 |
40 lemma sets_pair_measure_cong[measurable_cong, cong]: |
40 lemma%unimportant sets_pair_measure_cong[measurable_cong, cong]: |
41 "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')" |
41 "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')" |
42 unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) |
42 unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) |
43 |
43 |
44 lemma pair_measureI[intro, simp, measurable]: |
44 lemma%unimportant pair_measureI[intro, simp, measurable]: |
45 "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^sub>M B)" |
45 "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^sub>M B)" |
46 by (auto simp: sets_pair_measure) |
46 by (auto simp: sets_pair_measure) |
47 |
47 |
48 lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)" |
48 lemma%unimportant sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)" |
49 using pair_measureI[of "{x}" M1 "{y}" M2] by simp |
49 using pair_measureI[of "{x}" M1 "{y}" M2] by simp |
50 |
50 |
51 lemma measurable_pair_measureI: |
51 lemma%unimportant measurable_pair_measureI: |
52 assumes 1: "f \<in> space M \<rightarrow> space M1 \<times> space M2" |
52 assumes 1: "f \<in> space M \<rightarrow> space M1 \<times> space M2" |
53 assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M" |
53 assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M" |
54 shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
54 shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
55 unfolding pair_measure_def using 1 2 |
55 unfolding pair_measure_def using 1 2 |
56 by (intro measurable_measure_of) (auto dest: sets.sets_into_space) |
56 by (intro measurable_measure_of) (auto dest: sets.sets_into_space) |
57 |
57 |
58 lemma measurable_split_replace[measurable (raw)]: |
58 lemma%unimportant measurable_split_replace[measurable (raw)]: |
59 "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. case_prod (f x) (g x)) \<in> measurable M N" |
59 "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. case_prod (f x) (g x)) \<in> measurable M N" |
60 unfolding split_beta' . |
60 unfolding split_beta' . |
61 |
61 |
62 lemma measurable_Pair[measurable (raw)]: |
62 lemma%important measurable_Pair[measurable (raw)]: |
63 assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2" |
63 assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2" |
64 shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
64 shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
65 proof (rule measurable_pair_measureI) |
65 proof%unimportant (rule measurable_pair_measureI) |
66 show "(\<lambda>x. (f x, g x)) \<in> space M \<rightarrow> space M1 \<times> space M2" |
66 show "(\<lambda>x. (f x, g x)) \<in> space M \<rightarrow> space M1 \<times> space M2" |
67 using f g by (auto simp: measurable_def) |
67 using f g by (auto simp: measurable_def) |
68 fix A B assume *: "A \<in> sets M1" "B \<in> sets M2" |
68 fix A B assume *: "A \<in> sets M1" "B \<in> sets M2" |
69 have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)" |
69 have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)" |
70 by auto |
70 by auto |
71 also have "\<dots> \<in> sets M" |
71 also have "\<dots> \<in> sets M" |
72 by (rule sets.Int) (auto intro!: measurable_sets * f g) |
72 by (rule sets.Int) (auto intro!: measurable_sets * f g) |
73 finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" . |
73 finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" . |
74 qed |
74 qed |
75 |
75 |
76 lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^sub>M M2) M1" |
76 lemma%unimportant measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^sub>M M2) M1" |
77 by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times |
77 by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times |
78 measurable_def) |
78 measurable_def) |
79 |
79 |
80 lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^sub>M M2) M2" |
80 lemma%unimportant measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^sub>M M2) M2" |
81 by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times |
81 by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times |
82 measurable_def) |
82 measurable_def) |
83 |
83 |
84 lemma measurable_Pair_compose_split[measurable_dest]: |
84 lemma%unimportant measurable_Pair_compose_split[measurable_dest]: |
85 assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N" |
85 assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N" |
86 assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2" |
86 assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2" |
87 shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N" |
87 shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N" |
88 using measurable_compose[OF measurable_Pair f, OF g h] by simp |
88 using measurable_compose[OF measurable_Pair f, OF g h] by simp |
89 |
89 |
90 lemma measurable_Pair1_compose[measurable_dest]: |
90 lemma%unimportant measurable_Pair1_compose[measurable_dest]: |
91 assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
91 assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
92 assumes [measurable]: "h \<in> measurable N M" |
92 assumes [measurable]: "h \<in> measurable N M" |
93 shows "(\<lambda>x. f (h x)) \<in> measurable N M1" |
93 shows "(\<lambda>x. f (h x)) \<in> measurable N M1" |
94 using measurable_compose[OF f measurable_fst] by simp |
94 using measurable_compose[OF f measurable_fst] by simp |
95 |
95 |
96 lemma measurable_Pair2_compose[measurable_dest]: |
96 lemma%unimportant measurable_Pair2_compose[measurable_dest]: |
97 assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
97 assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
98 assumes [measurable]: "h \<in> measurable N M" |
98 assumes [measurable]: "h \<in> measurable N M" |
99 shows "(\<lambda>x. g (h x)) \<in> measurable N M2" |
99 shows "(\<lambda>x. g (h x)) \<in> measurable N M2" |
100 using measurable_compose[OF f measurable_snd] by simp |
100 using measurable_compose[OF f measurable_snd] by simp |
101 |
101 |
102 lemma measurable_pair: |
102 lemma%unimportant measurable_pair: |
103 assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" |
103 assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" |
104 shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
104 shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)" |
105 using measurable_Pair[OF assms] by simp |
105 using measurable_Pair[OF assms] by simp |
106 |
106 |
107 lemma |
107 lemma%unimportant (*FIX ME needs a name *) |
108 assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)" |
108 assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)" |
109 shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N" |
109 shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N" |
110 and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P" |
110 and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P" |
111 by simp_all |
111 by simp_all |
112 |
112 |
113 lemma |
113 lemma%unimportant (*FIX ME needs a name *) |
114 assumes f[measurable]: "f \<in> measurable M N" |
114 assumes f[measurable]: "f \<in> measurable M N" |
115 shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^sub>M P) N" |
115 shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^sub>M P) N" |
116 and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N" |
116 and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N" |
117 by simp_all |
117 by simp_all |
118 |
118 |
119 lemma sets_pair_in_sets: |
119 lemma%unimportant sets_pair_in_sets: |
120 assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N" |
120 assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N" |
121 shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N" |
121 shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N" |
122 unfolding sets_pair_measure |
122 unfolding sets_pair_measure |
123 by (intro sets.sigma_sets_subset') (auto intro!: assms) |
123 by (intro sets.sigma_sets_subset') (auto intro!: assms) |
124 |
124 |
125 lemma sets_pair_eq_sets_fst_snd: |
125 lemma%important sets_pair_eq_sets_fst_snd: |
126 "sets (A \<Otimes>\<^sub>M B) = sets (Sup {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})" |
126 "sets (A \<Otimes>\<^sub>M B) = sets (Sup {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})" |
127 (is "?P = sets (Sup {?fst, ?snd})") |
127 (is "?P = sets (Sup {?fst, ?snd})") |
128 proof - |
128 proof%unimportant - |
129 { fix a b assume ab: "a \<in> sets A" "b \<in> sets B" |
129 { fix a b assume ab: "a \<in> sets A" "b \<in> sets B" |
130 then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))" |
130 then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))" |
131 by (auto dest: sets.sets_into_space) |
131 by (auto dest: sets.sets_into_space) |
132 also have "\<dots> \<in> sets (Sup {?fst, ?snd})" |
132 also have "\<dots> \<in> sets (Sup {?fst, ?snd})" |
133 apply (rule sets.Int) |
133 apply (rule sets.Int) |
155 apply (simp add: space_pair_measure) |
155 apply (simp add: space_pair_measure) |
156 apply (auto simp add: space_pair_measure) |
156 apply (auto simp add: space_pair_measure) |
157 done |
157 done |
158 qed |
158 qed |
159 |
159 |
160 lemma measurable_pair_iff: |
160 lemma%unimportant measurable_pair_iff: |
161 "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" |
161 "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" |
162 by (auto intro: measurable_pair[of f M M1 M2]) |
162 by (auto intro: measurable_pair[of f M M1 M2]) |
163 |
163 |
164 lemma measurable_split_conv: |
164 lemma%unimportant measurable_split_conv: |
165 "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B" |
165 "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B" |
166 by (intro arg_cong2[where f="(\<in>)"]) auto |
166 by (intro arg_cong2[where f="(\<in>)"]) auto |
167 |
167 |
168 lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (M2 \<Otimes>\<^sub>M M1)" |
168 lemma%unimportant measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (M2 \<Otimes>\<^sub>M M1)" |
169 by (auto intro!: measurable_Pair simp: measurable_split_conv) |
169 by (auto intro!: measurable_Pair simp: measurable_split_conv) |
170 |
170 |
171 lemma measurable_pair_swap: |
171 lemma%unimportant measurable_pair_swap: |
172 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^sub>M M1) M" |
172 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^sub>M M1) M" |
173 using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def) |
173 using measurable_comp[OF measurable_Pair f] by (auto simp: measurable_split_conv comp_def) |
174 |
174 |
175 lemma measurable_pair_swap_iff: |
175 lemma%unimportant measurable_pair_swap_iff: |
176 "f \<in> measurable (M2 \<Otimes>\<^sub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" |
176 "f \<in> measurable (M2 \<Otimes>\<^sub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" |
177 by (auto dest: measurable_pair_swap) |
177 by (auto dest: measurable_pair_swap) |
178 |
178 |
179 lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^sub>M M2)" |
179 lemma%unimportant measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^sub>M M2)" |
180 by simp |
180 by simp |
181 |
181 |
182 lemma sets_Pair1[measurable (raw)]: |
182 lemma%unimportant sets_Pair1[measurable (raw)]: |
183 assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "Pair x -` A \<in> sets M2" |
183 assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "Pair x -` A \<in> sets M2" |
184 proof - |
184 proof - |
185 have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})" |
185 have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})" |
186 using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
186 using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
187 also have "\<dots> \<in> sets M2" |
187 also have "\<dots> \<in> sets M2" |
188 using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: if_split_asm) |
188 using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: if_split_asm) |
189 finally show ?thesis . |
189 finally show ?thesis . |
190 qed |
190 qed |
191 |
191 |
192 lemma measurable_Pair2': "y \<in> space M2 \<Longrightarrow> (\<lambda>x. (x, y)) \<in> measurable M1 (M1 \<Otimes>\<^sub>M M2)" |
192 lemma%unimportant measurable_Pair2': "y \<in> space M2 \<Longrightarrow> (\<lambda>x. (x, y)) \<in> measurable M1 (M1 \<Otimes>\<^sub>M M2)" |
193 by (auto intro!: measurable_Pair) |
193 by (auto intro!: measurable_Pair) |
194 |
194 |
195 lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1" |
195 lemma%unimportant sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1" |
196 proof - |
196 proof - |
197 have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})" |
197 have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})" |
198 using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
198 using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
199 also have "\<dots> \<in> sets M1" |
199 also have "\<dots> \<in> sets M1" |
200 using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: if_split_asm) |
200 using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: if_split_asm) |
201 finally show ?thesis . |
201 finally show ?thesis . |
202 qed |
202 qed |
203 |
203 |
204 lemma measurable_Pair2: |
204 lemma%unimportant measurable_Pair2: |
205 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" and x: "x \<in> space M1" |
205 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" and x: "x \<in> space M1" |
206 shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M" |
206 shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M" |
207 using measurable_comp[OF measurable_Pair1' f, OF x] |
207 using measurable_comp[OF measurable_Pair1' f, OF x] |
208 by (simp add: comp_def) |
208 by (simp add: comp_def) |
209 |
209 |
210 lemma measurable_Pair1: |
210 lemma%unimportant measurable_Pair1: |
211 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" and y: "y \<in> space M2" |
211 assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" and y: "y \<in> space M2" |
212 shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M" |
212 shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M" |
213 using measurable_comp[OF measurable_Pair2' f, OF y] |
213 using measurable_comp[OF measurable_Pair2' f, OF y] |
214 by (simp add: comp_def) |
214 by (simp add: comp_def) |
215 |
215 |
216 lemma Int_stable_pair_measure_generator: "Int_stable {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}" |
216 lemma%unimportant Int_stable_pair_measure_generator: "Int_stable {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}" |
217 unfolding Int_stable_def |
217 unfolding Int_stable_def |
218 by safe (auto simp add: times_Int_times) |
218 by safe (auto simp add: times_Int_times) |
219 |
219 |
220 lemma (in finite_measure) finite_measure_cut_measurable: |
220 lemma%unimportant (in finite_measure) finite_measure_cut_measurable: |
221 assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)" |
221 assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)" |
222 shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" |
222 shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" |
223 (is "?s Q \<in> _") |
223 (is "?s Q \<in> _") |
224 using Int_stable_pair_measure_generator pair_measure_closed assms |
224 using Int_stable_pair_measure_generator pair_measure_closed assms |
225 unfolding sets_pair_measure |
225 unfolding sets_pair_measure |
312 qed |
312 qed |
313 show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)" |
313 show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)" |
314 using sets.space_closed[of N] sets.space_closed[of M] by auto |
314 using sets.space_closed[of N] sets.space_closed[of M] by auto |
315 qed fact |
315 qed fact |
316 |
316 |
317 lemma (in sigma_finite_measure) emeasure_pair_measure_alt: |
317 lemma%unimportant (in sigma_finite_measure) emeasure_pair_measure_alt: |
318 assumes X: "X \<in> sets (N \<Otimes>\<^sub>M M)" |
318 assumes X: "X \<in> sets (N \<Otimes>\<^sub>M M)" |
319 shows "emeasure (N \<Otimes>\<^sub>M M) X = (\<integral>\<^sup>+x. emeasure M (Pair x -` X) \<partial>N)" |
319 shows "emeasure (N \<Otimes>\<^sub>M M) X = (\<integral>\<^sup>+x. emeasure M (Pair x -` X) \<partial>N)" |
320 proof - |
320 proof - |
321 have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y" |
321 have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y" |
322 by (auto simp: indicator_def) |
322 by (auto simp: indicator_def) |
323 show ?thesis |
323 show ?thesis |
324 using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1) |
324 using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1) |
325 qed |
325 qed |
326 |
326 |
327 lemma (in sigma_finite_measure) emeasure_pair_measure_Times: |
327 lemma%important (in sigma_finite_measure) emeasure_pair_measure_Times: |
328 assumes A: "A \<in> sets N" and B: "B \<in> sets M" |
328 assumes A: "A \<in> sets N" and B: "B \<in> sets M" |
329 shows "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = emeasure N A * emeasure M B" |
329 shows "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = emeasure N A * emeasure M B" |
330 proof - |
330 proof%unimportant - |
331 have "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = (\<integral>\<^sup>+x. emeasure M B * indicator A x \<partial>N)" |
331 have "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = (\<integral>\<^sup>+x. emeasure M B * indicator A x \<partial>N)" |
332 using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt) |
332 using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt) |
333 also have "\<dots> = emeasure M B * emeasure N A" |
333 also have "\<dots> = emeasure M B * emeasure N A" |
334 using A by (simp add: nn_integral_cmult_indicator) |
334 using A by (simp add: nn_integral_cmult_indicator) |
335 finally show ?thesis |
335 finally show ?thesis |
336 by (simp add: ac_simps) |
336 by (simp add: ac_simps) |
337 qed |
337 qed |
338 |
338 |
339 subsection \<open>Binary products of $\sigma$-finite emeasure spaces\<close> |
339 subsection%important \<open>Binary products of $\sigma$-finite emeasure spaces\<close> |
340 |
340 |
341 locale pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2 |
341 locale%important pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2 |
342 for M1 :: "'a measure" and M2 :: "'b measure" |
342 for M1 :: "'a measure" and M2 :: "'b measure" |
343 |
343 |
344 lemma (in pair_sigma_finite) measurable_emeasure_Pair1: |
344 lemma%unimportant (in pair_sigma_finite) measurable_emeasure_Pair1: |
345 "Q \<in> sets (M1 \<Otimes>\<^sub>M M2) \<Longrightarrow> (\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1" |
345 "Q \<in> sets (M1 \<Otimes>\<^sub>M M2) \<Longrightarrow> (\<lambda>x. emeasure M2 (Pair x -` Q)) \<in> borel_measurable M1" |
346 using M2.measurable_emeasure_Pair . |
346 using M2.measurable_emeasure_Pair . |
347 |
347 |
348 lemma (in pair_sigma_finite) measurable_emeasure_Pair2: |
348 lemma%important (in pair_sigma_finite) measurable_emeasure_Pair2: |
349 assumes Q: "Q \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "(\<lambda>y. emeasure M1 ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2" |
349 assumes Q: "Q \<in> sets (M1 \<Otimes>\<^sub>M M2)" shows "(\<lambda>y. emeasure M1 ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2" |
350 proof - |
350 proof%unimportant - |
351 have "(\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^sub>M M1) \<in> sets (M2 \<Otimes>\<^sub>M M1)" |
351 have "(\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^sub>M M1) \<in> sets (M2 \<Otimes>\<^sub>M M1)" |
352 using Q measurable_pair_swap' by (auto intro: measurable_sets) |
352 using Q measurable_pair_swap' by (auto intro: measurable_sets) |
353 note M1.measurable_emeasure_Pair[OF this] |
353 note M1.measurable_emeasure_Pair[OF this] |
354 moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^sub>M M1)) = (\<lambda>x. (x, y)) -` Q" |
354 moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^sub>M M1)) = (\<lambda>x. (x, y)) -` Q" |
355 using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
355 using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure) |
356 ultimately show ?thesis by simp |
356 ultimately show ?thesis by simp |
357 qed |
357 qed |
358 |
358 |
359 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: |
359 lemma%important (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: |
360 defines "E \<equiv> {A \<times> B | A B. A \<in> sets M1 \<and> B \<in> sets M2}" |
360 defines "E \<equiv> {A \<times> B | A B. A \<in> sets M1 \<and> B \<in> sets M2}" |
361 shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and> |
361 shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and> |
362 (\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>)" |
362 (\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>)" |
363 proof - |
363 proof%unimportant - |
364 from M1.sigma_finite_incseq guess F1 . note F1 = this |
364 from M1.sigma_finite_incseq guess F1 . note F1 = this |
365 from M2.sigma_finite_incseq guess F2 . note F2 = this |
365 from M2.sigma_finite_incseq guess F2 . note F2 = this |
366 from F1 F2 have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto |
366 from F1 F2 have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto |
367 let ?F = "\<lambda>i. F1 i \<times> F2 i" |
367 let ?F = "\<lambda>i. F1 i \<times> F2 i" |
368 show ?thesis |
368 show ?thesis |
392 with F1 F2 show "emeasure (M1 \<Otimes>\<^sub>M M2) (F1 i \<times> F2 i) \<noteq> \<infinity>" |
392 with F1 F2 show "emeasure (M1 \<Otimes>\<^sub>M M2) (F1 i \<times> F2 i) \<noteq> \<infinity>" |
393 by (auto simp add: emeasure_pair_measure_Times ennreal_mult_eq_top_iff) |
393 by (auto simp add: emeasure_pair_measure_Times ennreal_mult_eq_top_iff) |
394 qed |
394 qed |
395 qed |
395 qed |
396 |
396 |
397 sublocale pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2" |
397 sublocale%important pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2" |
398 proof |
398 proof |
399 from M1.sigma_finite_countable guess F1 .. |
399 from M1.sigma_finite_countable guess F1 .. |
400 moreover from M2.sigma_finite_countable guess F2 .. |
400 moreover from M2.sigma_finite_countable guess F2 .. |
401 ultimately show |
401 ultimately show |
402 "\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)" |
402 "\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)" |
403 by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI) |
403 by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI) |
404 (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff) |
404 (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff) |
405 qed |
405 qed |
406 |
406 |
407 lemma sigma_finite_pair_measure: |
407 lemma%unimportant sigma_finite_pair_measure: |
408 assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B" |
408 assumes A: "sigma_finite_measure A" and B: "sigma_finite_measure B" |
409 shows "sigma_finite_measure (A \<Otimes>\<^sub>M B)" |
409 shows "sigma_finite_measure (A \<Otimes>\<^sub>M B)" |
410 proof - |
410 proof - |
411 interpret A: sigma_finite_measure A by fact |
411 interpret A: sigma_finite_measure A by fact |
412 interpret B: sigma_finite_measure B by fact |
412 interpret B: sigma_finite_measure B by fact |
413 interpret AB: pair_sigma_finite A B .. |
413 interpret AB: pair_sigma_finite A B .. |
414 show ?thesis .. |
414 show ?thesis .. |
415 qed |
415 qed |
416 |
416 |
417 lemma sets_pair_swap: |
417 lemma%unimportant sets_pair_swap: |
418 assumes "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" |
418 assumes "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" |
419 shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^sub>M M1) \<in> sets (M2 \<Otimes>\<^sub>M M1)" |
419 shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^sub>M M1) \<in> sets (M2 \<Otimes>\<^sub>M M1)" |
420 using measurable_pair_swap' assms by (rule measurable_sets) |
420 using measurable_pair_swap' assms by (rule measurable_sets) |
421 |
421 |
422 lemma (in pair_sigma_finite) distr_pair_swap: |
422 lemma%important (in pair_sigma_finite) distr_pair_swap: |
423 "M1 \<Otimes>\<^sub>M M2 = distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D") |
423 "M1 \<Otimes>\<^sub>M M2 = distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D") |
424 proof - |
424 proof%unimportant - |
425 from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this |
425 from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this |
426 let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}" |
426 let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}" |
427 show ?thesis |
427 show ?thesis |
428 proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) |
428 proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) |
429 show "?E \<subseteq> Pow (space ?P)" |
429 show "?E \<subseteq> Pow (space ?P)" |
559 by (rule measurable_cong[THEN iffD1]) |
559 by (rule measurable_cong[THEN iffD1]) |
560 qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1 |
560 qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1 |
561 nn_integral_monotone_convergence_SUP incseq_def le_fun_def |
561 nn_integral_monotone_convergence_SUP incseq_def le_fun_def |
562 cong: measurable_cong) |
562 cong: measurable_cong) |
563 |
563 |
564 lemma (in sigma_finite_measure) nn_integral_fst: |
564 lemma%unimportant (in sigma_finite_measure) nn_integral_fst: |
565 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" |
565 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" |
566 shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _") |
566 shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _") |
567 using f proof induct |
567 using f proof induct |
568 case (cong u v) |
568 case (cong u v) |
569 then have "?I u = ?I v" |
569 then have "?I u = ?I v" |
570 by (intro nn_integral_cong) (auto simp: space_pair_measure) |
570 by (intro nn_integral_cong) (auto simp: space_pair_measure) |
571 with cong show ?case |
571 with cong show ?case |
572 by (simp cong: nn_integral_cong) |
572 by (simp cong: nn_integral_cong) |
573 qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add |
573 qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add |
574 nn_integral_monotone_convergence_SUP measurable_compose_Pair1 |
574 nn_integral_monotone_convergence_SUP measurable_compose_Pair1 |
575 borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def |
575 borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def |
576 cong: nn_integral_cong) |
576 cong: nn_integral_cong) |
577 |
577 |
578 lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]: |
578 lemma%unimportant (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]: |
579 "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N" |
579 "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N" |
580 using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp |
580 using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp |
581 |
581 |
582 lemma (in pair_sigma_finite) nn_integral_snd: |
582 lemma%important (in pair_sigma_finite) nn_integral_snd: |
583 assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
583 assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
584 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f" |
584 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f" |
585 proof - |
585 proof%unimportant - |
586 note measurable_pair_swap[OF f] |
586 note measurable_pair_swap[OF f] |
587 from M1.nn_integral_fst[OF this] |
587 from M1.nn_integral_fst[OF this] |
588 have "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1))" |
588 have "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1))" |
589 by simp |
589 by simp |
590 also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f" |
590 also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f" |
591 by (subst distr_pair_swap) (auto simp add: nn_integral_distr intro!: nn_integral_cong) |
591 by (subst distr_pair_swap) (auto simp add: nn_integral_distr intro!: nn_integral_cong) |
592 finally show ?thesis . |
592 finally show ?thesis . |
593 qed |
593 qed |
594 |
594 |
595 lemma (in pair_sigma_finite) Fubini: |
595 lemma%important (in pair_sigma_finite) Fubini: |
596 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
596 assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
597 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)" |
597 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)" |
598 unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] .. |
598 unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] .. |
599 |
599 |
600 lemma (in pair_sigma_finite) Fubini': |
600 lemma%important (in pair_sigma_finite) Fubini': |
601 assumes f: "case_prod f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
601 assumes f: "case_prod f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)" |
602 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f x y \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f x y \<partial>M2) \<partial>M1)" |
602 shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f x y \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f x y \<partial>M2) \<partial>M1)" |
603 using Fubini[OF f] by simp |
603 using Fubini[OF f] by simp |
604 |
604 |
605 subsection \<open>Products on counting spaces, densities and distributions\<close> |
605 subsection%important \<open>Products on counting spaces, densities and distributions\<close> |
606 |
606 |
607 lemma sigma_prod: |
607 lemma%important sigma_prod: |
608 assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X" |
608 assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X" |
609 assumes Y_cover: "\<exists>E\<subseteq>B. countable E \<and> Y = \<Union>E" and B: "B \<subseteq> Pow Y" |
609 assumes Y_cover: "\<exists>E\<subseteq>B. countable E \<and> Y = \<Union>E" and B: "B \<subseteq> Pow Y" |
610 shows "sigma X A \<Otimes>\<^sub>M sigma Y B = sigma (X \<times> Y) {a \<times> b | a b. a \<in> A \<and> b \<in> B}" |
610 shows "sigma X A \<Otimes>\<^sub>M sigma Y B = sigma (X \<times> Y) {a \<times> b | a b. a \<in> A \<and> b \<in> B}" |
611 (is "?P = ?S") |
611 (is "?P = ?S") |
612 proof (rule measure_eqI) |
612 proof%unimportant (rule measure_eqI) |
613 have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X" |
613 have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X" |
614 by auto |
614 by auto |
615 let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}" |
615 let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}" |
616 have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)" |
616 have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)" |
617 by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B) |
617 by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B) |
774 done |
774 done |
775 finally show "emeasure ?P X = emeasure ?C X" . |
775 finally show "emeasure ?P X = emeasure ?C X" . |
776 qed |
776 qed |
777 |
777 |
778 |
778 |
779 lemma emeasure_prod_count_space: |
779 lemma%unimportant emeasure_prod_count_space: |
780 assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M M)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)") |
780 assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M M)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)") |
781 shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator A (x, y) \<partial>?B \<partial>?A)" |
781 shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator A (x, y) \<partial>?B \<partial>?A)" |
782 by (rule emeasure_measure_of[OF pair_measure_def]) |
782 by (rule emeasure_measure_of[OF pair_measure_def]) |
783 (auto simp: countably_additive_def positive_def suminf_indicator A |
783 (auto simp: countably_additive_def positive_def suminf_indicator A |
784 nn_integral_suminf[symmetric] dest: sets.sets_into_space) |
784 nn_integral_suminf[symmetric] dest: sets.sets_into_space) |
785 |
785 |
786 lemma emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) {x} = 1" |
786 lemma%unimportant emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) {x} = 1" |
787 proof - |
787 proof - |
788 have [simp]: "\<And>a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ennreal)" |
788 have [simp]: "\<And>a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ennreal)" |
789 by (auto split: split_indicator) |
789 by (auto split: split_indicator) |
790 show ?thesis |
790 show ?thesis |
791 by (cases x) (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair) |
791 by (cases x) (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair) |
792 qed |
792 qed |
793 |
793 |
794 lemma emeasure_count_space_prod_eq: |
794 lemma%important emeasure_count_space_prod_eq: |
795 fixes A :: "('a \<times> 'b) set" |
795 fixes A :: "('a \<times> 'b) set" |
796 assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M count_space UNIV)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)") |
796 assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M count_space UNIV)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)") |
797 shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = emeasure (count_space UNIV) A" |
797 shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = emeasure (count_space UNIV) A" |
798 proof - |
798 proof%unimportant - |
799 { fix A :: "('a \<times> 'b) set" assume "countable A" |
799 { fix A :: "('a \<times> 'b) set" assume "countable A" |
800 then have "emeasure (?A \<Otimes>\<^sub>M ?B) (\<Union>a\<in>A. {a}) = (\<integral>\<^sup>+a. emeasure (?A \<Otimes>\<^sub>M ?B) {a} \<partial>count_space A)" |
800 then have "emeasure (?A \<Otimes>\<^sub>M ?B) (\<Union>a\<in>A. {a}) = (\<integral>\<^sup>+a. emeasure (?A \<Otimes>\<^sub>M ?B) {a} \<partial>count_space A)" |
801 by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def) |
801 by (intro emeasure_UN_countable) (auto simp: sets_Pair disjoint_family_on_def) |
802 also have "\<dots> = (\<integral>\<^sup>+a. indicator A a \<partial>count_space UNIV)" |
802 also have "\<dots> = (\<integral>\<^sup>+a. indicator A a \<partial>count_space UNIV)" |
803 by (subst nn_integral_count_space_indicator) auto |
803 by (subst nn_integral_count_space_indicator) auto |