1(* Title: HOL/Probability/Convolution.thy 2 Author: Sudeep Kanav, TU M��nchen 3 Author: Johannes H��lzl, TU M��nchen *) 4 5section \<open>Convolution Measure\<close> 6 7theory Convolution 8 imports Independent_Family 9begin 10 11lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M" 12 .. 13 14definition 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 17lemma 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 24lemma 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)" 29proof - 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]) 36qed 37 38lemma 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) 45 46lemma 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 54lemma 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 60 61lemma 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 71lemma 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 82 83lemma 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)" 87proof (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 101qed 102 103lemma 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 109lemma (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 117lemma (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 125lemma convolution_density: 126 fixes f g :: "real \<Rightarrow> ennreal" 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 shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)" 130 (is "?l = ?r") 131proof (intro measure_eqI) 132 fix A assume "A \<in> sets ?l" 133 then have [measurable]: "A \<in> sets borel" 134 by simp 135 136 have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) = 137 (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)" 138 proof (intro nn_integral_cong_AE, eventually_elim) 139 fix x 140 have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) = 141 (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)" 142 by (intro nn_integral_cmult[symmetric]) auto 143 then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) = 144 (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)" 145 by (simp add: ac_simps) 146 qed 147 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)" 148 by (intro lborel_pair.Fubini') simp 149 also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)" 150 proof (intro nn_integral_cong_AE, eventually_elim) 151 fix y 152 have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) = 153 g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)" 154 by (intro nn_integral_cmult) auto 155 also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)" 156 by (subst nn_integral_real_affine[where c=1 and t="-y"]) 157 (auto simp add: one_ennreal_def[symmetric]) 158 also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)" 159 by (intro nn_integral_cmult[symmetric]) auto 160 finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) = 161 (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)" 162 by (simp add: ac_simps) 163 qed 164 also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)" 165 by (intro lborel_pair.Fubini') simp 166 finally show "emeasure ?l A = emeasure ?r A" 167 by (auto simp: convolution_emeasure' nn_integral_density emeasure_density 168 nn_integral_multc) 169qed simp 170 171lemma (in prob_space) distributed_finite_measure_density: 172 "distributed M N X f \<Longrightarrow> finite_measure (density N f)" 173 using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp 174 175 176lemma (in prob_space) distributed_convolution: 177 fixes f :: "real \<Rightarrow> _" 178 fixes g :: "real \<Rightarrow> _" 179 assumes indep: "indep_var borel X borel Y" 180 assumes X: "distributed M lborel X f" 181 assumes Y: "distributed M lborel Y g" 182 shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)" 183 unfolding distributed_def 184proof safe 185 have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel" 186 using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all 187 188 show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel" 189 by measurable 190 191 have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)" 192 using distributed_measurable[OF X] distributed_measurable[OF Y] 193 by (intro sum_indep_random_variable) (auto simp: indep) 194 also have "\<dots> = (density lborel f \<star> density lborel g)" 195 using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] 196 by (simp cong: distr_cong) 197 also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)" 198 proof (rule convolution_density) 199 show "finite_measure (density lborel f)" 200 using X by (rule distributed_finite_measure_density) 201 show "finite_measure (density lborel g)" 202 using Y by (rule distributed_finite_measure_density) 203 qed fact+ 204 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)" 205 by (simp cong: distr_cong) 206 show "random_variable lborel (\<lambda>x. X x + Y x)" 207 using distributed_measurable[OF X] distributed_measurable[OF Y] by simp 208qed 209 210lemma prob_space_convolution_density: 211 fixes f:: "real \<Rightarrow> _" 212 fixes g:: "real \<Rightarrow> _" 213 assumes [measurable]: "f\<in> borel_measurable borel" 214 assumes [measurable]: "g\<in> borel_measurable borel" 215 assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" 216 assumes "prob_space (density lborel f)" (is "prob_space ?F") 217 assumes "prob_space (density lborel g)" (is "prob_space ?G") 218 shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D") 219proof (subst convolution_density[symmetric]) 220 interpret F: prob_space ?F by fact 221 show "finite_measure ?F" by unfold_locales 222 interpret G: prob_space ?G by fact 223 show "finite_measure ?G" by unfold_locales 224 interpret FG: pair_prob_space ?F ?G .. 225 226 show "prob_space (density lborel f \<star> density lborel g)" 227 unfolding convolution_def by (rule FG.prob_space_distr) simp 228qed simp_all 229 230end 231