src/HOL/Probability/Convolution.thy
author haftmann
Fri Jul 04 20:18:47 2014 +0200 (2014-07-04)
changeset 57512 cc97b347b301
parent 57235 b0b9a10e4bf4
child 57514 bdc2c6b40bf2
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
     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