src/HOL/Probability/Distributions.thy
author hoelzl
Thu Jun 12 15:47:36 2014 +0200 (2014-06-12)
changeset 57235 b0b9a10e4bf4
parent 56996 891e992e510f
child 57252 19b7ace1c5da
permissions -rw-r--r--
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl@57235
     1
(*  Title:      HOL/Probability/Distributions.thy
hoelzl@57235
     2
    Author:     Sudeep Kanav, TU München
hoelzl@57235
     3
    Author:     Johannes Hölzl, TU München *)
hoelzl@57235
     4
hoelzl@57235
     5
header {* Properties of Various Distributions *}
hoelzl@57235
     6
hoelzl@50419
     7
theory Distributions
hoelzl@57235
     8
  imports Probability_Measure Convolution
hoelzl@50419
     9
begin
hoelzl@50419
    10
hoelzl@57235
    11
lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)"
hoelzl@57235
    12
  by (auto simp: measure_def)
hoelzl@57235
    13
hoelzl@57235
    14
lemma integral_power:
hoelzl@57235
    15
  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
hoelzl@57235
    16
proof (subst integral_FTC_atLeastAtMost)
hoelzl@57235
    17
  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
hoelzl@57235
    18
    by (intro derivative_eq_intros) auto
hoelzl@57235
    19
qed (auto simp: field_simps)
hoelzl@57235
    20
hoelzl@57235
    21
lemma has_bochner_integral_nn_integral:
hoelzl@57235
    22
  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
hoelzl@57235
    23
  assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
hoelzl@57235
    24
  shows "has_bochner_integral M f x"
hoelzl@57235
    25
  unfolding has_bochner_integral_iff
hoelzl@57235
    26
proof
hoelzl@57235
    27
  show "integrable M f"
hoelzl@57235
    28
    using assms by (rule integrableI_nn_integral_finite)
hoelzl@57235
    29
qed (auto simp: assms integral_eq_nn_integral)
hoelzl@57235
    30
hoelzl@57235
    31
lemma (in prob_space) distributed_AE2:
hoelzl@57235
    32
  assumes [measurable]: "distributed M N X f" "Measurable.pred N P"
hoelzl@57235
    33
  shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)"
hoelzl@57235
    34
proof -
hoelzl@57235
    35
  have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)"
hoelzl@57235
    36
    by (simp add: AE_distr_iff)
hoelzl@57235
    37
  also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)"
hoelzl@57235
    38
    unfolding distributed_distr_eq_density[OF assms(1)] ..
hoelzl@57235
    39
  also have "\<dots> \<longleftrightarrow>  (AE x in N. 0 < f x \<longrightarrow> P x)"
hoelzl@57235
    40
    by (rule AE_density) simp
hoelzl@57235
    41
  finally show ?thesis .
hoelzl@57235
    42
qed
hoelzl@57235
    43
hoelzl@57235
    44
subsection {* Erlang *}
hoelzl@57235
    45
hoelzl@57235
    46
lemma nn_intergal_power_times_exp_Icc:
hoelzl@57235
    47
  assumes [arith]: "0 \<le> a"
hoelzl@57235
    48
  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) =
hoelzl@57235
    49
    (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _")
hoelzl@57235
    50
proof -
hoelzl@57235
    51
  let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
hoelzl@57235
    52
  let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
hoelzl@57235
    53
hoelzl@57235
    54
  have "?I * (inverse (fact k)) = 
hoelzl@57235
    55
      (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
hoelzl@57235
    56
    by (intro nn_integral_multc[symmetric]) auto
hoelzl@57235
    57
  also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
hoelzl@57235
    58
    by (intro nn_integral_cong) (simp add: field_simps)
hoelzl@57235
    59
  also have "\<dots> = ereal (?F k a) - (?F k 0)"
hoelzl@57235
    60
  proof (rule nn_integral_FTC_atLeastAtMost)
hoelzl@57235
    61
    fix x assume "x \<in> {0..a}"
hoelzl@57235
    62
    show "DERIV (?F k) x :> ?f k x"
hoelzl@57235
    63
    proof(induction k)
hoelzl@57235
    64
      case 0 show ?case by (auto intro!: derivative_eq_intros)
hoelzl@57235
    65
    next
hoelzl@57235
    66
      case (Suc k)
hoelzl@57235
    67
      have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
hoelzl@57235
    68
        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
hoelzl@57235
    69
        by (intro DERIV_diff Suc)
hoelzl@57235
    70
           (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
hoelzl@57235
    71
                 simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
hoelzl@57235
    72
      also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
hoelzl@57235
    73
        by simp
hoelzl@57235
    74
      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
hoelzl@57235
    75
        by (auto simp: field_simps simp del: fact_Suc)
hoelzl@57235
    76
           (simp_all add: real_of_nat_Suc field_simps)
hoelzl@57235
    77
      finally show ?case .
hoelzl@57235
    78
    qed
hoelzl@57235
    79
  qed auto
hoelzl@57235
    80
  also have "\<dots> = ereal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))"
hoelzl@57235
    81
    by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum_cases)
hoelzl@57235
    82
  finally show ?thesis
hoelzl@57235
    83
    by (cases "?I") (auto simp: field_simps)
hoelzl@57235
    84
qed
hoelzl@57235
    85
hoelzl@57235
    86
lemma nn_intergal_power_times_exp_Ici:
hoelzl@57235
    87
  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k"
hoelzl@57235
    88
proof (rule LIMSEQ_unique)
hoelzl@57235
    89
  let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
hoelzl@57235
    90
  show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
hoelzl@57235
    91
    apply (intro nn_integral_LIMSEQ)
hoelzl@57235
    92
    apply (auto simp: incseq_def le_fun_def eventually_sequentially
hoelzl@57235
    93
                split: split_indicator intro!: Lim_eventually)
hoelzl@57235
    94
    apply (metis natceiling_le_eq)
hoelzl@57235
    95
    done
hoelzl@57235
    96
hoelzl@57235
    97
  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"
hoelzl@57235
    98
    by (intro tendsto_intros tendsto_power_div_exp_0) simp
hoelzl@57235
    99
  then show "?X ----> fact k"
hoelzl@57235
   100
    by (subst nn_intergal_power_times_exp_Icc)
hoelzl@57235
   101
       (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
hoelzl@57235
   102
qed
hoelzl@57235
   103
hoelzl@57235
   104
definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
hoelzl@57235
   105
  "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)"
hoelzl@57235
   106
hoelzl@57235
   107
definition erlang_CDF ::  "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
hoelzl@57235
   108
  "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))"
hoelzl@57235
   109
hoelzl@57235
   110
lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x"
hoelzl@57235
   111
  by (simp add: erlang_density_def)
hoelzl@57235
   112
hoelzl@57235
   113
lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel"
hoelzl@57235
   114
  by (auto simp add: erlang_density_def[abs_def])
hoelzl@57235
   115
hoelzl@57235
   116
lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)"
hoelzl@57235
   117
  by (auto simp add: erlang_CDF_def mult_less_0_iff)
hoelzl@57235
   118
hoelzl@57235
   119
lemma nn_integral_erlang_density:
hoelzl@57235
   120
  assumes [arith]: "0 < l"
hoelzl@57235
   121
  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
hoelzl@57235
   122
proof cases
hoelzl@57235
   123
  assume [arith]: "0 \<le> a"
hoelzl@57235
   124
  have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
hoelzl@57235
   125
    by (simp add: field_simps split: split_indicator)
hoelzl@57235
   126
  have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
hoelzl@57235
   127
    (\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)"
hoelzl@57235
   128
    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator)
hoelzl@57235
   129
  also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)"
