src/HOL/Probability/Convolution.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 59048 7dc8ac6f0895 child 61808 fc1556774cfe permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
1 (*  Title:      HOL/Probability/Convolution.thy
2     Author:     Sudeep Kanav, TU München
3     Author:     Johannes Hölzl, TU München *)
5 section {* Convolution Measure *}
7 theory Convolution
8   imports Independent_Family
9 begin
11 lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
12   ..
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)"
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)
24 lemma nn_integral_convolution:
25   assumes "finite_measure M" "finite_measure N"
26   assumes [measurable_cong]: "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
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] ac_simps split:split_indicator)
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)
54 lemma convolution_finite:
55   assumes [simp]: "finite_measure M" "finite_measure N"
56   assumes [measurable_cong]: "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
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)
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 [measurable_cong, 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
83 lemma convolution_commutative:
84   assumes [simp]: "finite_measure M" "finite_measure N"
85   assumes [measurable_cong, 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 ..
92   show "sets (M \<star> N) = sets (N \<star> M)" by simp
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
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')
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"])
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)
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
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
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
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)
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
195   show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel"
196     by measurable
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
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 ..
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
241 end