src/HOL/Probability/Distributions.thy
author hoelzl
Mon, 19 May 2014 12:04:45 +0200
changeset 56993 e5366291d6aa
parent 56571 f4635657d66f
child 56996 891e992e510f
permissions -rw-r--r--
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     1
theory Distributions
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     2
  imports Probability_Measure
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     3
begin
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     4
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     5
subsection {* Exponential distribution *}
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     6
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     7
definition exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     8
  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
     9
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    10
lemma borel_measurable_exponential_density[measurable]: "exponential_density l \<in> borel_measurable borel"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    11
  by (auto simp add: exponential_density_def[abs_def])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    12
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    13
lemma (in prob_space) exponential_distributed_params:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    14
  assumes D: "distributed M lborel X (exponential_density l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    15
  shows "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    16
proof (cases l "0 :: real" rule: linorder_cases)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    17
  assume "l < 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    18
  have "emeasure lborel {0 <.. 1::real} \<le>
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    19
    emeasure lborel {x :: real \<in> space lborel. 0 < x}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    20
    by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    21
  also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    22
  proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    23
    have "AE x in lborel. 0 \<le> exponential_density l x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    24
      using assms by (auto simp: distributed_real_AE)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    25
    then have "AE x in lborel. x \<le> (0::real)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    26
      apply eventually_elim 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    27
      using `l < 0`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    28
      apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    29
      done
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    30
    then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    31
      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
    32
  qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    33
  finally show "0 < l" by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    34