hoelzl@57235
   130
    by (intro nn_integral_cmult) auto
hoelzl@57235
   131
  also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))"
hoelzl@57235
   132
    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
hoelzl@57235
   133
  also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))"
hoelzl@57235
   134
    by (subst nn_intergal_power_times_exp_Icc) auto
hoelzl@57235
   135
  also have "\<dots> = erlang_CDF k l a"
hoelzl@57235
   136
    by (auto simp: erlang_CDF_def)
hoelzl@57235
   137
  finally show ?thesis .
hoelzl@57235
   138
next
hoelzl@57235
   139
  assume "\<not> 0 \<le> a" 
hoelzl@57235
   140
  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))"
hoelzl@57235
   141
    by (intro nn_integral_cong) (auto simp: erlang_density_def)
hoelzl@57235
   142
  ultimately show ?thesis
hoelzl@57235
   143
    by (simp add: erlang_CDF_def)
hoelzl@57235
   144
qed
hoelzl@57235
   145
hoelzl@57235
   146
lemma emeasure_erlang_density: 
hoelzl@57235
   147
  "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a"
hoelzl@57235
   148
  by (simp add: emeasure_density nn_integral_erlang_density)
hoelzl@57235
   149
hoelzl@57235
   150
lemma nn_integral_erlang_ith_moment: 
hoelzl@57235
   151
  fixes k i :: nat and l :: real
hoelzl@57235
   152
  assumes [arith]: "0 < l" 
hoelzl@57235
   153
  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)"
hoelzl@57235
   154
proof -
hoelzl@57235
   155
  have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x"
hoelzl@57235
   156
    by (simp add: field_simps split: split_indicator)
hoelzl@57235
   157
  have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) =
hoelzl@57235
   158
    (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)"
hoelzl@57235
   159
    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator)
hoelzl@57235
   160
  also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)"
hoelzl@57235
   161
    by (intro nn_integral_cmult) auto
hoelzl@57235
   162
  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))"
hoelzl@57235
   163
    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
hoelzl@57235
   164
  also have "\<dots> = fact (k + i) / (fact k * l ^ i)"
hoelzl@57235
   165
    by (subst nn_intergal_power_times_exp_Ici) auto
hoelzl@57235
   166
  finally show ?thesis .
hoelzl@57235
   167
qed
hoelzl@57235
   168
hoelzl@57235
   169
lemma prob_space_erlang_density:
hoelzl@57235
   170
  assumes l[arith]: "0 < l"
hoelzl@57235
   171
  shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D")
hoelzl@57235
   172
proof
hoelzl@57235
   173
  show "emeasure ?D (space ?D) = 1"
hoelzl@57235
   174
    using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density)
hoelzl@57235
   175
qed
hoelzl@57235
   176
hoelzl@57235
   177
lemma (in prob_space) erlang_distributed_le:
hoelzl@57235
   178
  assumes D: "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   179
  assumes [simp, arith]: "0 < l" "0 \<le> a"
hoelzl@57235
   180
  shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a"
hoelzl@57235
   181
proof -
hoelzl@57235
   182
  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
hoelzl@57235
   183
    using distributed_measurable[OF D]
hoelzl@57235
   184
    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
hoelzl@57235
   185
  also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}"
hoelzl@57235
   186
    unfolding distributed_distr_eq_density[OF D] ..
hoelzl@57235
   187
  also have "\<dots> = erlang_CDF k l a"
hoelzl@57235
   188
    by (auto intro!: emeasure_erlang_density)
