author | nipkow |
Fri, 11 Apr 2014 13:36:57 +0200 | |
changeset 56536 | aefb4a8da31f |
parent 56381 | 0556204bc230 |
child 56571 | f4635657d66f |
permissions | -rw-r--r-- |
50419 | 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)" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
55 |
by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff) |
50419 | 56 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
57 |
have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)" |
50419 | 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" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
74 |
have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)" |
50419 | 75 |
by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator) |
76 |
(auto simp: exponential_density_def) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
77 |
also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)" |
50419 | 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) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
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)" |
50419 | 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 " |
|
56536 | 151 |
by (auto simp: exponential_density_def) |
50419 | 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) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
170 |
then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top" |
50419 | 171 |
proof eventually_elim |
172 |
fix b :: real assume [simp]: "0 \<le> b" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
173 |
have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^sup>L lborel (?f b)) = |
50419 | 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)" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
181 |
by (auto intro!: derivative_eq_intros) |
50419 | 182 |
show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x " |
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
53077
diff
changeset
|
183 |
by (intro continuous_intros) |
50419 | 184 |
qed fact |
185 |
also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)" |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
186 |
by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
187 |
finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" |
50419 | 188 |
by (auto simp: field_simps exp_minus inverse_eq_divide) |
189 |
qed |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
190 |
then have "((\<lambda>i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top" |
50419 | 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 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
196 |
then show "(\<lambda>i. integral\<^sup>L lborel (?f i)) ----> 1" |
50419 | 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 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
240 |
also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')" |
50419 | 241 |
using A B |
242 |
by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
243 |
also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')" |
50419 | 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 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
270 |
have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
271 |
(\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" |
50419 | 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) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
278 |
finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
50419 | 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]) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
328 |
also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)" |
50419 | 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 |
|
53077 | 375 |
show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" |
50419 | 376 |
using uniform_distributed_params[OF D] |
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
377 |
by (auto intro!: derivative_eq_intros) |
50419 | 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) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
381 |
have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = |
50419 | 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]) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset
|
385 |
show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" |
50419 | 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 |