src/HOL/Probability/Convolution.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59048 7dc8ac6f0895
child 61808 fc1556774cfe
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
hoelzl@57235
     1
(*  Title:      HOL/Probability/Convolution.thy
hoelzl@57235
     2
    Author:     Sudeep Kanav, TU München
hoelzl@57235
     3
    Author:     Johannes Hölzl, TU München *)
hoelzl@57235
     4
wenzelm@58876
     5
section {* Convolution Measure *}
hoelzl@57235
     6
hoelzl@57235
     7
theory Convolution
hoelzl@57235
     8
  imports Independent_Family
hoelzl@57235
     9
begin
hoelzl@57235
    10
hoelzl@57235
    11
lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
hoelzl@57235
    12
  ..
hoelzl@57235
    13
hoelzl@57235
    14
definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where
hoelzl@57235
    15
  "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)"
hoelzl@57235
    16
hoelzl@57235
    17
lemma
hoelzl@57235
    18
  shows space_convolution[simp]: "space (convolution M N) = space borel"
hoelzl@57235
    19
    and sets_convolution[simp]: "sets (convolution M N) = sets borel"
hoelzl@57235
    20
    and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel"
hoelzl@57235
    21
    and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B"
hoelzl@57235
    22
  by (simp_all add: convolution_def)
hoelzl@57235
    23
hoelzl@57235
    24
lemma nn_integral_convolution:
hoelzl@57235
    25
  assumes "finite_measure M" "finite_measure N"
hoelzl@59048
    26
  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
hoelzl@57235
    27
  assumes [measurable]: "f \<in> borel_measurable borel"
hoelzl@57235
    28
  shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
hoelzl@57235
    29
proof -
hoelzl@57235
    30
  interpret M: finite_measure M by fact
hoelzl@57235
    31
  interpret N: finite_measure N by fact
hoelzl@57235
    32
  interpret pair_sigma_finite M N ..
hoelzl@57235
    33
  show ?thesis
hoelzl@57235
    34
    unfolding convolution_def
hoelzl@57235
    35
    by (simp add: nn_integral_distr N.nn_integral_fst[symmetric])
hoelzl@57235
    36
qed
hoelzl@57235
    37
hoelzl@57235
    38
lemma convolution_emeasure:
hoelzl@57235
    39
  assumes "A \<in> sets borel" "finite_measure M" "finite_measure N"
hoelzl@57235
    40
  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
hoelzl@57235
    41
  assumes [simp]: "space M = space N" "space N = space borel"
hoelzl@57235
    42
  shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
hoelzl@57235
    43
  using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution 
haftmann@57514
    44
    nn_integral_indicator [symmetric] ac_simps split:split_indicator)
hoelzl@57235
    45
hoelzl@57235
    46
lemma convolution_emeasure':
hoelzl@57235
    47
  assumes [simp]:"A \<in> sets borel"
hoelzl@57235
    48
  assumes [simp]: "finite_measure M" "finite_measure N"
hoelzl@57235
    49
  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
hoelzl@57235
    50
  shows  "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y.  (indicator  A (x + y)) \<partial>N  \<partial>M"
hoelzl@57235
    51
  by (auto simp del: nn_integral_indicator simp: nn_integral_convolution
hoelzl@57235
    52
    nn_integral_indicator[symmetric] borel_measurable_indicator)
hoelzl@57235
    53
hoelzl@57235
    54
lemma convolution_finite:
hoelzl@57235
    55
  assumes [simp]: "finite_measure M" "finite_measure N"
hoelzl@59048
    56
  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
hoelzl@57235
    57
  shows "finite_measure (M \<star> N)"
hoelzl@57235
    58
  unfolding convolution_def
hoelzl@57235
    59
  by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
hoelzl@57235
    60
hoelzl@57235
    61
lemma convolution_emeasure_3:
hoelzl@57235
    62
  assumes [simp, measurable]: "A \<in> sets borel"
hoelzl@57235
    63
  assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
hoelzl@57235
    64
  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
hoelzl@57235
    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"
hoelzl@57235
    66
  apply (subst nn_integral_indicator[symmetric], simp)
hoelzl@57235
    67
  apply (subst nn_integral_convolution, 
hoelzl@57235
    68
        auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
haftmann@57512
    69
  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add.assoc)
hoelzl@57235
    70
hoelzl@57235
    71
lemma convolution_emeasure_3':
hoelzl@57235
    72
  assumes [simp, measurable]:"A \<in> sets borel"
hoelzl@57235
    73
  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
hoelzl@59048
    74
  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
hoelzl@57235
    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"
hoelzl@57235
    76
  apply (subst nn_integral_indicator[symmetric], simp)+
hoelzl@57235
    77
  apply (subst nn_integral_convolution)
hoelzl@57235
    78
  apply (simp_all add: convolution_finite)
hoelzl@57235
    79
  apply (subst nn_integral_convolution)
hoelzl@57235
    80
  apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral)
hoelzl@57235
    81
  done
hoelzl@57235
    82
hoelzl@57235
    83
lemma convolution_commutative:
hoelzl@57235
    84
  assumes [simp]: "finite_measure M" "finite_measure N"
