|
1 theory Distributions |
|
2 imports Probability_Measure |
|
3 begin |
|
4 |
|
5 subsection {* Exponential distribution *} |
|
6 |
|
7 definition exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where |
|
8 "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" |
|
9 |
|
10 lemma borel_measurable_exponential_density[measurable]: "exponential_density l \<in> borel_measurable borel" |
|
11 by (auto simp add: exponential_density_def[abs_def]) |
|
12 |
|
13 lemma (in prob_space) exponential_distributed_params: |
|
14 assumes D: "distributed M lborel X (exponential_density l)" |
|
15 shows "0 < l" |
|
16 proof (cases l "0 :: real" rule: linorder_cases) |
|
17 assume "l < 0" |
|
18 have "emeasure lborel {0 <.. 1::real} \<le> |
|
19 emeasure lborel {x :: real \<in> space lborel. 0 < x}" |
|
20 by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric]) |
|
21 also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" |
|
22 proof - |
|
23 have "AE x in lborel. 0 \<le> exponential_density l x" |
|
24 using assms by (auto simp: distributed_real_AE) |
|
25 then have "AE x in lborel. x \<le> (0::real)" |
|
26 apply eventually_elim |
|
27 using `l < 0` |
|
28 apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) |
|
29 done |
|
30 then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" |
|
31 by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) |
|
32 qed |
|
33 finally show "0 < l" by simp |
|
34 next |
|
35 assume "l = 0" |
|
36 then have [simp]: "\<And>x. ereal (exponential_density l x) = 0" |
|
37 by (simp add: exponential_density_def) |
|
38 interpret X: prob_space "distr M lborel X" |
|
39 using distributed_measurable[OF D] by (rule prob_space_distr) |
|
40 from X.emeasure_space_1 |
|
41 show "0 < l" |
|
42 by (simp add: emeasure_density distributed_distr_eq_density[OF D]) |
|
43 qed assumption |
|
44 |
|
45 lemma |
|
46 assumes [arith]: "0 < l" |
|
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!: DERIV_intros simp: zero_le_mult_iff) |
|
56 |
|
57 have "emeasure ?D (space ?D) = (\<integral>\<^isup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)" |
|
58 by (auto simp: emeasure_density exponential_density_def |
|
59 intro!: positive_integral_cong split: split_indicator) |
|
60 also have "\<dots> = ereal (0 - ?F 0)" |
|
61 proof (rule positive_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>\<^isup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)" |
|
75 by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator) |
|
76 (auto simp: exponential_density_def) |
|
77 also have "(\<integral>\<^isup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)" |
|
78 using `0 \<le> a` deriv by (intro positive_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 |
|
85 lemma (in prob_space) exponential_distributedD_le: |
|
86 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)" |
|
88 proof - |
|
89 have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}" |
|
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 |
|
100 lemma (in prob_space) exponential_distributedD_gt: |
|
101 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)" |
|
103 proof - |
|
104 have "exp (- a * l) = 1 - \<P>(x in M. X x \<le> a)" |
|
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 |
|
114 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" |
|
116 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" |
|
117 proof - |
|
118 have "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. a + t < X x) / \<P>(x in M. a < X x)" |
|
119 using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) |
|
120 also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)" |
|
121 using a t by (simp add: exponential_distributedD_gt[OF D]) |
|
122 also have "\<dots> = exp (- t * l)" |
|
123 using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) |
|
124 finally show ?thesis |
|
125 using t by (simp add: exponential_distributedD_gt[OF D]) |
|
126 qed |
|
127 |
|
128 lemma exponential_distributedI: |
|
129 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)" |
|
131 shows "distributed M lborel X (exponential_density l)" |
|
132 proof (rule distributedI_borel_atMost) |
|
133 fix a :: real |
|
134 |
|
135 { assume "a \<le> 0" |
|
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>\<^isup>+ 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 intro!: AE_I2 mult_nonneg_nonneg) |
|
152 qed simp_all |
|
153 |
|
154 lemma (in prob_space) exponential_distributed_iff: |
|
155 "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)))" |
|
157 using |
|
158 distributed_measurable[of M lborel X "exponential_density l"] |
|
159 exponential_distributed_params[of X l] |
|
160 emeasure_exponential_density_le0[of l] |
|
161 exponential_distributedD_le[of X l] |
|
162 by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure) |
|
163 |
|
164 lemma borel_integral_x_exp: |
|
165 "(\<integral>x. x * exp (- x) * indicator {0::real ..} x \<partial>lborel) = 1" |
|
166 proof (rule integral_monotone_convergence) |
|
167 let ?f = "\<lambda>i x. x * exp (- x) * indicator {0::real .. i} x" |
|
168 have "eventually (\<lambda>b::real. 0 \<le> b) at_top" |
|
169 by (rule eventually_ge_at_top) |
|
170 then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^isup>L lborel (?f b)) at_top" |
|
171 proof eventually_elim |
|
172 fix b :: real assume [simp]: "0 \<le> b" |
|
173 have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^isup>L lborel (?f b)) = |
|
174 (\<integral>x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \<partial>lborel)" |
|
175 by (subst integral_diff(2)[symmetric]) |
|
176 (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator) |
|
177 also have "\<dots> = b * exp (-b) - 0 * exp (- 0)" |
|
178 proof (rule integral_FTC_atLeastAtMost) |
|
179 fix x assume "0 \<le> x" "x \<le> b" |
|
180 show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" |
|
181 by (auto intro!: DERIV_intros) |
|
182 show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x " |
|
183 by (intro isCont_intros isCont_exp') |
|
184 qed fact |
|
185 also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)" |
|
186 by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) |
|
187 finally show "1 - (inverse (exp b) + b / exp b) = integral\<^isup>L lborel (?f b)" |
|
188 by (auto simp: field_simps exp_minus inverse_eq_divide) |
|
189 qed |
|
190 then have "((\<lambda>i. integral\<^isup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top" |
|
191 proof (rule Lim_transform_eventually) |
|
192 show "((\<lambda>i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top" |
|
193 using tendsto_power_div_exp_0[of 1] |
|
194 by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp |
|
195 qed |
|
196 then show "(\<lambda>i. integral\<^isup>L lborel (?f i)) ----> 1" |
|
197 by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp |
|
198 show "AE x in lborel. mono (\<lambda>n::nat. x * exp (- x) * indicator {0..real n} x)" |
|
199 by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator) |
|
200 show "\<And>i::nat. integrable lborel (\<lambda>x. x * exp (- x) * indicator {0..real i} x)" |
|
201 by (rule borel_integrable_atLeastAtMost) auto |
|
202 show "AE x in lborel. (\<lambda>i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x" |
|
203 apply (intro AE_I2 Lim_eventually ) |
|
204 apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI) |
|
205 apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator) |
|
206 done |
|
207 qed (auto intro!: borel_measurable_times borel_measurable_exp) |
|
208 |
|
209 lemma (in prob_space) exponential_distributed_expectation: |
|
210 assumes D: "distributed M lborel X (exponential_density l)" |
|
211 shows "expectation X = 1 / l" |
|
212 proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric]) |
|
213 have "0 < l" |
|
214 using exponential_distributed_params[OF D] . |
|
215 have [simp]: "\<And>x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) = |
|
216 x * exponential_density l x" |
|
217 using `0 < l` |
|
218 by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def) |
|
219 from borel_integral_x_exp `0 < l` |
|
220 show "(\<integral> x. exponential_density l x * x \<partial>lborel) = 1 / l" |
|
221 by (subst (asm) lebesgue_integral_real_affine[of "l" _ 0]) |
|
222 (simp_all add: borel_measurable_exp nonzero_eq_divide_eq ac_simps) |
|
223 qed simp |
|
224 |
|
225 subsection {* Uniform distribution *} |
|
226 |
|
227 lemma uniform_distrI: |
|
228 assumes X: "X \<in> measurable M M'" |
|
229 and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0" |
|
230 assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" |
|
231 shows "distr M M' X = uniform_measure M' A" |
|
232 unfolding uniform_measure_def |
|
233 proof (intro measure_eqI) |
|
234 let ?f = "\<lambda>x. indicator A x / emeasure M' A" |
|
235 fix B assume B: "B \<in> sets (distr M M' X)" |
|
236 with X have "emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" |
|
237 by (simp add: distr[of B] measurable_sets) |
|
238 also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)" |
|
239 by simp |
|
240 also have "\<dots> = (\<integral>\<^isup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')" |
|
241 using A B |
|
242 by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) |
|
243 also have "\<dots> = (\<integral>\<^isup>+ x. ?f x * indicator B x \<partial>M')" |
|
244 by (rule positive_integral_cong) (auto split: split_indicator) |
|
245 finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" |
|
246 using A B X by (auto simp add: emeasure_distr emeasure_density) |
|
247 qed simp |
|
248 |
|
249 lemma uniform_distrI_borel: |
|
250 fixes A :: "real set" |
|
251 assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r" |
|
252 and [measurable]: "A \<in> sets borel" |
|
253 assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r" |
|
254 shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)" |
|
255 proof (rule distributedI_borel_atMost) |
|
256 let ?f = "\<lambda>x. 1 / r * indicator A x" |
|
257 fix a |
|
258 have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A" |
|
259 using A by (intro emeasure_mono) auto |
|
260 also have "\<dots> < \<infinity>" |
|
261 using A by simp |
|
262 finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>" |
|
263 by simp |
|
264 from emeasure_eq_ereal_measure[OF this] |
|
265 have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ereal (measure lborel (A \<inter> {..a}) / r)" |
|
266 using A by simp |
|
267 then show "emeasure M {x\<in>space M. X x \<le> a} = ereal (measure lborel (A \<inter> {..a}) / r)" |
|
268 using distr by simp |
|
269 |
|
270 have "(\<integral>\<^isup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
|
271 (\<integral>\<^isup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" |
|
272 by (auto intro!: positive_integral_cong split: split_indicator) |
|
273 also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})" |
|
274 using `A \<in> sets borel` |
|
275 by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg) |
|
276 also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)" |
|
277 unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) |
|
278 finally show "(\<integral>\<^isup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
|
279 ereal (measure lborel (A \<inter> {..a}) / r)" . |
|
280 qed (auto intro!: divide_nonneg_nonneg measure_nonneg) |
|
281 |
|
282 lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: |
|
283 fixes a b :: real |
|
284 assumes X: "X \<in> borel_measurable M" and "a < b" |
|
285 assumes distr: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> \<P>(x in M. X x \<le> t) = (t - a) / (b - a)" |
|
286 shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})" |
|
287 proof (rule uniform_distrI_borel) |
|
288 fix t |
|
289 have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t" |
|
290 by auto |
|
291 then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b - a)" |
|
292 proof (elim disjE conjE) |
|
293 assume "t < a" |
|
294 then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}" |
|
295 using X by (auto intro!: emeasure_mono measurable_sets) |
|
296 also have "\<dots> = 0" |
|
297 using distr[of a] `a < b` by (simp add: emeasure_eq_measure) |
|
298 finally have "emeasure M {x\<in>space M. X x \<le> t} = 0" |
|
299 by (simp add: antisym measure_nonneg emeasure_le_0_iff) |
|
300 with `t < a` show ?thesis by simp |
|
301 next |
|
302 assume bnds: "a \<le> t" "t \<le> b" |
|
303 have "{a..b} \<inter> {..t} = {a..t}" |
|
304 using bnds by auto |
|
305 then show ?thesis using `a \<le> t` `a < b` |
|
306 using distr[OF bnds] by (simp add: emeasure_eq_measure) |
|
307 next |
|
308 assume "b < t" |
|
309 have "1 = emeasure M {x\<in>space M. X x \<le> b}" |
|
310 using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure) |
|
311 also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}" |
|
312 using X `b < t` by (auto intro!: emeasure_mono measurable_sets) |
|
313 finally have "emeasure M {x\<in>space M. X x \<le> t} = 1" |
|
314 by (simp add: antisym emeasure_eq_measure one_ereal_def) |
|
315 with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def) |
|
316 qed |
|
317 qed (insert X `a < b`, auto) |
|
318 |
|
319 lemma (in prob_space) uniform_distributed_measure: |
|
320 fixes a b :: real |
|
321 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" |
|
322 assumes " a \<le> t" "t \<le> b" |
|
323 shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)" |
|
324 proof - |
|
325 have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}" |
|
326 using distributed_measurable[OF D] |
|
327 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) |
|
328 also have "\<dots> = (\<integral>\<^isup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)" |
|
329 using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b` |
|
330 unfolding distributed_distr_eq_density[OF D] |
|
331 by (subst emeasure_density) |
|
332 (auto intro!: positive_integral_cong simp: measure_def split: split_indicator) |
|
333 also have "\<dots> = ereal (1 / (b - a)) * (t - a)" |
|
334 using `a \<le> t` `t \<le> b` |
|
335 by (subst positive_integral_cmult_indicator) auto |
|
336 finally show ?thesis |
|
337 by (simp add: measure_def) |
|
338 qed |
|
339 |
|
340 lemma (in prob_space) uniform_distributed_bounds: |
|
341 fixes a b :: real |
|
342 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" |
|
343 shows "a < b" |
|
344 proof (rule ccontr) |
|
345 assume "\<not> a < b" |
|
346 then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp |
|
347 with uniform_distributed_params[OF D] show False |
|
348 by (auto simp: measure_def) |
|
349 qed |
|
350 |
|
351 lemma (in prob_space) uniform_distributed_iff: |
|
352 fixes a b :: real |
|
353 shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> |
|
354 (X \<in> borel_measurable M \<and> a < b \<and> (\<forall>t\<in>{a .. b}. \<P>(x in M. X x \<le> t)= (t - a) / (b - a)))" |
|
355 using |
|
356 uniform_distributed_bounds[of X a b] |
|
357 uniform_distributed_measure[of X a b] |
|
358 distributed_measurable[of M lborel X] |
|
359 by (auto intro!: uniform_distrI_borel_atLeastAtMost simp: one_ereal_def emeasure_eq_measure) |
|
360 |
|
361 lemma (in prob_space) uniform_distributed_expectation: |
|
362 fixes a b :: real |
|
363 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" |
|
364 shows "expectation X = (a + b) / 2" |
|
365 proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric]) |
|
366 have "a < b" |
|
367 using uniform_distributed_bounds[OF D] . |
|
368 |
|
369 have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = |
|
370 (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)" |
|
371 by (intro integral_cong) auto |
|
372 also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2" |
|
373 proof (subst integral_FTC_atLeastAtMost) |
|
374 fix x |
|
375 show "DERIV (\<lambda>x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" |
|
376 using uniform_distributed_params[OF D] |
|
377 by (auto intro!: DERIV_intros) |
|
378 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" |
|
379 using uniform_distributed_params[OF D] |
|
380 by (auto intro!: isCont_divide) |
|
381 have *: "b\<twosuperior> / (2 * measure lborel {a..b}) - a\<twosuperior> / (2 * measure lborel {a..b}) = |
|
382 (b*b - a * a) / (2 * (b - a))" |
|
383 using `a < b` |
|
384 by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) |
|
385 show "b\<twosuperior> / (2 * measure lborel {a..b}) - a\<twosuperior> / (2 * measure lborel {a..b}) = (a + b) / 2" |
|
386 using `a < b` |
|
387 unfolding * square_diff_square_factored by (auto simp: field_simps) |
|
388 qed (insert `a < b`, simp) |
|
389 finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" . |
|
390 qed auto |
|
391 |
|
392 end |