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