hoelzl@57235
   189
  finally show ?thesis
hoelzl@57235
   190
    by (auto simp: measure_def)
hoelzl@57235
   191
qed
hoelzl@57235
   192
hoelzl@57235
   193
lemma (in prob_space) erlang_distributed_gt:
hoelzl@57235
   194
  assumes D[simp]: "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   195
  assumes [arith]: "0 < l" "0 \<le> a"
hoelzl@57235
   196
  shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)"
hoelzl@57235
   197
proof -
hoelzl@57235
   198
  have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto
hoelzl@57235
   199
  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
hoelzl@57235
   200
    using distributed_measurable[OF D] by (auto simp: prob_compl)
hoelzl@57235
   201
  also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le)
hoelzl@57235
   202
  finally show ?thesis by simp
hoelzl@57235
   203
qed
hoelzl@57235
   204
hoelzl@57235
   205
lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0"
hoelzl@57235
   206
  by (induction k) (auto simp: erlang_CDF_def)
hoelzl@57235
   207
hoelzl@57235
   208
lemma erlang_distributedI:
hoelzl@57235
   209
  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
hoelzl@57235
   210
    and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a"
hoelzl@57235
   211
  shows "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   212
proof (rule distributedI_borel_atMost)
hoelzl@57235
   213
  fix a :: real
hoelzl@57235
   214
  { assume "a \<le> 0"  
hoelzl@57235
   215
    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
hoelzl@57235
   216
      by (intro emeasure_mono) auto
hoelzl@57235
   217
    also have "... = 0"  by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0])
hoelzl@57235
   218
    finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp
hoelzl@57235
   219
    then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff)
hoelzl@57235
   220
  }
hoelzl@57235
   221
  note eq_0 = this
hoelzl@57235
   222
hoelzl@57235
   223
  show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)"
hoelzl@57235
   224
    using nn_integral_erlang_density[of l k a]
hoelzl@57235
   225
    by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps)
hoelzl@57235
   226
hoelzl@57235
   227
  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)"
hoelzl@57235
   228
    using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def)
hoelzl@57235
   229
qed (simp_all add: erlang_density_nonneg)
hoelzl@57235
   230
hoelzl@57235
   231
lemma (in prob_space) erlang_distributed_iff:
hoelzl@57235
   232
  assumes [arith]: "0<l"
hoelzl@57235
   233
  shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow>
hoelzl@57235
   234
    (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 ))"
hoelzl@57235
   235
  using
hoelzl@57235
   236
    distributed_measurable[of M lborel X "erlang_density k l"]
hoelzl@57235
   237
    emeasure_erlang_density[of l]
hoelzl@57235
   238
    erlang_distributed_le[of X k l]
hoelzl@57235
   239
  by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) 
hoelzl@57235
   240
hoelzl@57235
   241
lemma (in prob_space) erlang_distributed_mult_const:
hoelzl@57235
   242
  assumes erlX: "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   243
  assumes a_pos[arith]: "0 < \<alpha>"  "0 < l"
hoelzl@57235
   244
  shows  "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))"
hoelzl@57235
   245
proof (subst erlang_distributed_iff, safe)
hoelzl@57235
   246
  have [measurable]: "random_variable borel X"  and  [arith]: "0 < l " 
hoelzl@57235
   247
  and  [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a"
hoelzl@57235
   248
    by(insert erlX, auto simp: erlang_distributed_iff)
hoelzl@57235
   249
hoelzl@57235
   250
  show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>"  "0 < l / \<alpha>" 
hoelzl@57235
   251
    by (auto simp:field_simps)
hoelzl@57235
   252
  
hoelzl@57235
   253
  fix a:: real assume [arith]: "0 \<le> a"
hoelzl@57235
   254
  obtain b:: real  where [simp, arith]: "b = a/ \<alpha>" by blast 
hoelzl@57235
   255
hoelzl@57235
   256
  have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos)
hoelzl@57235
   257
 
hoelzl@57235
   258
  have "prob {x \<in> space M. \<alpha> * X x \<le> a}  = prob {x \<in> space M.  X x \<le> b}"
hoelzl@57235
   259
    by (rule arg_cong[where f= prob]) (auto simp:field_simps)
hoelzl@57235
   260
  
hoelzl@57235
   261
  moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto
hoelzl@57235
   262
  moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto
hoelzl@57235
   263
  ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce  
hoelzl@57235
   264
qed
hoelzl@57235
   265
hoelzl@57235
   266
lemma (in prob_space) has_bochner_integral_erlang_ith_moment:
hoelzl@57235
   267
  fixes k i :: nat and l :: real
hoelzl@57235
   268
  assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   269
  shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))"
hoelzl@57235
   270
proof (rule has_bochner_integral_nn_integral)
hoelzl@57235
   271
  show "AE x in M. 0 \<le> X x ^ i"
hoelzl@57235
   272
    by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def)
hoelzl@57235
   273
  show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))"
hoelzl@57235
   274
    using nn_integral_erlang_ith_moment[of l k i]
hoelzl@57235
   275
    by (subst distributed_nn_integral[symmetric, OF D]) auto
hoelzl@57235
   276
qed (insert distributed_measurable[OF D], simp)
hoelzl@57235
   277
hoelzl@57235
   278
lemma (in prob_space) erlang_ith_moment_integrable:
hoelzl@57235
   279
  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)"
hoelzl@57235
   280
  by rule (rule has_bochner_integral_erlang_ith_moment)
hoelzl@57235
   281
hoelzl@57235
   282
lemma (in prob_space) erlang_ith_moment:
hoelzl@57235
   283
  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow>
