hoelzl@57235: (* Title: HOL/Probability/Distributions.thy hoelzl@57235: Author: Sudeep Kanav, TU München hoelzl@57254: Author: Johannes Hölzl, TU München hoelzl@57254: Author: Jeremy Avigad, CMU *) hoelzl@57235: hoelzl@57235: header {* Properties of Various Distributions *} hoelzl@57235: hoelzl@50419: theory Distributions hoelzl@57252: imports Convolution Information hoelzl@50419: begin hoelzl@50419: hoelzl@57252: lemma (in prob_space) distributed_affine: hoelzl@57252: fixes f :: "real \ ereal" hoelzl@57252: assumes f: "distributed M lborel X f" hoelzl@57252: assumes c: "c \ 0" hoelzl@57252: shows "distributed M lborel (\x. t + c * X x) (\x. f ((x - t) / c) / \c\)" hoelzl@57252: unfolding distributed_def hoelzl@57252: proof safe hoelzl@57252: have [measurable]: "f \ borel_measurable borel" hoelzl@57252: using f by (simp add: distributed_def) hoelzl@57252: have [measurable]: "X \ borel_measurable M" hoelzl@57252: using f by (simp add: distributed_def) hoelzl@57252: hoelzl@57252: show "(\x. f ((x - t) / c) / \c\) \ borel_measurable lborel" hoelzl@57252: by simp hoelzl@57252: show "random_variable lborel (\x. t + c * X x)" hoelzl@57252: by simp hoelzl@57252: hoelzl@57252: have "AE x in lborel. 0 \ f x" hoelzl@57252: using f by (simp add: distributed_def) hoelzl@57252: from AE_borel_affine[OF _ _ this, where c="1/c" and t="- t / c"] c hoelzl@57252: show "AE x in lborel. 0 \ f ((x - t) / c) / ereal \c\" hoelzl@57252: by (auto simp add: field_simps) hoelzl@57252: hoelzl@57252: have eq: "\x. ereal \c\ * (f x / ereal \c\) = f x" haftmann@57514: using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric]) hoelzl@57252: hoelzl@57252: have "density lborel f = distr M lborel X" hoelzl@57252: using f by (simp add: distributed_def) hoelzl@57252: with c show "distr M lborel (\x. t + c * X x) = density lborel (\x. f ((x - t) / c) / ereal \c\)" hoelzl@57252: by (subst (2) lborel_real_affine[where c="c" and t="t"]) hoelzl@57252: (simp_all add: density_density_eq density_distr distr_distr field_simps eq cong: distr_cong) hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma (in prob_space) distributed_affineI: hoelzl@57252: fixes f :: "real \ ereal" hoelzl@57252: assumes f: "distributed M lborel (\x. (X x - t) / c) (\x. \c\ * f (x * c + t))" hoelzl@57252: assumes c: "c \ 0" hoelzl@57252: shows "distributed M lborel X f" hoelzl@57252: proof - hoelzl@57252: have eq: "\x. f x * ereal \c\ / ereal \c\ = f x" haftmann@57514: using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric]) hoelzl@57252: hoelzl@57252: show ?thesis hoelzl@57252: using distributed_affine[OF f c, where t=t] c hoelzl@57252: by (simp add: field_simps eq) hoelzl@57252: qed hoelzl@57252: hoelzl@57235: lemma (in prob_space) distributed_AE2: hoelzl@57235: assumes [measurable]: "distributed M N X f" "Measurable.pred N P" hoelzl@57235: shows "(AE x in M. P (X x)) \ (AE x in N. 0 < f x \ P x)" hoelzl@57235: proof - hoelzl@57235: have "(AE x in M. P (X x)) \ (AE x in distr M N X. P x)" hoelzl@57235: by (simp add: AE_distr_iff) hoelzl@57235: also have "\ \ (AE x in density N f. P x)" hoelzl@57235: unfolding distributed_distr_eq_density[OF assms(1)] .. hoelzl@57235: also have "\ \ (AE x in N. 0 < f x \ P x)" hoelzl@57235: by (rule AE_density) simp hoelzl@57235: finally show ?thesis . hoelzl@57235: qed hoelzl@57235: hoelzl@57235: subsection {* Erlang *} hoelzl@57235: hoelzl@57235: lemma nn_intergal_power_times_exp_Icc: hoelzl@57235: assumes [arith]: "0 \ a" hoelzl@57235: shows "(\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \lborel) = hoelzl@57235: (1 - (\n\k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _") hoelzl@57235: proof - hoelzl@57235: let ?f = "\k x. x^k * exp (-x) / fact k" hoelzl@57235: let ?F = "\k x. - (\n\k. (x^n * exp (-x)) / fact n)" hoelzl@57235: hoelzl@57235: have "?I * (inverse (fact k)) = hoelzl@57235: (\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \lborel)" hoelzl@57235: by (intro nn_integral_multc[symmetric]) auto hoelzl@57235: also have "\ = (\\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \lborel)" hoelzl@57235: by (intro nn_integral_cong) (simp add: field_simps) hoelzl@57447: also have "\ = ereal (?F k a - ?F k 0)" hoelzl@57447: proof (rule nn_integral_FTC_Icc) hoelzl@57235: fix x assume "x \ {0..a}" hoelzl@57235: show "DERIV (?F k) x :> ?f k x" hoelzl@57235: proof(induction k) hoelzl@57235: case 0 show ?case by (auto intro!: derivative_eq_intros) hoelzl@57235: next hoelzl@57235: case (Suc k) hoelzl@57235: have "DERIV (\x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :> hoelzl@57235: ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))" hoelzl@57235: by (intro DERIV_diff Suc) hoelzl@57235: (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc hoelzl@57235: simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric]) hoelzl@57235: also have "(\x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)" hoelzl@57235: by simp hoelzl@57235: also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x" hoelzl@57235: by (auto simp: field_simps simp del: fact_Suc) hoelzl@57235: (simp_all add: real_of_nat_Suc field_simps) hoelzl@57235: finally show ?case . hoelzl@57235: qed hoelzl@57235: qed auto hoelzl@57235: also have "\ = ereal (1 - (\n\k. (a^n * exp (-a)) / fact n))" haftmann@57418: by (auto simp: power_0_left if_distrib[where f="\x. x / a" for a] setsum.If_cases) hoelzl@57235: finally show ?thesis hoelzl@57235: by (cases "?I") (auto simp: field_simps) hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma nn_intergal_power_times_exp_Ici: hoelzl@57235: shows "(\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \lborel) = fact k" hoelzl@57235: proof (rule LIMSEQ_unique) hoelzl@57235: let ?X = "\n. \\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \lborel" hoelzl@57235: show "?X ----> (\\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \lborel)" hoelzl@57235: apply (intro nn_integral_LIMSEQ) hoelzl@57235: apply (auto simp: incseq_def le_fun_def eventually_sequentially hoelzl@57235: split: split_indicator intro!: Lim_eventually) hoelzl@57235: apply (metis natceiling_le_eq) hoelzl@57235: done hoelzl@57235: hoelzl@57235: have "((\x. (1 - (\n\k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\n\k. 0 / real (fact n))) * fact k) at_top" hoelzl@57235: by (intro tendsto_intros tendsto_power_div_exp_0) simp hoelzl@57235: then show "?X ----> fact k" hoelzl@57235: by (subst nn_intergal_power_times_exp_Icc) hoelzl@57235: (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially]) hoelzl@57235: qed hoelzl@57235: hoelzl@57235: definition erlang_density :: "nat \ real \ real \ real" where hoelzl@57235: "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)" hoelzl@57235: hoelzl@57235: definition erlang_CDF :: "nat \ real \ real \ real" where hoelzl@57235: "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\n\k. ((l * x)^n * exp (- l * x) / fact n)))" hoelzl@57235: hoelzl@57235: lemma erlang_density_nonneg: "0 \ l \ 0 \ erlang_density k l x" hoelzl@57235: by (simp add: erlang_density_def) hoelzl@57235: hoelzl@57235: lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \ borel_measurable borel" hoelzl@57235: by (auto simp add: erlang_density_def[abs_def]) hoelzl@57235: hoelzl@57235: lemma erlang_CDF_transform: "0 < l \ erlang_CDF k l a = erlang_CDF k 1 (l * a)" hoelzl@57235: by (auto simp add: erlang_CDF_def mult_less_0_iff) hoelzl@57235: hoelzl@57235: lemma nn_integral_erlang_density: hoelzl@57235: assumes [arith]: "0 < l" hoelzl@57235: shows "(\\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \lborel) = erlang_CDF k l a" hoelzl@57235: proof cases hoelzl@57235: assume [arith]: "0 \ a" hoelzl@57235: have eq: "\x. indicator {0..a} (x / l) = indicator {0..a*l} x" hoelzl@57235: by (simp add: field_simps split: split_indicator) hoelzl@57235: have "(\\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \lborel) = hoelzl@57235: (\\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \lborel)" hoelzl@57235: by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator) hoelzl@57235: also have "\ = (l/fact k) * (\\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \lborel)" hoelzl@57235: by (intro nn_integral_cmult) auto hoelzl@57235: also have "\ = ereal (l/fact k) * ((1/l) * (\\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \lborel))" hoelzl@57235: by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) hoelzl@57235: also have "\ = (1 - (\n\k. ((l * a)^n * exp (-(l * a))) / fact n))" hoelzl@57235: by (subst nn_intergal_power_times_exp_Icc) auto hoelzl@57235: also have "\ = erlang_CDF k l a" hoelzl@57235: by (auto simp: erlang_CDF_def) hoelzl@57235: finally show ?thesis . hoelzl@57235: next hoelzl@57235: assume "\ 0 \ a" hoelzl@57235: moreover then have "(\\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \lborel) = (\\<^sup>+x. 0 \(lborel::real measure))" hoelzl@57235: by (intro nn_integral_cong) (auto simp: erlang_density_def) hoelzl@57235: ultimately show ?thesis hoelzl@57235: by (simp add: erlang_CDF_def) hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma emeasure_erlang_density: hoelzl@57235: "0 < l \ emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a" hoelzl@57235: by (simp add: emeasure_density nn_integral_erlang_density) hoelzl@57235: hoelzl@57235: lemma nn_integral_erlang_ith_moment: hoelzl@57235: fixes k i :: nat and l :: real hoelzl@57235: assumes [arith]: "0 < l" hoelzl@57235: shows "(\\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \lborel) = fact (k + i) / (fact k * l ^ i)" hoelzl@57235: proof - hoelzl@57235: have eq: "\x. indicator {0..} (x / l) = indicator {0..} x" hoelzl@57235: by (simp add: field_simps split: split_indicator) hoelzl@57235: have "(\\<^sup>+ x. ereal (erlang_density k l x * x^i) \lborel) = hoelzl@57235: (\\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \lborel)" hoelzl@57235: by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator) hoelzl@57235: also have "\ = (l/(fact k * l^i)) * (\\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \lborel)" hoelzl@57235: by (intro nn_integral_cmult) auto hoelzl@57235: also have "\ = ereal (l/(fact k * l^i)) * ((1/l) * (\\<^sup>+x. ereal (x^(k+i) * exp (- x)) * indicator {0 ..} x \lborel))" hoelzl@57235: by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) hoelzl@57235: also have "\ = fact (k + i) / (fact k * l ^ i)" hoelzl@57235: by (subst nn_intergal_power_times_exp_Ici) auto hoelzl@57235: finally show ?thesis . hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma prob_space_erlang_density: hoelzl@57235: assumes l[arith]: "0 < l" hoelzl@57235: shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D") hoelzl@57235: proof hoelzl@57235: show "emeasure ?D (space ?D) = 1" hoelzl@57235: using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density) hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_distributed_le: hoelzl@57235: assumes D: "distributed M lborel X (erlang_density k l)" hoelzl@57235: assumes [simp, arith]: "0 < l" "0 \ a" hoelzl@57235: shows "\

