author  wenzelm 
Tue, 13 Aug 2013 16:25:47 +0200  
changeset 53015  a1119cf551e8 
parent 50419  3177d0374701 
child 53077  a1b3784f8129 
permissions  rwrr 
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 

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 " 

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) 

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

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) 

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 

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) 

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 