author  hoelzl 
Wed, 18 Jun 2014 07:31:12 +0200  
changeset 57275  0ddb5b755cdc 
parent 57254  d3d91422f408 
child 57418  6ab1c7cb0b8d 
permissions  rwrr 
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

1 
(* Title: HOL/Probability/Distributions.thy 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

2 
Author: Sudeep Kanav, TU München 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

3 
Author: Johannes Hölzl, TU München 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

4 
Author: Jeremy Avigad, CMU *) 
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

5 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

6 
header {* Properties of Various Distributions *} 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

7 

50419  8 
theory Distributions 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

9 
imports Convolution Information 
50419  10 
begin 
11 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

12 
lemma (in prob_space) distributed_affine: 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

13 
fixes f :: "real \<Rightarrow> ereal" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

14 
assumes f: "distributed M lborel X f" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

15 
assumes c: "c \<noteq> 0" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

16 
shows "distributed M lborel (\<lambda>x. t + c * X x) (\<lambda>x. f ((x  t) / c) / \<bar>c\<bar>)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

17 
unfolding distributed_def 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

18 
proof safe 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

19 
have [measurable]: "f \<in> borel_measurable borel" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

20 
using f by (simp add: distributed_def) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

21 
have [measurable]: "X \<in> borel_measurable M" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

22 
using f by (simp add: distributed_def) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

23 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

24 
show "(\<lambda>x. f ((x  t) / c) / \<bar>c\<bar>) \<in> borel_measurable lborel" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

25 
by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

26 
show "random_variable lborel (\<lambda>x. t + c * X x)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

27 
by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

28 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

29 
have "AE x in lborel. 0 \<le> f x" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

30 
using f by (simp add: distributed_def) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

31 
from AE_borel_affine[OF _ _ this, where c="1/c" and t=" t / c"] c 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

32 
show "AE x in lborel. 0 \<le> f ((x  t) / c) / ereal \<bar>c\<bar>" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

33 
by (auto simp add: field_simps) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

34 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

35 
have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

36 
using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

37 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

38 
have "density lborel f = distr M lborel X" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

39 
using f by (simp add: distributed_def) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

40 
with c show "distr M lborel (\<lambda>x. t + c * X x) = density lborel (\<lambda>x. f ((x  t) / c) / ereal \<bar>c\<bar>)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

41 
by (subst (2) lborel_real_affine[where c="c" and t="t"]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

42 
(simp_all add: density_density_eq density_distr distr_distr field_simps eq cong: distr_cong) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

43 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

44 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

45 
lemma (in prob_space) distributed_affineI: 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

46 
fixes f :: "real \<Rightarrow> ereal" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

47 
assumes f: "distributed M lborel (\<lambda>x. (X x  t) / c) (\<lambda>x. \<bar>c\<bar> * f (x * c + t))" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

48 
assumes c: "c \<noteq> 0" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

49 
shows "distributed M lborel X f" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

50 
proof  
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

51 
have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

52 
using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

53 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

54 
show ?thesis 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

55 
using distributed_affine[OF f c, where t=t] c 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

56 
by (simp add: field_simps eq) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

57 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

58 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

59 
lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b  a else 0)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

