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)"
|
|
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
|