next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    35
  assume "l = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    36
  then have [simp]: "\<And>x. ereal (exponential_density l x) = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    37
    by (simp add: exponential_density_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    38
  interpret X: prob_space "distr M lborel X"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    39
    using distributed_measurable[OF D] by (rule prob_space_distr)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    40
  from X.emeasure_space_1
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    41
  show "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    42
    by (simp add: emeasure_density distributed_distr_eq_density[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    43
qed assumption
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    44
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    45
lemma
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    46
  assumes [arith]: "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    47
  shows emeasure_exponential_density_le0: "0 \<le> a \<Longrightarrow> emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    48
    and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    49
      (is "prob_space ?D")
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    50
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    51
  let ?f = "\<lambda>x. l * exp (- x * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    52
  let ?F = "\<lambda>x. - exp (- x * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    53
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    54
  have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
    55
    by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    56
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
    57
  have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    58
    by (auto simp: emeasure_density exponential_density_def
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    59
             intro!: positive_integral_cong split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    60
  also have "\<dots> = ereal (0 - ?F 0)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    61
  proof (rule positive_integral_FTC_atLeast)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    62
    have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    63
      by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    64
         (simp_all add: tendsto_const filterlim_ident)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    65
    then show "((\<lambda>x. - exp (- x * l)) ---> 0) at_top"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    66
      unfolding filterlim_at_top_mirror
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    67
      by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    68
  qed (insert deriv, auto)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    69
  also have "\<dots> = 1" by (simp add: one_ereal_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    70
  finally have "emeasure ?D (space ?D) = 1" .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    71
  then show "prob_space ?D" by rule
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    72
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    73
  assume "0 \<le> a"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
    74
  have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    75
    by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    76
       (auto simp: exponential_density_def)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
    77
  also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    78
    using `0 \<le> a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    79
  also have "\<dots> = 1 - exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    80
    by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    81
  finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    82
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    83
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    84
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    85
lemma (in prob_space) exponential_distributedD_le:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    86
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    87
  shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    88
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    89
  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    90
    using distributed_measurable[OF D] 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    91
    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    92
  also have "\<dots> = emeasure (density lborel (exponential_density l)) {.. a}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    93
    unfolding distributed_distr_eq_density[OF D] ..
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    94
  also have "\<dots> = 1 - exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    95
    using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    96
  finally show ?thesis
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    97
    by (auto simp: measure_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    98
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
    99
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   100
lemma (in prob_space) exponential_distributedD_gt:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   101
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   102
  shows "\<P>(x in M. a < X x ) = exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   103
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   104
  have "exp (- a * l) = 1 - \<P>(x in M. X x \<le> a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   105
    unfolding exponential_distributedD_le[OF D a] by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   106
  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   107
    using distributed_measurable[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   108
    by (subst prob_compl) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   109
  also have "\<dots> = \<P>(x in M. a < X x )"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   110
    by (auto intro!: arg_cong[where f=prob] simp: not_le)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   111
  finally show ?thesis by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   112
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   113
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   114
lemma (in prob_space) exponential_distributed_memoryless:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   115
  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
   116
  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
   117
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   118
  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
   119
    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
   120
  also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   121
    using a t by (simp add: exponential_distributedD_gt[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   122
  also have "\<dots> = exp (- t * l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   123
    using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   124
  finally show ?thesis
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   125
    using t by (simp add: exponential_distributedD_gt[OF D])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   126
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   127
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   128
lemma exponential_distributedI:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   129
  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   130
    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
   131
  shows "distributed M lborel X (exponential_density l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   132
proof (rule distributedI_borel_atMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   133
  fix a :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   134
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   135
  { assume "a \<le> 0"  
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   136
    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   137
      by (intro emeasure_mono) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   138
    then have "emeasure M {x\<in>space M. X x \<le> a} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   139
      using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) }
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   140
  note eq_0 = this
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   141
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   142
  have "\<And>x. \<not> 0 \<le> a \<Longrightarrow> ereal (exponential_density l x) * indicator {..a} x = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   143
    by (simp add: exponential_density_def)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   144
  then show "(\<integral>\<^sup>+ x. exponential_density l x * indicator {..a} x \<partial>lborel) = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   145
    using emeasure_exponential_density_le0[of l a]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   146
    by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   147
             simp del: times_ereal.simps ereal_zero_times)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   148
  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   149
    using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   150
  show "AE x in lborel. 0 \<le> exponential_density l x "
56536
aefb4a8da31f made mult_nonneg_nonneg a simp rule
nipkow
parents: 56381
diff changeset
   151
    by (auto simp: exponential_density_def)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   152
qed simp_all
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   153
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   154
lemma (in prob_space) exponential_distributed_iff:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   155
  "distributed M lborel X (exponential_density l) \<longleftrightarrow>
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   156
    (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)))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   157
  using
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   158
    distributed_measurable[of M lborel X "exponential_density l"]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   159
    exponential_distributed_params[of X l]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   160
    emeasure_exponential_density_le0[of l]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   161
    exponential_distributedD_le[of X l]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   162
  by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   163
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   164
lemma borel_integral_x_exp:
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   165
  "has_bochner_integral lborel (\<lambda>x. x * exp (- x) * indicator {0::real ..} x) 1"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   166
proof (rule has_bochner_integral_monotone_convergence)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   167
  let ?f = "\<lambda>i x. x * exp (- x) * indicator {0::real .. i} x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   168
  have "eventually (\<lambda>b::real. 0 \<le> b) at_top"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   169
    by (rule eventually_ge_at_top)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   170
  then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   171
  proof eventually_elim
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   172
   fix b :: real assume [simp]: "0 \<le> b"
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   173
    have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^sup>L lborel (?f b)) = 
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   174
      (\<integral>x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \<partial>lborel)"
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   175
      by (subst integral_diff[symmetric])
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   176
         (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   177
    also have "\<dots> = b * exp (-b) - 0 * exp (- 0)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   178
    proof (rule integral_FTC_atLeastAtMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   179
      fix x assume "0 \<le> x" "x \<le> b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   180
      show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   181
        by (auto intro!: derivative_eq_intros)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   182
      show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 53077
diff changeset
   183
        by (intro continuous_intros)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   184
    qed fact
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   185
    also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   186
      by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   187
    finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   188
      by (auto simp: field_simps exp_minus inverse_eq_divide)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   189
  qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   190
  then have "((\<lambda>i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   191
  proof (rule Lim_transform_eventually)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   192
    show "((\<lambda>i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   193
      using tendsto_power_div_exp_0[of 1]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   194
      by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   195
  qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   196
  then show "(\<lambda>i. integral\<^sup>L lborel (?f i)) ----> 1"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   197
    by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   198
  show "AE x in lborel. mono (\<lambda>n::nat. x * exp (- x) * indicator {0..real n} x)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   199
    by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   200
  show "\<And>i::nat. integrable lborel (\<lambda>x. x * exp (- x) * indicator {0..real i} x)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   201
    by (rule borel_integrable_atLeastAtMost) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   202
  show "AE x in lborel. (\<lambda>i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   203
    apply (intro AE_I2 Lim_eventually )
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   204
    apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   205
    apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   206
    done
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   207
qed (auto intro!: borel_measurable_times borel_measurable_exp)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   208
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   209
lemma (in prob_space) exponential_distributed_expectation:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   210
  assumes D: "distributed M lborel X (exponential_density l)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   211
  shows "expectation X = 1 / l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   212
proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   213
  have "0 < l"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   214
   using exponential_distributed_params[OF D] .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   215
  have [simp]: "\<And>x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) =
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   216
    x * exponential_density l x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   217
    using `0 < l`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   218
    by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   219
  from borel_integral_x_exp `0 < l`
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   220
  have "has_bochner_integral lborel (\<lambda>x. exponential_density l x * x) (1 / l)"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   221
    by (subst (asm) lborel_has_bochner_integral_real_affine_iff[of l _ _ 0])
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   222
       (simp_all add: field_simps)
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   223
  then show "(\<integral> x. exponential_density l x * x \<partial>lborel) = 1 / l"
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 56571
diff changeset
   224
    by (metis has_bochner_integral_integral_eq)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   225
qed simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   226
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   227
subsection {* Uniform distribution *}
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   228
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   229
lemma uniform_distrI:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   230
  assumes X: "X \<in> measurable M M'"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   231
    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
   232
  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
   233
  shows "distr M M' X = uniform_measure M' A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   234
  unfolding uniform_measure_def
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   235
proof (intro measure_eqI)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   236
  let ?f = "\<lambda>x. indicator A x / emeasure M' A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   237
  fix B assume B: "B \<in> sets (distr M M' X)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   238
  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
   239
    by (simp add: distr[of B] measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   240
  also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   241
     by simp
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   242
  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
   243
    using A B
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   244
    by (intro positive_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
   245
  also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   246
    by (rule positive_integral_cong) (auto split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   247
  finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   248
    using A B X by (auto simp add: emeasure_distr emeasure_density)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   249
qed simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   250
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   251
lemma uniform_distrI_borel:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   252
  fixes A :: "real set"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   253
  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
   254
    and [measurable]: "A \<in> sets borel"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   255
  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
   256
  shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   257
proof (rule distributedI_borel_atMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   258
  let ?f = "\<lambda>x. 1 / r * indicator A x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   259
  fix a
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   260
  have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   261
    using A by (intro emeasure_mono) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   262
  also have "\<dots> < \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   263
    using A by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   264
  finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   265
    by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   266
  from emeasure_eq_ereal_measure[OF this]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   267
  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
   268
    using A by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   269
  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
   270
    using distr by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   271
 
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 50419
diff changeset
   272
  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
   273
    (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   274
    by (auto intro!: positive_integral_cong split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   275
  also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   276
    using `A \<in> sets borel`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   277
    by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   278
  also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   279
    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
   280
  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
   281
    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
   282
qed (auto simp: measure_nonneg)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   283
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   284
lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   285
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   286
  assumes X: "X \<in> borel_measurable M" and "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   287
  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
   288
  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
   289
proof (rule uniform_distrI_borel)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   290
  fix t
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   291
  have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   292
    by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   293
  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
   294
  proof (elim disjE conjE)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   295
    assume "t < a" 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   296
    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
   297
      using X by (auto intro!: emeasure_mono measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   298
    also have "\<dots> = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   299
      using distr[of a] `a < b` by (simp add: emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   300
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   301
      by (simp add: antisym measure_nonneg emeasure_le_0_iff)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   302
    with `t < a` show ?thesis by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   303
  next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   304
    assume bnds: "a \<le> t" "t \<le> b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   305
    have "{a..b} \<inter> {..t} = {a..t}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   306
      using bnds by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   307
    then show ?thesis using `a \<le> t` `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   308
      using distr[OF bnds] by (simp add: emeasure_eq_measure)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   309
  next
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   310
    assume "b < t" 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   311
    have "1 = emeasure M {x\<in>space M. X x \<le> b}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   312
      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
   313
    also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   314
      using X `b < t` by (auto intro!: emeasure_mono measurable_sets)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   315
    finally have "emeasure M {x\<in>space M. X x \<le> t} = 1"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   316
       by (simp add: antisym emeasure_eq_measure one_ereal_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   317
    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
   318
  qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   319
qed (insert X `a < b`, auto)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   320
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   321
lemma (in prob_space) uniform_distributed_measure:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   322
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   323
  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
   324
  assumes " a \<le> t" "t \<le> b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   325
  shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   326
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   327
  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
   328
    using distributed_measurable[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   329
    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
   330
  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
   331
    using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   332
    unfolding distributed_distr_eq_density[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   333
    by (subst emeasure_density)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   334
       (auto intro!: positive_integral_cong simp: measure_def split: split_indicator)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   335
  also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   336
    using `a \<le> t` `t \<le> b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   337
    by (subst positive_integral_cmult_indicator) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   338
  finally show ?thesis
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   339
    by (simp add: measure_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   340
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   341
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   342
lemma (in prob_space) uniform_distributed_bounds:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   343
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   344
  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
   345
  shows "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   346
proof (rule ccontr)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   347
  assume "\<not> a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   348
  then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   349
  with uniform_distributed_params[OF D] show False 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   350
    by (auto simp: measure_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   351
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   352
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   353
lemma (in prob_space) uniform_distributed_iff:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   354
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   355
  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
   356
    (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
   357
  using
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   358
    uniform_distributed_bounds[of X a b]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   359
    uniform_distributed_measure[of X a b]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   360
    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
   361
  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
   362
              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
   363
              simp del: measure_lborel)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   364
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   365
lemma (in prob_space) uniform_distributed_expectation:
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   366
  fixes a b :: real
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   367
  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
   368
  shows "expectation X = (a + b) / 2"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   369
proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   370
  have "a < b"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   371
    using uniform_distributed_bounds[OF D] .
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   372
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   373
  have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   374
    (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   375
    by (intro integral_cong) auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   376
  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
   377
  proof (subst integral_FTC_atLeastAtMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   378
    fix x
53077
a1b3784f8129 more symbols;
wenzelm
parents: 53015
diff changeset
   379
    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
   380
      using uniform_distributed_params[OF D]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   381
      by (auto intro!: derivative_eq_intros)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   382
    show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   383
      using uniform_distributed_params[OF D]
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   384
      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
   385
    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
   386
      (b*b - a * a) / (2 * (b - a))"
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   387
      using `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   388
      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
   389
    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
   390
      using `a < b`
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   391
      unfolding * square_diff_square_factored by (auto simp: field_simps)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   392
  qed (insert `a < b`, simp)
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   393
  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
   394
qed auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   395
3177d0374701 add exponential and uniform distributions
hoelzl
parents:
diff changeset
   396
end