|
1 (* Title: HOL/Probability/Distributions.thy |
|
2 Author: Sudeep Kanav, TU München |
|
3 Author: Johannes Hölzl, TU München *) |
|
4 |
|
5 header {* Properties of Various Distributions *} |
|
6 |
1 theory Distributions |
7 theory Distributions |
2 imports Probability_Measure |
8 imports Probability_Measure Convolution |
3 begin |
9 begin |
4 |
10 |
|
11 lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)" |
|
12 by (auto simp: measure_def) |
|
13 |
|
14 lemma integral_power: |
|
15 "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k" |
|
16 proof (subst integral_FTC_atLeastAtMost) |
|
17 fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k" |
|
18 by (intro derivative_eq_intros) auto |
|
19 qed (auto simp: field_simps) |
|
20 |
|
21 lemma has_bochner_integral_nn_integral: |
|
22 assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" |
|
23 assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x" |
|
24 shows "has_bochner_integral M f x" |
|
25 unfolding has_bochner_integral_iff |
|
26 proof |
|
27 show "integrable M f" |
|
28 using assms by (rule integrableI_nn_integral_finite) |
|
29 qed (auto simp: assms integral_eq_nn_integral) |
|
30 |
|
31 lemma (in prob_space) distributed_AE2: |
|
32 assumes [measurable]: "distributed M N X f" "Measurable.pred N P" |
|
33 shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" |
|
34 proof - |
|
35 have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)" |
|
36 by (simp add: AE_distr_iff) |
|
37 also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)" |
|
38 unfolding distributed_distr_eq_density[OF assms(1)] .. |
|
39 also have "\<dots> \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" |
|
40 by (rule AE_density) simp |
|
41 finally show ?thesis . |
|
42 qed |
|
43 |
|
44 subsection {* Erlang *} |
|
45 |
|
46 lemma nn_intergal_power_times_exp_Icc: |
|
47 assumes [arith]: "0 \<le> a" |
|
48 shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) = |
|
49 (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _") |
|
50 proof - |
|
51 let ?f = "\<lambda>k x. x^k * exp (-x) / fact k" |
|
52 let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)" |
|
53 |
|
54 have "?I * (inverse (fact k)) = |
|
55 (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)" |
|
56 by (intro nn_integral_multc[symmetric]) auto |
|
57 also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)" |
|
58 by (intro nn_integral_cong) (simp add: field_simps) |
|
59 also have "\<dots> = ereal (?F k a) - (?F k 0)" |
|
60 proof (rule nn_integral_FTC_atLeastAtMost) |
|
61 fix x assume "x \<in> {0..a}" |
|
62 show "DERIV (?F k) x :> ?f k x" |
|
63 proof(induction k) |
|
64 case 0 show ?case by (auto intro!: derivative_eq_intros) |
|
65 next |
|
66 case (Suc k) |
|
67 have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :> |
|
68 ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))" |
|
69 by (intro DERIV_diff Suc) |
|
70 (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc |
|
71 simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric]) |
|
72 also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)" |
|
73 by simp |
|
74 also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x" |
|
75 by (auto simp: field_simps simp del: fact_Suc) |
|
76 (simp_all add: real_of_nat_Suc field_simps) |
|
77 finally show ?case . |
|
78 qed |
|
79 qed auto |
|
80 also have "\<dots> = ereal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))" |
|
81 by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum_cases) |
|
82 finally show ?thesis |
|
83 by (cases "?I") (auto simp: field_simps) |
|
84 qed |
|
85 |
|
86 lemma nn_intergal_power_times_exp_Ici: |
|
87 shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k" |
|
88 proof (rule LIMSEQ_unique) |
|
89 let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel" |
|
90 show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)" |
|
91 apply (intro nn_integral_LIMSEQ) |
|
92 apply (auto simp: incseq_def le_fun_def eventually_sequentially |
|
93 split: split_indicator intro!: Lim_eventually) |
|
94 apply (metis natceiling_le_eq) |
|
95 done |
|
96 |
|
97 have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top" |
|
98 by (intro tendsto_intros tendsto_power_div_exp_0) simp |
|
99 then show "?X ----> fact k" |
|
100 by (subst nn_intergal_power_times_exp_Icc) |
|
101 (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially]) |
|
102 qed |
|
103 |
|
104 definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where |
|
105 "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)" |
|
106 |
|
107 definition erlang_CDF :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where |
|
108 "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))" |
|
109 |
|
110 lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x" |
|
111 by (simp add: erlang_density_def) |
|
112 |
|
113 lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel" |
|
114 by (auto simp add: erlang_density_def[abs_def]) |
|
115 |
|
116 lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)" |
|
117 by (auto simp add: erlang_CDF_def mult_less_0_iff) |
|
118 |
|
119 lemma nn_integral_erlang_density: |
|
120 assumes [arith]: "0 < l" |
|
121 shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a" |
|
122 proof cases |
|
123 assume [arith]: "0 \<le> a" |
|
124 have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x" |
|
125 by (simp add: field_simps split: split_indicator) |
|
126 have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = |
|
127 (\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)" |
|
128 by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator) |
|
129 also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)" |
|
130 by (intro nn_integral_cmult) auto |
|
131 also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))" |
|
132 by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) |
|
133 also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))" |
|
134 by (subst nn_intergal_power_times_exp_Icc) auto |
|
135 also have "\<dots> = erlang_CDF k l a" |
|
136 by (auto simp: erlang_CDF_def) |
|
137 finally show ?thesis . |
|
138 next |
|
139 assume "\<not> 0 \<le> a" |
|
140 moreover then have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))" |
|
141 by (intro nn_integral_cong) (auto simp: erlang_density_def) |
|
142 ultimately show ?thesis |
|
143 by (simp add: erlang_CDF_def) |
|
144 qed |
|
145 |
|
146 lemma emeasure_erlang_density: |
|
147 "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a" |
|
148 by (simp add: emeasure_density nn_integral_erlang_density) |
|
149 |
|
150 lemma nn_integral_erlang_ith_moment: |
|
151 fixes k i :: nat and l :: real |
|
152 assumes [arith]: "0 < l" |
|
153 shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)" |
|
154 proof - |
|
155 have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x" |
|
156 by (simp add: field_simps split: split_indicator) |
|
157 have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) = |
|
158 (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)" |
|
159 by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator) |
|
160 also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)" |
|
161 by (intro nn_integral_cmult) auto |
|
162 also have "\<dots> = ereal (l/(fact k * l^i)) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^(k+i) * exp (- x)) * indicator {0 ..} x \<partial>lborel))" |
|
163 by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) |
|
164 also have "\<dots> = fact (k + i) / (fact k * l ^ i)" |
|
165 by (subst nn_intergal_power_times_exp_Ici) auto |
|
166 finally show ?thesis . |
|
167 qed |
|
168 |
|
169 lemma prob_space_erlang_density: |
|
170 assumes l[arith]: "0 < l" |
|
171 shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D") |
|
172 proof |
|
173 show "emeasure ?D (space ?D) = 1" |
|
174 using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density) |
|
175 qed |
|
176 |
|
177 lemma (in prob_space) erlang_distributed_le: |
|
178 assumes D: "distributed M lborel X (erlang_density k l)" |
|
179 assumes [simp, arith]: "0 < l" "0 \<le> a" |
|
180 shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a" |
|
181 proof - |
|
182 have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}" |
|
183 using distributed_measurable[OF D] |
|
184 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) |
|
185 also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}" |
|
186 unfolding distributed_distr_eq_density[OF D] .. |
|
187 also have "\<dots> = erlang_CDF k l a" |
|
188 by (auto intro!: emeasure_erlang_density) |
|
189 finally show ?thesis |
|
190 by (auto simp: measure_def) |
|
191 qed |
|
192 |
|
193 lemma (in prob_space) erlang_distributed_gt: |
|
194 assumes D[simp]: "distributed M lborel X (erlang_density k l)" |
|
195 assumes [arith]: "0 < l" "0 \<le> a" |
|
196 shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)" |
|
197 proof - |
|
198 have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto |
|
199 also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })" |
|
200 using distributed_measurable[OF D] by (auto simp: prob_compl) |
|
201 also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le) |
|
202 finally show ?thesis by simp |
|
203 qed |
|
204 |
|
205 lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0" |
|
206 by (induction k) (auto simp: erlang_CDF_def) |
|
207 |
|
208 lemma erlang_distributedI: |
|
209 assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" |
|
210 and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a" |
|
211 shows "distributed M lborel X (erlang_density k l)" |
|
212 proof (rule distributedI_borel_atMost) |
|
213 fix a :: real |
|
214 { assume "a \<le> 0" |
|
215 with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}" |
|
216 by (intro emeasure_mono) auto |
|
217 also have "... = 0" by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0]) |
|
218 finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp |
|
219 then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff) |
|
220 } |
|
221 note eq_0 = this |
|
222 |
|
223 show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)" |
|
224 using nn_integral_erlang_density[of l k a] |
|
225 by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps) |
|
226 |
|
227 show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)" |
|
228 using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def) |
|
229 qed (simp_all add: erlang_density_nonneg) |
|
230 |
|
231 lemma (in prob_space) erlang_distributed_iff: |
|
232 assumes [arith]: "0<l" |
|
233 shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow> |
|
234 (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = erlang_CDF k l a ))" |
|
235 using |
|
236 distributed_measurable[of M lborel X "erlang_density k l"] |
|
237 emeasure_erlang_density[of l] |
|
238 erlang_distributed_le[of X k l] |
|
239 by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) |
|
240 |
|
241 lemma (in prob_space) erlang_distributed_mult_const: |
|
242 assumes erlX: "distributed M lborel X (erlang_density k l)" |
|
243 assumes a_pos[arith]: "0 < \<alpha>" "0 < l" |
|
244 shows "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))" |
|
245 proof (subst erlang_distributed_iff, safe) |
|
246 have [measurable]: "random_variable borel X" and [arith]: "0 < l " |
|
247 and [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a" |
|
248 by(insert erlX, auto simp: erlang_distributed_iff) |
|
249 |
|
250 show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>" "0 < l / \<alpha>" |
|
251 by (auto simp:field_simps) |
|
252 |
|
253 fix a:: real assume [arith]: "0 \<le> a" |
|
254 obtain b:: real where [simp, arith]: "b = a/ \<alpha>" by blast |
|
255 |
|
256 have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos) |
|
257 |
|
258 have "prob {x \<in> space M. \<alpha> * X x \<le> a} = prob {x \<in> space M. X x \<le> b}" |
|
259 by (rule arg_cong[where f= prob]) (auto simp:field_simps) |
|
260 |
|
261 moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto |
|
262 moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto |
|
263 ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce |
|
264 qed |
|
265 |
|
266 lemma (in prob_space) has_bochner_integral_erlang_ith_moment: |
|
267 fixes k i :: nat and l :: real |
|
268 assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)" |
|
269 shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))" |
|
270 proof (rule has_bochner_integral_nn_integral) |
|
271 show "AE x in M. 0 \<le> X x ^ i" |
|
272 by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def) |
|
273 show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))" |
|
274 using nn_integral_erlang_ith_moment[of l k i] |
|
275 by (subst distributed_nn_integral[symmetric, OF D]) auto |
|
276 qed (insert distributed_measurable[OF D], simp) |
|
277 |
|
278 lemma (in prob_space) erlang_ith_moment_integrable: |
|
279 "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)" |
|
280 by rule (rule has_bochner_integral_erlang_ith_moment) |
|
281 |
|
282 lemma (in prob_space) erlang_ith_moment: |
|
283 "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> |
|
284 expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)" |
|
285 by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment) |
|
286 |
|
287 lemma (in prob_space) erlang_distributed_variance: |
|
288 assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)" |
|
289 shows "variance X = (k + 1) / l\<^sup>2" |
|
290 proof (subst variance_eq) |
|
291 show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)" |
|
292 using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2] |
|
293 by auto |
|
294 |
|
295 show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" |
|
296 using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] |
|
297 by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc) |
|
298 qed |
|
299 |
5 subsection {* Exponential distribution *} |
300 subsection {* Exponential distribution *} |
6 |
301 |
7 definition exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where |
302 abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where |
|
303 "exponential_density \<equiv> erlang_density 0" |
|
304 |
|
305 lemma exponential_density_def: |
8 "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" |
306 "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" |
9 |
307 by (simp add: fun_eq_iff erlang_density_def) |
10 lemma borel_measurable_exponential_density[measurable]: "exponential_density l \<in> borel_measurable borel" |
308 |
11 by (auto simp add: exponential_density_def[abs_def]) |
309 lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)" |
|
310 by (simp add: erlang_CDF_def) |
12 |
311 |
13 lemma (in prob_space) exponential_distributed_params: |
312 lemma (in prob_space) exponential_distributed_params: |
14 assumes D: "distributed M lborel X (exponential_density l)" |
313 assumes D: "distributed M lborel X (exponential_density l)" |
15 shows "0 < l" |
314 shows "0 < l" |
16 proof (cases l "0 :: real" rule: linorder_cases) |
315 proof (cases l "0 :: real" rule: linorder_cases) |
40 from X.emeasure_space_1 |
339 from X.emeasure_space_1 |
41 show "0 < l" |
340 show "0 < l" |
42 by (simp add: emeasure_density distributed_distr_eq_density[OF D]) |
341 by (simp add: emeasure_density distributed_distr_eq_density[OF D]) |
43 qed assumption |
342 qed assumption |
44 |
343 |
45 lemma |
344 lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))" |
46 assumes [arith]: "0 < l" |
345 by (rule prob_space_erlang_density) |
47 shows emeasure_exponential_density_le0: "0 \<le> a \<Longrightarrow> emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)" |
|
48 and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))" |
|
49 (is "prob_space ?D") |
|
50 proof - |
|
51 let ?f = "\<lambda>x. l * exp (- x * l)" |
|
52 let ?F = "\<lambda>x. - exp (- x * l)" |
|
53 |
|
54 have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)" |
|
55 by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff) |
|
56 |
|
57 have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)" |
|
58 by (auto simp: emeasure_density exponential_density_def |
|
59 intro!: nn_integral_cong split: split_indicator) |
|
60 also have "\<dots> = ereal (0 - ?F 0)" |
|
61 proof (rule nn_integral_FTC_atLeast) |
|
62 have "((\<lambda>x. exp (l * x)) ---> 0) at_bot" |
|
63 by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]]) |
|
64 (simp_all add: tendsto_const filterlim_ident) |
|
65 then show "((\<lambda>x. - exp (- x * l)) ---> 0) at_top" |
|
66 unfolding filterlim_at_top_mirror |
|
67 by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps) |
|
68 qed (insert deriv, auto) |
|
69 also have "\<dots> = 1" by (simp add: one_ereal_def) |
|
70 finally have "emeasure ?D (space ?D) = 1" . |
|
71 then show "prob_space ?D" by rule |
|
72 |
|
73 assume "0 \<le> a" |
|
74 have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)" |
|
75 by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator) |
|
76 (auto simp: exponential_density_def) |
|
77 also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)" |
|
78 using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto |
|
79 also have "\<dots> = 1 - exp (- a * l)" |
|
80 by simp |
|
81 finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" . |
|
82 qed |
|
83 |
|
84 |
346 |
85 lemma (in prob_space) exponential_distributedD_le: |
347 lemma (in prob_space) exponential_distributedD_le: |
86 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" |
348 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" |
87 shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)" |
349 shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)" |
88 proof - |
350 using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a |
89 have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}" |
351 by (simp add: erlang_CDF_def) |
90 using distributed_measurable[OF D] |
|
91 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) |
|
92 also have "\<dots> = emeasure (density lborel (exponential_density l)) {.. a}" |
|
93 unfolding distributed_distr_eq_density[OF D] .. |
|
94 also have "\<dots> = 1 - exp (- a * l)" |
|
95 using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] . |
|
96 finally show ?thesis |
|
97 by (auto simp: measure_def) |
|
98 qed |
|
99 |
352 |
100 lemma (in prob_space) exponential_distributedD_gt: |
353 lemma (in prob_space) exponential_distributedD_gt: |
101 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" |
354 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" |
102 shows "\<P>(x in M. a < X x ) = exp (- a * l)" |
355 shows "\<P>(x in M. a < X x ) = exp (- a * l)" |
103 proof - |
356 using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a |
104 have "exp (- a * l) = 1 - \<P>(x in M. X x \<le> a)" |
357 by (simp add: erlang_CDF_def) |
105 unfolding exponential_distributedD_le[OF D a] by simp |
|
106 also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })" |
|
107 using distributed_measurable[OF D] |
|
108 by (subst prob_compl) auto |
|
109 also have "\<dots> = \<P>(x in M. a < X x )" |
|
110 by (auto intro!: arg_cong[where f=prob] simp: not_le) |
|
111 finally show ?thesis by simp |
|
112 qed |
|
113 |
358 |
114 lemma (in prob_space) exponential_distributed_memoryless: |
359 lemma (in prob_space) exponential_distributed_memoryless: |
115 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t" |
360 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t" |
116 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" |
361 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" |
117 proof - |
362 proof - |
127 |
372 |
128 lemma exponential_distributedI: |
373 lemma exponential_distributedI: |
129 assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" |
374 assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" |
130 and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)" |
375 and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)" |
131 shows "distributed M lborel X (exponential_density l)" |
376 shows "distributed M lborel X (exponential_density l)" |
132 proof (rule distributedI_borel_atMost) |
377 proof (rule erlang_distributedI) |
133 fix a :: real |
378 fix a :: real assume "0 \<le> a" then show "emeasure M {x \<in> space M. X x \<le> a} = ereal (erlang_CDF 0 l a)" |
134 |
379 using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def) |
135 { assume "a \<le> 0" |
380 qed fact+ |
136 with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}" |
|
137 by (intro emeasure_mono) auto |
|
138 then have "emeasure M {x\<in>space M. X x \<le> a} = 0" |
|
139 using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) } |
|
140 note eq_0 = this |
|
141 |
|
142 have "\<And>x. \<not> 0 \<le> a \<Longrightarrow> ereal (exponential_density l x) * indicator {..a} x = 0" |
|
143 by (simp add: exponential_density_def) |
|
144 then show "(\<integral>\<^sup>+ x. exponential_density l x * indicator {..a} x \<partial>lborel) = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)" |
|
145 using emeasure_exponential_density_le0[of l a] |
|
146 by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator |
|
147 simp del: times_ereal.simps ereal_zero_times) |
|
148 show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)" |
|
149 using X_distr[of a] eq_0 by (auto simp: one_ereal_def) |
|
150 show "AE x in lborel. 0 \<le> exponential_density l x " |
|
151 by (auto simp: exponential_density_def) |
|
152 qed simp_all |
|
153 |
381 |
154 lemma (in prob_space) exponential_distributed_iff: |
382 lemma (in prob_space) exponential_distributed_iff: |
155 "distributed M lborel X (exponential_density l) \<longleftrightarrow> |
383 "distributed M lborel X (exponential_density l) \<longleftrightarrow> |
156 (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))" |
384 (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))" |
157 using |
385 using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0) |
158 distributed_measurable[of M lborel X "exponential_density l"] |
386 |
159 exponential_distributed_params[of X l] |
387 |
160 emeasure_exponential_density_le0[of l] |
388 lemma (in prob_space) exponential_distributed_expectation: |
161 exponential_distributedD_le[of X l] |
389 "distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l" |
162 by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure) |
390 using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp |
163 |
391 |
164 lemma borel_integral_x_exp: |
392 lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x" |
165 "has_bochner_integral lborel (\<lambda>x. x * exp (- x) * indicator {0::real ..} x) 1" |
393 by (auto simp: exponential_density_def) |
166 proof (rule has_bochner_integral_monotone_convergence) |
394 |
167 let ?f = "\<lambda>i x. x * exp (- x) * indicator {0::real .. i} x" |
395 lemma (in prob_space) exponential_distributed_min: |
168 have "eventually (\<lambda>b::real. 0 \<le> b) at_top" |
396 assumes expX: "distributed M lborel X (exponential_density l)" |
169 by (rule eventually_ge_at_top) |
397 assumes expY: "distributed M lborel Y (exponential_density u)" |
170 then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top" |
398 assumes ind: "indep_var borel X borel Y" |
171 proof eventually_elim |
399 shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))" |
172 fix b :: real assume [simp]: "0 \<le> b" |
400 proof (subst exponential_distributed_iff, safe) |
173 have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^sup>L lborel (?f b)) = |
401 have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff) |
174 (\<integral>x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \<partial>lborel)" |
402 moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff) |
175 by (subst integral_diff[symmetric]) |
403 ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto |
176 (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator) |
404 |
177 also have "\<dots> = b * exp (-b) - 0 * exp (- 0)" |
405 have "0 < l" by (rule exponential_distributed_params) fact |
178 proof (rule integral_FTC_atLeastAtMost) |
406 moreover have "0 < u" by (rule exponential_distributed_params) fact |
179 fix x assume "0 \<le> x" "x \<le> b" |
407 ultimately show " 0 < l + u" by force |
180 show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" |
408 |
181 by (auto intro!: derivative_eq_intros) |
409 fix a::real assume a[arith]: "0 \<le> a" |
182 show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x " |
410 have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) |
183 by (intro continuous_intros) |
411 have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) |
184 qed fact |
412 |
185 also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)" |
413 have "\<P>(x in M. a < (min (X x) (Y x)) ) = \<P>(x in M. a < (X x) \<and> a < (Y x))" by (auto intro!:arg_cong[where f=prob]) |
186 by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros) |
414 |
187 finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" |
415 also have " ... = \<P>(x in M. a < (X x)) * \<P>(x in M. a< (Y x) )" |
188 by (auto simp: field_simps exp_minus inverse_eq_divide) |
416 using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp |
|
417 also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp) |
|
418 finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" . |
|
419 |
|
420 have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })" |
|
421 by auto |
|
422 then have "1 - prob {x \<in> space M. a < (min (X x) (Y x))} = prob {x \<in> space M. (min (X x) (Y x)) \<le> a}" |
|
423 using randX randY by (auto simp: prob_compl) |
|
424 then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))" |
|
425 using indep_prob by auto |
|
426 qed |
|
427 |
|
428 lemma (in prob_space) exponential_distributed_Min: |
|
429 assumes finI: "finite I" |
|
430 assumes A: "I \<noteq> {}" |
|
431 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))" |
|
432 assumes ind: "indep_vars (\<lambda>i. borel) X I" |
|
433 shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))" |
|
434 using assms |
|
435 proof (induct rule: finite_ne_induct) |
|
436 case (singleton i) then show ?case by simp |
|
437 next |
|
438 case (insert i I) |
|
439 then have "distributed M lborel (\<lambda>x. min (X i x) (Min ((\<lambda>i. X i x)`I))) (exponential_density (l i + (\<Sum>i\<in>I. l i)))" |
|
440 by (intro exponential_distributed_min indep_vars_Min insert) |
|
441 (auto intro: indep_vars_subset) |
|
442 then show ?case |
|
443 using insert by simp |
|
444 qed |
|
445 |
|
446 lemma (in prob_space) exponential_distributed_variance: |
|
447 "distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2" |
|
448 using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp |
|
449 |
|
450 lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0" |
|
451 by (simp cong: nn_integral_cong_AE) |
|
452 |
|
453 lemma convolution_erlang_density: |
|
454 fixes k\<^sub>1 k\<^sub>2 :: nat |
|
455 assumes [simp, arith]: "0 < l" |
|
456 shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y)) * ereal (erlang_density k\<^sub>2 l y) \<partial>lborel) = |
|
457 (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" |
|
458 (is "?LHS = ?RHS") |
|
459 proof |
|
460 fix x :: real |
|
461 have "x \<le> 0 \<or> 0 < x" |
|
462 by arith |
|
463 then show "?LHS x = ?RHS x" |
|
464 proof |
|
465 assume "x \<le> 0" then show ?thesis |
|
466 apply (subst nn_integral_zero') |
|
467 apply (rule AE_I[where N="{0}"]) |
|
468 apply (auto simp add: erlang_density_def not_less) |
|
469 done |
|
470 next |
|
471 note zero_le_mult_iff[simp] zero_le_divide_iff[simp] |
|
472 |
|
473 have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1" |
|
474 using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc) |
|
475 |
|
476 have 1: "(\<integral>\<^sup>+ x. ereal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \<partial>lborel) = 1" |
|
477 apply (subst I_eq1[symmetric]) |
|
478 unfolding erlang_density_def |
|
479 by (auto intro!: nn_integral_cong split:split_indicator) |
|
480 |
|
481 have "prob_space (density lborel ?LHS)" |
|
482 unfolding times_ereal.simps[symmetric] |
|
483 by (intro prob_space_convolution_density) |
|
484 (auto intro!: prob_space_erlang_density erlang_density_nonneg) |
|
485 then have 2: "integral\<^sup>N lborel ?LHS = 1" |
|
486 by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density) |
|
487 |
|
488 let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))" |
|
489 let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))" |
|
490 let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" |
|
491 let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)" |
|
492 |
|
493 { fix x :: real assume [arith]: "0 < x" |
|
494 have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n" |
|
495 unfolding power_mult_distrib[symmetric] by (simp add: field_simps) |
|
496 |
|
497 have "?LHS x = ?L x" |
|
498 unfolding erlang_density_def |
|
499 by (auto intro!: nn_integral_cong split:split_indicator) |
|
500 also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x" |
|
501 apply (subst nn_integral_real_affine[where c=x and t = 0]) |
|
502 apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc) |
|
503 apply (intro nn_integral_cong) |
|
504 apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add * |
|
505 simp del: fact_Suc split: split_indicator) |
|
506 done |
|
507 finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = |
|
508 (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x" |
|
509 by simp } |
|
510 note * = this |
|
511 |
|
512 assume [arith]: "0 < x" |
|
513 have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)" |
|
514 by (subst 2[symmetric]) |
|
515 (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] |
|
516 simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: split_if_asm) |
|
517 also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))" |
|
518 by (auto intro!: nn_integral_cong simp: * split: split_indicator) |
|
519 also have "... = ereal (?C) * ?I" |
|
520 using 1 |
|
521 by (auto simp: nn_integral_nonneg nn_integral_cmult) |
|
522 finally have " ereal (?C) * ?I = 1" by presburger |
|
523 |
|
524 then show ?thesis |
|
525 using * by simp |
189 qed |
526 qed |
190 then have "((\<lambda>i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top" |
527 qed |
191 proof (rule Lim_transform_eventually) |
528 |
192 show "((\<lambda>i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top" |
529 lemma (in prob_space) sum_indep_erlang: |
193 using tendsto_power_div_exp_0[of 1] |
530 assumes indep: "indep_var borel X borel Y" |
194 by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp |
531 assumes [simp, arith]: "0 < l" |
195 qed |
532 assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" |
196 then show "(\<lambda>i. integral\<^sup>L lborel (?f i)) ----> 1" |
533 assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" |
197 by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp |
534 shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" |
198 show "AE x in lborel. mono (\<lambda>n::nat. x * exp (- x) * indicator {0..real n} x)" |
535 using assms |
199 by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator) |
536 apply (subst convolution_erlang_density[symmetric, OF `0<l`]) |
200 show "\<And>i::nat. integrable lborel (\<lambda>x. x * exp (- x) * indicator {0..real i} x)" |
537 apply (intro distributed_convolution) |
201 by (rule borel_integrable_atLeastAtMost) auto |
538 apply auto |
202 show "AE x in lborel. (\<lambda>i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x" |
539 done |
203 apply (intro AE_I2 Lim_eventually ) |
540 |
204 apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI) |
541 lemma (in prob_space) erlang_distributed_setsum: |
205 apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator) |
542 assumes finI : "finite I" |
206 done |
543 assumes A: "I \<noteq> {}" |
207 qed (auto intro!: borel_measurable_times borel_measurable_exp) |
544 assumes [simp, arith]: "0 < l" |
208 |
545 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)" |
209 lemma (in prob_space) exponential_distributed_expectation: |
546 assumes ind: "indep_vars (\<lambda>i. borel) X I" |
210 assumes D: "distributed M lborel X (exponential_density l)" |
547 shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)" |
211 shows "expectation X = 1 / l" |
548 using assms |
212 proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric]) |
549 proof (induct rule: finite_ne_induct) |
213 have "0 < l" |
550 case (singleton i) then show ?case by auto |
214 using exponential_distributed_params[OF D] . |
551 next |
215 have [simp]: "\<And>x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) = |
552 case (insert i I) |
216 x * exponential_density l x" |
553 then have "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) (erlang_density (Suc (k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1) l)" |
217 using `0 < l` |
554 by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset) |
218 by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def) |
555 also have "(\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) = (\<lambda>x. \<Sum>i\<in>insert i I. X i x)" |
219 from borel_integral_x_exp `0 < l` |
556 using insert by auto |
220 have "has_bochner_integral lborel (\<lambda>x. exponential_density l x * x) (1 / l)" |
557 also have "Suc(k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1 = (\<Sum>i\<in>insert i I. Suc (k i)) - 1" |
221 by (subst (asm) lborel_has_bochner_integral_real_affine_iff[of l _ _ 0]) |
558 using insert by (auto intro!: Suc_pred simp: ac_simps) |
222 (simp_all add: field_simps) |
559 finally show ?case by fast |
223 then show "(\<integral> x. exponential_density l x * x \<partial>lborel) = 1 / l" |
560 qed |
224 by (metis has_bochner_integral_integral_eq) |
561 |
225 qed simp |
562 lemma (in prob_space) exponential_distributed_setsum: |
|
563 assumes finI: "finite I" |
|
564 assumes A: "I \<noteq> {}" |
|
565 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)" |
|
566 assumes ind: "indep_vars (\<lambda>i. borel) X I" |
|
567 shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)" |
|
568 proof - |
|
569 obtain i where "i \<in> I" using assms by auto |
|
570 note exponential_distributed_params[OF expX[OF this]] |
|
571 from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp |
|
572 qed |
226 |
573 |
227 subsection {* Uniform distribution *} |
574 subsection {* Uniform distribution *} |
228 |
575 |
229 lemma uniform_distrI: |
576 lemma uniform_distrI: |
230 assumes X: "X \<in> measurable M M'" |
577 assumes X: "X \<in> measurable M M'" |