theory Distributions imports Probability_Measure begin subsection {* Exponential distribution *} definition exponential_density :: "real \ real \ real" where "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" lemma borel_measurable_exponential_density[measurable]: "exponential_density l \ borel_measurable borel" by (auto simp add: exponential_density_def[abs_def]) lemma (in prob_space) exponential_distributed_params: assumes D: "distributed M lborel X (exponential_density l)" shows "0 < l" proof (cases l "0 :: real" rule: linorder_cases) assume "l < 0" have "emeasure lborel {0 <.. 1::real} \ emeasure lborel {x :: real \ space lborel. 0 < x}" by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric]) also have "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" proof - have "AE x in lborel. 0 \ exponential_density l x" using assms by (auto simp: distributed_real_AE) then have "AE x in lborel. x \ (0::real)" apply eventually_elim using `l < 0` apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) done then show "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) qed finally show "0 < l" by simp next assume "l = 0" then have [simp]: "\x. ereal (exponential_density l x) = 0" by (simp add: exponential_density_def) interpret X: prob_space "distr M lborel X" using distributed_measurable[OF D] by (rule prob_space_distr) from X.emeasure_space_1 show "0 < l" by (simp add: emeasure_density distributed_distr_eq_density[OF D]) qed assumption lemma assumes [arith]: "0 < l" shows emeasure_exponential_density_le0: "0 \ a \ emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)" and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))" (is "prob_space ?D") proof - let ?f = "\x. l * exp (- x * l)" let ?F = "\x. - exp (- x * l)" have deriv: "\x. DERIV ?F x :> ?f x" "\x. 0 \ l * exp (- x * l)" by (auto intro!: DERIV_intros simp: zero_le_mult_iff) have "emeasure ?D (space ?D) = (\\<^sup>+ x. ereal (?f x) * indicator {0..} x \lborel)" by (auto simp: emeasure_density exponential_density_def intro!: positive_integral_cong split: split_indicator) also have "\ = ereal (0 - ?F 0)" proof (rule positive_integral_FTC_atLeast) have "((\x. exp (l * x)) ---> 0) at_bot" by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]]) (simp_all add: tendsto_const filterlim_ident) then show "((\x. - exp (- x * l)) ---> 0) at_top" unfolding filterlim_at_top_mirror by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps) qed (insert deriv, auto) also have "\ = 1" by (simp add: one_ereal_def) finally have "emeasure ?D (space ?D) = 1" . then show "prob_space ?D" by rule assume "0 \ a" have "emeasure ?D {..a} = (\\<^sup>+x. ereal (?f x) * indicator {0..a} x \lborel)" by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator) (auto simp: exponential_density_def) also have "(\\<^sup>+x. ereal (?f x) * indicator {0..a} x \lborel) = ereal (?F a) - ereal (?F 0)" using `0 \ a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto also have "\ = 1 - exp (- a * l)" by simp finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" . qed lemma (in prob_space) exponential_distributedD_le: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" shows "\

(x in M. X x \ a) = 1 - exp (- a * l)" proof - have "emeasure M {x \ space M. X x \ a } = emeasure (distr M lborel X) {.. a}" using distributed_measurable[OF D] by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) also have "\ = emeasure (density lborel (exponential_density l)) {.. a}" unfolding distributed_distr_eq_density[OF D] .. also have "\ = 1 - exp (- a * l)" using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] . finally show ?thesis by (auto simp: measure_def) qed lemma (in prob_space) exponential_distributedD_gt: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" shows "\

(x in M. a < X x ) = exp (- a * l)" proof - have "exp (- a * l) = 1 - \

(x in M. X x \ a)" unfolding exponential_distributedD_le[OF D a] by simp also have "\ = prob (space M - {x \ space M. X x \ a })" using distributed_measurable[OF D] by (subst prob_compl) auto also have "\ = \

(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le) finally show ?thesis by simp qed lemma (in prob_space) exponential_distributed_memoryless: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a"and t: "0 \ t" shows "\

(x in M. a + t < X x \ a < X x) = \

(x in M. t < X x)" proof - have "\

(x in M. a + t < X x \ a < X x) = \

(x in M. a + t < X x) / \

(x in M. a < X x)" using `0 \ t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) also have "\ = exp (- (a + t) * l) / exp (- a * l)" using a t by (simp add: exponential_distributedD_gt[OF D]) also have "\ = exp (- t * l)" using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) finally show ?thesis using t by (simp add: exponential_distributedD_gt[OF D]) qed lemma exponential_distributedI: assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l" and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = 1 - exp (- a * l)" shows "distributed M lborel X (exponential_density l)" proof (rule distributedI_borel_atMost) fix a :: real { assume "a \ 0" with X have "emeasure M {x\space M. X x \ a} \ emeasure M {x\space M. X x \ 0}" by (intro emeasure_mono) auto then have "emeasure M {x\space M. X x \ a} = 0" using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) } note eq_0 = this have "\x. \ 0 \ a \ ereal (exponential_density l x) * indicator {..a} x = 0" by (simp add: exponential_density_def) then show "(\\<^sup>+ x. exponential_density l x * indicator {..a} x \lborel) = ereal (if 0 \ a then 1 - exp (- a * l) else 0)" using emeasure_exponential_density_le0[of l a] by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator simp del: times_ereal.simps ereal_zero_times) show "emeasure M {x\space M. X x \ a} = ereal (if 0 \ a then 1 - exp (- a * l) else 0)" using X_distr[of a] eq_0 by (auto simp: one_ereal_def) show "AE x in lborel. 0 \ exponential_density l x " by (auto simp: exponential_density_def intro!: AE_I2 mult_nonneg_nonneg) qed simp_all lemma (in prob_space) exponential_distributed_iff: "distributed M lborel X (exponential_density l) \ (X \ borel_measurable M \ 0 < l \ (\a\0. \