hoelzl@59048
    85
  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel"
hoelzl@57235
    86
  shows "(M \<star> N) = (N \<star> M)"
hoelzl@57235
    87
proof (rule measure_eqI)  
hoelzl@57235
    88
  interpret M: finite_measure M by fact
hoelzl@57235
    89
  interpret N: finite_measure N by fact
hoelzl@57235
    90
  interpret pair_sigma_finite M N ..
hoelzl@57235
    91
hoelzl@57235
    92
  show "sets (M \<star> N) = sets (N \<star> M)" by simp
hoelzl@57235
    93
hoelzl@57235
    94
  fix A assume "A \<in> sets (M \<star> N)"
hoelzl@57235
    95
  then have 1[measurable]:"A \<in> sets borel" by simp
hoelzl@57235
    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')
hoelzl@57235
    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)
hoelzl@57235
    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
haftmann@57512
    99
  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add.commute convolution_emeasure')
hoelzl@57235
   100
  finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp
hoelzl@57235
   101
qed
hoelzl@57235
   102
hoelzl@57235
   103
lemma convolution_associative:
hoelzl@57235
   104
  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
hoelzl@57235
   105
  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
hoelzl@57235
   106
  shows "(L \<star> (M \<star> N)) = ((L \<star> M) \<star> N)"
hoelzl@57235
   107
  by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3')
hoelzl@57235
   108
hoelzl@57235
   109
lemma (in prob_space) sum_indep_random_variable:
hoelzl@57235
   110
  assumes ind: "indep_var borel X borel Y"
hoelzl@57235
   111
  assumes [simp, measurable]: "random_variable borel X"
hoelzl@57235
   112
  assumes [simp, measurable]: "random_variable borel Y"
hoelzl@57235
   113
  shows "distr M borel (\<lambda>x. X x + Y x) = convolution (distr M borel X)  (distr M borel Y)"
hoelzl@57235
   114
  using ind unfolding indep_var_distribution_eq convolution_def
hoelzl@57235
   115
  by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"])
hoelzl@57235
   116
hoelzl@57235
   117
lemma (in prob_space) sum_indep_random_variable_lborel:
hoelzl@57235
   118
  assumes ind: "indep_var borel X borel Y"
hoelzl@57235
   119
  assumes [simp, measurable]: "random_variable lborel X"
hoelzl@57235
   120
  assumes [simp, measurable]:"random_variable lborel Y" 
hoelzl@57235
   121
  shows "distr M lborel (\<lambda>x. X x + Y x) = convolution (distr M lborel X)  (distr M lborel Y)"
hoelzl@57235
   122
  using ind unfolding indep_var_distribution_eq convolution_def 
hoelzl@57235
   123
  by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong)
hoelzl@57235
   124
hoelzl@57235
   125
lemma convolution_density:
hoelzl@57235
   126
  fixes f g :: "real \<Rightarrow> ereal"
hoelzl@57235
   127
  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
hoelzl@57235
   128
  assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)"
hoelzl@57235
   129
  assumes gt_0[simp]: "AE x in lborel. 0 \<le> f x" "AE x in lborel. 0 \<le> g x"
hoelzl@57235
   130
  shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
hoelzl@57235
   131
    (is "?l = ?r")
hoelzl@57235
   132
proof (intro measure_eqI)
hoelzl@57235
   133
  fix A assume "A \<in> sets ?l"
hoelzl@57235
   134
  then have [measurable]: "A \<in> sets borel"
hoelzl@57235
   135
    by simp
hoelzl@57235
   136
hoelzl@57235
   137
  have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) =
hoelzl@57235
   138
    (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
hoelzl@57235
   139
    using gt_0
hoelzl@57235
   140
  proof (intro nn_integral_cong_AE, eventually_elim)
hoelzl@57235
   141
    fix x assume "0 \<le> f x"
hoelzl@57235
   142
    then have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
hoelzl@57235
   143
      (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)"
hoelzl@57235
   144
      by (intro nn_integral_cmult[symmetric]) auto
hoelzl@57235
   145
    then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
hoelzl@57235
   146
      (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)"
hoelzl@57235
   147
      by (simp add: ac_simps)
hoelzl@57235
   148
  qed
hoelzl@57235
   149
  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
hoelzl@57235
   150
    by (intro lborel_pair.Fubini') simp
hoelzl@57235
   151
  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
hoelzl@57235
   152
    using gt_0
hoelzl@57235
   153
  proof (intro nn_integral_cong_AE, eventually_elim)
hoelzl@57235
   154
    fix y assume "0 \<le> g y"
hoelzl@57235
   155
    then have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
hoelzl@57235
   156
      g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)"
hoelzl@57235
   157
      by (intro nn_integral_cmult) auto
hoelzl@57235
   158
    also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)"
hoelzl@57235
   159
      using gt_0
hoelzl@57235
   160
      by (subst nn_integral_real_affine[where c=1 and t="-y"])
hoelzl@57235
   161
         (auto simp del: gt_0 simp add: one_ereal_def[symmetric])
hoelzl@57235
   162
    also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)"
hoelzl@57235
   163
      using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto
