|
1 (* Title: HOL/Probability/Convolution.thy |
|
2 Author: Sudeep Kanav, TU München |
|
3 Author: Johannes Hölzl, TU München *) |
|
4 |
|
5 header {* Convolution Measure *} |
|
6 |
|
7 theory Convolution |
|
8 imports Independent_Family |
|
9 begin |
|
10 |
|
11 lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M" |
|
12 .. |
|
13 |
|
14 definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where |
|
15 "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)" |
|
16 |
|
17 lemma |
|
18 shows space_convolution[simp]: "space (convolution M N) = space borel" |
|
19 and sets_convolution[simp]: "sets (convolution M N) = sets borel" |
|
20 and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel" |
|
21 and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B" |
|
22 by (simp_all add: convolution_def) |
|
23 |
|
24 lemma nn_integral_convolution: |
|
25 assumes "finite_measure M" "finite_measure N" |
|
26 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
|
27 assumes [measurable]: "f \<in> borel_measurable borel" |
|
28 shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)" |
|
29 proof - |
|
30 interpret M: finite_measure M by fact |
|
31 interpret N: finite_measure N by fact |
|
32 interpret pair_sigma_finite M N .. |
|
33 show ?thesis |
|
34 unfolding convolution_def |
|
35 by (simp add: nn_integral_distr N.nn_integral_fst[symmetric]) |
|
36 qed |
|
37 |
|
38 lemma convolution_emeasure: |
|
39 assumes "A \<in> sets borel" "finite_measure M" "finite_measure N" |
|
40 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
|
41 assumes [simp]: "space M = space N" "space N = space borel" |
|
42 shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M " |
|
43 using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution |
|
44 nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator) |
|
45 |
|
46 lemma convolution_emeasure': |
|
47 assumes [simp]:"A \<in> sets borel" |
|
48 assumes [simp]: "finite_measure M" "finite_measure N" |
|
49 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
|
50 shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. (indicator A (x + y)) \<partial>N \<partial>M" |
|
51 by (auto simp del: nn_integral_indicator simp: nn_integral_convolution |
|
52 nn_integral_indicator[symmetric] borel_measurable_indicator) |
|
53 |
|
54 lemma convolution_finite: |
|
55 assumes [simp]: "finite_measure M" "finite_measure N" |
|
56 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
|
57 shows "finite_measure (M \<star> N)" |
|
58 unfolding convolution_def |
|
59 by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto |
|
60 |
|
61 lemma convolution_emeasure_3: |
|
62 assumes [simp, measurable]: "A \<in> sets borel" |
|
63 assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L" |
|
64 assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel" |
|
65 shows "emeasure (L \<star> (M \<star> N )) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. \<integral>\<^sup>+z. indicator A (x + y + z) \<partial>N \<partial>M \<partial>L" |
|
66 apply (subst nn_integral_indicator[symmetric], simp) |
|
67 apply (subst nn_integral_convolution, |
|
68 auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+ |
|
69 by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add_assoc) |
|
70 |
|
71 lemma convolution_emeasure_3': |
|
72 assumes [simp, measurable]:"A \<in> sets borel" |
|
73 assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L" |
|
74 assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel" |
|
75 shows "emeasure ((L \<star> M) \<star> N ) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. \<integral>\<^sup>+z. indicator A (x + y + z) \<partial>N \<partial>M \<partial>L" |
|
76 apply (subst nn_integral_indicator[symmetric], simp)+ |
|
77 apply (subst nn_integral_convolution) |
|
78 apply (simp_all add: convolution_finite) |
|
79 apply (subst nn_integral_convolution) |
|
80 apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral) |
|
81 done |
|
82 |
|
83 lemma convolution_commutative: |
|
84 assumes [simp]: "finite_measure M" "finite_measure N" |
|
85 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
|
86 shows "(M \<star> N) = (N \<star> M)" |
|
87 proof (rule measure_eqI) |
|
88 interpret M: finite_measure M by fact |
|
89 interpret N: finite_measure N by fact |
|
90 interpret pair_sigma_finite M N .. |
|
91 |
|
92 show "sets (M \<star> N) = sets (N \<star> M)" by simp |
|
93 |
|
94 fix A assume "A \<in> sets (M \<star> N)" |
|
95 then have 1[measurable]:"A \<in> sets borel" by simp |
|
96 have "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator A (x + y) \<partial>N \<partial>M" by (auto intro!: convolution_emeasure') |
|
97 also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>N \<partial>M" by (auto intro!: nn_integral_cong) |
|
98 also have "... = \<integral>\<^sup>+y. \<integral>\<^sup>+x. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>M \<partial>N" by (rule Fubini[symmetric]) simp |
|
99 also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add_commute convolution_emeasure') |
|
100 finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp |
|
101 qed |
|
102 |
|
103 lemma convolution_associative: |
|
104 assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L" |
|
105 assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel" |
|
106 shows "(L \<star> (M \<star> N)) = ((L \<star> M) \<star> N)" |
|
107 by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3') |
|
108 |
|
109 lemma (in prob_space) sum_indep_random_variable: |
|
110 assumes ind: "indep_var borel X borel Y" |
|
111 assumes [simp, measurable]: "random_variable borel X" |
|
112 assumes [simp, measurable]: "random_variable borel Y" |
|
113 shows "distr M borel (\<lambda>x. X x + Y x) = convolution (distr M borel X) (distr M borel Y)" |
|
114 using ind unfolding indep_var_distribution_eq convolution_def |
|
115 by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"]) |
|
116 |
|
117 lemma (in prob_space) sum_indep_random_variable_lborel: |
|
118 assumes ind: "indep_var borel X borel Y" |
|
119 assumes [simp, measurable]: "random_variable lborel X" |
|
120 assumes [simp, measurable]:"random_variable lborel Y" |
|
121 shows "distr M lborel (\<lambda>x. X x + Y x) = convolution (distr M lborel X) (distr M lborel Y)" |
|
122 using ind unfolding indep_var_distribution_eq convolution_def |
|
123 by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong) |
|
124 |
|
125 lemma convolution_density: |
|
126 fixes f g :: "real \<Rightarrow> ereal" |
|
127 assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" |
|
128 assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)" |
|
129 assumes gt_0[simp]: "AE x in lborel. 0 \<le> f x" "AE x in lborel. 0 \<le> g x" |
|
130 shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)" |
|
131 (is "?l = ?r") |
|
132 proof (intro measure_eqI) |
|
133 fix A assume "A \<in> sets ?l" |
|
134 then have [measurable]: "A \<in> sets borel" |
|
135 by simp |
|
136 |
|
137 have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) = |
|
138 (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)" |
|
139 using gt_0 |
|
140 proof (intro nn_integral_cong_AE, eventually_elim) |
|
141 fix x assume "0 \<le> f x" |
|
142 then have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) = |
|
143 (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)" |
|
144 by (intro nn_integral_cmult[symmetric]) auto |
|
145 then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) = |
|
146 (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)" |
|
147 by (simp add: ac_simps) |
|
148 qed |
|
149 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)" |
|
150 by (intro lborel_pair.Fubini') simp |
|
151 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)" |
|
152 using gt_0 |
|
153 proof (intro nn_integral_cong_AE, eventually_elim) |
|
154 fix y assume "0 \<le> g y" |
|
155 then have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) = |
|
156 g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)" |
|
157 by (intro nn_integral_cmult) auto |
|
158 also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)" |
|
159 using gt_0 |
|
160 by (subst nn_integral_real_affine[where c=1 and t="-y"]) |
|
161 (auto simp del: gt_0 simp add: one_ereal_def[symmetric]) |
|
162 also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)" |
|
163 using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto |
|
164 finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) = |
|
165 (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)" |
|
166 by (simp add: ac_simps) |
|
167 qed |
|
168 also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)" |
|
169 by (intro lborel_pair.Fubini') simp |
|
170 finally show "emeasure ?l A = emeasure ?r A" |
|
171 by (auto simp: convolution_emeasure' nn_integral_density emeasure_density |
|
172 nn_integral_multc) |
|
173 qed simp |
|
174 |
|
175 lemma (in prob_space) distributed_finite_measure_density: |
|
176 "distributed M N X f \<Longrightarrow> finite_measure (density N f)" |
|
177 using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp |
|
178 |
|
179 |
|
180 lemma (in prob_space) distributed_convolution: |
|
181 fixes f :: "real \<Rightarrow> _" |
|
182 fixes g :: "real \<Rightarrow> _" |
|
183 assumes indep: "indep_var borel X borel Y" |
|
184 assumes X: "distributed M lborel X f" |
|
185 assumes Y: "distributed M lborel Y g" |
|
186 shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)" |
|
187 unfolding distributed_def |
|
188 proof safe |
|
189 show "AE x in lborel. 0 \<le> \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel" |
|
190 by (auto simp: nn_integral_nonneg) |
|
191 |
|
192 have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" |
|
193 using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all |
|
194 |
|
195 show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel" |
|
196 by measurable |
|
197 |
|
198 have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)" |
|
199 using distributed_measurable[OF X] distributed_measurable[OF Y] |
|
200 by (intro sum_indep_random_variable) (auto simp: indep) |
|
201 also have "\<dots> = (density lborel f \<star> density lborel g)" |
|
202 using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] |
|
203 by (simp cong: distr_cong) |
|
204 also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)" |
|
205 proof (rule convolution_density) |
|
206 show "finite_measure (density lborel f)" |
|
207 using X by (rule distributed_finite_measure_density) |
|
208 show "finite_measure (density lborel g)" |
|
209 using Y by (rule distributed_finite_measure_density) |
|
210 show "AE x in lborel. 0 \<le> f x" |
|
211 using X by (rule distributed_AE) |
|
212 show "AE x in lborel. 0 \<le> g x" |
|
213 using Y by (rule distributed_AE) |
|
214 qed fact+ |
|
215 finally show "distr M lborel (\<lambda>x. X x + Y x) = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)" |
|
216 by (simp cong: distr_cong) |
|
217 show "random_variable lborel (\<lambda>x. X x + Y x)" |
|
218 using distributed_measurable[OF X] distributed_measurable[OF Y] by simp |
|
219 qed |
|
220 |
|
221 lemma prob_space_convolution_density: |
|
222 fixes f:: "real \<Rightarrow> _" |
|
223 fixes g:: "real \<Rightarrow> _" |
|
224 assumes [measurable]: "f\<in> borel_measurable borel" |
|
225 assumes [measurable]: "g\<in> borel_measurable borel" |
|
226 assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" |
|
227 assumes "prob_space (density lborel f)" (is "prob_space ?F") |
|
228 assumes "prob_space (density lborel g)" (is "prob_space ?G") |
|
229 shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D") |
|
230 proof (subst convolution_density[symmetric]) |
|
231 interpret F: prob_space ?F by fact |
|
232 show "finite_measure ?F" by unfold_locales |
|
233 interpret G: prob_space ?G by fact |
|
234 show "finite_measure ?G" by unfold_locales |
|
235 interpret FG: pair_prob_space ?F ?G .. |
|
236 |
|
237 show "prob_space (density lborel f \<star> density lborel g)" |
|
238 unfolding convolution_def by (rule FG.prob_space_distr) simp |
|
239 qed simp_all |
|
240 |
|
241 end |