(x in M. X x \ a) = erlang_CDF k l a" hoelzl@57235: proof - hoelzl@57235: have "emeasure M {x \ space M. X x \ a } = emeasure (distr M lborel X) {.. a}" hoelzl@57235: using distributed_measurable[OF D] hoelzl@57235: by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) hoelzl@57235: also have "\ = emeasure (density lborel (erlang_density k l)) {.. a}" hoelzl@57235: unfolding distributed_distr_eq_density[OF D] .. hoelzl@57235: also have "\ = erlang_CDF k l a" hoelzl@57235: by (auto intro!: emeasure_erlang_density) hoelzl@57235: finally show ?thesis hoelzl@57235: by (auto simp: measure_def) hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_distributed_gt: hoelzl@57235: assumes D[simp]: "distributed M lborel X (erlang_density k l)" hoelzl@57235: assumes [arith]: "0 < l" "0 \ a" hoelzl@57235: shows "\

(x in M. a < X x ) = 1 - (erlang_CDF k l a)" hoelzl@57235: proof - hoelzl@57235: have " 1 - (erlang_CDF k l a) = 1 - \

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

(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le) hoelzl@57235: finally show ?thesis by simp hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0" hoelzl@57235: by (induction k) (auto simp: erlang_CDF_def) hoelzl@57235: hoelzl@57235: lemma erlang_distributedI: hoelzl@57235: assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l" hoelzl@57235: and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = erlang_CDF k l a" hoelzl@57235: shows "distributed M lborel X (erlang_density k l)" hoelzl@57235: proof (rule distributedI_borel_atMost) hoelzl@57235: fix a :: real hoelzl@57235: { assume "a \ 0" hoelzl@57235: with X have "emeasure M {x\space M. X x \ a} \ emeasure M {x\space M. X x \ 0}" hoelzl@57235: by (intro emeasure_mono) auto hoelzl@57235: also have "... = 0" by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0]) hoelzl@57235: finally have "emeasure M {x\space M. X x \ a} \ 0" by simp hoelzl@57235: then have "emeasure M {x\space M. X x \ a} = 0" by (simp add:emeasure_le_0_iff) hoelzl@57235: } hoelzl@57235: note eq_0 = this hoelzl@57235: hoelzl@57235: show "(\\<^sup>+ x. erlang_density k l x * indicator {..a} x \lborel) = ereal (erlang_CDF k l a)" hoelzl@57235: using nn_integral_erlang_density[of l k a] hoelzl@57235: by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps) hoelzl@57235: hoelzl@57235: show "emeasure M {x\space M. X x \ a} = ereal (erlang_CDF k l a)" hoelzl@57235: using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def) hoelzl@57235: qed (simp_all add: erlang_density_nonneg) hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_distributed_iff: hoelzl@57235: assumes [arith]: "0 hoelzl@57235: (X \ borel_measurable M \ 0 < l \ (\a\0. \

(x in M. X x \ a) = erlang_CDF k l a ))" hoelzl@57235: using hoelzl@57235: distributed_measurable[of M lborel X "erlang_density k l"] hoelzl@57235: emeasure_erlang_density[of l] hoelzl@57235: erlang_distributed_le[of X k l] hoelzl@57235: by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_distributed_mult_const: hoelzl@57235: assumes erlX: "distributed M lborel X (erlang_density k l)" hoelzl@57235: assumes a_pos[arith]: "0 < \" "0 < l" hoelzl@57235: shows "distributed M lborel (\x. \ * X x) (erlang_density k (l / \))" hoelzl@57235: proof (subst erlang_distributed_iff, safe) hoelzl@57235: have [measurable]: "random_variable borel X" and [arith]: "0 < l " hoelzl@57235: and [simp]: "\a. 0 \ a \ prob {x \ space M. X x \ a} = erlang_CDF k l a" hoelzl@57235: by(insert erlX, auto simp: erlang_distributed_iff) hoelzl@57235: hoelzl@57235: show "random_variable borel (\x. \ * X x)" "0 < l / \" "0 < l / \" hoelzl@57235: by (auto simp:field_simps) hoelzl@57235: hoelzl@57235: fix a:: real assume [arith]: "0 \ a" hoelzl@57235: obtain b:: real where [simp, arith]: "b = a/ \" by blast hoelzl@57235: hoelzl@57235: have [arith]: "0 \ b" by (auto simp: divide_nonneg_pos) hoelzl@57235: hoelzl@57235: have "prob {x \ space M. \ * X x \ a} = prob {x \ space M. X x \ b}" hoelzl@57235: by (rule arg_cong[where f= prob]) (auto simp:field_simps) hoelzl@57235: hoelzl@57235: moreover have "prob {x \ space M. X x \ b} = erlang_CDF k l b" by auto hoelzl@57235: moreover have "erlang_CDF k (l / \) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto hoelzl@57235: ultimately show "prob {x \ space M. \ * X x \ a} = erlang_CDF k (l / \) a" by fastforce hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) has_bochner_integral_erlang_ith_moment: hoelzl@57235: fixes k i :: nat and l :: real hoelzl@57235: assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)" hoelzl@57235: shows "has_bochner_integral M (\x. X x ^ i) (fact (k + i) / (fact k * l ^ i))" hoelzl@57235: proof (rule has_bochner_integral_nn_integral) hoelzl@57235: show "AE x in M. 0 \ X x ^ i" hoelzl@57235: by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def) hoelzl@57235: show "(\\<^sup>+ x. ereal (X x ^ i) \M) = ereal (fact (k + i) / (fact k * l ^ i))" hoelzl@57235: using nn_integral_erlang_ith_moment[of l k i] hoelzl@57235: by (subst distributed_nn_integral[symmetric, OF D]) auto hoelzl@57235: qed (insert distributed_measurable[OF D], simp) hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_ith_moment_integrable: hoelzl@57235: "0 < l \ distributed M lborel X (erlang_density k l) \ integrable M (\x. X x ^ i)" hoelzl@57235: by rule (rule has_bochner_integral_erlang_ith_moment) hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_ith_moment: hoelzl@57235: "0 < l \ distributed M lborel X (erlang_density k l) \ hoelzl@57235: expectation (\x. X x ^ i) = fact (k + i) / (fact k * l ^ i)" hoelzl@57235: by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment) hoelzl@57235: hoelzl@57235: lemma (in prob_space) erlang_distributed_variance: hoelzl@57235: assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)" hoelzl@57235: shows "variance X = (k + 1) / l\<^sup>2" hoelzl@57235: proof (subst variance_eq) hoelzl@57235: show "integrable M X" "integrable M (\x. (X x)\<^sup>2)" hoelzl@57235: using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2] hoelzl@57235: by auto hoelzl@57235: hoelzl@57235: show "expectation (\x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" hoelzl@57235: using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] hoelzl@57235: by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc) hoelzl@57235: qed hoelzl@57235: hoelzl@50419: subsection {* Exponential distribution *} hoelzl@50419: hoelzl@57235: abbreviation exponential_density :: "real \ real \ real" where hoelzl@57235: "exponential_density \ erlang_density 0" hoelzl@50419: hoelzl@57235: lemma exponential_density_def: hoelzl@57235: "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" hoelzl@57235: by (simp add: fun_eq_iff erlang_density_def) hoelzl@57235: hoelzl@57235: lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \ a then 1 - exp (- l * a) else 0)" hoelzl@57235: by (simp add: erlang_CDF_def) hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributed_params: hoelzl@50419: assumes D: "distributed M lborel X (exponential_density l)" hoelzl@50419: shows "0 < l" hoelzl@50419: proof (cases l "0 :: real" rule: linorder_cases) hoelzl@50419: assume "l < 0" hoelzl@50419: have "emeasure lborel {0 <.. 1::real} \ hoelzl@50419: emeasure lborel {x :: real \ space lborel. 0 < x}" hoelzl@50419: by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric]) hoelzl@50419: also have "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" hoelzl@50419: proof - hoelzl@50419: have "AE x in lborel. 0 \ exponential_density l x" hoelzl@50419: using assms by (auto simp: distributed_real_AE) hoelzl@50419: then have "AE x in lborel. x \ (0::real)" hoelzl@50419: apply eventually_elim hoelzl@50419: using `l < 0` hoelzl@50419: apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) hoelzl@50419: done hoelzl@50419: then show "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" hoelzl@50419: by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) hoelzl@50419: qed hoelzl@50419: finally show "0 < l" by simp hoelzl@50419: next hoelzl@50419: assume "l = 0" hoelzl@50419: then have [simp]: "\x. ereal (exponential_density l x) = 0" hoelzl@50419: by (simp add: exponential_density_def) hoelzl@50419: interpret X: prob_space "distr M lborel X" hoelzl@50419: using distributed_measurable[OF D] by (rule prob_space_distr) hoelzl@50419: from X.emeasure_space_1 hoelzl@50419: show "0 < l" hoelzl@50419: by (simp add: emeasure_density distributed_distr_eq_density[OF D]) hoelzl@50419: qed assumption hoelzl@50419: hoelzl@57235: lemma prob_space_exponential_density: "0 < l \ prob_space (density lborel (exponential_density l))" hoelzl@57235: by (rule prob_space_erlang_density) hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributedD_le: hoelzl@50419: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" hoelzl@50419: shows "\

