src/HOL/Probability/Convolution.thy
 changeset 57235 b0b9a10e4bf4 child 57512 cc97b347b301
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Convolution.thy	Thu Jun 12 15:47:36 2014 +0200
1.3 @@ -0,0 +1,241 @@
1.4 +(*  Title:      HOL/Probability/Convolution.thy
1.5 +    Author:     Sudeep Kanav, TU München
1.6 +    Author:     Johannes Hölzl, TU München *)
1.7 +
1.8 +header {* Convolution Measure *}
1.9 +
1.10 +theory Convolution
1.11 +  imports Independent_Family
1.12 +begin
1.13 +
1.14 +lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
1.15 +  ..
1.16 +
1.17 +definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where
1.18 +  "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)"
1.19 +
1.20 +lemma
1.21 +  shows space_convolution[simp]: "space (convolution M N) = space borel"
1.22 +    and sets_convolution[simp]: "sets (convolution M N) = sets borel"
1.23 +    and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel"
1.24 +    and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B"
1.25 +  by (simp_all add: convolution_def)
1.26 +
1.27 +lemma nn_integral_convolution:
1.28 +  assumes "finite_measure M" "finite_measure N"
1.29 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
1.30 +  assumes [measurable]: "f \<in> borel_measurable borel"
1.31 +  shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
1.32 +proof -
1.33 +  interpret M: finite_measure M by fact
1.34 +  interpret N: finite_measure N by fact
1.35 +  interpret pair_sigma_finite M N ..
1.36 +  show ?thesis
1.37 +    unfolding convolution_def
1.38 +    by (simp add: nn_integral_distr N.nn_integral_fst[symmetric])
1.39 +qed
1.40 +
1.41 +lemma convolution_emeasure:
1.42 +  assumes "A \<in> sets borel" "finite_measure M" "finite_measure N"
1.43 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
1.44 +  assumes [simp]: "space M = space N" "space N = space borel"
1.45 +  shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
1.46 +  using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution
1.47 +    nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
1.48 +
1.49 +lemma convolution_emeasure':
1.50 +  assumes [simp]:"A \<in> sets borel"
1.51 +  assumes [simp]: "finite_measure M" "finite_measure N"
1.52 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
1.53 +  shows  "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y.  (indicator  A (x + y)) \<partial>N  \<partial>M"
1.54 +  by (auto simp del: nn_integral_indicator simp: nn_integral_convolution
1.55 +    nn_integral_indicator[symmetric] borel_measurable_indicator)
1.56 +
1.57 +lemma convolution_finite:
1.58 +  assumes [simp]: "finite_measure M" "finite_measure N"
1.59 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
1.60 +  shows "finite_measure (M \<star> N)"
1.61 +  unfolding convolution_def
1.62 +  by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
1.63 +
1.64 +lemma convolution_emeasure_3:
1.65 +  assumes [simp, measurable]: "A \<in> sets borel"
1.66 +  assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
1.67 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
1.68 +  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"
1.69 +  apply (subst nn_integral_indicator[symmetric], simp)
1.70 +  apply (subst nn_integral_convolution,
1.71 +        auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
1.72 +  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add_assoc)
1.73 +
1.74 +lemma convolution_emeasure_3':
1.75 +  assumes [simp, measurable]:"A \<in> sets borel"
1.76 +  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
1.77 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
1.78 +  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"
1.79 +  apply (subst nn_integral_indicator[symmetric], simp)+
1.80 +  apply (subst nn_integral_convolution)
1.81 +  apply (simp_all add: convolution_finite)
1.82 +  apply (subst nn_integral_convolution)
1.83 +  apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral)
1.84 +  done
1.85 +
1.86 +lemma convolution_commutative:
1.87 +  assumes [simp]: "finite_measure M" "finite_measure N"
1.88 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
1.89 +  shows "(M \<star> N) = (N \<star> M)"
1.90 +proof (rule measure_eqI)
1.91 +  interpret M: finite_measure M by fact
1.92 +  interpret N: finite_measure N by fact
1.93 +  interpret pair_sigma_finite M N ..
1.94 +
1.95 +  show "sets (M \<star> N) = sets (N \<star> M)" by simp
1.96 +
1.97 +  fix A assume "A \<in> sets (M \<star> N)"
1.98 +  then have 1[measurable]:"A \<in> sets borel" by simp
1.99 +  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')
1.100 +  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)
1.101 +  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
1.102 +  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add_commute convolution_emeasure')
1.103 +  finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp
1.104 +qed
1.105 +
1.106 +lemma convolution_associative:
1.107 +  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
1.108 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
1.109 +  shows "(L \<star> (M \<star> N)) = ((L \<star> M) \<star> N)"
1.110 +  by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3')
1.111 +
1.112 +lemma (in prob_space) sum_indep_random_variable:
1.113 +  assumes ind: "indep_var borel X borel Y"
1.114 +  assumes [simp, measurable]: "random_variable borel X"
1.115 +  assumes [simp, measurable]: "random_variable borel Y"
1.116 +  shows "distr M borel (\<lambda>x. X x + Y x) = convolution (distr M borel X)  (distr M borel Y)"
1.117 +  using ind unfolding indep_var_distribution_eq convolution_def
1.118 +  by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"])
1.119 +
1.120 +lemma (in prob_space) sum_indep_random_variable_lborel:
1.121 +  assumes ind: "indep_var borel X borel Y"
1.122 +  assumes [simp, measurable]: "random_variable lborel X"
1.123 +  assumes [simp, measurable]:"random_variable lborel Y"
1.124 +  shows "distr M lborel (\<lambda>x. X x + Y x) = convolution (distr M lborel X)  (distr M lborel Y)"
1.125 +  using ind unfolding indep_var_distribution_eq convolution_def
1.126 +  by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong)
1.127 +
1.128 +lemma convolution_density:
1.129 +  fixes f g :: "real \<Rightarrow> ereal"
1.130 +  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
1.131 +  assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)"
1.132 +  assumes gt_0[simp]: "AE x in lborel. 0 \<le> f x" "AE x in lborel. 0 \<le> g x"
1.133 +  shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
1.134 +    (is "?l = ?r")
1.135 +proof (intro measure_eqI)
1.136 +  fix A assume "A \<in> sets ?l"
1.137 +  then have [measurable]: "A \<in> sets borel"
1.138 +    by simp
1.139 +
1.140 +  have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) =
1.141 +    (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
1.142 +    using gt_0
1.143 +  proof (intro nn_integral_cong_AE, eventually_elim)
1.144 +    fix x assume "0 \<le> f x"
1.145 +    then have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
1.146 +      (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)"
1.147 +      by (intro nn_integral_cmult[symmetric]) auto
1.148 +    then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
1.149 +      (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)"
1.150 +      by (simp add: ac_simps)
1.151 +  qed
1.152 +  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
1.153 +    by (intro lborel_pair.Fubini') simp
1.154 +  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
1.155 +    using gt_0
1.156 +  proof (intro nn_integral_cong_AE, eventually_elim)
1.157 +    fix y assume "0 \<le> g y"
1.158 +    then have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
1.159 +      g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)"
1.160 +      by (intro nn_integral_cmult) auto
1.161 +    also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)"
1.162 +      using gt_0
1.163 +      by (subst nn_integral_real_affine[where c=1 and t="-y"])
1.164 +         (auto simp del: gt_0 simp add: one_ereal_def[symmetric])
1.165 +    also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)"
1.166 +      using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto
1.167 +    finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
1.168 +      (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
1.169 +      by (simp add: ac_simps)
1.170 +  qed
1.171 +  also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
1.172 +    by (intro lborel_pair.Fubini') simp
1.173 +  finally show "emeasure ?l A = emeasure ?r A"
1.174 +    by (auto simp: convolution_emeasure' nn_integral_density emeasure_density
1.175 +      nn_integral_multc)
1.176 +qed simp
1.177 +
1.178 +lemma (in prob_space) distributed_finite_measure_density:
1.179 +  "distributed M N X f \<Longrightarrow> finite_measure (density N f)"
1.180 +  using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp
1.181 +
1.182 +
1.183 +lemma (in prob_space) distributed_convolution:
1.184 +  fixes f :: "real \<Rightarrow> _"
1.185 +  fixes g :: "real \<Rightarrow> _"
1.186 +  assumes indep: "indep_var borel X borel Y"
1.187 +  assumes X: "distributed M lborel X f"
1.188 +  assumes Y: "distributed M lborel Y g"
1.189 +  shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
1.190 +  unfolding distributed_def
1.191 +proof safe
1.192 +  show "AE x in lborel. 0 \<le> \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel"
1.193 +    by (auto simp: nn_integral_nonneg)
1.194 +
1.195 +  have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
1.196 +    using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all
1.197 +
1.198 +  show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel"
1.199 +    by measurable
1.200 +
1.201 +  have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)"
1.202 +    using distributed_measurable[OF X] distributed_measurable[OF Y]
1.203 +    by (intro sum_indep_random_variable) (auto simp: indep)
1.204 +  also have "\<dots> = (density lborel f \<star> density lborel g)"
1.205 +    using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
1.206 +    by (simp cong: distr_cong)
1.207 +  also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)"
1.208 +  proof (rule convolution_density)
1.209 +    show "finite_measure (density lborel f)"
1.210 +      using X by (rule distributed_finite_measure_density)
1.211 +    show "finite_measure (density lborel g)"
1.212 +      using Y by (rule distributed_finite_measure_density)
1.213 +    show "AE x in lborel. 0 \<le> f x"
1.214 +      using X by (rule distributed_AE)
1.215 +    show "AE x in lborel. 0 \<le> g x"
1.216 +      using Y by (rule distributed_AE)
1.217 +  qed fact+
1.218 +  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)"
1.219 +    by (simp cong: distr_cong)
1.220 +  show "random_variable lborel (\<lambda>x. X x + Y x)"
1.221 +    using distributed_measurable[OF X] distributed_measurable[OF Y] by simp
1.222 +qed
1.223 +
1.224 +lemma prob_space_convolution_density:
1.225 +  fixes f:: "real \<Rightarrow> _"
1.226 +  fixes g:: "real \<Rightarrow> _"
1.227 +  assumes [measurable]: "f\<in> borel_measurable borel"
1.228 +  assumes [measurable]: "g\<in> borel_measurable borel"
1.229 +  assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
1.230 +  assumes "prob_space (density lborel f)" (is "prob_space ?F")
1.231 +  assumes "prob_space (density lborel g)" (is "prob_space ?G")
1.232 +  shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D")
1.233 +proof (subst convolution_density[symmetric])
1.234 +  interpret F: prob_space ?F by fact
1.235 +  show "finite_measure ?F" by unfold_locales
1.236 +  interpret G: prob_space ?G by fact
1.237 +  show "finite_measure ?G" by unfold_locales
1.238 +  interpret FG: pair_prob_space ?F ?G ..
1.239 +
1.240 +  show "prob_space (density lborel f \<star> density lborel g)"
1.241 +    unfolding convolution_def by (rule FG.prob_space_distr) simp
1.242 +qed simp_all
1.243 +
1.244 +end
```