(x in M. X x \ a) = 1 - exp (- a * l)))" using distributed_measurable[of M lborel X "exponential_density l"] exponential_distributed_params[of X l] emeasure_exponential_density_le0[of l] exponential_distributedD_le[of X l] by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure) lemma borel_integral_x_exp: "(\x. x * exp (- x) * indicator {0::real ..} x \lborel) = 1" proof (rule integral_monotone_convergence) let ?f = "\i x. x * exp (- x) * indicator {0::real .. i} x" have "eventually (\b::real. 0 \ b) at_top" by (rule eventually_ge_at_top) then have "eventually (\b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top" proof eventually_elim fix b :: real assume [simp]: "0 \ b" have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) - (integral\<^sup>L lborel (?f b)) = (\x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \lborel)" by (subst integral_diff(2)[symmetric]) (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator) also have "\ = b * exp (-b) - 0 * exp (- 0)" proof (rule integral_FTC_atLeastAtMost) fix x assume "0 \ x" "x \ b" show "DERIV (\x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" by (auto intro!: DERIV_intros) show "isCont (\x. exp (- x) - x * exp (- x)) x " by (intro isCont_intros isCont_exp') qed fact also have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) = - exp (- b) - - exp (- 0)" by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" by (auto simp: field_simps exp_minus inverse_eq_divide) qed then have "((\i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top" proof (rule Lim_transform_eventually) show "((\i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top" using tendsto_power_div_exp_0[of 1] by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp qed then show "(\i. integral\<^sup>L lborel (?f i)) ----> 1" by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp show "AE x in lborel. mono (\n::nat. x * exp (- x) * indicator {0..real n} x)" by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator) show "\i::nat. integrable lborel (\x. x * exp (- x) * indicator {0..real i} x)" by (rule borel_integrable_atLeastAtMost) auto show "AE x in lborel. (\i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x" apply (intro AE_I2 Lim_eventually ) apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI) apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator) done qed (auto intro!: borel_measurable_times borel_measurable_exp) lemma (in prob_space) exponential_distributed_expectation: assumes D: "distributed M lborel X (exponential_density l)" shows "expectation X = 1 / l" proof (subst distributed_integral[OF D, of "\x. x", symmetric]) have "0 < l" using exponential_distributed_params[OF D] . have [simp]: "\x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) = x * exponential_density l x" using `0 < l` by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def) from borel_integral_x_exp `0 < l` show "(\ x. exponential_density l x * x \lborel) = 1 / l" by (subst (asm) lebesgue_integral_real_affine[of "l" _ 0]) (simp_all add: borel_measurable_exp nonzero_eq_divide_eq ac_simps) qed simp subsection {* Uniform distribution *} lemma uniform_distrI: assumes X: "X \ measurable M M'" and A: "A \ sets M'" "emeasure M' A \ \" "emeasure M' A \ 0" assumes distr: "\B. B \ sets M' \ emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" shows "distr M M' X = uniform_measure M' A" unfolding uniform_measure_def proof (intro measure_eqI) let ?f = "\x. indicator A x / emeasure M' A" fix B assume B: "B \ sets (distr M M' X)" with X have "emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" by (simp add: distr[of B] measurable_sets) also have "\ = (1 / emeasure M' A) * emeasure M' (A \ B)" by simp also have "\ = (\\<^sup>+ x. (1 / emeasure M' A) * indicator (A \ B) x \M')" using A B by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) also have "\ = (\\<^sup>+ x. ?f x * indicator B x \M')" by (rule positive_integral_cong) (auto split: split_indicator) finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" using A B X by (auto simp add: emeasure_distr emeasure_density) qed simp lemma uniform_distrI_borel: fixes A :: "real set" assumes X[measurable]: "X \ borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r" and [measurable]: "A \ sets borel" assumes distr: "\a. emeasure M {x\space M. X x \ a} = emeasure lborel (A \ {.. a}) / r" shows "distributed M lborel X (\x. indicator A x / measure lborel A)" proof (rule distributedI_borel_atMost) let ?f = "\x. 1 / r * indicator A x" fix a have "emeasure lborel (A \ {..a}) \ emeasure lborel A" using A by (intro emeasure_mono) auto also have "\ < \" using A by simp finally have fin: "emeasure lborel (A \ {..a}) \ \" by simp from emeasure_eq_ereal_measure[OF this] have fin_eq: "emeasure lborel (A \ {..a}) / r = ereal (measure lborel (A \ {..a}) / r)" using A by simp then show "emeasure M {x\space M. X x \ a} = ereal (measure lborel (A \ {..a}) / r)" using distr by simp have "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = (\\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \ {..a}) x \lborel)" by (auto intro!: positive_integral_cong split: split_indicator) also have "\ = ereal (1 / measure lborel A) * emeasure lborel (A \ {..a})" using `A \ sets borel` by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg) also have "\ = ereal (measure lborel (A \ {..a}) / r)" unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) finally show "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = ereal (measure lborel (A \ {..a}) / r)" . qed (auto intro!: divide_nonneg_nonneg measure_nonneg) lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: fixes a b :: real assumes X: "X \ borel_measurable M" and "a < b" assumes distr: "\t. a \ t \ t \ b \ \

(x in M. X x \ t) = (t - a) / (b - a)" shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b})" proof (rule uniform_distrI_borel) fix t have "t < a \ (a \ t \ t \ b) \ b < t" by auto then show "emeasure M {x\space M. X x \ t} = emeasure lborel ({a .. b} \ {..t}) / (b - a)" proof (elim disjE conjE) assume "t < a" then have "emeasure M {x\space M. X x \ t} \ emeasure M {x\space M. X x \ a}" using X by (auto intro!: emeasure_mono measurable_sets) also have "\ = 0" using distr[of a] `a < b` by (simp add: emeasure_eq_measure) finally have "emeasure M {x\space M. X x \ t} = 0" by (simp add: antisym measure_nonneg emeasure_le_0_iff) with `t < a` show ?thesis by simp next assume bnds: "a \ t" "t \ b" have "{a..b} \ {..t} = {a..t}" using bnds by auto then show ?thesis using `a \ t` `a < b` using distr[OF bnds] by (simp add: emeasure_eq_measure) next assume "b < t" have "1 = emeasure M {x\space M. X x \ b}" using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure) also have "\ \ emeasure M {x\space M. X x \ t}" using X `b < t` by (auto intro!: emeasure_mono measurable_sets) finally have "emeasure M {x\space M. X x \ t} = 1" by (simp add: antisym emeasure_eq_measure one_ereal_def) with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def) qed qed (insert X `a < b`, auto) lemma (in prob_space) uniform_distributed_measure: fixes a b :: real assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" assumes " a \ t" "t \ b" shows "\

(x in M. X x \ t) = (t - a) / (b - a)" proof - have "emeasure M {x \ space M. X x \ t} = emeasure (distr M lborel X) {.. t}" using distributed_measurable[OF D] by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) also have "\ = (\\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \lborel)" using distributed_borel_measurable[OF D] `a \ t` `t \ b` unfolding distributed_distr_eq_density[OF D] by (subst emeasure_density) (auto intro!: positive_integral_cong simp: measure_def split: split_indicator) also have "\ = ereal (1 / (b - a)) * (t - a)" using `a \ t` `t \ b` by (subst positive_integral_cmult_indicator) auto finally show ?thesis by (simp add: measure_def) qed lemma (in prob_space) uniform_distributed_bounds: fixes a b :: real assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" shows "a < b" proof (rule ccontr) assume "\ a < b" then have "{a .. b} = {} \ {a .. b} = {a .. a}" by simp with uniform_distributed_params[OF D] show False by (auto simp: measure_def) qed lemma (in prob_space) uniform_distributed_iff: fixes a b :: real shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b}) \ (X \ borel_measurable M \ a < b \ (\t\{a .. b}. \

(x in M. X x \ t)= (t - a) / (b - a)))" using uniform_distributed_bounds[of X a b] uniform_distributed_measure[of X a b] distributed_measurable[of M lborel X] by (auto intro!: uniform_distrI_borel_atLeastAtMost simp: one_ereal_def emeasure_eq_measure) lemma (in prob_space) uniform_distributed_expectation: fixes a b :: real assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" shows "expectation X = (a + b) / 2" proof (subst distributed_integral[OF D, of "\x. x", symmetric]) have "a < b" using uniform_distributed_bounds[OF D] . have "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel)" by (intro integral_cong) auto also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2" proof (subst integral_FTC_atLeastAtMost) fix x show "DERIV (\x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" using uniform_distributed_params[OF D] by (auto intro!: DERIV_intros) show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x" using uniform_distributed_params[OF D] by (auto intro!: isCont_divide) have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (b*b - a * a) / (2 * (b - a))" using `a < b` by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" using `a < b` unfolding * square_diff_square_factored by (auto simp: field_simps) qed (insert `a < b`, simp) finally show "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (a + b) / 2" . qed auto end