HOL-Probability: generalize theorems about cumulative distribution function
authorhoelzl
Thu Oct 20 18:42:01 2016 +0200 (2016-10-20)
changeset 6432195be866e49fc
parent 64320 ba194424b895
child 64323 20d15328b248
HOL-Probability: generalize theorems about cumulative distribution function
src/HOL/Probability/Distribution_Functions.thy
     1.1 --- a/src/HOL/Probability/Distribution_Functions.thy	Thu Oct 20 18:41:59 2016 +0200
     1.2 +++ b/src/HOL/Probability/Distribution_Functions.thy	Thu Oct 20 18:42:01 2016 +0200
     1.3 @@ -36,11 +36,11 @@
     1.4    by (simp add: cdf_def)
     1.5  
     1.6  locale finite_borel_measure = finite_measure M for M :: "real measure" +
     1.7 -  assumes M_super_borel: "sets borel \<subseteq> sets M"
     1.8 +  assumes M_is_borel: "sets M = sets borel"
     1.9  begin
    1.10  
    1.11  lemma sets_M[intro]: "a \<in> sets borel \<Longrightarrow> a \<in> sets M"
    1.12 -  using M_super_borel by auto
    1.13 +  using M_is_borel by auto
    1.14  
    1.15  lemma cdf_diff_eq:
    1.16    assumes "x < y"
    1.17 @@ -57,7 +57,7 @@
    1.18    unfolding cdf_def by (auto intro!: finite_measure_mono)
    1.19  
    1.20  lemma borel_UNIV: "space M = UNIV"
    1.21 - by (metis in_mono sets.sets_into_space space_in_borel top_le M_super_borel)
    1.22 + by (metis in_mono sets.sets_into_space space_in_borel top_le M_is_borel)
    1.23  
    1.24  lemma cdf_nonneg: "cdf M x \<ge> 0"
    1.25    unfolding cdf_def by (rule measure_nonneg)
    1.26 @@ -142,11 +142,17 @@
    1.27  end
    1.28  
    1.29  locale real_distribution = prob_space M for M :: "real measure" +
    1.30 -  assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel" and space_eq_univ [simp]: "space M = UNIV"
    1.31 +  assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel"
    1.32  begin
    1.33  
    1.34 +lemma finite_borel_measure_M: "finite_borel_measure M"
    1.35 +  by standard auto
    1.36 +
    1.37  sublocale finite_borel_measure M
    1.38 -  by standard auto
    1.39 +  by (rule finite_borel_measure_M)
    1.40 +
    1.41 +lemma space_eq_univ [simp]: "space M = UNIV"
    1.42 +  using events_eq_borel[THEN sets_eq_imp_space_eq] by simp
    1.43  
    1.44  lemma cdf_bounded_prob: "\<And>x. cdf M x \<le> 1"
    1.45    by (subst prob_space [symmetric], rule cdf_bounded)
    1.46 @@ -167,20 +173,23 @@
    1.47    "random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
    1.48    unfolding real_distribution_def real_distribution_axioms_def by (auto intro!: prob_space_distr)
    1.49  
    1.50 -subsection \<open>uniqueness\<close>
    1.51 +subsection \<open>Uniqueness\<close>
    1.52  
    1.53 -lemma (in real_distribution) emeasure_Ioc:
    1.54 +lemma (in finite_borel_measure) emeasure_Ioc:
    1.55    assumes "a \<le> b" shows "emeasure M {a <.. b} = cdf M b - cdf M a"
    1.56  proof -
    1.57    have "{a <.. b} = {..b} - {..a}"
    1.58      by auto
    1.59 -  with \<open>a \<le> b\<close> show ?thesis
    1.60 +  moreover have "{..x} \<in> sets M" for x
    1.61 +    using atMost_borel[of x] M_is_borel by auto
    1.62 +  moreover note \<open>a \<le> b\<close>
    1.63 +  ultimately show ?thesis
    1.64      by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
    1.65  qed
    1.66  
    1.67 -lemma cdf_unique:
    1.68 +lemma cdf_unique':
    1.69    fixes M1 M2
    1.70 -  assumes "real_distribution M1" and "real_distribution M2"
    1.71 +  assumes "finite_borel_measure M1" and "finite_borel_measure M2"
    1.72    assumes "cdf M1 = cdf M2"
    1.73    shows "M1 = M2"
    1.74  proof (rule measure_eqI_generator_eq[where \<Omega>=UNIV])
    1.75 @@ -188,14 +197,56 @@
    1.76    then obtain a b where Xeq: "X = {a<..b}" by auto
    1.77    then show "emeasure M1 X = emeasure M2 X"
    1.78      by (cases "a \<le> b")
    1.79 -       (simp_all add: assms(1,2)[THEN real_distribution.emeasure_Ioc] assms(3))
    1.80 +       (simp_all add: assms(1,2)[THEN finite_borel_measure.emeasure_Ioc] assms(3))
    1.81  next
    1.82    show "(\<Union>i. {- real (i::nat)<..real i}) = UNIV"
    1.83      by (rule UN_Ioc_eq_UNIV)
    1.84 -qed (auto simp: real_distribution.emeasure_Ioc[OF assms(1)]
    1.85 -  assms(1,2)[THEN real_distribution.events_eq_borel] borel_sigma_sets_Ioc
    1.86 +qed (auto simp: finite_borel_measure.emeasure_Ioc[OF assms(1)]
    1.87 +  assms(1,2)[THEN finite_borel_measure.M_is_borel] borel_sigma_sets_Ioc
    1.88    Int_stable_def)
    1.89  
    1.90 +lemma cdf_unique:
    1.91 +  "real_distribution M1 \<Longrightarrow> real_distribution M2 \<Longrightarrow> cdf M1 = cdf M2 \<Longrightarrow> M1 = M2"
    1.92 +  using cdf_unique'[of M1 M2] by (simp add: real_distribution.finite_borel_measure_M)
    1.93 +
    1.94 +lemma
    1.95 +  fixes F :: "real \<Rightarrow> real"
    1.96 +  assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y"
    1.97 +    and right_cont_F : "\<And>a. continuous (at_right a) F"
    1.98 +    and lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
    1.99 +    and lim_F_at_top : "(F \<longlongrightarrow> m) at_top"
   1.100 +    and m: "0 \<le> m"
   1.101 +  shows interval_measure_UNIV: "emeasure (interval_measure F) UNIV = m"
   1.102 +    and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
   1.103 +proof -
   1.104 +  let ?F = "interval_measure F"
   1.105 +  { have "ennreal (m - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
   1.106 +      by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
   1.107 +                lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
   1.108 +                lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
   1.109 +                filterlim_uminus_at_top[THEN iffD1])
   1.110 +         (auto simp: incseq_def nondecF intro!: diff_mono)
   1.111 +    also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
   1.112 +      by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
   1.113 +    also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
   1.114 +      by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
   1.115 +    also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
   1.116 +      by (simp add: UN_Ioc_eq_UNIV)
   1.117 +    finally have "emeasure ?F (space ?F) = m"
   1.118 +      by simp }
   1.119 +  note * = this
   1.120 +  then show "emeasure (interval_measure F) UNIV = m"
   1.121 +    by simp
   1.122 +
   1.123 +  interpret finite_measure ?F
   1.124 +  proof
   1.125 +    show "emeasure ?F (space ?F) \<noteq> \<infinity>"
   1.126 +      using * by simp
   1.127 +  qed
   1.128 +  show "finite_borel_measure (interval_measure F)"
   1.129 +    proof qed simp_all
   1.130 +qed
   1.131 +
   1.132  lemma real_distribution_interval_measure:
   1.133    fixes F :: "real \<Rightarrow> real"
   1.134    assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
   1.135 @@ -206,53 +257,47 @@
   1.136  proof -
   1.137    let ?F = "interval_measure F"
   1.138    interpret prob_space ?F
   1.139 -  proof
   1.140 -    have "ennreal (1 - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
   1.141 -      by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
   1.142 -                lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
   1.143 -                lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
   1.144 -                filterlim_uminus_at_top[THEN iffD1])
   1.145 -         (auto simp: incseq_def nondecF intro!: diff_mono)
   1.146 -    also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
   1.147 -      by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
   1.148 -    also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
   1.149 -      by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
   1.150 -    also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
   1.151 -      by (simp add: UN_Ioc_eq_UNIV)
   1.152 -    finally show "emeasure ?F (space ?F) = 1"
   1.153 -      by (simp add: one_ereal_def)
   1.154 -  qed
   1.155 +    proof qed (use interval_measure_UNIV[OF assms] in simp)
   1.156    show ?thesis
   1.157      proof qed simp_all
   1.158  qed
   1.159  
   1.160 -lemma cdf_interval_measure:
   1.161 +lemma
   1.162    fixes F :: "real \<Rightarrow> real"
   1.163    assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
   1.164      right_cont_F : "\<And>a. continuous (at_right a) F" and
   1.165 -    lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
   1.166 -    lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
   1.167 -  shows "cdf (interval_measure F) = F"
   1.168 +    lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
   1.169 +  shows emeasure_interval_measure_Iic: "emeasure (interval_measure F) {.. x} = F x"
   1.170 +    and measure_interval_measure_Iic: "measure (interval_measure F) {.. x} = F x"
   1.171    unfolding cdf_def
   1.172 -proof (intro ext)
   1.173 -  interpret real_distribution "interval_measure F"
   1.174 -    by (rule real_distribution_interval_measure) fact+
   1.175 -  fix x
   1.176 -  have "F x - 0 = measure (interval_measure F) (\<Union>i::nat. {-real i <.. x})"
   1.177 -  proof (intro LIMSEQ_unique[OF _ finite_Lim_measure_incseq])
   1.178 +proof -
   1.179 +  have F_nonneg[simp]: "0 \<le> F y" for y
   1.180 +    using lim_F_at_bot by (rule tendsto_upperbound) (auto simp: eventually_at_bot_linorder nondecF intro!: exI[of _ y])
   1.181 +
   1.182 +  have "emeasure (interval_measure F) (\<Union>i::nat. {-real i <.. x}) = F x - ennreal 0"
   1.183 +  proof (intro LIMSEQ_unique[OF Lim_emeasure_incseq])
   1.184      have "(\<lambda>i. F x - F (- real i)) \<longlonglongrightarrow> F x - 0"
   1.185        by (intro tendsto_intros lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
   1.186                  filterlim_uminus_at_top[THEN iffD1])
   1.187 -    then show "(\<lambda>i. measure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - 0"
   1.188 -      apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
   1.189 +    from tendsto_ennrealI[OF this]
   1.190 +    show "(\<lambda>i. emeasure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - ennreal 0"
   1.191 +      apply (rule filterlim_cong[THEN iffD1, rotated 3])
   1.192 +        apply simp
   1.193 +       apply simp
   1.194        apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
   1.195 -      apply (simp add: measure_interval_measure_Ioc right_cont_F nondecF)
   1.196 +      apply (simp add: emeasure_interval_measure_Ioc right_cont_F nondecF)
   1.197        done
   1.198    qed (auto simp: incseq_def)
   1.199    also have "(\<Union>i::nat. {-real i <.. x}) = {..x}"
   1.200      by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
   1.201 -  finally show "measure (interval_measure F) {..x} = F x"
   1.202 +  finally show "emeasure (interval_measure F) {..x} = F x"
   1.203      by simp
   1.204 +  then show "measure (interval_measure F) {..x} = F x"
   1.205 +    by (simp add: measure_def)
   1.206  qed
   1.207  
   1.208 +lemma cdf_interval_measure:
   1.209 +  "(\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow> (F \<longlongrightarrow> 0) at_bot \<Longrightarrow> cdf (interval_measure F) = F"
   1.210 +  by (simp add: cdf_def fun_eq_iff measure_interval_measure_Iic)
   1.211 +
   1.212  end