(x in M. X x \ a) = 1 - exp (- a * l)" hoelzl@57235: using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a hoelzl@57235: by (simp add: erlang_CDF_def) hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributedD_gt: hoelzl@50419: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" hoelzl@50419: shows "\

(x in M. a < X x ) = exp (- a * l)" hoelzl@57235: using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a hoelzl@57235: by (simp add: erlang_CDF_def) hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributed_memoryless: hoelzl@50419: assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a"and t: "0 \ t" hoelzl@50419: shows "\

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

(x in M. t < X x)" hoelzl@50419: proof - hoelzl@50419: have "\

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

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

(x in M. a < X x)" hoelzl@50419: using `0 \ t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) hoelzl@50419: also have "\ = exp (- (a + t) * l) / exp (- a * l)" hoelzl@50419: using a t by (simp add: exponential_distributedD_gt[OF D]) hoelzl@50419: also have "\ = exp (- t * l)" hoelzl@50419: using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) hoelzl@50419: finally show ?thesis hoelzl@50419: using t by (simp add: exponential_distributedD_gt[OF D]) hoelzl@50419: qed hoelzl@50419: hoelzl@50419: lemma exponential_distributedI: hoelzl@50419: assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l" hoelzl@50419: and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = 1 - exp (- a * l)" hoelzl@50419: shows "distributed M lborel X (exponential_density l)" hoelzl@57235: proof (rule erlang_distributedI) hoelzl@57235: fix a :: real assume "0 \ a" then show "emeasure M {x \ space M. X x \ a} = ereal (erlang_CDF 0 l a)" hoelzl@57235: using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def) hoelzl@57235: qed fact+ hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributed_iff: hoelzl@50419: "distributed M lborel X (exponential_density l) \ hoelzl@50419: (X \ borel_measurable M \ 0 < l \ (\a\0. \

(x in M. X x \ a) = 1 - exp (- a * l)))" hoelzl@57235: using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0) hoelzl@50419: hoelzl@50419: hoelzl@50419: lemma (in prob_space) exponential_distributed_expectation: hoelzl@57235: "distributed M lborel X (exponential_density l) \ expectation X = 1 / l" hoelzl@57235: using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp hoelzl@57235: hoelzl@57235: lemma exponential_density_nonneg: "0 < l \ 0 \ exponential_density l x" hoelzl@57235: by (auto simp: exponential_density_def) hoelzl@57235: hoelzl@57235: lemma (in prob_space) exponential_distributed_min: hoelzl@57235: assumes expX: "distributed M lborel X (exponential_density l)" hoelzl@57235: assumes expY: "distributed M lborel Y (exponential_density u)" hoelzl@57235: assumes ind: "indep_var borel X borel Y" hoelzl@57235: shows "distributed M lborel (\x. min (X x) (Y x)) (exponential_density (l + u))" hoelzl@57235: proof (subst exponential_distributed_iff, safe) hoelzl@57235: have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff) hoelzl@57235: moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff) hoelzl@57235: ultimately show "random_variable borel (\x. min (X x) (Y x))" by auto hoelzl@57235: hoelzl@57235: have "0 < l" by (rule exponential_distributed_params) fact hoelzl@57235: moreover have "0 < u" by (rule exponential_distributed_params) fact hoelzl@57235: ultimately show " 0 < l + u" by force hoelzl@57235: hoelzl@57235: fix a::real assume a[arith]: "0 \ a" hoelzl@57235: have gt1[simp]: "\

(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) hoelzl@57235: have gt2[simp]: "\

(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) hoelzl@57235: hoelzl@57235: have "\

(x in M. a < (min (X x) (Y x)) ) = \

(x in M. a < (X x) \ a < (Y x))" by (auto intro!:arg_cong[where f=prob]) hoelzl@57235: hoelzl@57235: also have " ... = \

(x in M. a < (X x)) * \

(x in M. a< (Y x) )" hoelzl@57235: using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp hoelzl@57235: also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp) hoelzl@57235: finally have indep_prob: "\

