src/HOL/Probability/Distributions.thy
author haftmann
Sat, 28 Jun 2014 09:16:42 +0200
changeset 57418 6ab1c7cb0b8d
parent 57275 0ddb5b755cdc
child 57447 87429bdecad5
permissions -rw-r--r--
fact consolidation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     8
theory Distributions
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
     9
  imports Convolution Information
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    10
begin
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    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))"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 57275
diff changeset
   129
    by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum.If_cases)
57235
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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   348
subsection {* Exponential distribution *}
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   359
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   360
lemma (in prob_space) exponential_distributed_params:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   361
  assumes D: "distributed M lborel X (exponential_density l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   362
  shows "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   363
proof (cases l "0 :: real" rule: linorder_cases)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   364
  assume "l < 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   365
  have "emeasure lborel {0 <.. 1::real} \<le>
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   366
    emeasure lborel {x :: real \<in> space lborel. 0 < x}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   367
    by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   368
  also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   369
  proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   370
    have "AE x in lborel. 0 \<le> exponential_density l x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   371
      using assms by (auto simp: distributed_real_AE)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   372
    then have "AE x in lborel. x \<le> (0::real)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   373
      apply eventually_elim 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   374
      using `l < 0`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   375
      apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   376
      done
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   377
    then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   378
      by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   379
  qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   380
  finally show "0 < l" by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   381
