src/HOL/Probability/Convolution.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 61808 fc1556774cfe child 62975 1d066f6ab25d permissions -rw-r--r--
generalize more theorems to support enat and ennreal
```     1 (*  Title:      HOL/Probability/Convolution.thy
```
```     2     Author:     Sudeep Kanav, TU München
```
```     3     Author:     Johannes Hölzl, TU München *)
```
```     4
```
```     5 section \<open>Convolution Measure\<close>
```
```     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 [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
```
```    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] ac_simps 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 [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
```
```    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 [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
```
```    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 ..
```
```    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 \<open>0 \<le> g y\<close> 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
```