hoelzl@57235
   284
    expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)"
hoelzl@57235
   285
  by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment)
hoelzl@57235
   286
hoelzl@57235
   287
lemma (in prob_space) erlang_distributed_variance:
hoelzl@57235
   288
  assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)"
hoelzl@57235
   289
  shows "variance X = (k + 1) / l\<^sup>2"
hoelzl@57235
   290
proof (subst variance_eq)
hoelzl@57235
   291
  show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)"
hoelzl@57235
   292
    using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2]
hoelzl@57235
   293
    by auto
hoelzl@57235
   294
hoelzl@57235
   295
  show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2"
hoelzl@57235
   296
    using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2]
hoelzl@57235
   297
    by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc)
hoelzl@57235
   298
qed
hoelzl@57235
   299
hoelzl@50419
   300
subsection {* Exponential distribution *}
hoelzl@50419
   301
hoelzl@57235
   302
abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
hoelzl@57235
   303
  "exponential_density \<equiv> erlang_density 0"
hoelzl@50419
   304
hoelzl@57235
   305
lemma exponential_density_def:
hoelzl@57235
   306
  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
hoelzl@57235
   307
  by (simp add: fun_eq_iff erlang_density_def)
hoelzl@57235
   308
hoelzl@57235
   309
lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)"
hoelzl@57235
   310
  by (simp add: erlang_CDF_def)
hoelzl@50419
   311
hoelzl@50419
   312
lemma (in prob_space) exponential_distributed_params:
hoelzl@50419
   313
  assumes D: "distributed M lborel X (exponential_density l)"
hoelzl@50419
   314
  shows "0 < l"
hoelzl@50419
   315
proof (cases l "0 :: real" rule: linorder_cases)
hoelzl@50419
   316
  assume "l < 0"
hoelzl@50419
   317
  have "emeasure lborel {0 <.. 1::real} \<le>
hoelzl@50419
   318
    emeasure lborel {x :: real \<in> space lborel. 0 < x}"
hoelzl@50419
   319
    by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric])
hoelzl@50419
   320
  also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
hoelzl@50419
   321
  proof -
hoelzl@50419
   322
    have "AE x in lborel. 0 \<le> exponential_density l x"
hoelzl@50419
   323
      using assms by (auto simp: distributed_real_AE)
hoelzl@50419
   324
    then have "AE x in lborel. x \<le> (0::real)"
hoelzl@50419
   325
      apply eventually_elim 
hoelzl@50419
   326
      using `l < 0`
hoelzl@50419
   327
      apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm)
hoelzl@50419
   328
      done
hoelzl@50419
   329
    then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
hoelzl@50419
   330
      by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric])
hoelzl@50419
   331
  qed
hoelzl@50419
   332
  finally show "0 < l" by simp
hoelzl@50419
   333
next
hoelzl@50419
   334
  assume "l = 0"
hoelzl@50419
   335
  then have [simp]: "\<And>x. ereal (exponential_density l x) = 0"
hoelzl@50419
   336
    by (simp add: exponential_density_def)
hoelzl@50419
   337
  interpret X: prob_space "distr M lborel X"
hoelzl@50419
   338
    using distributed_measurable[OF D] by (rule prob_space_distr)
hoelzl@50419
   339
  from X.emeasure_space_1
hoelzl@50419
   340
  show "0 < l"
hoelzl@50419
   341
    by (simp add: emeasure_density distributed_distr_eq_density[OF D])
hoelzl@50419
   342
qed assumption
hoelzl@50419
   343
hoelzl@57235
   344
lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))"
hoelzl@57235
   345
  by (rule prob_space_erlang_density)
hoelzl@50419
   346
hoelzl@50419
   347
lemma (in prob_space) exponential_distributedD_le:
hoelzl@50419
   348
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
hoelzl@50419
   349
  shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)"
hoelzl@57235
   350
  using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a
hoelzl@57235
   351
  by (simp add: erlang_CDF_def)
hoelzl@50419
   352
hoelzl@50419
   353
lemma (in prob_space) exponential_distributedD_gt:
hoelzl@50419
   354
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
hoelzl@50419
   355
  shows "\<P>(x in M. a < X x ) = exp (- a * l)"
hoelzl@57235
   356
  using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a
hoelzl@57235
   357
  by (simp add: erlang_CDF_def)
hoelzl@50419
   358
hoelzl@50419
   359
lemma (in prob_space) exponential_distributed_memoryless:
hoelzl@50419
   360
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t"
hoelzl@50419
   361
  shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)"
hoelzl@50419
   362
proof -
hoelzl@50419
   363
  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)"
hoelzl@50419
   364
    using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"])
hoelzl@50419
   365
  also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)"
hoelzl@50419
   366
    using a t by (simp add: exponential_distributedD_gt[OF D])
hoelzl@50419
   367
  also have "\<dots> = exp (- t * l)"
hoelzl@50419
   368
    using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric])
hoelzl@50419
   369
  finally show ?thesis
hoelzl@50419
   370
    using t by (simp add: exponential_distributedD_gt[OF D])
hoelzl@50419
   371
qed
hoelzl@50419
   372
hoelzl@50419
   373
lemma exponential_distributedI:
hoelzl@50419
   374
  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
hoelzl@50419
   375
    and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)"
hoelzl@50419
   376
  shows "distributed M lborel X (exponential_density l)"
hoelzl@57235
   377
proof (rule erlang_distributedI)
hoelzl@57235
   378
  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)"
hoelzl@57235
   379
    using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def)
hoelzl@57235
   380
qed fact+
hoelzl@50419
   381
