author hoelzl Thu Oct 20 18:42:01 2016 +0200 (2016-10-20) changeset 64321 95be866e49fc parent 64320 ba194424b895 child 64323 20d15328b248
HOL-Probability: generalize theorems about cumulative distribution function
```     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.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
```