hoelzl@57235
   164
    finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
hoelzl@57235
   165
      (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
hoelzl@57235
   166
      by (simp add: ac_simps)
hoelzl@57235
   167
  qed
hoelzl@57235
   168
  also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
hoelzl@57235
   169
    by (intro lborel_pair.Fubini') simp
hoelzl@57235
   170
  finally show "emeasure ?l A = emeasure ?r A"
hoelzl@57235
   171
    by (auto simp: convolution_emeasure' nn_integral_density emeasure_density
hoelzl@57235
   172
      nn_integral_multc)
hoelzl@57235
   173
qed simp
hoelzl@57235
   174
hoelzl@57235
   175
lemma (in prob_space) distributed_finite_measure_density:
hoelzl@57235
   176
  "distributed M N X f \<Longrightarrow> finite_measure (density N f)"
hoelzl@57235
   177
  using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp
hoelzl@57235
   178
  
hoelzl@57235
   179
hoelzl@57235
   180
lemma (in prob_space) distributed_convolution:
hoelzl@57235
   181
  fixes f :: "real \<Rightarrow> _"
hoelzl@57235
   182
  fixes g :: "real \<Rightarrow> _"
hoelzl@57235
   183
  assumes indep: "indep_var borel X borel Y"
hoelzl@57235
   184
  assumes X: "distributed M lborel X f"
hoelzl@57235
   185
  assumes Y: "distributed M lborel Y g"
hoelzl@57235
   186
  shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
hoelzl@57235
   187
  unfolding distributed_def
hoelzl@57235
   188
proof safe
hoelzl@57235
   189
  show "AE x in lborel. 0 \<le> \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel"
hoelzl@57235
   190
    by (auto simp: nn_integral_nonneg)
hoelzl@57235
   191
hoelzl@57235
   192
  have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
hoelzl@57235
   193
    using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all
hoelzl@57235
   194
  
hoelzl@57235
   195
  show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel" 
hoelzl@57235
   196
    by measurable
hoelzl@57235
   197
hoelzl@57235
   198
  have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)"
hoelzl@57235
   199
    using distributed_measurable[OF X] distributed_measurable[OF Y]
hoelzl@57235
   200
    by (intro sum_indep_random_variable) (auto simp: indep)
hoelzl@57235
   201
  also have "\<dots> = (density lborel f \<star> density lborel g)"
hoelzl@57235
   202
    using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
hoelzl@57235
   203
    by (simp cong: distr_cong)
hoelzl@57235
   204
  also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)"
hoelzl@57235
   205
  proof (rule convolution_density)
hoelzl@57235
   206
    show "finite_measure (density lborel f)"
hoelzl@57235
   207
      using X by (rule distributed_finite_measure_density)
hoelzl@57235
   208
    show "finite_measure (density lborel g)"
hoelzl@57235
   209
      using Y by (rule distributed_finite_measure_density)
hoelzl@57235
   210
    show "AE x in lborel. 0 \<le> f x"
hoelzl@57235
   211
      using X by (rule distributed_AE)
hoelzl@57235
   212
    show "AE x in lborel. 0 \<le> g x"
hoelzl@57235
   213
      using Y by (rule distributed_AE)
hoelzl@57235
   214
  qed fact+
hoelzl@57235
   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)"
hoelzl@57235
   216
    by (simp cong: distr_cong)
hoelzl@57235
   217
  show "random_variable lborel (\<lambda>x. X x + Y x)"
hoelzl@57235
   218
    using distributed_measurable[OF X] distributed_measurable[OF Y] by simp
hoelzl@57235
   219
qed
hoelzl@57235
   220
hoelzl@57235
   221
lemma prob_space_convolution_density:
hoelzl@57235
   222
  fixes f:: "real \<Rightarrow> _"
hoelzl@57235
   223
  fixes g:: "real \<Rightarrow> _"
hoelzl@57235
   224
  assumes [measurable]: "f\<in> borel_measurable borel"
hoelzl@57235
   225
  assumes [measurable]: "g\<in> borel_measurable borel"
hoelzl@57235
   226
  assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
hoelzl@57235
   227
  assumes "prob_space (density lborel f)" (is "prob_space ?F")
hoelzl@57235
   228
  assumes "prob_space (density lborel g)" (is "prob_space ?G")
hoelzl@57235
   229
  shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D")
hoelzl@57235
   230
proof (subst convolution_density[symmetric])
hoelzl@57235
   231
  interpret F: prob_space ?F by fact
hoelzl@57235
   232
  show "finite_measure ?F" by unfold_locales
hoelzl@57235
   233
  interpret G: prob_space ?G by fact
hoelzl@57235
   234
  show "finite_measure ?G" by unfold_locales
hoelzl@57235
   235
  interpret FG: pair_prob_space ?F ?G ..
hoelzl@57235
   236
hoelzl@57235
   237
  show "prob_space (density lborel f \<star> density lborel g)"
hoelzl@57235
   238
    unfolding convolution_def by (rule FG.prob_space_distr) simp
hoelzl@57235
   239
qed simp_all
hoelzl@57235
   240
hoelzl@57235
   241
end