hoelzl@50419
   382
lemma (in prob_space) exponential_distributed_iff:
hoelzl@50419
   383
  "distributed M lborel X (exponential_density l) \<longleftrightarrow>
hoelzl@50419
   384
    (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)))"
hoelzl@57235
   385
  using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0)
hoelzl@50419
   386
hoelzl@50419
   387
hoelzl@50419
   388
lemma (in prob_space) exponential_distributed_expectation:
hoelzl@57235
   389
  "distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l"
hoelzl@57235
   390
  using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp
hoelzl@57235
   391
hoelzl@57235
   392
lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x"
hoelzl@57235
   393
  by (auto simp: exponential_density_def)
hoelzl@57235
   394
hoelzl@57235
   395
lemma (in prob_space) exponential_distributed_min:
hoelzl@57235
   396
  assumes expX: "distributed M lborel X (exponential_density l)"
hoelzl@57235
   397
  assumes expY: "distributed M lborel Y (exponential_density u)"
hoelzl@57235
   398
  assumes ind: "indep_var borel X borel Y"
hoelzl@57235
   399
  shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))"
hoelzl@57235
   400
proof (subst exponential_distributed_iff, safe)
hoelzl@57235
   401
  have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff)
hoelzl@57235
   402
  moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff)
hoelzl@57235
   403
  ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto
hoelzl@57235
   404
  
hoelzl@57235
   405
  have "0 < l" by (rule exponential_distributed_params) fact
hoelzl@57235
   406
  moreover have "0 < u" by (rule exponential_distributed_params) fact
hoelzl@57235
   407
  ultimately  show " 0 < l + u" by force
hoelzl@57235
   408
hoelzl@57235
   409
  fix a::real assume a[arith]: "0 \<le> a"
hoelzl@57235
   410
  have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) 
hoelzl@57235
   411
  have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) 
hoelzl@57235
   412
hoelzl@57235
   413
  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])
hoelzl@57235
   414
hoelzl@57235
   415
  also have " ... =  \<P>(x in M. a < (X x)) *  \<P>(x in M. a< (Y x) )"
hoelzl@57235
   416
    using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp
hoelzl@57235
   417
  also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp)
hoelzl@57235
   418
  finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" .
hoelzl@57235
   419
hoelzl@57235
   420
  have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })"
hoelzl@57235
   421
    by auto
hoelzl@57235
   422
  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}"
hoelzl@57235
   423
    using randX randY by (auto simp: prob_compl) 
hoelzl@57235
   424
  then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))"
hoelzl@57235
   425
    using indep_prob by auto
hoelzl@57235
   426
qed
hoelzl@57235
   427
 
hoelzl@57235
   428
lemma (in prob_space) exponential_distributed_Min:
hoelzl@57235
   429
  assumes finI: "finite I"
hoelzl@57235
   430
  assumes A: "I \<noteq> {}"
hoelzl@57235
   431
  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))"
hoelzl@57235
   432
  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
hoelzl@57235
   433
  shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))"
hoelzl@57235
   434
using assms
hoelzl@57235
   435
proof (induct rule: finite_ne_induct)
hoelzl@57235
   436
  case (singleton i) then show ?case by simp
hoelzl@57235
   437
next
hoelzl@57235
   438
  case (insert i I)
hoelzl@57235
   439
  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)))"
hoelzl@57235
   440
      by (intro exponential_distributed_min indep_vars_Min insert)
hoelzl@57235
   441
         (auto intro: indep_vars_subset) 
hoelzl@57235
   442
  then show ?case
hoelzl@57235
   443
    using insert by simp
hoelzl@57235
   444
qed
hoelzl@57235
   445
hoelzl@57235
   446
lemma (in prob_space) exponential_distributed_variance:
hoelzl@57235
   447
  "distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2"
hoelzl@57235
   448
  using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp
hoelzl@57235
   449
hoelzl@57235
   450
lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0"
hoelzl@57235
   451
  by (simp cong: nn_integral_cong_AE)
hoelzl@57235
   452
hoelzl@57235
   453
lemma convolution_erlang_density:
hoelzl@57235
   454
  fixes k\<^sub>1 k\<^sub>2 :: nat
hoelzl@57235
   455
  assumes [simp, arith]: "0 < l"
hoelzl@57235
   456
  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) =
hoelzl@57235
   457
    (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
hoelzl@57235
   458
      (is "?LHS = ?RHS")
hoelzl@57235
   459
proof
hoelzl@57235
   460
  fix x :: real
hoelzl@57235
   461
  have "x \<le> 0 \<or> 0 < x"
hoelzl@57235
   462
    by arith
hoelzl@57235
   463
  then show "?LHS x = ?RHS x"
hoelzl@57235
   464
  proof
hoelzl@57235
   465
    assume "x \<le> 0" then show ?thesis
hoelzl@57235
   466
      apply (subst nn_integral_zero')
hoelzl@57235
   467
      apply (rule AE_I[where N="{0}"])
hoelzl@57235
   468
      apply (auto simp add: erlang_density_def not_less)
hoelzl@57235
   469
      done
hoelzl@57235
   470
  next
hoelzl@57235
   471
    note zero_le_mult_iff[simp] zero_le_divide_iff[simp]
hoelzl@57235
   472
  
hoelzl@57235
   473
    have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1"
hoelzl@57235
   474
      using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc)
hoelzl@57235
   475
  
hoelzl@57235
   476
    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"
hoelzl@57235
   477
      apply (subst I_eq1[symmetric])
hoelzl@57235
   478
      unfolding erlang_density_def
hoelzl@57235
   479
      by (auto intro!: nn_integral_cong split:split_indicator)
hoelzl@57235
   480
  
hoelzl@57235
   481
    have "prob_space (density lborel ?LHS)"
hoelzl@57235
   482
      unfolding times_ereal.simps[symmetric]
hoelzl@57235
   483
      by (intro prob_space_convolution_density) 
hoelzl@57235
   484
         (auto intro!: prob_space_erlang_density erlang_density_nonneg)
hoelzl@57235
   485
    then have 2: "integral\<^sup>N lborel ?LHS = 1"
hoelzl@57235
   486
      by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
hoelzl@57235
   487
  
hoelzl@57235
   488
    let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
hoelzl@57235
   489
    let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
hoelzl@57235
   490
    let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
hoelzl@57235
   491
    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)"