next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   382
  assume "l = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   383
  then have [simp]: "\<And>x. ereal (exponential_density l x) = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   384
    by (simp add: exponential_density_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   385
  interpret X: prob_space "distr M lborel X"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   386
    using distributed_measurable[OF D] by (rule prob_space_distr)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   387
  from X.emeasure_space_1
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   388
  show "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   389
    by (simp add: emeasure_density distributed_distr_eq_density[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   390
qed assumption
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   394
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   395
lemma (in prob_space) exponential_distributedD_le:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   396
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   400
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   401
lemma (in prob_space) exponential_distributedD_gt:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   402
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   406
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   407
lemma (in prob_space) exponential_distributed_memoryless:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   408
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   409
  shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   410
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   412
    using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   413
  also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   414
    using a t by (simp add: exponential_distributedD_gt[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   415
  also have "\<dots> = exp (- t * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   416
    using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   417
  finally show ?thesis
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   418
    using t by (simp add: exponential_distributedD_gt[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   419
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   420
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   421
lemma exponential_distributedI:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   422
  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   423
    and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   429
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   430
lemma (in prob_space) exponential_distributed_iff:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   431
  "distributed M lborel X (exponential_density l) \<longleftrightarrow>
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   434
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   435
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   651
subsection {* Uniform distribution *}
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   652
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   653
lemma uniform_distrI:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   654
  assumes X: "X \<in> measurable M M'"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   655
    and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   657
  shows "distr M M' X = uniform_measure M' A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   658
  unfolding uniform_measure_def
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   659
proof (intro measure_eqI)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   660
  let ?f = "\<lambda>x. indicator A x / emeasure M' A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   661
  fix B assume B: "B \<in> sets (distr M M' X)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   662
  with X have "emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   663
    by (simp add: distr[of B] measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   664
  also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   667
    using A B
56996
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   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
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   670
    by (rule nn_integral_cong) (auto split: split_indicator)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   671
  finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   672
    using A B X by (auto simp add: emeasure_distr emeasure_density)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   673
qed simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   674
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   675
lemma uniform_distrI_borel:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   676
  fixes A :: "real set"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   677
  assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   678
    and [measurable]: "A \<in> sets borel"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   679
  assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   680
  shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   681
proof (rule distributedI_borel_atMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   682
  let ?f = "\<lambda>x. 1 / r * indicator A x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   683
  fix a
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   684
  have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   685
    using A by (intro emeasure_mono) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   686
  also have "\<dots> < \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   687
    using A by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   688
  finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   689
    by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   690
  from emeasure_eq_ereal_measure[OF this]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   691
  have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ereal (measure lborel (A \<inter> {..a}) / r)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   692
    using A by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   693
  then show "emeasure M {x\<in>space M. X x \<le> a} = ereal (measure lborel (A \<inter> {..a}) / r)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   694
    using distr by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   698
    by (auto intro!: nn_integral_cong split: split_indicator)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   699
  also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   700
    using `A \<in> sets borel`
56996
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   701
    by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   702
  also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   707
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   708
lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   709
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   710
  assumes X: "X \<in> borel_measurable M" and "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   712
  shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   713
proof (rule uniform_distrI_borel)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   714
  fix t
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   715
  have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   716
    by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   717
  then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b - a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   718
  proof (elim disjE conjE)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   719
    assume "t < a" 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   720
    then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   721
      using X by (auto intro!: emeasure_mono measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   722
    also have "\<dots> = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   723
      using distr[of a] `a < b` by (simp add: emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   724
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   725
      by (simp add: antisym measure_nonneg emeasure_le_0_iff)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   726
    with `t < a` show ?thesis by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   727
  next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   728
    assume bnds: "a \<le> t" "t \<le> b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   729
    have "{a..b} \<inter> {..t} = {a..t}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   730
      using bnds by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   731
    then show ?thesis using `a \<le> t` `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   732
      using distr[OF bnds] by (simp add: emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   733
  next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   734
    assume "b < t" 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   735
    have "1 = emeasure M {x\<in>space M. X x \<le> b}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   736
      using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   737
    also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   738
      using X `b < t` by (auto intro!: emeasure_mono measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   739
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 1"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   740
       by (simp add: antisym emeasure_eq_measure one_ereal_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   741
    with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   742
  qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   743
qed (insert X `a < b`, auto)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   744
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   745
lemma (in prob_space) uniform_distributed_measure:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   746
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   747
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   748
  assumes " a \<le> t" "t \<le> b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   749
  shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   750
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   751
  have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   752
    using distributed_measurable[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   755
    using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   756
    unfolding distributed_distr_eq_density[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   757
    by (subst emeasure_density)
56996
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   758
       (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   759
  also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   760
    using `a \<le> t` `t \<le> b`
56996
891e992e510f renamed positive_integral to nn_integral
hoelzl
parents: 56993
diff changeset
   761
    by (subst nn_integral_cmult_indicator) auto
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   762
  finally show ?thesis
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   763
    by (simp add: measure_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   764
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   765
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   766
lemma (in prob_space) uniform_distributed_bounds:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   767
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   768
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   769
  shows "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   770
proof (rule ccontr)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   771
  assume "\<not> a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   772
  then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   773
  with uniform_distributed_params[OF D] show False 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   774
    by (auto simp: measure_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   775
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   776
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   777
lemma (in prob_space) uniform_distributed_iff:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   778
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   779
  shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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)))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   781
  using
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   782
    uniform_distributed_bounds[of X a b]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   783
    uniform_distributed_measure[of X a b]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   784
    distributed_measurable[of M lborel X]
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   785
  by (auto intro!: uniform_distrI_borel_atLeastAtMost 
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   786
              simp: one_ereal_def emeasure_eq_measure
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   787
              simp del: measure_lborel)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   788
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   789
lemma (in prob_space) uniform_distributed_expectation:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   790
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   791
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   792
  shows "expectation X = (a + b) / 2"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   793
proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   794
  have "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   795
    using uniform_distributed_bounds[OF D] .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   796
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   797
  have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   798
    (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   799
    by (intro integral_cong) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   800
  also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   801
  proof (subst integral_FTC_atLeastAtMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   802
    fix x
53077
a1b3784f8129 more symbols;
wenzelm
parents: 53015
diff changeset
   803
    show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   806
    show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   807
      using uniform_distributed_params[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   810
      (b*b - a * a) / (2 * (b - a))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   811
      using `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   814
      using `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   815
      unfolding * square_diff_square_factored by (auto simp: field_simps)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   816
  qed (insert `a < b`, simp)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   817
  finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   818
qed auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   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
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
  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
  1228
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1229
lemma (in prob_space) normal_standard_normal_convert:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1230
  assumes pos_var[simp, arith]: "0 < \<sigma>"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1231
  shows "distributed M lborel X (normal_density  \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1232
proof auto
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1233
  assume "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1234
  then have "distributed M lborel (\<lambda>x. -\<mu> / \<sigma> + (1/\<sigma>) * X x) (\<lambda>x. ereal (normal_density (-\<mu> / \<sigma> + (1/\<sigma>)* \<mu>) (\<bar>1/\<sigma>\<bar> * \<sigma>) x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1235
    by(rule normal_density_affine) auto
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1236
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1237
  then show "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1238
    by (simp add: diff_divide_distrib[symmetric] field_simps)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1239
next
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1240
  assume *: "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1241
  have "distributed M lborel (\<lambda>x. \<mu> + \<sigma> * ((X x - \<mu>) / \<sigma>)) (\<lambda>x. ereal (normal_density \<mu> \<bar>\<sigma>\<bar> x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1242
    using normal_density_affine[OF *, of \<sigma> \<mu>] by simp  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1243
  then show "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))" by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1244
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1245
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1246
lemma conv_normal_density_zero_mean:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1247
  assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1248
  shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (normal_density 0 \<sigma> (x - y) * normal_density 0 \<tau> y) \<partial>lborel) =
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1249
    normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))"  (is "?LHS = ?RHS")
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1250
proof -
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1251
  def \<sigma>' \<equiv> "\<sigma>\<^sup>2" and \<tau>' \<equiv> "\<tau>\<^sup>2"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1252
  then have [simp, arith]: "0 < \<sigma>'" "0 < \<tau>'"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1253
    by simp_all
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1254
  let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))"  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1255
  have sqrt: "(sqrt (2 * pi * (\<sigma>' + \<tau>')) * sqrt (2 * pi * (\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))) = 
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1256
    (sqrt (2 * pi * \<sigma>') * sqrt (2 * pi * \<tau>'))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1257
    by (subst power_eq_iff_eq_base[symmetric, where n=2])
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1258
       (simp_all add: real_sqrt_mult[symmetric] power2_eq_square)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1259
  have "?LHS =
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1260
    (\<lambda>x. \<integral>\<^sup>+y. ereal((normal_density 0 (sqrt (\<sigma>' + \<tau>')) x) * normal_density (\<tau>' * x / (\<sigma>' + \<tau>')) ?\<sigma> y) \<partial>lborel)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1261
    apply (intro ext nn_integral_cong)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1262
    apply (simp add: normal_density_def \<sigma>'_def[symmetric] \<tau>'_def[symmetric] sqrt mult_exp_exp)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1263
    apply (simp add: divide_simps power2_eq_square)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1264
    apply (simp add: field_simps)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1265
    done
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1266
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1267
  also have "... =
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1268
    (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x) * \<integral>\<^sup>+y. ereal( normal_density (\<tau>\<^sup>2* x / (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) ?\<sigma> y) \<partial>lborel)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1269
    by (subst nn_integral_cmult[symmetric]) (auto simp: \<sigma>'_def \<tau>'_def normal_density_def)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1270
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1271
  also have "... = (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1272
    by (subst nn_integral_eq_integral) (auto simp: normal_density_nonneg)
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1273
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1274
  finally show ?thesis by fast
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1275
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1276
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1277
lemma conv_std_normal_density:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1278
  "(\<lambda>x. \<integral>\<^sup>+y. ereal (std_normal_density (x - y) * std_normal_density y) \<partial>lborel) =
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1279
  (normal_density 0 (sqrt 2))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1280
  by (subst conv_normal_density_zero_mean) simp_all
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1281
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1282
lemma (in prob_space) sum_indep_normal:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1283
  assumes indep: "indep_var borel X borel Y"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1284
  assumes pos_var[arith]: "0 < \<sigma>" "0 < \<tau>"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1285
  assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1286
  assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1287
  shows "distributed M lborel (\<lambda>x. X x + Y x) (normal_density (\<mu> + \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1288
proof -
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1289
  have ind[simp]: "indep_var borel (\<lambda>x. - \<mu> + X x) borel (\<lambda>x. - \<nu> + Y x)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1290
  proof -
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1291
    have "indep_var borel ( (\<lambda>x. -\<mu> + x) o X) borel ((\<lambda>x. - \<nu> + x) o Y)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1292
      by (auto intro!: indep_var_compose assms) 
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1293
    then show ?thesis by (simp add: o_def)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1294
  qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1295
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1296
  have "distributed M lborel (\<lambda>x. -\<mu> + 1 * X x) (normal_density (- \<mu> + 1 * \<mu>) (\<bar>1\<bar> * \<sigma>))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1297
    by(rule normal_density_affine[OF normalX pos_var(1), of 1 "-\<mu>"]) simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1298
  then have 1[simp]: "distributed M lborel (\<lambda>x. - \<mu> +  X x) (normal_density 0 \<sigma>)" by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1299
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1300
  have "distributed M lborel (\<lambda>x. -\<nu> + 1 * Y x) (normal_density (- \<nu> + 1 * \<nu>) (\<bar>1\<bar> * \<tau>))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1301
    by(rule normal_density_affine[OF normalY pos_var(2), of 1 "-\<nu>"]) simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1302
  then have 2[simp]: "distributed M lborel (\<lambda>x. - \<nu> +  Y x) (normal_density 0 \<tau>)" by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1303
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1304
  have *: "distributed M lborel (\<lambda>x. (- \<mu> + X x) + (- \<nu> + Y x)) (\<lambda>x. ereal (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1305
    using distributed_convolution[OF ind 1 2] conv_normal_density_zero_mean[OF pos_var] by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1306
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1307
  have "distributed M lborel (\<lambda>x. \<mu> + \<nu> + 1 * (- \<mu> + X x + (- \<nu> + Y x)))
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1308
        (\<lambda>x. ereal (normal_density (\<mu> + \<nu> + 1 * 0) (\<bar>1\<bar> * sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1309
    by (rule normal_density_affine[OF *, of 1 "\<mu> + \<nu>"]) (auto simp: add_pos_pos)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1310
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1311
  then show ?thesis by auto
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1312
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1313
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1314
lemma (in prob_space) diff_indep_normal:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1315
  assumes indep[simp]: "indep_var borel X borel Y"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1316
  assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1317
  assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1318
  assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1319
  shows "distributed M lborel (\<lambda>x. X x - Y x) (normal_density (\<mu> - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1320
proof -
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1321
  have "distributed M lborel (\<lambda>x. 0 + - 1 * Y x) (\<lambda>x. ereal (normal_density (0 + - 1 * \<nu>) (\<bar>- 1\<bar> * \<tau>) x))" 
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1322
    by(rule normal_density_affine, auto)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1323
  then have [simp]:"distributed M lborel (\<lambda>x. - Y x) (\<lambda>x. ereal (normal_density (- \<nu>) \<tau> x))" by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1324
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1325
  have "distributed M lborel (\<lambda>x. X x + (- Y x)) (normal_density (\<mu> + - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1326
    apply (rule sum_indep_normal)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1327
    apply (rule indep_var_compose[unfolded comp_def, of borel _ borel _ "\<lambda>x. x" _ "\<lambda>x. - x"])
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1328
    apply simp_all
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1329
    done
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1330
  then show ?thesis by simp
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1331
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1332
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1333
lemma (in prob_space) setsum_indep_normal:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1334
  assumes "finite I" "I \<noteq> {}" "indep_vars (\<lambda>i. borel) X I"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1335
  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 < \<sigma> i"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1336
  assumes normal: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (normal_density (\<mu> i) (\<sigma> i))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1337
  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (normal_density (\<Sum>i\<in>I. \<mu> i) (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2)))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1338
  using assms 
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1339
proof (induct I rule: finite_ne_induct)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1340
  case (singleton i) then show ?case by (simp add : abs_of_pos)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1341
next
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1342
  case (insert i I)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1343
    then have 1: "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in>I. X i x)) 
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1344
                (normal_density (\<mu> i  + setsum \<mu> I)  (sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1345
      apply (intro sum_indep_normal indep_vars_setsum insert real_sqrt_gt_zero)  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1346
      apply (auto intro: indep_vars_subset intro!: setsum_pos)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1347
      apply fastforce
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1348
      done
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1349
    have 2: "(\<lambda>x. (X i x)+ (\<Sum>i\<in>I. X i x)) = (\<lambda>x. (\<Sum>j\<in>insert i I. X j x))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1350
          "\<mu> i + setsum \<mu> I = setsum \<mu> (insert i I)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1351
      using insert by auto
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1352
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1353
    have 3: "(sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)) = (sqrt (\<Sum>i\<in>insert i I. (\<sigma> i)\<^sup>2))"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1354
      using insert by (simp add: setsum_nonneg)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1355
  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1356
    show ?case using 1 2 3 by simp  
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1357
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1358
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1359
lemma (in prob_space) standard_normal_distributed_expectation:
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1360
  assumes D: "distributed M lborel X std_normal_density"
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1361
  shows "expectation X = 0"
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1362
  using integral_std_normal_moment_odd[of 0]
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1363
  by (auto simp: distributed_integral[OF D, of "\<lambda>x. x", symmetric])
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1364
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1365
lemma (in prob_space) normal_distributed_expectation:
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1366
  assumes \<sigma>[arith]: "0 < \<sigma>"
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1367
  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1368
  shows "expectation X = \<mu>"
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1369
  using integral_normal_moment_nz_1[OF \<sigma>, of \<mu>] distributed_integral[OF D, of "\<lambda>x. x", symmetric]
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1370
  by (auto simp: field_simps)
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1371
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1372
lemma (in prob_space) normal_distributed_variance:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1373
  fixes a b :: real
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1374
  assumes [simp, arith]: "0 < \<sigma>"
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1375
  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1376
  shows "variance X = \<sigma>\<^sup>2"
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1377
  using integral_normal_moment_even[of \<sigma> \<mu> 1]
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1378
  by (subst distributed_integral[OF D, symmetric])
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1379
     (simp_all add: eval_nat_numeral normal_distributed_expectation[OF assms])
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1380
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1381
lemma (in prob_space) standard_normal_distributed_variance:
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1382
  "distributed M lborel X std_normal_density \<Longrightarrow> variance X = 1"
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1383
  using normal_distributed_variance[of 1 X 0] by simp
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1384
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1385
lemma (in information_space) entropy_normal_density:
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1386
  assumes [arith]: "0 < \<sigma>"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1387
  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1388
  shows "entropy b lborel X = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1389
proof -
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1390
  have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1391
    using D by (rule entropy_distr)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1392
  also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1393
    by (intro arg_cong[where f="uminus"] integral_cong)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1394
       (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1395
  also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1396
    by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1397
  also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1398
    by (simp del: minus_add_distrib)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1399
  also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
57254
d3d91422f408 lemmas about the moments of the normal distribution
hoelzl
parents: 57252
diff changeset
  1400
    using integral_normal_moment_even[of \<sigma> \<mu> 1] by (simp add: integrable_normal_moment fact_numeral)
57252
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1401
  also have "\<dots> = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1402
    by (simp add: log_def field_simps ln_mult)
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1403
  finally show ?thesis .
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1404
qed
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1405
19b7ace1c5da properties of normal distributed random variables (by Sudeep Kanav)
hoelzl
parents: 57235
diff changeset
  1406
end