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