hoelzl@57235
   492
hoelzl@57235
   493
    { fix x :: real assume [arith]: "0 < x"
hoelzl@57235
   494
      have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n"
hoelzl@57235
   495
        unfolding power_mult_distrib[symmetric] by (simp add: field_simps)
hoelzl@57235
   496
    
hoelzl@57235
   497
      have "?LHS x = ?L x"
hoelzl@57235
   498
        unfolding erlang_density_def
hoelzl@57235
   499
        by (auto intro!: nn_integral_cong split:split_indicator)
hoelzl@57235
   500
      also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
hoelzl@57235
   501
        apply (subst nn_integral_real_affine[where c=x and t = 0])
hoelzl@57235
   502
        apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc)
hoelzl@57235
   503
        apply (intro nn_integral_cong)
hoelzl@57235
   504
        apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add *
hoelzl@57235
   505
                    simp del: fact_Suc split: split_indicator)
hoelzl@57235
   506
        done
hoelzl@57235
   507
      finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 
hoelzl@57235
   508
        (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
hoelzl@57235
   509
        by simp }
hoelzl@57235
   510
    note * = this
hoelzl@57235
   511
hoelzl@57235
   512
    assume [arith]: "0 < x"
hoelzl@57235
   513
    have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)"
hoelzl@57235
   514
      by (subst 2[symmetric])
hoelzl@57235
   515
         (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
hoelzl@57235
   516
               simp: erlang_density_def  nn_integral_multc[symmetric] indicator_def split: split_if_asm)
hoelzl@57235
   517
    also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
hoelzl@57235
   518
      by (auto intro!: nn_integral_cong simp: * split: split_indicator)
hoelzl@57235
   519
    also have "... = ereal (?C) * ?I"
hoelzl@57235
   520
      using 1
hoelzl@57235
   521
      by (auto simp: nn_integral_nonneg nn_integral_cmult)  
hoelzl@57235
   522
    finally have " ereal (?C) * ?I = 1" by presburger
hoelzl@57235
   523
  
hoelzl@57235
   524
    then show ?thesis
hoelzl@57235
   525
      using * by simp
hoelzl@57235
   526
  qed
hoelzl@57235
   527
qed
hoelzl@57235
   528
hoelzl@57235
   529
lemma (in prob_space) sum_indep_erlang:
hoelzl@57235
   530
  assumes indep: "indep_var borel X borel Y"
hoelzl@57235
   531
  assumes [simp, arith]: "0 < l"
hoelzl@57235
   532
  assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
hoelzl@57235
   533
  assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
hoelzl@57235
   534
  shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
hoelzl@57235
   535
  using assms
hoelzl@57235
   536
  apply (subst convolution_erlang_density[symmetric, OF `0<l`])
hoelzl@57235
   537
  apply (intro distributed_convolution)
hoelzl@57235
   538
  apply auto
hoelzl@57235
   539
  done
hoelzl@57235
   540
hoelzl@57235
   541
lemma (in prob_space) erlang_distributed_setsum:
hoelzl@57235
   542
  assumes finI : "finite I"
hoelzl@57235
   543
  assumes A: "I \<noteq> {}"
hoelzl@57235
   544
  assumes [simp, arith]: "0 < l"
hoelzl@57235
   545
  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)"
hoelzl@57235
   546
  assumes ind: "indep_vars (\<lambda>i. borel) X I"
hoelzl@57235
   547
  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)"
hoelzl@57235
   548
using assms
hoelzl@57235
   549
proof (induct rule: finite_ne_induct)
hoelzl@57235
   550
  case (singleton i) then show ?case by auto
hoelzl@57235
   551
next
hoelzl@57235
   552
  case (insert i I)
hoelzl@57235
   553
    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)"
hoelzl@57235
   554
      by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset)
hoelzl@57235
   555
    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)"
hoelzl@57235
   556
      using insert by auto
hoelzl@57235
   557
    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"
hoelzl@57235
   558
      using insert by (auto intro!: Suc_pred simp: ac_simps)    
hoelzl@57235
   559
    finally show ?case by fast
hoelzl@57235
   560
qed
hoelzl@57235
   561
hoelzl@57235
   562
lemma (in prob_space) exponential_distributed_setsum:
hoelzl@57235
   563
  assumes finI: "finite I"
hoelzl@57235
   564
  assumes A: "I \<noteq> {}"
hoelzl@57235
   565
  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)"
hoelzl@57235
   566
  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
hoelzl@57235
   567
  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)"
hoelzl@57235
   568
proof -
hoelzl@57235
   569
  obtain i where "i \<in> I" using assms by auto
hoelzl@57235
   570
  note exponential_distributed_params[OF expX[OF this]]
hoelzl@57235
   571
  from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp
hoelzl@57235
   572
qed
hoelzl@50419
   573
