1 (* Title: HOL/Probability/Distributions.thy |
1 (* Title: HOL/Probability/Distributions.thy |
2 Author: Sudeep Kanav, TU München |
2 Author: Sudeep Kanav, TU München |
3 Author: Johannes Hölzl, TU München |
3 Author: Johannes Hölzl, TU München |
4 Author: Jeremy Avigad, CMU *) |
4 Author: Jeremy Avigad, CMU *) |
5 |
5 |
6 section {* Properties of Various Distributions *} |
6 section \<open>Properties of Various Distributions\<close> |
7 |
7 |
8 theory Distributions |
8 theory Distributions |
9 imports Convolution Information |
9 imports Convolution Information |
10 begin |
10 begin |
11 |
11 |
67 also have "\<dots> \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" |
67 also have "\<dots> \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" |
68 by (rule AE_density) simp |
68 by (rule AE_density) simp |
69 finally show ?thesis . |
69 finally show ?thesis . |
70 qed |
70 qed |
71 |
71 |
72 subsection {* Erlang *} |
72 subsection \<open>Erlang\<close> |
73 |
73 |
74 lemma nn_intergal_power_times_exp_Icc: |
74 lemma nn_intergal_power_times_exp_Icc: |
75 assumes [arith]: "0 \<le> a" |
75 assumes [arith]: "0 \<le> a" |
76 shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) = |
76 shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) = |
77 (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _") |
77 (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _") |
325 show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" |
325 show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" |
326 using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] |
326 using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] |
327 by simp (auto simp: power2_eq_square field_simps of_nat_Suc) |
327 by simp (auto simp: power2_eq_square field_simps of_nat_Suc) |
328 qed |
328 qed |
329 |
329 |
330 subsection {* Exponential distribution *} |
330 subsection \<open>Exponential distribution\<close> |
331 |
331 |
332 abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where |
332 abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where |
333 "exponential_density \<equiv> erlang_density 0" |
333 "exponential_density \<equiv> erlang_density 0" |
334 |
334 |
335 lemma exponential_density_def: |
335 lemma exponential_density_def: |
351 proof - |
351 proof - |
352 have "AE x in lborel. 0 \<le> exponential_density l x" |
352 have "AE x in lborel. 0 \<le> exponential_density l x" |
353 using assms by (auto simp: distributed_real_AE) |
353 using assms by (auto simp: distributed_real_AE) |
354 then have "AE x in lborel. x \<le> (0::real)" |
354 then have "AE x in lborel. x \<le> (0::real)" |
355 apply eventually_elim |
355 apply eventually_elim |
356 using `l < 0` |
356 using \<open>l < 0\<close> |
357 apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) |
357 apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) |
358 done |
358 done |
359 then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" |
359 then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" |
360 by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) |
360 by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) |
361 qed |
361 qed |
389 lemma (in prob_space) exponential_distributed_memoryless: |
389 lemma (in prob_space) exponential_distributed_memoryless: |
390 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t" |
390 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t" |
391 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" |
391 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" |
392 proof - |
392 proof - |
393 have "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. a + t < X x) / \<P>(x in M. a < X x)" |
393 have "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. a + t < X x) / \<P>(x in M. a < X x)" |
394 using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) |
394 using \<open>0 \<le> t\<close> by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) |
395 also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)" |
395 also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)" |
396 using a t by (simp add: exponential_distributedD_gt[OF D]) |
396 using a t by (simp add: exponential_distributedD_gt[OF D]) |
397 also have "\<dots> = exp (- t * l)" |
397 also have "\<dots> = exp (- t * l)" |
398 using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) |
398 using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) |
399 finally show ?thesis |
399 finally show ?thesis |
561 assumes [simp, arith]: "0 < l" |
561 assumes [simp, arith]: "0 < l" |
562 assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" |
562 assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" |
563 assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" |
563 assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" |
564 shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" |
564 shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" |
565 using assms |
565 using assms |
566 apply (subst convolution_erlang_density[symmetric, OF `0<l`]) |
566 apply (subst convolution_erlang_density[symmetric, OF \<open>0<l\<close>]) |
567 apply (intro distributed_convolution) |
567 apply (intro distributed_convolution) |
568 apply auto |
568 apply auto |
569 done |
569 done |
570 |
570 |
571 lemma (in prob_space) erlang_distributed_setsum: |
571 lemma (in prob_space) erlang_distributed_setsum: |
628 by simp |
628 by simp |
629 finally show ?thesis |
629 finally show ?thesis |
630 by (simp add: log_def divide_simps ln_div) |
630 by (simp add: log_def divide_simps ln_div) |
631 qed |
631 qed |
632 |
632 |
633 subsection {* Uniform distribution *} |
633 subsection \<open>Uniform distribution\<close> |
634 |
634 |
635 lemma uniform_distrI: |
635 lemma uniform_distrI: |
636 assumes X: "X \<in> measurable M M'" |
636 assumes X: "X \<in> measurable M M'" |
637 and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0" |
637 and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0" |
638 assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" |
638 assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" |
677 |
677 |
678 have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
678 have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
679 (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" |
679 (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" |
680 by (auto intro!: nn_integral_cong split: split_indicator) |
680 by (auto intro!: nn_integral_cong split: split_indicator) |
681 also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})" |
681 also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})" |
682 using `A \<in> sets borel` |
682 using \<open>A \<in> sets borel\<close> |
683 by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg) |
683 by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg) |
684 also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)" |
684 also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)" |
685 unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) |
685 unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) |
686 finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
686 finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = |
687 ereal (measure lborel (A \<inter> {..a}) / r)" . |
687 ereal (measure lborel (A \<inter> {..a}) / r)" . |
700 proof (elim disjE conjE) |
700 proof (elim disjE conjE) |
701 assume "t < a" |
701 assume "t < a" |
702 then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}" |
702 then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}" |
703 using X by (auto intro!: emeasure_mono measurable_sets) |
703 using X by (auto intro!: emeasure_mono measurable_sets) |
704 also have "\<dots> = 0" |
704 also have "\<dots> = 0" |
705 using distr[of a] `a < b` by (simp add: emeasure_eq_measure) |
705 using distr[of a] \<open>a < b\<close> by (simp add: emeasure_eq_measure) |
706 finally have "emeasure M {x\<in>space M. X x \<le> t} = 0" |
706 finally have "emeasure M {x\<in>space M. X x \<le> t} = 0" |
707 by (simp add: antisym measure_nonneg emeasure_le_0_iff) |
707 by (simp add: antisym measure_nonneg emeasure_le_0_iff) |
708 with `t < a` show ?thesis by simp |
708 with \<open>t < a\<close> show ?thesis by simp |
709 next |
709 next |
710 assume bnds: "a \<le> t" "t \<le> b" |
710 assume bnds: "a \<le> t" "t \<le> b" |
711 have "{a..b} \<inter> {..t} = {a..t}" |
711 have "{a..b} \<inter> {..t} = {a..t}" |
712 using bnds by auto |
712 using bnds by auto |
713 then show ?thesis using `a \<le> t` `a < b` |
713 then show ?thesis using \<open>a \<le> t\<close> \<open>a < b\<close> |
714 using distr[OF bnds] by (simp add: emeasure_eq_measure) |
714 using distr[OF bnds] by (simp add: emeasure_eq_measure) |
715 next |
715 next |
716 assume "b < t" |
716 assume "b < t" |
717 have "1 = emeasure M {x\<in>space M. X x \<le> b}" |
717 have "1 = emeasure M {x\<in>space M. X x \<le> b}" |
718 using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure) |
718 using distr[of b] \<open>a < b\<close> by (simp add: one_ereal_def emeasure_eq_measure) |
719 also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}" |
719 also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}" |
720 using X `b < t` by (auto intro!: emeasure_mono measurable_sets) |
720 using X \<open>b < t\<close> by (auto intro!: emeasure_mono measurable_sets) |
721 finally have "emeasure M {x\<in>space M. X x \<le> t} = 1" |
721 finally have "emeasure M {x\<in>space M. X x \<le> t} = 1" |
722 by (simp add: antisym emeasure_eq_measure one_ereal_def) |
722 by (simp add: antisym emeasure_eq_measure one_ereal_def) |
723 with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def) |
723 with \<open>b < t\<close> \<open>a < b\<close> show ?thesis by (simp add: measure_def one_ereal_def) |
724 qed |
724 qed |
725 qed (insert X `a < b`, auto) |
725 qed (insert X \<open>a < b\<close>, auto) |
726 |
726 |
727 lemma (in prob_space) uniform_distributed_measure: |
727 lemma (in prob_space) uniform_distributed_measure: |
728 fixes a b :: real |
728 fixes a b :: real |
729 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" |
729 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" |
730 assumes " a \<le> t" "t \<le> b" |
730 assumes " a \<le> t" "t \<le> b" |
732 proof - |
732 proof - |
733 have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}" |
733 have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}" |
734 using distributed_measurable[OF D] |
734 using distributed_measurable[OF D] |
735 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) |
735 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) |
736 also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)" |
736 also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)" |
737 using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b` |
737 using distributed_borel_measurable[OF D] \<open>a \<le> t\<close> \<open>t \<le> b\<close> |
738 unfolding distributed_distr_eq_density[OF D] |
738 unfolding distributed_distr_eq_density[OF D] |
739 by (subst emeasure_density) |
739 by (subst emeasure_density) |
740 (auto intro!: nn_integral_cong simp: measure_def split: split_indicator) |
740 (auto intro!: nn_integral_cong simp: measure_def split: split_indicator) |
741 also have "\<dots> = ereal (1 / (b - a)) * (t - a)" |
741 also have "\<dots> = ereal (1 / (b - a)) * (t - a)" |
742 using `a \<le> t` `t \<le> b` |
742 using \<open>a \<le> t\<close> \<open>t \<le> b\<close> |
743 by (subst nn_integral_cmult_indicator) auto |
743 by (subst nn_integral_cmult_indicator) auto |
744 finally show ?thesis |
744 finally show ?thesis |
745 by (simp add: measure_def) |
745 by (simp add: measure_def) |
746 qed |
746 qed |
747 |
747 |
786 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" |
786 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" |
787 using uniform_distributed_params[OF D] |
787 using uniform_distributed_params[OF D] |
788 by (auto intro!: isCont_divide) |
788 by (auto intro!: isCont_divide) |
789 have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = |
789 have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = |
790 (b*b - a * a) / (2 * (b - a))" |
790 (b*b - a * a) / (2 * (b - a))" |
791 using `a < b` |
791 using \<open>a < b\<close> |
792 by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) |
792 by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) |
793 show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" |
793 show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" |
794 using `a < b` |
794 using \<open>a < b\<close> |
795 unfolding * square_diff_square_factored by (auto simp: field_simps) |
795 unfolding * square_diff_square_factored by (auto simp: field_simps) |
796 qed (insert `a < b`, simp) |
796 qed (insert \<open>a < b\<close>, simp) |
797 finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" . |
797 finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" . |
798 qed auto |
798 qed auto |
799 |
799 |
800 lemma (in prob_space) uniform_distributed_variance: |
800 lemma (in prob_space) uniform_distributed_variance: |
801 fixes a b :: real |
801 fixes a b :: real |
810 by (simp add: integral_power uniform_distributed_expectation[OF D]) |
810 by (simp add: integral_power uniform_distributed_expectation[OF D]) |
811 (simp add: eval_nat_numeral field_simps ) |
811 (simp add: eval_nat_numeral field_simps ) |
812 finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" . |
812 finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" . |
813 qed fact |
813 qed fact |
814 |
814 |
815 subsection {* Normal distribution *} |
815 subsection \<open>Normal distribution\<close> |
816 |
816 |
817 |
817 |
818 definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where |
818 definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where |
819 "normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp (-(x - \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))" |
819 "normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp (-(x - \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))" |
820 |
820 |
934 have "2 \<noteq> (0::real)" |
934 have "2 \<noteq> (0::real)" |
935 by linarith |
935 by linarith |
936 let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel" |
936 let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel" |
937 have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) ---> |
937 have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) ---> |
938 (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto) |
938 (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto) |
939 proof (intro tendsto_intros `2 \<noteq> 0` tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) |
939 proof (intro tendsto_intros \<open>2 \<noteq> 0\<close> tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) |
940 show "(?M (k + 1) ---> 0) at_top" |
940 show "(?M (k + 1) ---> 0) at_top" |
941 proof cases |
941 proof cases |
942 assume "even k" |
942 assume "even k" |
943 have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top" |
943 have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top" |
944 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] |
944 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] |
945 filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) |
945 filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) |
946 auto |
946 auto |
947 also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)" |
947 also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)" |
948 using `even k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE) |
948 using \<open>even k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE) |
949 finally show ?thesis by simp |
949 finally show ?thesis by simp |
950 next |
950 next |
951 assume "odd k" |
951 assume "odd k" |
952 have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top" |
952 have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top" |
953 by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity |
953 by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity |
954 filterlim_ident filterlim_pow_at_top) |
954 filterlim_ident filterlim_pow_at_top) |
955 auto |
955 auto |
956 also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)" |
956 also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)" |
957 using `odd k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE) |
957 using \<open>odd k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE) |
958 finally show ?thesis by simp |
958 finally show ?thesis by simp |
959 qed |
959 qed |
960 qed |
960 qed |
961 also have "?tendsto \<longleftrightarrow> ((?f ---> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top)" |
961 also have "?tendsto \<longleftrightarrow> ((?f ---> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top)" |
962 proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) |
962 proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) |
1201 have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) = |
1201 have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) = |
1202 normal_density \<mu> \<sigma> x" |
1202 normal_density \<mu> \<sigma> x" |
1203 by (simp add: normal_density_def real_sqrt_mult field_simps) |
1203 by (simp add: normal_density_def real_sqrt_mult field_simps) |
1204 (simp add: power2_eq_square field_simps) |
1204 (simp add: power2_eq_square field_simps) |
1205 show ?thesis |
1205 show ?thesis |
1206 by (rule distributed_affineI[OF _ `\<alpha> \<noteq> 0`, where t=\<beta>]) (simp_all add: eq X) |
1206 by (rule distributed_affineI[OF _ \<open>\<alpha> \<noteq> 0\<close>, where t=\<beta>]) (simp_all add: eq X) |
1207 qed |
1207 qed |
1208 |
1208 |
1209 lemma (in prob_space) normal_standard_normal_convert: |
1209 lemma (in prob_space) normal_standard_normal_convert: |
1210 assumes pos_var[simp, arith]: "0 < \<sigma>" |
1210 assumes pos_var[simp, arith]: "0 < \<sigma>" |
1211 shows "distributed M lborel X (normal_density \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density" |
1211 shows "distributed M lborel X (normal_density \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density" |