21 and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B" |
21 and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B" |
22 by (simp_all add: convolution_def) |
22 by (simp_all add: convolution_def) |
23 |
23 |
24 lemma nn_integral_convolution: |
24 lemma nn_integral_convolution: |
25 assumes "finite_measure M" "finite_measure N" |
25 assumes "finite_measure M" "finite_measure N" |
26 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
26 assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel" |
27 assumes [measurable]: "f \<in> borel_measurable 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)" |
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 - |
29 proof - |
30 interpret M: finite_measure M by fact |
30 interpret M: finite_measure M by fact |
31 interpret N: finite_measure N by fact |
31 interpret N: finite_measure N by fact |
51 by (auto simp del: nn_integral_indicator simp: nn_integral_convolution |
51 by (auto simp del: nn_integral_indicator simp: nn_integral_convolution |
52 nn_integral_indicator[symmetric] borel_measurable_indicator) |
52 nn_integral_indicator[symmetric] borel_measurable_indicator) |
53 |
53 |
54 lemma convolution_finite: |
54 lemma convolution_finite: |
55 assumes [simp]: "finite_measure M" "finite_measure N" |
55 assumes [simp]: "finite_measure M" "finite_measure N" |
56 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
56 assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel" |
57 shows "finite_measure (M \<star> N)" |
57 shows "finite_measure (M \<star> N)" |
58 unfolding convolution_def |
58 unfolding convolution_def |
59 by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto |
59 by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto |
60 |
60 |
61 lemma convolution_emeasure_3: |
61 lemma convolution_emeasure_3: |
69 by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add.assoc) |
69 by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add.assoc) |
70 |
70 |
71 lemma convolution_emeasure_3': |
71 lemma convolution_emeasure_3': |
72 assumes [simp, measurable]:"A \<in> sets borel" |
72 assumes [simp, measurable]:"A \<in> sets borel" |
73 assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L" |
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" |
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" |
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)+ |
76 apply (subst nn_integral_indicator[symmetric], simp)+ |
77 apply (subst nn_integral_convolution) |
77 apply (subst nn_integral_convolution) |
78 apply (simp_all add: convolution_finite) |
78 apply (simp_all add: convolution_finite) |
79 apply (subst nn_integral_convolution) |
79 apply (subst nn_integral_convolution) |
80 apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral) |
80 apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral) |
81 done |
81 done |
82 |
82 |
83 lemma convolution_commutative: |
83 lemma convolution_commutative: |
84 assumes [simp]: "finite_measure M" "finite_measure N" |
84 assumes [simp]: "finite_measure M" "finite_measure N" |
85 assumes [simp]: "sets N = sets borel" "sets M = sets borel" |
85 assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel" |
86 shows "(M \<star> N) = (N \<star> M)" |
86 shows "(M \<star> N) = (N \<star> M)" |
87 proof (rule measure_eqI) |
87 proof (rule measure_eqI) |
88 interpret M: finite_measure M by fact |
88 interpret M: finite_measure M by fact |
89 interpret N: finite_measure N by fact |
89 interpret N: finite_measure N by fact |
90 interpret pair_sigma_finite M N .. |
90 interpret pair_sigma_finite M N .. |