hoelzl@50419
   574
subsection {* Uniform distribution *}
hoelzl@50419
   575
hoelzl@50419
   576
lemma uniform_distrI:
hoelzl@50419
   577
  assumes X: "X \<in> measurable M M'"
hoelzl@50419
   578
    and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0"
hoelzl@50419
   579
  assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A"
hoelzl@50419
   580
  shows "distr M M' X = uniform_measure M' A"
hoelzl@50419
   581
  unfolding uniform_measure_def
hoelzl@50419
   582
proof (intro measure_eqI)
hoelzl@50419
   583
  let ?f = "\<lambda>x. indicator A x / emeasure M' A"
hoelzl@50419
   584
  fix B assume B: "B \<in> sets (distr M M' X)"
hoelzl@50419
   585
  with X have "emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A"
hoelzl@50419
   586
    by (simp add: distr[of B] measurable_sets)
hoelzl@50419
   587
  also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)"
hoelzl@50419
   588
     by simp
wenzelm@53015
   589
  also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')"
hoelzl@50419
   590
    using A B
hoelzl@56996
   591
    by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
wenzelm@53015
   592
  also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
hoelzl@56996
   593
    by (rule nn_integral_cong) (auto split: split_indicator)
hoelzl@50419
   594
  finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
hoelzl@50419
   595
    using A B X by (auto simp add: emeasure_distr emeasure_density)
hoelzl@50419
   596
qed simp
hoelzl@50419
   597
hoelzl@50419
   598
lemma uniform_distrI_borel:
hoelzl@50419
   599
  fixes A :: "real set"
hoelzl@50419
   600
  assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r"
hoelzl@50419
   601
    and [measurable]: "A \<in> sets borel"
hoelzl@50419
   602
  assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r"
hoelzl@50419
   603
  shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)"
hoelzl@50419
   604
proof (rule distributedI_borel_atMost)
hoelzl@50419
   605
  let ?f = "\<lambda>x. 1 / r * indicator A x"
hoelzl@50419
   606
  fix a
hoelzl@50419
   607
  have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A"
hoelzl@50419
   608
    using A by (intro emeasure_mono) auto
hoelzl@50419
   609
  also have "\<dots> < \<infinity>"
hoelzl@50419
   610
    using A by simp
hoelzl@50419
   611
  finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>"
hoelzl@50419
   612
    by simp
hoelzl@50419
   613
  from emeasure_eq_ereal_measure[OF this]
hoelzl@50419
   614
  have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ereal (measure lborel (A \<inter> {..a}) / r)"
hoelzl@50419
   615
    using A by simp
hoelzl@50419
   616
  then show "emeasure M {x\<in>space M. X x \<le> a} = ereal (measure lborel (A \<inter> {..a}) / r)"
hoelzl@50419
   617
    using distr by simp
hoelzl@50419
   618
 
wenzelm@53015
   619
  have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
wenzelm@53015
   620
    (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
hoelzl@56996
   621
    by (auto intro!: nn_integral_cong split: split_indicator)
hoelzl@50419
   622
  also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
hoelzl@50419
   623
    using `A \<in> sets borel`
hoelzl@56996
   624
    by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
hoelzl@50419
   625
  also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
hoelzl@50419
   626
    unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
wenzelm@53015
   627
  finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
hoelzl@50419
   628
    ereal (measure lborel (A \<inter> {..a}) / r)" .
hoelzl@56571
   629
qed (auto simp: measure_nonneg)
hoelzl@50419
   630
hoelzl@50419
   631
lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
hoelzl@50419
   632
  fixes a b :: real
hoelzl@50419
   633
  assumes X: "X \<in> borel_measurable M" and "a < b"
hoelzl@50419
   634
  assumes distr: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> \<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
hoelzl@50419
   635
  shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})"
hoelzl@50419
   636
proof (rule uniform_distrI_borel)
hoelzl@50419
   637
  fix t
hoelzl@50419
   638
  have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t"
hoelzl@50419
   639
    by auto
hoelzl@50419
   640
  then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b - a)"
hoelzl@50419
   641
  proof (elim disjE conjE)
hoelzl@50419
   642
    assume "t < a" 
hoelzl@50419
   643
    then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}"
hoelzl@50419
   644
      using X by (auto intro!: emeasure_mono measurable_sets)
hoelzl@50419
   645
    also have "\<dots> = 0"
hoelzl@50419
   646
      using distr[of a] `a < b` by (simp add: emeasure_eq_measure)
hoelzl@50419
   647
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 0"
hoelzl@50419
   648
      by (simp add: antisym measure_nonneg emeasure_le_0_iff)
hoelzl@50419
   649
    with `t < a` show ?thesis by simp
hoelzl@50419
   650
  next
hoelzl@50419
   651
    assume bnds: "a \<le> t" "t \<le> b"
hoelzl@50419
   652
    have "{a..b} \<inter> {..t} = {a..t}"
hoelzl@50419
   653
      using bnds by auto
hoelzl@50419
   654
    then show ?thesis using `a \<le> t` `a < b`
hoelzl@50419
   655
      using distr[OF bnds] by (simp add: emeasure_eq_measure)
hoelzl@50419
   656
  next
hoelzl@50419
   657
    assume "b < t" 
hoelzl@50419
   658
    have "1 = emeasure M {x\<in>space M. X x \<le> b}"
hoelzl@50419
   659
      using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure)
hoelzl@50419
   660
    also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}"
hoelzl@50419
   661
      using X `b < t` by (auto intro!: emeasure_mono measurable_sets)