(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" . hoelzl@57235: hoelzl@57235: have "{x \ space M. (min (X x) (Y x)) \a } = (space M - {x \ space M. a<(min (X x) (Y x)) })" hoelzl@57235: by auto hoelzl@57235: then have "1 - prob {x \ space M. a < (min (X x) (Y x))} = prob {x \ space M. (min (X x) (Y x)) \ a}" hoelzl@57235: using randX randY by (auto simp: prob_compl) hoelzl@57235: then show "prob {x \ space M. (min (X x) (Y x)) \ a} = 1 - exp (- a * (l + u))" hoelzl@57235: using indep_prob by auto hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) exponential_distributed_Min: hoelzl@57235: assumes finI: "finite I" hoelzl@57235: assumes A: "I \ {}" hoelzl@57235: assumes expX: "\i. i \ I \ distributed M lborel (X i) (exponential_density (l i))" hoelzl@57235: assumes ind: "indep_vars (\i. borel) X I" hoelzl@57235: shows "distributed M lborel (\x. Min ((\i. X i x)`I)) (exponential_density (\i\I. l i))" hoelzl@57235: using assms hoelzl@57235: proof (induct rule: finite_ne_induct) hoelzl@57235: case (singleton i) then show ?case by simp hoelzl@57235: next hoelzl@57235: case (insert i I) hoelzl@57235: then have "distributed M lborel (\x. min (X i x) (Min ((\i. X i x)`I))) (exponential_density (l i + (\i\I. l i)))" hoelzl@57235: by (intro exponential_distributed_min indep_vars_Min insert) hoelzl@57235: (auto intro: indep_vars_subset) hoelzl@57235: then show ?case hoelzl@57235: using insert by simp hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) exponential_distributed_variance: hoelzl@57235: "distributed M lborel X (exponential_density l) \ variance X = 1 / l\<^sup>2" hoelzl@57235: using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp hoelzl@57235: hoelzl@57235: lemma nn_integral_zero': "AE x in M. f x = 0 \ (\\<^sup>+x. f x \M) = 0" hoelzl@57235: by (simp cong: nn_integral_cong_AE) hoelzl@57235: hoelzl@57235: lemma convolution_erlang_density: hoelzl@57235: fixes k\<^sub>1 k\<^sub>2 :: nat hoelzl@57235: assumes [simp, arith]: "0 < l" hoelzl@57235: shows "(\x. \\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y)) * ereal (erlang_density k\<^sub>2 l y) \lborel) = hoelzl@57235: (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" hoelzl@57235: (is "?LHS = ?RHS") hoelzl@57235: proof hoelzl@57235: fix x :: real hoelzl@57235: have "x \ 0 \ 0 < x" hoelzl@57235: by arith hoelzl@57235: then show "?LHS x = ?RHS x" hoelzl@57235: proof hoelzl@57235: assume "x \ 0" then show ?thesis hoelzl@57235: apply (subst nn_integral_zero') hoelzl@57235: apply (rule AE_I[where N="{0}"]) hoelzl@57235: apply (auto simp add: erlang_density_def not_less) hoelzl@57235: done hoelzl@57235: next hoelzl@57235: note zero_le_mult_iff[simp] zero_le_divide_iff[simp] hoelzl@57235: hoelzl@57235: have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1" hoelzl@57235: using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc) hoelzl@57235: hoelzl@57235: have 1: "(\\<^sup>+ x. ereal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \lborel) = 1" hoelzl@57235: apply (subst I_eq1[symmetric]) hoelzl@57235: unfolding erlang_density_def hoelzl@57235: by (auto intro!: nn_integral_cong split:split_indicator) hoelzl@57235: hoelzl@57235: have "prob_space (density lborel ?LHS)" hoelzl@57235: unfolding times_ereal.simps[symmetric] hoelzl@57235: by (intro prob_space_convolution_density) hoelzl@57235: (auto intro!: prob_space_erlang_density erlang_density_nonneg) hoelzl@57235: then have 2: "integral\<^sup>N lborel ?LHS = 1" hoelzl@57235: by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density) hoelzl@57235: hoelzl@57235: let ?I = "(integral\<^sup>N lborel (\y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))" hoelzl@57235: let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))" hoelzl@57235: let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" hoelzl@57235: let ?L = "(\x. \\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \lborel)" hoelzl@57235: hoelzl@57235: { fix x :: real assume [arith]: "0 < x" hoelzl@57235: have *: "\x y n. (x - y * x::real)^n = x^n * (1 - y)^n" hoelzl@57235: unfolding power_mult_distrib[symmetric] by (simp add: field_simps) hoelzl@57235: hoelzl@57235: have "?LHS x = ?L x" hoelzl@57235: unfolding erlang_density_def hoelzl@57235: by (auto intro!: nn_integral_cong split:split_indicator) hoelzl@57235: also have "... = (\x. ereal ?C * ?I * erlang_density ?s l x) x" hoelzl@57235: apply (subst nn_integral_real_affine[where c=x and t = 0]) hoelzl@57235: apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc) hoelzl@57235: apply (intro nn_integral_cong) hoelzl@57235: apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add * hoelzl@57235: simp del: fact_Suc split: split_indicator) hoelzl@57235: done hoelzl@57235: finally have "(\\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \lborel) = hoelzl@57235: (\x. ereal ?C * ?I * erlang_density ?s l x) x" hoelzl@57235: by simp } hoelzl@57235: note * = this hoelzl@57235: hoelzl@57235: assume [arith]: "0 < x" hoelzl@57235: have 3: "1 = integral\<^sup>N lborel (\xa. ?LHS xa * indicator {0<..} xa)" hoelzl@57235: by (subst 2[symmetric]) hoelzl@57235: (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] hoelzl@57235: simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: split_if_asm) hoelzl@57235: also have "... = integral\<^sup>N lborel (\x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))" hoelzl@57235: by (auto intro!: nn_integral_cong simp: * split: split_indicator) hoelzl@57235: also have "... = ereal (?C) * ?I" hoelzl@57235: using 1 hoelzl@57235: by (auto simp: nn_integral_nonneg nn_integral_cmult) hoelzl@57235: finally have " ereal (?C) * ?I = 1" by presburger hoelzl@57235: hoelzl@57235: then show ?thesis hoelzl@57235: using * by simp hoelzl@57235: qed hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) sum_indep_erlang: hoelzl@57235: assumes indep: "indep_var borel X borel Y" hoelzl@57235: assumes [simp, arith]: "0 < l" hoelzl@57235: assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" hoelzl@57235: assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" hoelzl@57235: shows "distributed M lborel (\x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" hoelzl@57235: using assms hoelzl@57235: apply (subst convolution_erlang_density[symmetric, OF `0 {}" hoelzl@57235: assumes [simp, arith]: "0 < l" hoelzl@57235: assumes expX: "\i. i \ I \ distributed M lborel (X i) (erlang_density (k i) l)" hoelzl@57235: assumes ind: "indep_vars (\i. borel) X I" hoelzl@57235: shows "distributed M lborel (\x. \i\I. X i x) (erlang_density ((\i\I. Suc (k i)) - 1) l)" hoelzl@57235: using assms hoelzl@57235: proof (induct rule: finite_ne_induct) hoelzl@57235: case (singleton i) then show ?case by auto hoelzl@57235: next hoelzl@57235: case (insert i I) hoelzl@57235: then have "distributed M lborel (\x. (X i x) + (\i\ I. X i x)) (erlang_density (Suc (k i) + Suc ((\i\I. Suc (k i)) - 1) - 1) l)" hoelzl@57235: by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset) hoelzl@57235: also have "(\x. (X i x) + (\i\ I. X i x)) = (\x. \i\insert i I. X i x)" hoelzl@57235: using insert by auto hoelzl@57235: also have "Suc(k i) + Suc ((\i\I. Suc (k i)) - 1) - 1 = (\i\insert i I. Suc (k i)) - 1" hoelzl@57235: using insert by (auto intro!: Suc_pred simp: ac_simps) hoelzl@57235: finally show ?case by fast hoelzl@57235: qed hoelzl@57235: hoelzl@57235: lemma (in prob_space) exponential_distributed_setsum: hoelzl@57235: assumes finI: "finite I" hoelzl@57235: assumes A: "I \ {}" hoelzl@57235: assumes expX: "\i. i \ I \ distributed M lborel (X i) (exponential_density l)" hoelzl@57235: assumes ind: "indep_vars (\i. borel) X I" hoelzl@57235: shows "distributed M lborel (\x. \i\I. X i x) (erlang_density ((card I) - 1) l)" hoelzl@57235: proof - hoelzl@57235: obtain i where "i \ I" using assms by auto hoelzl@57235: note exponential_distributed_params[OF expX[OF this]] hoelzl@57235: from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp hoelzl@57235: qed hoelzl@50419: hoelzl@57252: lemma (in information_space) entropy_exponential: hoelzl@57252: assumes D: "distributed M lborel X (exponential_density l)" hoelzl@57252: shows "entropy b lborel X = log b (exp 1 / l)" hoelzl@57252: proof - hoelzl@57252: have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D]) hoelzl@57252: hoelzl@57252: have [simp]: "integrable lborel (exponential_density l)" hoelzl@57252: using distributed_integrable[OF D, of "\_. 1"] by simp hoelzl@57252: hoelzl@57252: have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1" hoelzl@57252: using distributed_integral[OF D, of "\_. 1"] by (simp add: prob_space) hoelzl@57252: hoelzl@57252: have [simp]: "integrable lborel (\x. exponential_density l x * x)" hoelzl@57252: using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\x. x"] by simp hoelzl@57252: hoelzl@57252: have [simp]: "integral\<^sup>L lborel (\x. exponential_density l x * x) = 1 / l" hoelzl@57252: using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\x. x"] by simp hoelzl@57252: hoelzl@57252: have "entropy b lborel X = - (\ x. exponential_density l x * log b (exponential_density l x) \lborel)" hoelzl@57252: using D by (rule entropy_distr) hoelzl@57252: also have "(\ x. exponential_density l x * log b (exponential_density l x) \lborel) = hoelzl@57252: (\ x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \lborel)" hoelzl@57252: by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps) hoelzl@57252: also have "\ = (ln l - 1) / ln b" hoelzl@57252: by simp hoelzl@57252: finally show ?thesis hoelzl@57252: by (simp add: log_def divide_simps ln_div) hoelzl@57252: qed hoelzl@57252: hoelzl@50419: subsection {* Uniform distribution *} hoelzl@50419: hoelzl@50419: lemma uniform_distrI: hoelzl@50419: assumes X: "X \ measurable M M'" hoelzl@50419: and A: "A \ sets M'" "emeasure M' A \ \" "emeasure M' A \ 0" hoelzl@50419: assumes distr: "\B. B \ sets M' \ emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" hoelzl@50419: shows "distr M M' X = uniform_measure M' A" hoelzl@50419: unfolding uniform_measure_def hoelzl@50419: proof (intro measure_eqI) hoelzl@50419: let ?f = "\x. indicator A x / emeasure M' A" hoelzl@50419: fix B assume B: "B \ sets (distr M M' X)" hoelzl@50419: with X have "emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" hoelzl@50419: by (simp add: distr[of B] measurable_sets) hoelzl@50419: also have "\ = (1 / emeasure M' A) * emeasure M' (A \ B)" hoelzl@50419: by simp wenzelm@53015: also have "\ = (\\<^sup>+ x. (1 / emeasure M' A) * indicator (A \ B) x \M')" hoelzl@50419: using A B hoelzl@56996: by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) wenzelm@53015: also have "\ = (\\<^sup>+ x. ?f x * indicator B x \M')" hoelzl@56996: by (rule nn_integral_cong) (auto split: split_indicator) hoelzl@50419: finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" hoelzl@50419: using A B X by (auto simp add: emeasure_distr emeasure_density) hoelzl@50419: qed simp hoelzl@50419: hoelzl@50419: lemma uniform_distrI_borel: hoelzl@50419: fixes A :: "real set" hoelzl@50419: assumes X[measurable]: "X \ borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r" hoelzl@50419: and [measurable]: "A \ sets borel" hoelzl@50419: assumes distr: "\a. emeasure M {x\space M. X x \ a} = emeasure lborel (A \ {.. a}) / r" hoelzl@50419: shows "distributed M lborel X (\x. indicator A x / measure lborel A)" hoelzl@50419: proof (rule distributedI_borel_atMost) hoelzl@50419: let ?f = "\x. 1 / r * indicator A x" hoelzl@50419: fix a hoelzl@50419: have "emeasure lborel (A \ {..a}) \ emeasure lborel A" hoelzl@50419: using A by (intro emeasure_mono) auto hoelzl@50419: also have "\ < \" hoelzl@50419: using A by simp hoelzl@50419: finally have fin: "emeasure lborel (A \ {..a}) \ \" hoelzl@50419: by simp hoelzl@50419: from emeasure_eq_ereal_measure[OF this] hoelzl@50419: have fin_eq: "emeasure lborel (A \ {..a}) / r = ereal (measure lborel (A \ {..a}) / r)" hoelzl@50419: using A by simp hoelzl@50419: then show "emeasure M {x\space M. X x \ a} = ereal (measure lborel (A \ {..a}) / r)" hoelzl@50419: using distr by simp hoelzl@50419: wenzelm@53015: have "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = wenzelm@53015: (\\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \ {..a}) x \lborel)" hoelzl@56996: by (auto intro!: nn_integral_cong split: split_indicator) hoelzl@50419: also have "\ = ereal (1 / measure lborel A) * emeasure lborel (A \ {..a})" hoelzl@50419: using `A \ sets borel` hoelzl@56996: by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg) hoelzl@50419: also have "\ = ereal (measure lborel (A \ {..a}) / r)" hoelzl@50419: unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) wenzelm@53015: finally show "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = hoelzl@50419: ereal (measure lborel (A \ {..a}) / r)" . hoelzl@56571: qed (auto simp: measure_nonneg) hoelzl@50419: hoelzl@50419: lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: hoelzl@50419: fixes a b :: real hoelzl@50419: assumes X: "X \ borel_measurable M" and "a < b" hoelzl@50419: assumes distr: "\t. a \ t \ t \ b \ \

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

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

(x in M. X x \ t)= (t - a) / (b - a)))" hoelzl@50419: using hoelzl@50419: uniform_distributed_bounds[of X a b] hoelzl@50419: uniform_distributed_measure[of X a b] hoelzl@50419: distributed_measurable[of M lborel X] hoelzl@57447: by (auto intro!: uniform_distrI_borel_atLeastAtMost) hoelzl@50419: hoelzl@50419: lemma (in prob_space) uniform_distributed_expectation: hoelzl@50419: fixes a b :: real hoelzl@50419: assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" hoelzl@50419: shows "expectation X = (a + b) / 2" hoelzl@50419: proof (subst distributed_integral[OF D, of "\x. x", symmetric]) hoelzl@50419: have "a < b" hoelzl@50419: using uniform_distributed_bounds[OF D] . hoelzl@50419: hoelzl@50419: have "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = hoelzl@50419: (\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel)" hoelzl@50419: by (intro integral_cong) auto hoelzl@50419: also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2" hoelzl@57447: proof (subst integral_FTC_Icc_real) hoelzl@50419: fix x wenzelm@53077: show "DERIV (\x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" hoelzl@50419: using uniform_distributed_params[OF D] hoelzl@56381: by (auto intro!: derivative_eq_intros) hoelzl@50419: show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x" hoelzl@50419: using uniform_distributed_params[OF D] hoelzl@50419: by (auto intro!: isCont_divide) wenzelm@53015: have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = hoelzl@50419: (b*b - a * a) / (2 * (b - a))" hoelzl@50419: using `a < b` hoelzl@50419: by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) wenzelm@53015: show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" hoelzl@50419: using `a < b` hoelzl@50419: unfolding * square_diff_square_factored by (auto simp: field_simps) hoelzl@50419: qed (insert `a < b`, simp) hoelzl@50419: finally show "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (a + b) / 2" . hoelzl@50419: qed auto hoelzl@50419: hoelzl@57235: lemma (in prob_space) uniform_distributed_variance: hoelzl@57235: fixes a b :: real hoelzl@57235: assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" hoelzl@57235: shows "variance X = (b - a)\<^sup>2 / 12" hoelzl@57235: proof (subst distributed_variance) hoelzl@57235: have [arith]: "a < b" using uniform_distributed_bounds[OF D] . hoelzl@57235: let ?\ = "expectation X" let ?D = "\x. indicator {a..b} (x + ?\) / measure lborel {a..b}" hoelzl@57235: have "(\x. x\<^sup>2 * (?D x) \lborel) = (\x. x\<^sup>2 * (indicator {a - ?\ .. b - ?\} x) / measure lborel {a .. b} \lborel)" hoelzl@57235: by (intro integral_cong) (auto split: split_indicator) hoelzl@57235: also have "\ = (b - a)\<^sup>2 / 12" hoelzl@57447: by (simp add: integral_power uniform_distributed_expectation[OF D]) hoelzl@57235: (simp add: eval_nat_numeral field_simps ) hoelzl@57235: finally show "(\x. x\<^sup>2 * ?D x \lborel) = (b - a)\<^sup>2 / 12" . hoelzl@57235: qed fact hoelzl@57235: hoelzl@57252: subsection {* Normal distribution *} hoelzl@57252: hoelzl@57254: hoelzl@57252: definition normal_density :: "real \ real \ real \ real" where hoelzl@57252: "normal_density \ \ x = 1 / sqrt (2 * pi * \\<^sup>2) * exp (-(x - \)\<^sup>2/ (2 * \\<^sup>2))" hoelzl@57252: hoelzl@57252: abbreviation std_normal_density :: "real \ real" where hoelzl@57252: "std_normal_density \ normal_density 0 1" hoelzl@57252: hoelzl@57252: lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp (- x\<^sup>2 / 2)" hoelzl@57252: unfolding normal_density_def by simp hoelzl@57252: hoelzl@57254: lemma normal_density_nonneg: "0 \ normal_density \ \ x" hoelzl@57254: by (auto simp: normal_density_def) hoelzl@57254: hoelzl@57254: lemma normal_density_pos: "0 < \ \ 0 < normal_density \ \ x" hoelzl@57254: by (auto simp: normal_density_def) hoelzl@57254: hoelzl@57252: lemma borel_measurable_normal_density[measurable]: "normal_density \ \ \ borel_measurable borel" hoelzl@57252: by (auto simp: normal_density_def[abs_def]) hoelzl@57252: hoelzl@57254: lemma gaussian_moment_0: hoelzl@57254: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2)) (sqrt pi / 2)" hoelzl@57252: proof - hoelzl@57252: let ?pI = "\f. (\\<^sup>+s. f (s::real) * indicator {0..} s \lborel)" hoelzl@57252: let ?gauss = "\x. exp (- x\<^sup>2)" hoelzl@57252: hoelzl@57254: let ?I = "indicator {0<..} :: real \ real" hoelzl@57254: let ?ff= "\x s. x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) :: real" hoelzl@57254: hoelzl@57254: have *: "?pI ?gauss = (\\<^sup>+x. ?gauss x * ?I x \lborel)" hoelzl@57254: by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator) hoelzl@57254: hoelzl@57254: have "?pI ?gauss * ?pI ?gauss = (\\<^sup>+x. \\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel \lborel)" hoelzl@57254: by (auto simp: nn_integral_nonneg nn_integral_cmult[symmetric] nn_integral_multc[symmetric] * hoelzl@57254: intro!: nn_integral_cong split: split_indicator) hoelzl@57254: also have "\ = (\\<^sup>+x. \\<^sup>+s. ?ff x s * ?I s * ?I x \lborel \lborel)" hoelzl@57254: proof (rule nn_integral_cong, cases) hoelzl@57254: fix x :: real assume "x \ 0" hoelzl@57254: then show "(\\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel) = (\\<^sup>+s. ?ff x s * ?I s * ?I x \lborel)" hoelzl@57254: by (subst nn_integral_real_affine[where t="0" and c="x"]) hoelzl@57254: (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff hoelzl@57254: intro!: nn_integral_cong split: split_indicator) hoelzl@57254: qed simp hoelzl@57254: also have "... = \\<^sup>+s. \\<^sup>+x. ?ff x s * ?I s * ?I x \lborel \lborel" hoelzl@57254: by (rule lborel_pair.Fubini'[symmetric]) auto hoelzl@57254: also have "... = ?pI (\s. ?pI (\x. ?ff x s))" hoelzl@57254: by (rule nn_integral_cong_AE) hoelzl@57254: (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm) hoelzl@57252: also have "\ = ?pI (\s. ereal (1 / (2 * (1 + s\<^sup>2))))" hoelzl@57252: proof (intro nn_integral_cong ereal_right_mult_cong) hoelzl@57254: fix s :: real show "?pI (\x. ?ff x s) = ereal (1 / (2 * (1 + s\<^sup>2)))" hoelzl@57252: proof (subst nn_integral_FTC_atLeast) hoelzl@57252: have "((\a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top" hoelzl@57252: apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top]) haftmann@57512: apply (subst mult.commute) hoelzl@57254: apply (auto intro!: filterlim_tendsto_pos_mult_at_top hoelzl@57254: filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] hoelzl@57254: simp: add_pos_nonneg power2_eq_square add_nonneg_eq_0_iff) hoelzl@57254: done hoelzl@57252: then show "((\a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top" hoelzl@57252: by (simp add: field_simps) hoelzl@57252: qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff) hoelzl@57252: qed hoelzl@57252: also have "... = ereal (pi / 4)" hoelzl@57252: proof (subst nn_integral_FTC_atLeast) hoelzl@57252: show "((\a. arctan a / 2) ---> (pi / 2) / 2 ) at_top" hoelzl@57252: by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top) hoelzl@57252: qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square) hoelzl@57252: finally have "?pI ?gauss^2 = pi / 4" hoelzl@57252: by (simp add: power2_eq_square) hoelzl@57252: then have "?pI ?gauss = sqrt (pi / 4)" hoelzl@57252: using power_eq_iff_eq_base[of 2 "real (?pI ?gauss)" "sqrt (pi / 4)"] hoelzl@57254: nn_integral_nonneg[of lborel "\x. ?gauss x * indicator {0..} x"] hoelzl@57252: by (cases "?pI ?gauss") auto hoelzl@57254: also have "?pI ?gauss = (\\<^sup>+x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2) \lborel)" hoelzl@57254: by (intro nn_integral_cong) (simp split: split_indicator) hoelzl@57254: also have "sqrt (pi / 4) = sqrt pi / 2" hoelzl@57254: by (simp add: real_sqrt_divide) hoelzl@57254: finally show ?thesis hoelzl@57254: by (rule has_bochner_integral_nn_integral[rotated 2]) auto hoelzl@57254: qed hoelzl@57254: hoelzl@57254: lemma gaussian_moment_1: hoelzl@57254: "has_bochner_integral lborel (\x::real. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x)) (1 / 2)" hoelzl@57254: proof - hoelzl@57254: have "(\\<^sup>+x. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x) \lborel) = hoelzl@57254: (\\<^sup>+x. ereal (x * exp (- x\<^sup>2)) * indicator {0..} x \lborel)" hoelzl@57254: by (intro nn_integral_cong) hoelzl@57254: (auto simp: ac_simps times_ereal.simps(1)[symmetric] ereal_indicator simp del: times_ereal.simps) hoelzl@57254: also have "\ = ereal (0 - (- exp (- 0\<^sup>2) / 2))" hoelzl@57254: proof (rule nn_integral_FTC_atLeast) hoelzl@57254: have "((\x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top" hoelzl@57254: by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot] hoelzl@57275: filterlim_compose[OF filterlim_uminus_at_bot_at_top] hoelzl@57275: filterlim_pow_at_top filterlim_ident) hoelzl@57254: auto hoelzl@57254: then show "((\a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top" hoelzl@57254: by simp hoelzl@57254: qed (auto intro!: derivative_eq_intros) hoelzl@57254: also have "\ = ereal (1 / 2)" hoelzl@57254: by simp hoelzl@57254: finally show ?thesis hoelzl@57254: by (rule has_bochner_integral_nn_integral[rotated 2]) (auto split: split_indicator) hoelzl@57252: qed hoelzl@57252: hoelzl@57254: lemma hoelzl@57254: fixes k :: nat hoelzl@57254: shows gaussian_moment_even_pos: hoelzl@57254: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k))) hoelzl@57254: ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" (is "?even") hoelzl@57254: and gaussian_moment_odd_pos: hoelzl@57254: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" (is "?odd") hoelzl@57254: proof - hoelzl@57254: let ?M = "\k x. exp (- x\<^sup>2) * x^k :: real" hoelzl@57254: hoelzl@57254: { fix k I assume Mk: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R ?M k x) I" hoelzl@57254: have "2 \ (0::real)" hoelzl@57254: by linarith hoelzl@57254: let ?f = "\b. \x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \lborel" hoelzl@57254: have "((\b. (k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \lborel) - ?M (k + 1) b / 2) ---> hoelzl@57254: (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top" (is ?tendsto) hoelzl@57254: proof (intro tendsto_intros `2 \ 0` tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) hoelzl@57254: show "(?M (k + 1) ---> 0) at_top" hoelzl@57254: proof cases hoelzl@57254: assume "even k" hoelzl@57254: have "((\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top" hoelzl@57254: by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] hoelzl@57275: filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) hoelzl@57275: auto hoelzl@57254: also have "(\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)" hoelzl@57254: using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult) hoelzl@57254: finally show ?thesis by simp hoelzl@57254: next hoelzl@57254: assume "odd k" hoelzl@57254: have "((\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top" hoelzl@57275: by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity hoelzl@57275: filterlim_ident filterlim_pow_at_top) hoelzl@57275: auto hoelzl@57254: also have "(\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)" hoelzl@57254: using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult) hoelzl@57254: finally show ?thesis by simp hoelzl@57254: qed hoelzl@57254: qed hoelzl@57254: also have "?tendsto \ ((?f ---> (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top)" hoelzl@57254: proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) hoelzl@57254: fix b :: real assume b: "0 \ b" hoelzl@57254: have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) = (\x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \lborel)" hoelzl@57254: unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto hoelzl@57254: also have "\ = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) - hoelzl@57254: (\x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \lborel)" hoelzl@57254: by (rule integral_by_parts') hoelzl@57254: (auto intro!: derivative_eq_intros b hoelzl@57254: simp: real_of_nat_def[symmetric] diff_Suc real_of_nat_Suc field_simps split: nat.split) hoelzl@57254: also have "(\x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \lborel) = hoelzl@57254: (\x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \lborel)" hoelzl@57254: by (intro integral_cong) auto hoelzl@57254: finally have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) = hoelzl@57254: exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \lborel)" hoelzl@57254: apply (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric]) hoelzl@57254: apply (subst integral_mult_right_zero[symmetric]) hoelzl@57254: apply (intro integral_cong) hoelzl@57254: apply simp_all hoelzl@57254: done hoelzl@57254: then show "(k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b" hoelzl@57254: by (simp add: field_simps atLeastAtMost_def indicator_inter_arith) hoelzl@57254: qed hoelzl@57254: finally have int_M_at_top: "((?f ---> (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel)) at_top)" hoelzl@57254: by simp hoelzl@57254: hoelzl@57254: have "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)" hoelzl@57254: proof (rule has_bochner_integral_monotone_convergence_at_top) hoelzl@57254: fix y :: real hoelzl@57254: have *: "(\x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..y} x::real) = hoelzl@57254: (\x. indicator {0..y} x *\<^sub>R ?M (k + 2) x)" hoelzl@57254: by rule (simp split: split_indicator) hoelzl@57254: show "integrable lborel (\x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)" hoelzl@57254: unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros) hoelzl@57254: show "((?f ---> (k + 1) / 2 * I) at_top)" hoelzl@57254: using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp hoelzl@57254: qed (auto split: split_indicator) } hoelzl@57254: note step = this hoelzl@57254: hoelzl@57254: show ?even hoelzl@57254: proof (induct k) hoelzl@57254: case (Suc k) hoelzl@57254: note step[OF this] hoelzl@57254: also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * (real (fact (2 * k)) / real (2 ^ (2 * k) * fact k)))) = hoelzl@57254: sqrt pi / 2 * (real (fact (2 * Suc k)) / real (2 ^ (2 * Suc k) * fact (Suc k)))" hoelzl@57254: by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps) hoelzl@57254: finally show ?case hoelzl@57254: by simp hoelzl@57254: qed (insert gaussian_moment_0, simp) hoelzl@57252: hoelzl@57254: show ?odd hoelzl@57254: proof (induct k) hoelzl@57254: case (Suc k) hoelzl@57254: note step[OF this] hoelzl@57254: also have "(real (2 * k + 1 + 1) / 2 * (real (fact k) / 2)) = real (fact (Suc k)) / 2" hoelzl@57254: by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps) hoelzl@57254: finally show ?case hoelzl@57254: by simp hoelzl@57254: qed (insert gaussian_moment_1, simp) hoelzl@57254: qed hoelzl@57254: hoelzl@57254: context hoelzl@57254: fixes k :: nat and \ \ :: real assumes [arith]: "0 < \" hoelzl@57254: begin hoelzl@57254: hoelzl@57254: lemma normal_moment_even: hoelzl@57254: "has_bochner_integral lborel (\x. normal_density \ \ x * (x - \) ^ (2 * k)) (fact (2 * k) / ((2 / \\<^sup>2)^k * fact k))" hoelzl@57254: proof - hoelzl@57254: have eq: "\x::real. x\<^sup>2^k = (x^k)\<^sup>2" hoelzl@57254: by (simp add: power_mult[symmetric] ac_simps) hoelzl@57254: hoelzl@57254: have "has_bochner_integral lborel (\x. exp (-x\<^sup>2)*x^(2 * k)) hoelzl@57254: (sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" hoelzl@57254: using has_bochner_integral_even_function[OF gaussian_moment_even_pos[where k=k]] by simp hoelzl@57254: then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2))) hoelzl@57254: ((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2)))" hoelzl@57254: by (rule has_bochner_integral_mult_left) hoelzl@57254: also have "(\x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2))) = hoelzl@57254: (\x. exp (- ((sqrt 2 * \) * x)\<^sup>2 / (2*\\<^sup>2)) * ((sqrt 2 * \) * x) ^ (2 * k) / sqrt (2 * pi * \\<^sup>2))" hoelzl@57254: by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult hoelzl@57254: real_sqrt_divide power_mult eq) hoelzl@57254: also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2))) = hoelzl@57254: (inverse (sqrt 2 * \) * (real (fact (2 * k))) / ((2/\\<^sup>2) ^ k * real (fact k)))" hoelzl@57254: by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult hoelzl@57254: power2_eq_square) hoelzl@57254: finally show ?thesis hoelzl@57254: unfolding normal_density_def hoelzl@57254: by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\]) simp_all hoelzl@57254: qed hoelzl@57252: hoelzl@57254: lemma normal_moment_abs_odd: hoelzl@57254: "has_bochner_integral lborel (\x. normal_density \ \ x * \x - \\^(2 * k + 1)) (2^k * \^(2 * k + 1) * fact k * sqrt (2 / pi))" hoelzl@57254: proof - hoelzl@57254: have "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\x\^(2 * k + 1))) (fact k / 2)" hoelzl@57254: by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto hoelzl@57254: from has_bochner_integral_even_function[OF this] hoelzl@57254: have "has_bochner_integral lborel (\x. exp (-x\<^sup>2)*\x\^(2 * k + 1)) (fact k)" hoelzl@57254: by simp hoelzl@57254: then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*\x\^(2 * k + 1)) * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2))) hoelzl@57254: (fact k * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2)))" hoelzl@57254: by (rule has_bochner_integral_mult_left) hoelzl@57254: also have "(\x. (exp (-x\<^sup>2)*\x\^(2 * k + 1)) * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2))) = hoelzl@57254: (\x. exp (- (((sqrt 2 * \) * x)\<^sup>2 / (2 * \\<^sup>2))) * \sqrt 2 * \ * x\ ^ (2 * k + 1) / sqrt (2 * pi * \\<^sup>2))" hoelzl@57254: by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult) hoelzl@57254: also have "(fact k * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2))) = hoelzl@57254: (inverse (sqrt 2) * inverse \ * (2 ^ k * (\ * \ ^ (2 * k)) * real (fact k) * sqrt (2 / pi)))" hoelzl@57254: by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide hoelzl@57254: real_sqrt_mult) hoelzl@57254: finally show ?thesis hoelzl@57254: unfolding normal_density_def hoelzl@57254: by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\]) hoelzl@57254: simp_all hoelzl@57254: qed hoelzl@57254: hoelzl@57254: lemma normal_moment_odd: hoelzl@57254: "has_bochner_integral lborel (\x. normal_density \ \ x * (x - \)^(2 * k + 1)) 0" hoelzl@57254: proof - hoelzl@57254: have "has_bochner_integral lborel (\x. exp (- x\<^sup>2) * x^(2 * k + 1)::real) 0" hoelzl@57254: using gaussian_moment_odd_pos by (rule has_bochner_integral_odd_function) simp hoelzl@57254: then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\^(2*k)/sqrt pi)) hoelzl@57254: (0 * (2^k*\^(2*k)/sqrt pi))" hoelzl@57254: by (rule has_bochner_integral_mult_left) hoelzl@57254: also have "(\x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\^(2*k)/sqrt pi)) = hoelzl@57254: (\x. exp (- ((sqrt 2 * \ * x)\<^sup>2 / (2 * \\<^sup>2))) * hoelzl@57254: (sqrt 2 * \ * x * (sqrt 2 * \ * x) ^ (2 * k)) / hoelzl@57254: sqrt (2 * pi * \\<^sup>2))" hoelzl@57254: unfolding real_sqrt_mult hoelzl@57254: by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult fun_eq_iff) hoelzl@57254: finally show ?thesis hoelzl@57254: unfolding normal_density_def hoelzl@57254: by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\]) simp_all hoelzl@57254: qed hoelzl@57254: hoelzl@57254: lemma integral_normal_moment_even: hoelzl@57254: "integral\<^sup>L lborel (\x. normal_density \ \ x * (x - \)^(2 * k)) = fact (2 * k) / ((2 / \\<^sup>2)^k * fact k)" hoelzl@57254: using normal_moment_even by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integral_normal_moment_abs_odd: hoelzl@57254: "integral\<^sup>L lborel (\x. normal_density \ \ x * \x - \\^(2 * k + 1)) = 2 ^ k * \ ^ (2 * k + 1) * fact k * sqrt (2 / pi)" hoelzl@57254: using normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integral_normal_moment_odd: hoelzl@57254: "integral\<^sup>L lborel (\x. normal_density \ \ x * (x - \)^(2 * k + 1)) = 0" hoelzl@57254: using normal_moment_odd by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: end hoelzl@57254: hoelzl@57252: hoelzl@57252: context hoelzl@57252: fixes \ :: real hoelzl@57252: assumes \_pos[arith]: "0 < \" hoelzl@57252: begin hoelzl@57252: hoelzl@57254: lemma normal_moment_nz_1: "has_bochner_integral lborel (\x. normal_density \ \ x * x) \" hoelzl@57254: proof - hoelzl@57254: note normal_moment_even[OF \_pos, of \ 0] hoelzl@57254: note normal_moment_odd[OF \_pos, of \ 0] has_bochner_integral_mult_left[of \, OF this] hoelzl@57254: note has_bochner_integral_add[OF this] hoelzl@57254: then show ?thesis hoelzl@57254: by (simp add: power2_eq_square field_simps) hoelzl@57254: qed hoelzl@57254: hoelzl@57254: lemma integral_normal_moment_nz_1: hoelzl@57254: "integral\<^sup>L lborel (\x. normal_density \ \ x * x) = \" hoelzl@57254: using normal_moment_nz_1 by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integrable_normal_moment_nz_1: "integrable lborel (\x. normal_density \ \ x * x)" hoelzl@57254: using normal_moment_nz_1 by rule hoelzl@57252: hoelzl@57254: lemma integrable_normal_moment: "integrable lborel (\x. normal_density \ \ x * (x - \)^k)" hoelzl@57254: proof cases hoelzl@57254: assume "even k" then show ?thesis hoelzl@57254: using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex) hoelzl@57254: next hoelzl@57254: assume "odd k" then show ?thesis hoelzl@57254: using integrable.intros[OF normal_moment_odd] by (auto simp add: odd_Suc_mult_two_ex) hoelzl@57254: qed hoelzl@57252: hoelzl@57254: lemma integrable_normal_moment_abs: "integrable lborel (\x. normal_density \ \ x * \x - \\^k)" hoelzl@57254: proof cases hoelzl@57254: assume "even k" then show ?thesis hoelzl@57254: using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex power_even_abs) hoelzl@57254: next hoelzl@57254: assume "odd k" then show ?thesis hoelzl@57254: using integrable.intros[OF normal_moment_abs_odd] by (auto simp add: odd_Suc_mult_two_ex) hoelzl@57254: qed hoelzl@57254: hoelzl@57254: lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \ \)" hoelzl@57254: using integrable_normal_moment[of \ 0] by simp hoelzl@57252: hoelzl@57252: lemma integral_normal_density[simp]: "(\x. normal_density \ \ x \lborel) = 1" hoelzl@57254: using integral_normal_moment_even[of \ \ 0] by simp hoelzl@57252: hoelzl@57252: lemma prob_space_normal_density: hoelzl@57254: "prob_space (density lborel (normal_density \ \))" hoelzl@57254: proof qed (simp add: emeasure_density nn_integral_eq_integral normal_density_nonneg) hoelzl@57254: hoelzl@57254: end hoelzl@57254: hoelzl@57254: hoelzl@57254: hoelzl@57254: context hoelzl@57254: fixes k :: nat hoelzl@57254: begin hoelzl@57254: hoelzl@57254: lemma std_normal_moment_even: hoelzl@57254: "has_bochner_integral lborel (\x. std_normal_density x * x ^ (2 * k)) (fact (2 * k) / (2^k * fact k))" hoelzl@57254: using normal_moment_even[of 1 0 k] by simp hoelzl@57254: hoelzl@57254: lemma std_normal_moment_abs_odd: hoelzl@57254: "has_bochner_integral lborel (\x. std_normal_density x * \x\^(2 * k + 1)) (sqrt (2/pi) * 2^k * fact k)" hoelzl@57254: using normal_moment_abs_odd[of 1 0 k] by (simp add: ac_simps) hoelzl@57254: hoelzl@57254: lemma std_normal_moment_odd: hoelzl@57254: "has_bochner_integral lborel (\x. std_normal_density x * x^(2 * k + 1)) 0" hoelzl@57254: using normal_moment_odd[of 1 0 k] by simp hoelzl@57254: hoelzl@57254: lemma integral_std_normal_moment_even: hoelzl@57254: "integral\<^sup>L lborel (\x. std_normal_density x * x^(2*k)) = fact (2 * k) / (2^k * fact k)" hoelzl@57254: using std_normal_moment_even by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integral_std_normal_moment_abs_odd: hoelzl@57254: "integral\<^sup>L lborel (\x. std_normal_density x * \x\^(2 * k + 1)) = sqrt (2 / pi) * 2^k * fact k" hoelzl@57254: using std_normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integral_std_normal_moment_odd: hoelzl@57254: "integral\<^sup>L lborel (\x. std_normal_density x * x^(2 * k + 1)) = 0" hoelzl@57254: using std_normal_moment_odd by (rule has_bochner_integral_integral_eq) hoelzl@57254: hoelzl@57254: lemma integrable_std_normal_moment_abs: "integrable lborel (\x. std_normal_density x * \x\^k)" hoelzl@57254: using integrable_normal_moment_abs[of 1 0 k] by simp hoelzl@57254: hoelzl@57254: lemma integrable_std_normal_moment: "integrable lborel (\x. std_normal_density x * x^k)" hoelzl@57254: using integrable_normal_moment[of 1 0 k] by simp hoelzl@57252: hoelzl@50419: end hoelzl@57252: hoelzl@57252: lemma (in prob_space) normal_density_affine: hoelzl@57252: assumes X: "distributed M lborel X (normal_density \ \)" hoelzl@57252: assumes [simp, arith]: "0 < \" "\ \ 0" hoelzl@57252: shows "distributed M lborel (\x. \ + \ * X x) (normal_density (\ + \ * \) (\\\ * \))" hoelzl@57252: proof - hoelzl@57252: have eq: "\x. \\\ * normal_density (\ + \ * \) (\\\ * \) (x * \ + \) = hoelzl@57252: normal_density \ \ x" hoelzl@57252: by (simp add: normal_density_def real_sqrt_mult field_simps) hoelzl@57252: (simp add: power2_eq_square field_simps) hoelzl@57252: show ?thesis hoelzl@57252: by (rule distributed_affineI[OF _ `\ \ 0`, where t=\]) (simp_all add: eq X) hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma (in prob_space) normal_standard_normal_convert: hoelzl@57252: assumes pos_var[simp, arith]: "0 < \" hoelzl@57252: shows "distributed M lborel X (normal_density \ \) = distributed M lborel (\x. (X x - \) / \) std_normal_density" hoelzl@57252: proof auto hoelzl@57252: assume "distributed M lborel X (\x. ereal (normal_density \ \ x))" hoelzl@57252: then have "distributed M lborel (\x. -\ / \ + (1/\) * X x) (\x. ereal (normal_density (-\ / \ + (1/\)* \) (\1/\\ * \) x))" hoelzl@57252: by(rule normal_density_affine) auto hoelzl@57252: hoelzl@57252: then show "distributed M lborel (\x. (X x - \) / \) (\x. ereal (std_normal_density x))" hoelzl@57252: by (simp add: diff_divide_distrib[symmetric] field_simps) hoelzl@57252: next hoelzl@57252: assume *: "distributed M lborel (\x. (X x - \) / \) (\x. ereal (std_normal_density x))" hoelzl@57252: have "distributed M lborel (\x. \ + \ * ((X x - \) / \)) (\x. ereal (normal_density \ \\\ x))" hoelzl@57252: using normal_density_affine[OF *, of \ \] by simp hoelzl@57252: then show "distributed M lborel X (\x. ereal (normal_density \ \ x))" by simp hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma conv_normal_density_zero_mean: hoelzl@57252: assumes [simp, arith]: "0 < \" "0 < \" hoelzl@57252: shows "(\x. \\<^sup>+y. ereal (normal_density 0 \ (x - y) * normal_density 0 \ y) \lborel) = hoelzl@57252: normal_density 0 (sqrt (\\<^sup>2 + \\<^sup>2))" (is "?LHS = ?RHS") hoelzl@57252: proof - hoelzl@57252: def \' \ "\\<^sup>2" and \' \ "\\<^sup>2" hoelzl@57252: then have [simp, arith]: "0 < \'" "0 < \'" hoelzl@57252: by simp_all hoelzl@57252: let ?\ = "sqrt ((\' * \') / (\' + \'))" hoelzl@57252: have sqrt: "(sqrt (2 * pi * (\' + \')) * sqrt (2 * pi * (\' * \') / (\' + \'))) = hoelzl@57252: (sqrt (2 * pi * \') * sqrt (2 * pi * \'))" hoelzl@57252: by (subst power_eq_iff_eq_base[symmetric, where n=2]) hoelzl@57252: (simp_all add: real_sqrt_mult[symmetric] power2_eq_square) hoelzl@57252: have "?LHS = hoelzl@57252: (\x. \\<^sup>+y. ereal((normal_density 0 (sqrt (\' + \')) x) * normal_density (\' * x / (\' + \')) ?\ y) \lborel)" hoelzl@57252: apply (intro ext nn_integral_cong) hoelzl@57252: apply (simp add: normal_density_def \'_def[symmetric] \'_def[symmetric] sqrt mult_exp_exp) hoelzl@57252: apply (simp add: divide_simps power2_eq_square) hoelzl@57252: apply (simp add: field_simps) hoelzl@57252: done hoelzl@57252: hoelzl@57252: also have "... = hoelzl@57252: (\x. (normal_density 0 (sqrt (\\<^sup>2 + \\<^sup>2)) x) * \\<^sup>+y. ereal( normal_density (\\<^sup>2* x / (\\<^sup>2 + \\<^sup>2)) ?\ y) \lborel)" hoelzl@57252: by (subst nn_integral_cmult[symmetric]) (auto simp: \'_def \'_def normal_density_def) hoelzl@57252: hoelzl@57252: also have "... = (\x. (normal_density 0 (sqrt (\\<^sup>2 + \\<^sup>2)) x))" hoelzl@57254: by (subst nn_integral_eq_integral) (auto simp: normal_density_nonneg) hoelzl@57252: hoelzl@57252: finally show ?thesis by fast hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma conv_std_normal_density: hoelzl@57252: "(\x. \\<^sup>+y. ereal (std_normal_density (x - y) * std_normal_density y) \lborel) = hoelzl@57252: (normal_density 0 (sqrt 2))" hoelzl@57252: by (subst conv_normal_density_zero_mean) simp_all hoelzl@57252: hoelzl@57252: lemma (in prob_space) sum_indep_normal: hoelzl@57252: assumes indep: "indep_var borel X borel Y" hoelzl@57252: assumes pos_var[arith]: "0 < \" "0 < \" hoelzl@57252: assumes normalX[simp]: "distributed M lborel X (normal_density \ \)" hoelzl@57252: assumes normalY[simp]: "distributed M lborel Y (normal_density \ \)" hoelzl@57252: shows "distributed M lborel (\x. X x + Y x) (normal_density (\ + \) (sqrt (\\<^sup>2 + \\<^sup>2)))" hoelzl@57252: proof - hoelzl@57252: have ind[simp]: "indep_var borel (\x. - \ + X x) borel (\x. - \ + Y x)" hoelzl@57252: proof - hoelzl@57252: have "indep_var borel ( (\x. -\ + x) o X) borel ((\x. - \ + x) o Y)" hoelzl@57252: by (auto intro!: indep_var_compose assms) hoelzl@57252: then show ?thesis by (simp add: o_def) hoelzl@57252: qed hoelzl@57252: hoelzl@57252: have "distributed M lborel (\x. -\ + 1 * X x) (normal_density (- \ + 1 * \) (\1\ * \))" hoelzl@57252: by(rule normal_density_affine[OF normalX pos_var(1), of 1 "-\"]) simp hoelzl@57252: then have 1[simp]: "distributed M lborel (\x. - \ + X x) (normal_density 0 \)" by simp hoelzl@57252: hoelzl@57252: have "distributed M lborel (\x. -\ + 1 * Y x) (normal_density (- \ + 1 * \) (\1\ * \))" hoelzl@57252: by(rule normal_density_affine[OF normalY pos_var(2), of 1 "-\"]) simp hoelzl@57252: then have 2[simp]: "distributed M lborel (\x. - \ + Y x) (normal_density 0 \)" by simp hoelzl@57252: hoelzl@57252: have *: "distributed M lborel (\x. (- \ + X x) + (- \ + Y x)) (\x. ereal (normal_density 0 (sqrt (\\<^sup>2 + \\<^sup>2)) x))" hoelzl@57252: using distributed_convolution[OF ind 1 2] conv_normal_density_zero_mean[OF pos_var] by simp hoelzl@57252: hoelzl@57252: have "distributed M lborel (\x. \ + \ + 1 * (- \ + X x + (- \ + Y x))) hoelzl@57252: (\x. ereal (normal_density (\ + \ + 1 * 0) (\1\ * sqrt (\\<^sup>2 + \\<^sup>2)) x))" hoelzl@57252: by (rule normal_density_affine[OF *, of 1 "\ + \"]) (auto simp: add_pos_pos) hoelzl@57252: hoelzl@57252: then show ?thesis by auto hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma (in prob_space) diff_indep_normal: hoelzl@57252: assumes indep[simp]: "indep_var borel X borel Y" hoelzl@57252: assumes [simp, arith]: "0 < \" "0 < \" hoelzl@57252: assumes normalX[simp]: "distributed M lborel X (normal_density \ \)" hoelzl@57252: assumes normalY[simp]: "distributed M lborel Y (normal_density \ \)" hoelzl@57252: shows "distributed M lborel (\x. X x - Y x) (normal_density (\ - \) (sqrt (\\<^sup>2 + \\<^sup>2)))" hoelzl@57252: proof - hoelzl@57252: have "distributed M lborel (\x. 0 + - 1 * Y x) (\x. ereal (normal_density (0 + - 1 * \) (\- 1\ * \) x))" hoelzl@57252: by(rule normal_density_affine, auto) hoelzl@57252: then have [simp]:"distributed M lborel (\x. - Y x) (\x. ereal (normal_density (- \) \ x))" by simp hoelzl@57252: hoelzl@57252: have "distributed M lborel (\x. X x + (- Y x)) (normal_density (\ + - \) (sqrt (\\<^sup>2 + \\<^sup>2)))" hoelzl@57252: apply (rule sum_indep_normal) hoelzl@57252: apply (rule indep_var_compose[unfolded comp_def, of borel _ borel _ "\x. x" _ "\x. - x"]) hoelzl@57252: apply simp_all hoelzl@57252: done hoelzl@57252: then show ?thesis by simp hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma (in prob_space) setsum_indep_normal: hoelzl@57252: assumes "finite I" "I \ {}" "indep_vars (\i. borel) X I" hoelzl@57252: assumes "\i. i \ I \ 0 < \ i" hoelzl@57252: assumes normal: "\i. i \ I \ distributed M lborel (X i) (normal_density (\ i) (\ i))" hoelzl@57252: shows "distributed M lborel (\x. \i\I. X i x) (normal_density (\i\I. \ i) (sqrt (\i\I. (\ i)\<^sup>2)))" hoelzl@57252: using assms hoelzl@57252: proof (induct I rule: finite_ne_induct) hoelzl@57252: case (singleton i) then show ?case by (simp add : abs_of_pos) hoelzl@57252: next hoelzl@57252: case (insert i I) hoelzl@57252: then have 1: "distributed M lborel (\x. (X i x) + (\i\I. X i x)) hoelzl@57252: (normal_density (\ i + setsum \ I) (sqrt ((\ i)\<^sup>2 + (sqrt (\i\I. (\ i)\<^sup>2))\<^sup>2)))" hoelzl@57252: apply (intro sum_indep_normal indep_vars_setsum insert real_sqrt_gt_zero) hoelzl@57252: apply (auto intro: indep_vars_subset intro!: setsum_pos) hoelzl@57252: apply fastforce hoelzl@57252: done hoelzl@57252: have 2: "(\x. (X i x)+ (\i\I. X i x)) = (\x. (\j\insert i I. X j x))" hoelzl@57252: "\ i + setsum \ I = setsum \ (insert i I)" hoelzl@57252: using insert by auto hoelzl@57252: hoelzl@57252: have 3: "(sqrt ((\ i)\<^sup>2 + (sqrt (\i\I. (\ i)\<^sup>2))\<^sup>2)) = (sqrt (\i\insert i I. (\ i)\<^sup>2))" hoelzl@57252: using insert by (simp add: setsum_nonneg) hoelzl@57252: hoelzl@57252: show ?case using 1 2 3 by simp hoelzl@57252: qed hoelzl@57252: hoelzl@57252: lemma (in prob_space) standard_normal_distributed_expectation: hoelzl@57254: assumes D: "distributed M lborel X std_normal_density" hoelzl@57252: shows "expectation X = 0" hoelzl@57254: using integral_std_normal_moment_odd[of 0] hoelzl@57252: by (auto simp: distributed_integral[OF D, of "\x. x", symmetric]) hoelzl@57252: hoelzl@57252: lemma (in prob_space) normal_distributed_expectation: hoelzl@57254: assumes \[arith]: "0 < \" hoelzl@57252: assumes D: "distributed M lborel X (normal_density \ \)" hoelzl@57252: shows "expectation X = \" hoelzl@57254: using integral_normal_moment_nz_1[OF \, of \] distributed_integral[OF D, of "\x. x", symmetric] hoelzl@57254: by (auto simp: field_simps) hoelzl@57252: hoelzl@57252: lemma (in prob_space) normal_distributed_variance: hoelzl@57252: fixes a b :: real hoelzl@57254: assumes [simp, arith]: "0 < \" hoelzl@57252: assumes D: "distributed M lborel X (normal_density \ \)" hoelzl@57252: shows "variance X = \\<^sup>2" hoelzl@57254: using integral_normal_moment_even[of \ \ 1] hoelzl@57254: by (subst distributed_integral[OF D, symmetric]) hoelzl@57254: (simp_all add: eval_nat_numeral normal_distributed_expectation[OF assms]) hoelzl@57252: hoelzl@57254: lemma (in prob_space) standard_normal_distributed_variance: hoelzl@57254: "distributed M lborel X std_normal_density \ variance X = 1" hoelzl@57254: using normal_distributed_variance[of 1 X 0] by simp hoelzl@57252: hoelzl@57252: lemma (in information_space) entropy_normal_density: hoelzl@57252: assumes [arith]: "0 < \" hoelzl@57252: assumes D: "distributed M lborel X (normal_density \ \)" hoelzl@57252: shows "entropy b lborel X = log b (2 * pi * exp 1 * \\<^sup>2) / 2" hoelzl@57252: proof - hoelzl@57252: have "entropy b lborel X = - (\ x. normal_density \ \ x * log b (normal_density \ \ x) \lborel)" hoelzl@57252: using D by (rule entropy_distr) hoelzl@57252: also have "\ = - (\ x. normal_density \ \ x * (- ln (2 * pi * \\<^sup>2) - (x - \)\<^sup>2 / \\<^sup>2) / (2 * ln b) \lborel)" hoelzl@57252: by (intro arg_cong[where f="uminus"] integral_cong) hoelzl@57252: (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt) hoelzl@57252: also have "\ = - (\x. - (normal_density \ \ x * (ln (2 * pi * \\<^sup>2)) + (normal_density \ \ x * (x - \)\<^sup>2) / \\<^sup>2) / (2 * ln b) \lborel)" hoelzl@57252: by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps) hoelzl@57252: also have "\ = (\x. normal_density \ \ x * (ln (2 * pi * \\<^sup>2)) + (normal_density \ \ x * (x - \)\<^sup>2) / \\<^sup>2 \lborel) / (2 * ln b)" hoelzl@57252: by (simp del: minus_add_distrib) hoelzl@57252: also have "\ = (ln (2 * pi * \\<^sup>2) + 1) / (2 * ln b)" hoelzl@57254: using integral_normal_moment_even[of \ \ 1] by (simp add: integrable_normal_moment fact_numeral) hoelzl@57252: also have "\ = log b (2 * pi * exp 1 * \\<^sup>2) / 2" hoelzl@57252: by (simp add: log_def field_simps ln_mult) hoelzl@57252: finally show ?thesis . hoelzl@57252: qed hoelzl@57252: hoelzl@57252: end