60 
by (auto simp: measure_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

61 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

62 
lemma integral_power: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

63 
"a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k  a^Suc k) / Suc k" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

64 
proof (subst integral_FTC_atLeastAtMost) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

65 
fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

66 
by (intro derivative_eq_intros) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

67 
qed (auto simp: field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

68 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

69 
lemma has_bochner_integral_nn_integral: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

70 
assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

71 
assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

72 
shows "has_bochner_integral M f x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

73 
unfolding has_bochner_integral_iff 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

74 
proof 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

75 
show "integrable M f" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

76 
using assms by (rule integrableI_nn_integral_finite) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

77 
qed (auto simp: assms integral_eq_nn_integral) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

78 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

79 
lemma (in prob_space) distributed_AE2: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

80 
assumes [measurable]: "distributed M N X f" "Measurable.pred N P" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

81 
shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

82 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

83 
have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

84 
by (simp add: AE_distr_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

85 
also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

86 
unfolding distributed_distr_eq_density[OF assms(1)] .. 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

87 
also have "\<dots> \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

88 
by (rule AE_density) simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

89 
finally show ?thesis . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

90 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

91 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

92 
subsection {* Erlang *} 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

93 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

94 
lemma nn_intergal_power_times_exp_Icc: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

95 
assumes [arith]: "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

96 
shows "(\<integral>\<^sup>+x. ereal (x^k * exp (x)) * indicator {0 .. a} x \<partial>lborel) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

97 
(1  (\<Sum>n\<le>k. (a^n * exp (a)) / fact n)) * fact k" (is "?I = _") 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

98 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

99 
let ?f = "\<lambda>k x. x^k * exp (x) / fact k" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

100 
let ?F = "\<lambda>k x.  (\<Sum>n\<le>k. (x^n * exp (x)) / fact n)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

101 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

102 
have "?I * (inverse (fact k)) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

103 
(\<integral>\<^sup>+x. ereal (x^k * exp (x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

104 
by (intro nn_integral_multc[symmetric]) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

105 
also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

106 
by (intro nn_integral_cong) (simp add: field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

107 
also have "\<dots> = ereal (?F k a)  (?F k 0)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

108 
proof (rule nn_integral_FTC_atLeastAtMost) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

109 
fix x assume "x \<in> {0..a}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

110 
show "DERIV (?F k) x :> ?f k x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

111 
proof(induction k) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

112 
case 0 show ?case by (auto intro!: derivative_eq_intros) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

113 
next 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

114 
case (Suc k) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

115 
have "DERIV (\<lambda>x. ?F k x  (x^Suc k * exp (x)) / fact (Suc k)) x :> 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

116 
?f k x  ((real (Suc k)  x) * x ^ k * exp ( x)) / real (fact (Suc k))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

117 
by (intro DERIV_diff Suc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

118 
(auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

119 
simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

120 
also have "(\<lambda>x. ?F k x  (x^Suc k * exp (x)) / fact (Suc k)) = ?F (Suc k)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

121 
by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

122 
also have "?f k x  ((real (Suc k)  x) * x ^ k * exp ( x)) / real (fact (Suc k)) = ?f (Suc k) x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

123 
by (auto simp: field_simps simp del: fact_Suc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

124 
(simp_all add: real_of_nat_Suc field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

125 
finally show ?case . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

126 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

127 
qed auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

128 
also have "\<dots> = ereal (1  (\<Sum>n\<le>k. (a^n * exp (a)) / fact n))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

129 
by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum_cases) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

130 
finally show ?thesis 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

131 
by (cases "?I") (auto simp: field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

132 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

133 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

134 
lemma nn_intergal_power_times_exp_Ici: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

135 
shows "(\<integral>\<^sup>+x. ereal (x^k * exp (x)) * indicator {0 ..} x \<partial>lborel) = fact k" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

136 
proof (rule LIMSEQ_unique) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

137 
let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (x)) * indicator {0 .. real n} x \<partial>lborel" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

138 
show "?X > (\<integral>\<^sup>+x. ereal (x^k * exp (x)) * indicator {0 ..} x \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

139 
apply (intro nn_integral_LIMSEQ) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

140 
apply (auto simp: incseq_def le_fun_def eventually_sequentially 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

141 
split: split_indicator intro!: Lim_eventually) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

142 
apply (metis natceiling_le_eq) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

143 
done 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

144 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

145 
have "((\<lambda>x. (1  (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) > (1  (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

146 
by (intro tendsto_intros tendsto_power_div_exp_0) simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

147 
then show "?X > fact k" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

148 
by (subst nn_intergal_power_times_exp_Icc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

149 
(auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

150 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

151 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

152 
definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

153 
"erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp ( l * x)) / fact k)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

154 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

155 
definition erlang_CDF :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

156 
"erlang_CDF k l x = (if x < 0 then 0 else 1  (\<Sum>n\<le>k. ((l * x)^n * exp ( l * x) / fact n)))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

157 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

158 
lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

159 
by (simp add: erlang_density_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

160 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

161 
lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

162 
by (auto simp add: erlang_density_def[abs_def]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

163 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

164 
lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

165 
by (auto simp add: erlang_CDF_def mult_less_0_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

166 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

167 
lemma nn_integral_erlang_density: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

168 
assumes [arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

169 
shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

170 
proof cases 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

171 
assume [arith]: "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

172 
have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

173 
by (simp add: field_simps split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

174 
have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

175 
(\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp ( (l*x))) * indicator {0 .. a} x) \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

176 
by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

177 
also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp ( (l*x))) * indicator {0 .. a} x \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

178 
by (intro nn_integral_cmult) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

179 
also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp ( x)) * indicator {0 .. l * a} x \<partial>lborel))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

180 
by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

181 
also have "\<dots> = (1  (\<Sum>n\<le>k. ((l * a)^n * exp ((l * a))) / fact n))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

182 
by (subst nn_intergal_power_times_exp_Icc) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

183 
also have "\<dots> = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

184 
by (auto simp: erlang_CDF_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

185 
finally show ?thesis . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

186 
next 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

187 
assume "\<not> 0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

188 
moreover then have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

189 
by (intro nn_integral_cong) (auto simp: erlang_density_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

190 
ultimately show ?thesis 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

191 
by (simp add: erlang_CDF_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

192 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

193 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

194 
lemma emeasure_erlang_density: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

195 
"0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

196 
by (simp add: emeasure_density nn_integral_erlang_density) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

197 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

198 
lemma nn_integral_erlang_ith_moment: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

199 
fixes k i :: nat and l :: real 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

200 
assumes [arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

201 
shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

202 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

203 
have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

204 
by (simp add: field_simps split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

205 
have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

206 
(\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp ( (l*x))) * indicator {0 ..} x) \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

207 
by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

208 
also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp ( (l*x))) * indicator {0 ..} x \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

209 
by (intro nn_integral_cmult) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

210 
also have "\<dots> = ereal (l/(fact k * l^i)) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^(k+i) * exp ( x)) * indicator {0 ..} x \<partial>lborel))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

211 
by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

212 
also have "\<dots> = fact (k + i) / (fact k * l ^ i)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

213 
by (subst nn_intergal_power_times_exp_Ici) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

214 
finally show ?thesis . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

215 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

216 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

217 
lemma prob_space_erlang_density: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

218 
assumes l[arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

219 
shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D") 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

220 
proof 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

221 
show "emeasure ?D (space ?D) = 1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

222 
using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

223 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

224 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

225 
lemma (in prob_space) erlang_distributed_le: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

226 
assumes D: "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

227 
assumes [simp, arith]: "0 < l" "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

228 
shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

229 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

230 
have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

231 
using distributed_measurable[OF D] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

232 
by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

233 
also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

234 
unfolding distributed_distr_eq_density[OF D] .. 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

235 
also have "\<dots> = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

236 
by (auto intro!: emeasure_erlang_density) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

237 
finally show ?thesis 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

238 
by (auto simp: measure_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

239 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

240 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

241 
lemma (in prob_space) erlang_distributed_gt: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

242 
assumes D[simp]: "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

243 
assumes [arith]: "0 < l" "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

244 
shows "\<P>(x in M. a < X x ) = 1  (erlang_CDF k l a)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

245 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

246 
have " 1  (erlang_CDF k l a) = 1  \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

247 
also have "\<dots> = prob (space M  {x \<in> space M. X x \<le> a })" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

248 
using distributed_measurable[OF D] by (auto simp: prob_compl) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

249 
also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

250 
finally show ?thesis by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

251 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

252 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

253 
lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

254 
by (induction k) (auto simp: erlang_CDF_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

255 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

256 
lemma erlang_distributedI: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

257 
assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

258 
and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

259 
shows "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

260 
proof (rule distributedI_borel_atMost) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

261 
fix a :: real 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

262 
{ assume "a \<le> 0" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

263 
with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

264 
by (intro emeasure_mono) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

265 
also have "... = 0" by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

266 
finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

267 
then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

268 
} 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

269 
note eq_0 = this 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

270 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

271 
show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

272 
using nn_integral_erlang_density[of l k a] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

273 
by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

274 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

275 
show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

276 
using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

277 
qed (simp_all add: erlang_density_nonneg) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

278 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

279 
lemma (in prob_space) erlang_distributed_iff: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

280 
assumes [arith]: "0<l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

281 
shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow> 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

282 
(X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = erlang_CDF k l a ))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

283 
using 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

284 
distributed_measurable[of M lborel X "erlang_density k l"] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

285 
emeasure_erlang_density[of l] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

286 
erlang_distributed_le[of X k l] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

287 
by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

288 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

289 
lemma (in prob_space) erlang_distributed_mult_const: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

290 
assumes erlX: "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

291 
assumes a_pos[arith]: "0 < \<alpha>" "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

292 
shows "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

293 
proof (subst erlang_distributed_iff, safe) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

294 
have [measurable]: "random_variable borel X" and [arith]: "0 < l " 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

295 
and [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

296 
by(insert erlX, auto simp: erlang_distributed_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

297 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

298 
show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>" "0 < l / \<alpha>" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

299 
by (auto simp:field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

300 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

301 
fix a:: real assume [arith]: "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

302 
obtain b:: real where [simp, arith]: "b = a/ \<alpha>" by blast 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

303 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

304 
have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

305 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

306 
have "prob {x \<in> space M. \<alpha> * X x \<le> a} = prob {x \<in> space M. X x \<le> b}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

307 
by (rule arg_cong[where f= prob]) (auto simp:field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

308 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

309 
moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

310 
moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

311 
ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

312 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

313 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

314 
lemma (in prob_space) has_bochner_integral_erlang_ith_moment: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

315 
fixes k i :: nat and l :: real 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

316 
assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

317 
shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

318 
proof (rule has_bochner_integral_nn_integral) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

319 
show "AE x in M. 0 \<le> X x ^ i" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

320 
by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

321 
show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

322 
using nn_integral_erlang_ith_moment[of l k i] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

323 
by (subst distributed_nn_integral[symmetric, OF D]) auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

324 
qed (insert distributed_measurable[OF D], simp) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

325 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

326 
lemma (in prob_space) erlang_ith_moment_integrable: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

327 
"0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

328 
by rule (rule has_bochner_integral_erlang_ith_moment) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

329 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

330 
lemma (in prob_space) erlang_ith_moment: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

331 
"0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

332 
expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

333 
by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

334 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

335 
lemma (in prob_space) erlang_distributed_variance: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

336 
assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

337 
shows "variance X = (k + 1) / l\<^sup>2" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

338 
proof (subst variance_eq) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

339 
show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

340 
using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

341 
by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

342 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

343 
show "expectation (\<lambda>x. (X x)\<^sup>2)  (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

344 
using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

345 
by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

346 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

347 

50419  348 
subsection {* Exponential distribution *} 
349 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

350 
abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

351 
"exponential_density \<equiv> erlang_density 0" 
50419  352 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

353 
lemma exponential_density_def: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

354 
"exponential_density l x = (if x < 0 then 0 else l * exp ( x * l))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

355 
by (simp add: fun_eq_iff erlang_density_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

356 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

357 
lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1  exp ( l * a) else 0)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

358 
by (simp add: erlang_CDF_def) 
50419  359 

360 
lemma (in prob_space) exponential_distributed_params: 

361 
assumes D: "distributed M lborel X (exponential_density l)" 

362 
shows "0 < l" 

363 
proof (cases l "0 :: real" rule: linorder_cases) 

364 
assume "l < 0" 

365 
have "emeasure lborel {0 <.. 1::real} \<le> 

366 
emeasure lborel {x :: real \<in> space lborel. 0 < x}" 

367 
by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric]) 

368 
also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" 

369 
proof  

370 
have "AE x in lborel. 0 \<le> exponential_density l x" 

371 
using assms by (auto simp: distributed_real_AE) 

372 
then have "AE x in lborel. x \<le> (0::real)" 

373 
apply eventually_elim 

374 
using `l < 0` 

375 
apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) 

376 
done 

377 
then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0" 

378 
by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) 

379 
qed 

380 
finally show "0 < l" by simp 

381 
next 

382 
assume "l = 0" 

383 
then have [simp]: "\<And>x. ereal (exponential_density l x) = 0" 

384 
by (simp add: exponential_density_def) 

385 
interpret X: prob_space "distr M lborel X" 

386 
using distributed_measurable[OF D] by (rule prob_space_distr) 

387 
from X.emeasure_space_1 

388 
show "0 < l" 

389 
by (simp add: emeasure_density distributed_distr_eq_density[OF D]) 

390 
qed assumption 

391 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

392 
lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

393 
by (rule prob_space_erlang_density) 
50419  394 

395 
lemma (in prob_space) exponential_distributedD_le: 

396 
assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" 

397 
shows "\<P>(x in M. X x \<le> a) = 1  exp ( a * l)" 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

398 
using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

399 
by (simp add: erlang_CDF_def) 
50419  400 

401 
lemma (in prob_space) exponential_distributedD_gt: 

402 
assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" 

403 
shows "\<P>(x in M. a < X x ) = exp ( a * l)" 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

404 
using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

405 
by (simp add: erlang_CDF_def) 
50419  406 

407 
lemma (in prob_space) exponential_distributed_memoryless: 

408 
assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t" 

409 
shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" 

410 
proof  

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

412 
using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) 

413 
also have "\<dots> = exp ( (a + t) * l) / exp ( a * l)" 

414 
using a t by (simp add: exponential_distributedD_gt[OF D]) 

415 
also have "\<dots> = exp ( t * l)" 

416 
using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) 

417 
finally show ?thesis 

418 
using t by (simp add: exponential_distributedD_gt[OF D]) 

419 
qed 

420 

421 
lemma exponential_distributedI: 

422 
assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" 

423 
and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1  exp ( a * l)" 

424 
shows "distributed M lborel X (exponential_density l)" 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

425 
proof (rule erlang_distributedI) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

426 
fix a :: real assume "0 \<le> a" then show "emeasure M {x \<in> space M. X x \<le> a} = ereal (erlang_CDF 0 l a)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

427 
using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

428 
qed fact+ 
50419  429 

430 
lemma (in prob_space) exponential_distributed_iff: 

431 
"distributed M lborel X (exponential_density l) \<longleftrightarrow> 

432 
(X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1  exp ( a * l)))" 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

433 
using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0) 
50419  434 

435 

436 
lemma (in prob_space) exponential_distributed_expectation: 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

437 
"distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

438 
using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

439 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

440 
lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

441 
by (auto simp: exponential_density_def) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

442 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

443 
lemma (in prob_space) exponential_distributed_min: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

444 
assumes expX: "distributed M lborel X (exponential_density l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

445 
assumes expY: "distributed M lborel Y (exponential_density u)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

446 
assumes ind: "indep_var borel X borel Y" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

447 
shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

448 
proof (subst exponential_distributed_iff, safe) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

449 
have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

450 
moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

451 
ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

452 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

453 
have "0 < l" by (rule exponential_distributed_params) fact 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

454 
moreover have "0 < u" by (rule exponential_distributed_params) fact 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

455 
ultimately show " 0 < l + u" by force 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

456 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

457 
fix a::real assume a[arith]: "0 \<le> a" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

458 
have gt1[simp]: "\<P>(x in M. a < X x ) = exp ( a * l)" by (rule exponential_distributedD_gt[OF expX a]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

459 
have gt2[simp]: "\<P>(x in M. a < Y x ) = exp ( a * u)" by (rule exponential_distributedD_gt[OF expY a]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

460 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

461 
have "\<P>(x in M. a < (min (X x) (Y x)) ) = \<P>(x in M. a < (X x) \<and> a < (Y x))" by (auto intro!:arg_cong[where f=prob]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

462 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

463 
also have " ... = \<P>(x in M. a < (X x)) * \<P>(x in M. a< (Y x) )" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

464 
using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

465 
also have " ... = exp ( a * (l + u))" by (auto simp:field_simps mult_exp_exp) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

466 
finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp ( a * (l + u))" . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

467 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

468 
have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M  {x \<in> space M. a<(min (X x) (Y x)) })" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

469 
by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

470 
then have "1  prob {x \<in> space M. a < (min (X x) (Y x))} = prob {x \<in> space M. (min (X x) (Y x)) \<le> a}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

471 
using randX randY by (auto simp: prob_compl) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

472 
then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1  exp ( a * (l + u))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

473 
using indep_prob by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

474 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

475 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

476 
lemma (in prob_space) exponential_distributed_Min: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

477 
assumes finI: "finite I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

478 
assumes A: "I \<noteq> {}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

479 
assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

480 
assumes ind: "indep_vars (\<lambda>i. borel) X I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

481 
shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

482 
using assms 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

483 
proof (induct rule: finite_ne_induct) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

484 
case (singleton i) then show ?case by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

485 
next 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

486 
case (insert i I) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

487 
then have "distributed M lborel (\<lambda>x. min (X i x) (Min ((\<lambda>i. X i x)`I))) (exponential_density (l i + (\<Sum>i\<in>I. l i)))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

488 
by (intro exponential_distributed_min indep_vars_Min insert) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

489 
(auto intro: indep_vars_subset) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

490 
then show ?case 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

491 
using insert by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

492 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

493 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

494 
lemma (in prob_space) exponential_distributed_variance: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

495 
"distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

496 
using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

497 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

498 
lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

499 
by (simp cong: nn_integral_cong_AE) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

500 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

501 
lemma convolution_erlang_density: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

502 
fixes k\<^sub>1 k\<^sub>2 :: nat 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

503 
assumes [simp, arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

504 
shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x  y)) * ereal (erlang_density k\<^sub>2 l y) \<partial>lborel) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

505 
(erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2  1) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

506 
(is "?LHS = ?RHS") 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

507 
proof 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

508 
fix x :: real 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

509 
have "x \<le> 0 \<or> 0 < x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

510 
by arith 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

511 
then show "?LHS x = ?RHS x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

512 
proof 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

513 
assume "x \<le> 0" then show ?thesis 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

514 
apply (subst nn_integral_zero') 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

515 
apply (rule AE_I[where N="{0}"]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

516 
apply (auto simp add: erlang_density_def not_less) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

517 
done 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

518 
next 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

519 
note zero_le_mult_iff[simp] zero_le_divide_iff[simp] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

520 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

521 
have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2  1) l) = 1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

522 
using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2  1" 0] by (simp del: fact_Suc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

523 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

524 
have 1: "(\<integral>\<^sup>+ x. ereal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2  1) l x * indicator {0<..} x) \<partial>lborel) = 1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

525 
apply (subst I_eq1[symmetric]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

526 
unfolding erlang_density_def 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

527 
by (auto intro!: nn_integral_cong split:split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

528 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

529 
have "prob_space (density lborel ?LHS)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

530 
unfolding times_ereal.simps[symmetric] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

531 
by (intro prob_space_convolution_density) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

532 
(auto intro!: prob_space_erlang_density erlang_density_nonneg) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

533 
then have 2: "integral\<^sup>N lborel ?LHS = 1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

534 
by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

535 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

536 
let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1  y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

537 
let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

538 
let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2  1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

539 
let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

540 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

541 
{ fix x :: real assume [arith]: "0 < x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

542 
have *: "\<And>x y n. (x  y * x::real)^n = x^n * (1  y)^n" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

543 
unfolding power_mult_distrib[symmetric] by (simp add: field_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

544 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

545 
have "?LHS x = ?L x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

546 
unfolding erlang_density_def 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

547 
by (auto intro!: nn_integral_cong split:split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

548 
also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

549 
apply (subst nn_integral_real_affine[where c=x and t = 0]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

550 
apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

551 
apply (intro nn_integral_cong) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

552 
apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add * 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

553 
simp del: fact_Suc split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

554 
done 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

555 
finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x  y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

556 
(\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

557 
by simp } 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

558 
note * = this 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

559 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

560 
assume [arith]: "0 < x" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

561 
have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

562 
by (subst 2[symmetric]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

563 
(auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

564 
simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: split_if_asm) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

565 
also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

566 
by (auto intro!: nn_integral_cong simp: * split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

567 
also have "... = ereal (?C) * ?I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

568 
using 1 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

569 
by (auto simp: nn_integral_nonneg nn_integral_cmult) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

570 
finally have " ereal (?C) * ?I = 1" by presburger 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

571 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

572 
then show ?thesis 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

573 
using * by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

574 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

575 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

576 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

577 
lemma (in prob_space) sum_indep_erlang: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

578 
assumes indep: "indep_var borel X borel Y" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

579 
assumes [simp, arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

580 
assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

581 
assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

582 
shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2  1) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

583 
using assms 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

584 
apply (subst convolution_erlang_density[symmetric, OF `0<l`]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

585 
apply (intro distributed_convolution) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

586 
apply auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

587 
done 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

588 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

589 
lemma (in prob_space) erlang_distributed_setsum: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

590 
assumes finI : "finite I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

591 
assumes A: "I \<noteq> {}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

592 
assumes [simp, arith]: "0 < l" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

593 
assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

594 
assumes ind: "indep_vars (\<lambda>i. borel) X I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

595 
shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i))  1) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

596 
using assms 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

597 
proof (induct rule: finite_ne_induct) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

598 
case (singleton i) then show ?case by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

599 
next 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

600 
case (insert i I) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

601 
then have "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) (erlang_density (Suc (k i) + Suc ((\<Sum>i\<in>I. Suc (k i))  1)  1) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

602 
by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

603 
also have "(\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) = (\<lambda>x. \<Sum>i\<in>insert i I. X i x)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

604 
using insert by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

605 
also have "Suc(k i) + Suc ((\<Sum>i\<in>I. Suc (k i))  1)  1 = (\<Sum>i\<in>insert i I. Suc (k i))  1" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

606 
using insert by (auto intro!: Suc_pred simp: ac_simps) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

607 
finally show ?case by fast 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

608 
qed 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

609 

b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

610 
lemma (in prob_space) exponential_distributed_setsum: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

611 
assumes finI: "finite I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

612 
assumes A: "I \<noteq> {}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

613 
assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

614 
assumes ind: "indep_vars (\<lambda>i. borel) X I" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

615 
shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I)  1) l)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

616 
proof  
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

617 
obtain i where "i \<in> I" using assms by auto 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

618 
note exponential_distributed_params[OF expX[OF this]] 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

619 
from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

620 
qed 
50419  621 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

622 
lemma (in information_space) entropy_exponential: 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

623 
assumes D: "distributed M lborel X (exponential_density l)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

624 
shows "entropy b lborel X = log b (exp 1 / l)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

625 
proof  
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

626 
have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

627 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

628 
have [simp]: "integrable lborel (exponential_density l)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

629 
using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

630 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

631 
have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

632 
using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

633 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

634 
have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

635 
using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

636 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

637 
have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

638 
using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

639 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

640 
have "entropy b lborel X =  (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

641 
using D by (rule entropy_distr) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

642 
also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

643 
(\<integral> x. (ln l * exponential_density l x  l * (exponential_density l x * x)) / ln b \<partial>lborel)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

644 
by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

645 
also have "\<dots> = (ln l  1) / ln b" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

646 
by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

647 
finally show ?thesis 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

648 
by (simp add: log_def divide_simps ln_div) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

649 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

650 

50419  651 
subsection {* Uniform distribution *} 
652 

653 
lemma uniform_distrI: 

654 
assumes X: "X \<in> measurable M M'" 

655 
and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0" 

656 
assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X ` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" 

657 
shows "distr M M' X = uniform_measure M' A" 

658 
unfolding uniform_measure_def 

659 
proof (intro measure_eqI) 

660 
let ?f = "\<lambda>x. indicator A x / emeasure M' A" 

661 
fix B assume B: "B \<in> sets (distr M M' X)" 

662 
with X have "emeasure M (X ` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" 

663 
by (simp add: distr[of B] measurable_sets) 

664 
also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)" 

665 
by simp 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

666 
also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')" 
50419  667 
using A B 
56996  668 
by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

669 
also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')" 
56996  670 
by (rule nn_integral_cong) (auto split: split_indicator) 
50419  671 
finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" 
672 
using A B X by (auto simp add: emeasure_distr emeasure_density) 

673 
qed simp 

674 

675 
lemma uniform_distrI_borel: 

676 
fixes A :: "real set" 

677 
assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r" 

678 
and [measurable]: "A \<in> sets borel" 

679 
assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r" 

680 
shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)" 

681 
proof (rule distributedI_borel_atMost) 

682 
let ?f = "\<lambda>x. 1 / r * indicator A x" 

683 
fix a 

684 
have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A" 

685 
using A by (intro emeasure_mono) auto 

686 
also have "\<dots> < \<infinity>" 

687 
using A by simp 

688 
finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>" 

689 
by simp 

690 
from emeasure_eq_ereal_measure[OF this] 

691 
have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ereal (measure lborel (A \<inter> {..a}) / r)" 

692 
using A by simp 

693 
then show "emeasure M {x\<in>space M. X x \<le> a} = ereal (measure lborel (A \<inter> {..a}) / r)" 

694 
using distr by simp 

695 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

696 
have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

697 
(\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" 
56996  698 
by (auto intro!: nn_integral_cong split: split_indicator) 
50419  699 
also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})" 
700 
using `A \<in> sets borel` 

56996  701 
by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg) 
50419  702 
also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)" 
703 
unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

704 
finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = 
50419  705 
ereal (measure lborel (A \<inter> {..a}) / r)" . 
56571
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56536
diff
changeset

706 
qed (auto simp: measure_nonneg) 
50419  707 

708 
lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: 

709 
fixes a b :: real 

710 
assumes X: "X \<in> borel_measurable M" and "a < b" 

711 
assumes distr: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> \<P>(x in M. X x \<le> t) = (t  a) / (b  a)" 

712 
shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})" 

713 
proof (rule uniform_distrI_borel) 

714 
fix t 

715 
have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t" 

716 
by auto 

717 
then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b  a)" 

718 
proof (elim disjE conjE) 

719 
assume "t < a" 

720 
then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}" 

721 
using X by (auto intro!: emeasure_mono measurable_sets) 

722 
also have "\<dots> = 0" 

723 
using distr[of a] `a < b` by (simp add: emeasure_eq_measure) 

724 
finally have "emeasure M {x\<in>space M. X x \<le> t} = 0" 

725 
by (simp add: antisym measure_nonneg emeasure_le_0_iff) 

726 
with `t < a` show ?thesis by simp 

727 
next 

728 
assume bnds: "a \<le> t" "t \<le> b" 

729 
have "{a..b} \<inter> {..t} = {a..t}" 

730 
using bnds by auto 

731 
then show ?thesis using `a \<le> t` `a < b` 

732 
using distr[OF bnds] by (simp add: emeasure_eq_measure) 

733 
next 

734 
assume "b < t" 

735 
have "1 = emeasure M {x\<in>space M. X x \<le> b}" 

736 
using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure) 

737 
also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}" 

738 
using X `b < t` by (auto intro!: emeasure_mono measurable_sets) 

739 
finally have "emeasure M {x\<in>space M. X x \<le> t} = 1" 

740 
by (simp add: antisym emeasure_eq_measure one_ereal_def) 

741 
with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def) 

742 
qed 

743 
qed (insert X `a < b`, auto) 

744 

745 
lemma (in prob_space) uniform_distributed_measure: 

746 
fixes a b :: real 

747 
assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 

748 
assumes " a \<le> t" "t \<le> b" 

749 
shows "\<P>(x in M. X x \<le> t) = (t  a) / (b  a)" 

750 
proof  

751 
have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}" 

752 
using distributed_measurable[OF D] 

753 
by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

754 
also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b  a)) * indicator {a .. t} x \<partial>lborel)" 
50419  755 
using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b` 
756 
unfolding distributed_distr_eq_density[OF D] 

757 
by (subst emeasure_density) 

56996  758 
(auto intro!: nn_integral_cong simp: measure_def split: split_indicator) 
50419  759 
also have "\<dots> = ereal (1 / (b  a)) * (t  a)" 
760 
using `a \<le> t` `t \<le> b` 

56996  761 
by (subst nn_integral_cmult_indicator) auto 
50419  762 
finally show ?thesis 
763 
by (simp add: measure_def) 

764 
qed 

765 

766 
lemma (in prob_space) uniform_distributed_bounds: 

767 
fixes a b :: real 

768 
assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 

769 
shows "a < b" 

770 
proof (rule ccontr) 

771 
assume "\<not> a < b" 

772 
then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp 

773 
with uniform_distributed_params[OF D] show False 

774 
by (auto simp: measure_def) 

775 
qed 

776 

777 
lemma (in prob_space) uniform_distributed_iff: 

778 
fixes a b :: real 

779 
shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> 

780 
(X \<in> borel_measurable M \<and> a < b \<and> (\<forall>t\<in>{a .. b}. \<P>(x in M. X x \<le> t)= (t  a) / (b  a)))" 

781 
using 

782 
uniform_distributed_bounds[of X a b] 

783 
uniform_distributed_measure[of X a b] 

784 
distributed_measurable[of M lborel X] 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56571
diff
changeset

785 
by (auto intro!: uniform_distrI_borel_atLeastAtMost 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56571
diff
changeset

786 
simp: one_ereal_def emeasure_eq_measure 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56571
diff
changeset

787 
simp del: measure_lborel) 
50419  788 

789 
lemma (in prob_space) uniform_distributed_expectation: 

790 
fixes a b :: real 

791 
assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 

792 
shows "expectation X = (a + b) / 2" 

793 
proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric]) 

794 
have "a < b" 

795 
using uniform_distributed_bounds[OF D] . 

796 

797 
have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 

798 
(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)" 

799 
by (intro integral_cong) auto 

800 
also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2" 

801 
proof (subst integral_FTC_atLeastAtMost) 

802 
fix x 

53077  803 
show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" 
50419  804 
using uniform_distributed_params[OF D] 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

805 
by (auto intro!: derivative_eq_intros) 
50419  806 
show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" 
807 
using uniform_distributed_params[OF D] 

808 
by (auto intro!: isCont_divide) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

809 
have *: "b\<^sup>2 / (2 * measure lborel {a..b})  a\<^sup>2 / (2 * measure lborel {a..b}) = 
50419  810 
(b*b  a * a) / (2 * (b  a))" 
811 
using `a < b` 

812 
by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
50419
diff
changeset

813 
show "b\<^sup>2 / (2 * measure lborel {a..b})  a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" 
50419  814 
using `a < b` 
815 
unfolding * square_diff_square_factored by (auto simp: field_simps) 

816 
qed (insert `a < b`, simp) 

817 
finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" . 

818 
qed auto 

819 

57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

820 
lemma (in prob_space) uniform_distributed_variance: 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

821 
fixes a b :: real 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

822 
assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

823 
shows "variance X = (b  a)\<^sup>2 / 12" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

824 
proof (subst distributed_variance) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

825 
have [arith]: "a < b" using uniform_distributed_bounds[OF D] . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

826 
let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

827 
have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a  ?\<mu> .. b  ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

828 
by (intro integral_cong) (auto split: split_indicator) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

829 
also have "\<dots> = (b  a)\<^sup>2 / 12" 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

830 
by (simp add: integral_power measure_lebesgue_Icc uniform_distributed_expectation[OF D]) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

831 
(simp add: eval_nat_numeral field_simps ) 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

832 
finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b  a)\<^sup>2 / 12" . 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

833 
qed fact 
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
56996
diff
changeset

834 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

835 
subsection {* Normal distribution *} 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

836 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

837 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

838 
definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

839 
"normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp ((x  \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

840 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

841 
abbreviation std_normal_density :: "real \<Rightarrow> real" where 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

842 
"std_normal_density \<equiv> normal_density 0 1" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

843 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

844 
lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp ( x\<^sup>2 / 2)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

845 
unfolding normal_density_def by simp 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

846 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

847 
lemma normal_density_nonneg: "0 \<le> normal_density \<mu> \<sigma> x" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

848 
by (auto simp: normal_density_def) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

849 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

850 
lemma normal_density_pos: "0 < \<sigma> \<Longrightarrow> 0 < normal_density \<mu> \<sigma> x" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

851 
by (auto simp: normal_density_def) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

852 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

853 
lemma borel_measurable_normal_density[measurable]: "normal_density \<mu> \<sigma> \<in> borel_measurable borel" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

854 
by (auto simp: normal_density_def[abs_def]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

855 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

856 
lemma gaussian_moment_0: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

857 
"has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R exp ( x\<^sup>2)) (sqrt pi / 2)" 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

858 
proof  
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

859 
let ?pI = "\<lambda>f. (\<integral>\<^sup>+s. f (s::real) * indicator {0..} s \<partial>lborel)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

860 
let ?gauss = "\<lambda>x. exp ( x\<^sup>2)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

861 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

862 
let ?I = "indicator {0<..} :: real \<Rightarrow> real" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

863 
let ?ff= "\<lambda>x s. x * exp ( x\<^sup>2 * (1 + s\<^sup>2)) :: real" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

864 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

865 
have *: "?pI ?gauss = (\<integral>\<^sup>+x. ?gauss x * ?I x \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

866 
by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

867 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

868 
have "?pI ?gauss * ?pI ?gauss = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

869 
by (auto simp: nn_integral_nonneg nn_integral_cmult[symmetric] nn_integral_multc[symmetric] * 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

870 
intro!: nn_integral_cong split: split_indicator) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

871 
also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

872 
proof (rule nn_integral_cong, cases) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

873 
fix x :: real assume "x \<noteq> 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

874 
then show "(\<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel) = (\<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

875 
by (subst nn_integral_real_affine[where t="0" and c="x"]) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

876 
(auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

877 
intro!: nn_integral_cong split: split_indicator) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

878 
qed simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

879 
also have "... = \<integral>\<^sup>+s. \<integral>\<^sup>+x. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

880 
by (rule lborel_pair.Fubini'[symmetric]) auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

881 
also have "... = ?pI (\<lambda>s. ?pI (\<lambda>x. ?ff x s))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

882 
by (rule nn_integral_cong_AE) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

883 
(auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm) 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

884 
also have "\<dots> = ?pI (\<lambda>s. ereal (1 / (2 * (1 + s\<^sup>2))))" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

885 
proof (intro nn_integral_cong ereal_right_mult_cong) 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

886 
fix s :: real show "?pI (\<lambda>x. ?ff x s) = ereal (1 / (2 * (1 + s\<^sup>2)))" 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

887 
proof (subst nn_integral_FTC_atLeast) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

888 
have "((\<lambda>a.  (exp ( (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) > ( (0 / (2 + 2 * s\<^sup>2)))) at_top" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

889 
apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top]) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

890 
apply (subst mult_commute) 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

891 
apply (auto intro!: filterlim_tendsto_pos_mult_at_top 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

892 
filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

893 
simp: add_pos_nonneg power2_eq_square add_nonneg_eq_0_iff) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

894 
done 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

895 
then show "((\<lambda>a.  (exp ( a\<^sup>2  s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) > 0) at_top" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

896 
by (simp add: field_simps) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

897 
qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

898 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

899 
also have "... = ereal (pi / 4)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

900 
proof (subst nn_integral_FTC_atLeast) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

901 
show "((\<lambda>a. arctan a / 2) > (pi / 2) / 2 ) at_top" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

902 
by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

903 
qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

904 
finally have "?pI ?gauss^2 = pi / 4" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

905 
by (simp add: power2_eq_square) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

906 
then have "?pI ?gauss = sqrt (pi / 4)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

907 
using power_eq_iff_eq_base[of 2 "real (?pI ?gauss)" "sqrt (pi / 4)"] 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

908 
nn_integral_nonneg[of lborel "\<lambda>x. ?gauss x * indicator {0..} x"] 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

909 
by (cases "?pI ?gauss") auto 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

910 
also have "?pI ?gauss = (\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R exp ( x\<^sup>2) \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

911 
by (intro nn_integral_cong) (simp split: split_indicator) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

912 
also have "sqrt (pi / 4) = sqrt pi / 2" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

913 
by (simp add: real_sqrt_divide) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

914 
finally show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

915 
by (rule has_bochner_integral_nn_integral[rotated 2]) auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

916 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

917 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

918 
lemma gaussian_moment_1: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

919 
"has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp ( x\<^sup>2) * x)) (1 / 2)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

920 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

921 
have "(\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R (exp ( x\<^sup>2) * x) \<partial>lborel) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

922 
(\<integral>\<^sup>+x. ereal (x * exp ( x\<^sup>2)) * indicator {0..} x \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

923 
by (intro nn_integral_cong) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

924 
(auto simp: ac_simps times_ereal.simps(1)[symmetric] ereal_indicator simp del: times_ereal.simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

925 
also have "\<dots> = ereal (0  ( exp ( 0\<^sup>2) / 2))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

926 
proof (rule nn_integral_FTC_atLeast) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

927 
have "((\<lambda>x::real.  exp ( x\<^sup>2) / 2) >  0 / 2) at_top" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

928 
by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot] 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

929 
filterlim_compose[OF filterlim_uminus_at_bot_at_top] 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

930 
filterlim_pow_at_top filterlim_ident) 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

931 
auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

932 
then show "((\<lambda>a::real.  exp ( a\<^sup>2) / 2) > 0) at_top" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

933 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

934 
qed (auto intro!: derivative_eq_intros) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

935 
also have "\<dots> = ereal (1 / 2)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

936 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

937 
finally show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

938 
by (rule has_bochner_integral_nn_integral[rotated 2]) (auto split: split_indicator) 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

939 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

940 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

941 
lemma 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

942 
fixes k :: nat 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

943 
shows gaussian_moment_even_pos: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

944 
"has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (x\<^sup>2)*x^(2 * k))) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

945 
((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" (is "?even") 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

946 
and gaussian_moment_odd_pos: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

947 
"has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" (is "?odd") 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

948 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

949 
let ?M = "\<lambda>k x. exp ( x\<^sup>2) * x^k :: real" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

950 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

951 
{ fix k I assume Mk: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M k x) I" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

952 
have "2 \<noteq> (0::real)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

953 
by linarith 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

954 
let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

955 
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) > 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

956 
(k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)  0 / 2) at_top" (is ?tendsto) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

957 
proof (intro tendsto_intros `2 \<noteq> 0` tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

958 
show "(?M (k + 1) > 0) at_top" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

959 
proof cases 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

960 
assume "even k" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

961 
have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) > 0 * 0) at_top" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

962 
by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

963 
filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

964 
auto 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

965 
also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

966 
using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

967 
finally show ?thesis by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

968 
next 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

969 
assume "odd k" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

970 
have "((\<lambda>x. ((x\<^sup>2)^((k  1) div 2 + 1) / exp (x\<^sup>2)) :: real) > 0) at_top" 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

971 
by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

972 
filterlim_ident filterlim_pow_at_top) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57254
diff
changeset

973 
auto 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

974 
also have "(\<lambda>x. ((x\<^sup>2)^((k  1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

975 
using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

976 
finally show ?thesis by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

977 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

978 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

979 
also have "?tendsto \<longleftrightarrow> ((?f > (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)  0 / 2) at_top)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

980 
proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

981 
fix b :: real assume b: "0 \<le> b" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

982 
have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp ( x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

983 
unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

984 
also have "\<dots> = exp ( b\<^sup>2) * b ^ (Suc k)  exp ( 0\<^sup>2) * 0 ^ (Suc k)  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

985 
(\<integral>x. indicator {0..b} x *\<^sub>R ( 2 * x * exp ( x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

986 
by (rule integral_by_parts') 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

987 
(auto intro!: derivative_eq_intros b 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

988 
simp: real_of_nat_def[symmetric] diff_Suc real_of_nat_Suc field_simps split: nat.split) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

989 
also have "(\<integral>x. indicator {0..b} x *\<^sub>R ( 2 * x * exp ( x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

990 
(\<integral>x. indicator {0..b} x *\<^sub>R ( 2 * (exp ( x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

991 
by (intro integral_cong) auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

992 
finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

993 
exp ( b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

994 
apply (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric]) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

995 
apply (subst integral_mult_right_zero[symmetric]) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

996 
apply (intro integral_cong) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

997 
apply simp_all 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

998 
done 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

999 
then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel)  exp ( b\<^sup>2) * b ^ (k + 1) / 2 = ?f b" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1000 
by (simp add: field_simps atLeastAtMost_def indicator_inter_arith) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1001 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1002 
finally have int_M_at_top: "((?f > (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)) at_top)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1003 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1004 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1005 
have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1006 
proof (rule has_bochner_integral_monotone_convergence_at_top) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1007 
fix y :: real 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1008 
have *: "(\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..y} x::real) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1009 
(\<lambda>x. indicator {0..y} x *\<^sub>R ?M (k + 2) x)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1010 
by rule (simp split: split_indicator) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1011 
show "integrable lborel (\<lambda>x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1012 
unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1013 
show "((?f > (k + 1) / 2 * I) at_top)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1014 
using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1015 
qed (auto split: split_indicator) } 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1016 
note step = this 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1017 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1018 
show ?even 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1019 
proof (induct k) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1020 
case (Suc k) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1021 
note step[OF this] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1022 
also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * (real (fact (2 * k)) / real (2 ^ (2 * k) * fact k)))) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1023 
sqrt pi / 2 * (real (fact (2 * Suc k)) / real (2 ^ (2 * Suc k) * fact (Suc k)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1024 
by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1025 
finally show ?case 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1026 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1027 
qed (insert gaussian_moment_0, simp) 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1028 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1029 
show ?odd 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1030 
proof (induct k) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1031 
case (Suc k) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1032 
note step[OF this] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1033 
also have "(real (2 * k + 1 + 1) / 2 * (real (fact k) / 2)) = real (fact (Suc k)) / 2" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1034 
by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1035 
finally show ?case 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1036 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1037 
qed (insert gaussian_moment_1, simp) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1038 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1039 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1040 
context 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1041 
fixes k :: nat and \<mu> \<sigma> :: real assumes [arith]: "0 < \<sigma>" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1042 
begin 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1043 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1044 
lemma normal_moment_even: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1045 
"has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x  \<mu>) ^ (2 * k)) (fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1046 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1047 
have eq: "\<And>x::real. x\<^sup>2^k = (x^k)\<^sup>2" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1048 
by (simp add: power_mult[symmetric] ac_simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1049 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1050 
have "has_bochner_integral lborel (\<lambda>x. exp (x\<^sup>2)*x^(2 * k)) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1051 
(sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1052 
using has_bochner_integral_even_function[OF gaussian_moment_even_pos[where k=k]] by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1053 
then have "has_bochner_integral lborel (\<lambda>x. (exp (x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1054 
((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1055 
by (rule has_bochner_integral_mult_left) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1056 
also have "(\<lambda>x. (exp (x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1057 
(\<lambda>x. exp ( ((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2*\<sigma>\<^sup>2)) * ((sqrt 2 * \<sigma>) * x) ^ (2 * k) / sqrt (2 * pi * \<sigma>\<^sup>2))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1058 
by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1059 
real_sqrt_divide power_mult eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1060 
also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1061 
(inverse (sqrt 2 * \<sigma>) * (real (fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * real (fact k)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1062 
by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1063 
power2_eq_square) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1064 
finally show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1065 
unfolding normal_density_def 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1066 
by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1067 
qed 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1068 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1069 
lemma normal_moment_abs_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1070 
"has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x  \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1071 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1072 
have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1073 
by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1074 
from has_bochner_integral_even_function[OF this] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1075 
have "has_bochner_integral lborel (\<lambda>x. exp (x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1076 
by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1077 
then have "has_bochner_integral lborel (\<lambda>x. (exp (x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1078 
(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1079 
by (rule has_bochner_integral_mult_left) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1080 
also have "(\<lambda>x. (exp (x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1081 
(\<lambda>x. exp ( (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1082 
by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1083 
also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1084 
(inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * real (fact k) * sqrt (2 / pi)))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1085 
by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1086 
real_sqrt_mult) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1087 
finally show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1088 
unfolding normal_density_def 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1089 
by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1090 
simp_all 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1091 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1092 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1093 
lemma normal_moment_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1094 
"has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x  \<mu>)^(2 * k + 1)) 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1095 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1096 
have "has_bochner_integral lborel (\<lambda>x. exp ( x\<^sup>2) * x^(2 * k + 1)::real) 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1097 
using gaussian_moment_odd_pos by (rule has_bochner_integral_odd_function) simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1098 
then have "has_bochner_integral lborel (\<lambda>x. (exp (x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi)) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1099 
(0 * (2^k*\<sigma>^(2*k)/sqrt pi))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1100 
by (rule has_bochner_integral_mult_left) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1101 
also have "(\<lambda>x. (exp (x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi)) = 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1102 
(\<lambda>x. exp ( ((sqrt 2 * \<sigma> * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1103 
(sqrt 2 * \<sigma> * x * (sqrt 2 * \<sigma> * x) ^ (2 * k)) / 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1104 
sqrt (2 * pi * \<sigma>\<^sup>2))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1105 
unfolding real_sqrt_mult 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1106 
by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult fun_eq_iff) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1107 
finally show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1108 
unfolding normal_density_def 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1109 
by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1110 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1111 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1112 
lemma integral_normal_moment_even: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1113 
"integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x  \<mu>)^(2 * k)) = fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1114 
using normal_moment_even by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1115 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1116 
lemma integral_normal_moment_abs_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1117 
"integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x  \<mu>\<bar>^(2 * k + 1)) = 2 ^ k * \<sigma> ^ (2 * k + 1) * fact k * sqrt (2 / pi)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1118 
using normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1119 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1120 
lemma integral_normal_moment_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1121 
"integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x  \<mu>)^(2 * k + 1)) = 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1122 
using normal_moment_odd by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1123 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1124 
end 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1125 

57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1126 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1127 
context 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1128 
fixes \<sigma> :: real 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1129 
assumes \<sigma>_pos[arith]: "0 < \<sigma>" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1130 
begin 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1131 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1132 
lemma normal_moment_nz_1: "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) \<mu>" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1133 
proof  
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1134 
note normal_moment_even[OF \<sigma>_pos, of \<mu> 0] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1135 
note normal_moment_odd[OF \<sigma>_pos, of \<mu> 0] has_bochner_integral_mult_left[of \<mu>, OF this] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1136 
note has_bochner_integral_add[OF this] 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1137 
then show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1138 
by (simp add: power2_eq_square field_simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1139 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1140 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1141 
lemma integral_normal_moment_nz_1: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1142 
"integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) = \<mu>" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1143 
using normal_moment_nz_1 by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1144 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1145 
lemma integrable_normal_moment_nz_1: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1146 
using normal_moment_nz_1 by rule 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1147 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1148 
lemma integrable_normal_moment: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x  \<mu>)^k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1149 
proof cases 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1150 
assume "even k" then show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1151 
using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1152 
next 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1153 
assume "odd k" then show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1154 
using integrable.intros[OF normal_moment_odd] by (auto simp add: odd_Suc_mult_two_ex) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1155 
qed 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1156 

57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1157 
lemma integrable_normal_moment_abs: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x  \<mu>\<bar>^k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1158 
proof cases 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1159 
assume "even k" then show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1160 
using integrable.intros[OF normal_moment_even] by (auto simp add: even_mult_two_ex power_even_abs) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1161 
next 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1162 
assume "odd k" then show ?thesis 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1163 
using integrable.intros[OF normal_moment_abs_odd] by (auto simp add: odd_Suc_mult_two_ex) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1164 
qed 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1165 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1166 
lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \<mu> \<sigma>)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1167 
using integrable_normal_moment[of \<mu> 0] by simp 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1168 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1169 
lemma integral_normal_density[simp]: "(\<integral>x. normal_density \<mu> \<sigma> x \<partial>lborel) = 1" 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1170 
using integral_normal_moment_even[of \<sigma> \<mu> 0] by simp 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1171 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1172 
lemma prob_space_normal_density: 
57254
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1173 
"prob_space (density lborel (normal_density \<mu> \<sigma>))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1174 
proof qed (simp add: emeasure_density nn_integral_eq_integral normal_density_nonneg) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1175 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1176 
end 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1177 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1178 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1179 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1180 
context 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1181 
fixes k :: nat 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1182 
begin 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1183 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1184 
lemma std_normal_moment_even: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1185 
"has_bochner_integral lborel (\<lambda>x. std_normal_density x * x ^ (2 * k)) (fact (2 * k) / (2^k * fact k))" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1186 
using normal_moment_even[of 1 0 k] by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1187 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1188 
lemma std_normal_moment_abs_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1189 
"has_bochner_integral lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) (sqrt (2/pi) * 2^k * fact k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1190 
using normal_moment_abs_odd[of 1 0 k] by (simp add: ac_simps) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1191 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1192 
lemma std_normal_moment_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1193 
"has_bochner_integral lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1194 
using normal_moment_odd[of 1 0 k] by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1195 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1196 
lemma integral_std_normal_moment_even: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1197 
"integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2*k)) = fact (2 * k) / (2^k * fact k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1198 
using std_normal_moment_even by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1199 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1200 
lemma integral_std_normal_moment_abs_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1201 
"integral\<^sup>L lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2^k * fact k" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1202 
using std_normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1203 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1204 
lemma integral_std_normal_moment_odd: 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1205 
"integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) = 0" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1206 
using std_normal_moment_odd by (rule has_bochner_integral_integral_eq) 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1207 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1208 
lemma integrable_std_normal_moment_abs: "integrable lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1209 
using integrable_normal_moment_abs[of 1 0 k] by simp 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1210 

d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1211 
lemma integrable_std_normal_moment: "integrable lborel (\<lambda>x. std_normal_density x * x^k)" 
d3d91422f408
lemmas about the moments of the normal distribution
hoelzl
parents:
57252
diff
changeset

1212 
using integrable_normal_moment[of 1 0 k] by simp 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1213 

50419  1214 
end 
57252
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1215 

19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1216 
lemma (in prob_space) normal_density_affine: 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1217 
assumes X: "distributed M lborel X (normal_density \<mu> \<sigma>)" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1218 
assumes [simp, arith]: "0 < \<sigma>" "\<alpha> \<noteq> 0" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1219 
shows "distributed M lborel (\<lambda>x. \<beta> + \<alpha> * X x) (normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>))" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1220 
proof  
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1221 
have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) = 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1222 
normal_density \<mu> \<sigma> x" 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1223 
by (simp add: normal_density_def real_sqrt_mult field_simps) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1224 
(simp add: power2_eq_square field_simps) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1225 
show ?thesis 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1226 
by (rule distributed_affineI[OF _ `\<alpha> \<noteq> 0`, where t=\<beta>]) (simp_all add: eq X) 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset

1227 
qed 
19b7ace1c5da
properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57235
diff
changeset