hoelzl@50419
   662
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 1"
hoelzl@50419
   663
       by (simp add: antisym emeasure_eq_measure one_ereal_def)
hoelzl@50419
   664
    with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def)
hoelzl@50419
   665
  qed
hoelzl@50419
   666
qed (insert X `a < b`, auto)
hoelzl@50419
   667
hoelzl@50419
   668
lemma (in prob_space) uniform_distributed_measure:
hoelzl@50419
   669
  fixes a b :: real
hoelzl@50419
   670
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
hoelzl@50419
   671
  assumes " a \<le> t" "t \<le> b"
hoelzl@50419
   672
  shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
hoelzl@50419
   673
proof -
hoelzl@50419
   674
  have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}"
hoelzl@50419
   675
    using distributed_measurable[OF D]
hoelzl@50419
   676
    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
wenzelm@53015
   677
  also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)"
hoelzl@50419
   678
    using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
hoelzl@50419
   679
    unfolding distributed_distr_eq_density[OF D]
hoelzl@50419
   680
    by (subst emeasure_density)
hoelzl@56996
   681
       (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
hoelzl@50419
   682
  also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
hoelzl@50419
   683
    using `a \<le> t` `t \<le> b`
hoelzl@56996
   684
    by (subst nn_integral_cmult_indicator) auto
hoelzl@50419
   685
  finally show ?thesis
hoelzl@50419
   686
    by (simp add: measure_def)
hoelzl@50419
   687
qed
hoelzl@50419
   688
hoelzl@50419
   689
lemma (in prob_space) uniform_distributed_bounds:
hoelzl@50419
   690
  fixes a b :: real
hoelzl@50419
   691
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
hoelzl@50419
   692
  shows "a < b"
hoelzl@50419
   693
proof (rule ccontr)
hoelzl@50419
   694
  assume "\<not> a < b"
hoelzl@50419
   695
  then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp
hoelzl@50419
   696
  with uniform_distributed_params[OF D] show False 
hoelzl@50419
   697
    by (auto simp: measure_def)
hoelzl@50419
   698
qed
hoelzl@50419
   699
hoelzl@50419
   700
lemma (in prob_space) uniform_distributed_iff:
hoelzl@50419
   701
  fixes a b :: real
hoelzl@50419
   702
  shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> 
hoelzl@50419
   703
    (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)))"
hoelzl@50419
   704
  using
hoelzl@50419
   705
    uniform_distributed_bounds[of X a b]
hoelzl@50419
   706
    uniform_distributed_measure[of X a b]
hoelzl@50419
   707
    distributed_measurable[of M lborel X]
hoelzl@56993
   708
  by (auto intro!: uniform_distrI_borel_atLeastAtMost 
hoelzl@56993
   709
              simp: one_ereal_def emeasure_eq_measure
hoelzl@56993
   710
              simp del: measure_lborel)
hoelzl@50419
   711
hoelzl@50419
   712
lemma (in prob_space) uniform_distributed_expectation:
hoelzl@50419
   713
  fixes a b :: real
hoelzl@50419
   714
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
hoelzl@50419
   715
  shows "expectation X = (a + b) / 2"
hoelzl@50419
   716
proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
hoelzl@50419
   717
  have "a < b"
hoelzl@50419
   718
    using uniform_distributed_bounds[OF D] .
hoelzl@50419
   719
hoelzl@50419
   720
  have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 
hoelzl@50419
   721
    (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
hoelzl@50419
   722
    by (intro integral_cong) auto
hoelzl@50419
   723
  also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
hoelzl@50419
   724
  proof (subst integral_FTC_atLeastAtMost)
hoelzl@50419
   725
    fix x
wenzelm@53077
   726
    show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
hoelzl@50419
   727
      using uniform_distributed_params[OF D]
hoelzl@56381
   728
      by (auto intro!: derivative_eq_intros)
hoelzl@50419
   729
    show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
hoelzl@50419
   730
      using uniform_distributed_params[OF D]
hoelzl@50419
   731
      by (auto intro!: isCont_divide)
wenzelm@53015
   732
    have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) =
hoelzl@50419
   733
      (b*b - a * a) / (2 * (b - a))"
hoelzl@50419
   734
      using `a < b`
hoelzl@50419
   735
      by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric])
wenzelm@53015
   736
    show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2"
hoelzl@50419
   737
      using `a < b`
hoelzl@50419
   738
      unfolding * square_diff_square_factored by (auto simp: field_simps)
hoelzl@50419
   739
  qed (insert `a < b`, simp)
hoelzl@50419
   740
  finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" .
hoelzl@50419
   741
qed auto
hoelzl@50419
   742
hoelzl@57235
   743
lemma (in prob_space) uniform_distributed_variance:
hoelzl@57235
   744
  fixes a b :: real
hoelzl@57235
   745
  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
hoelzl@57235
   746
  shows "variance X = (b - a)\<^sup>2 / 12"
hoelzl@57235
   747
proof (subst distributed_variance)
hoelzl@57235
   748
  have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
hoelzl@57235
   749
  let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
hoelzl@57235
   750
  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)"
hoelzl@57235
   751
    by (intro integral_cong) (auto split: split_indicator)
hoelzl@57235
   752
  also have "\<dots> = (b - a)\<^sup>2 / 12"
hoelzl@57235
   753
    by (simp add: integral_power measure_lebesgue_Icc uniform_distributed_expectation[OF D])
hoelzl@57235
   754
       (simp add: eval_nat_numeral field_simps )
hoelzl@57235
   755
  finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
hoelzl@57235
   756
qed fact
hoelzl@57235
   757
hoelzl@50419
   758
end