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