src/HOL/Probability/Regularity.thy
changeset 50245 dea9363887a6
parent 50244 de72bbe42190
child 50530 6266e44b3396
     1.1 --- a/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4  qed
     1.5  
     1.6  lemma
     1.7 -  fixes M::"'a::{enumerable_basis, complete_space} measure"
     1.8 +  fixes M::"'a::{countable_basis_space, complete_space} measure"
     1.9    assumes sb: "sets M = sets borel"
    1.10    assumes "emeasure M (space M) \<noteq> \<infinity>"
    1.11    assumes "B \<in> sets borel"
    1.12 @@ -124,43 +124,48 @@
    1.13      (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ereal e) \<Longrightarrow> ?outer A"
    1.14      by (rule ereal_approx_INF)
    1.15         (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
    1.16 -  from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
    1.17 +  from countable_dense_setE guess X::"'a set"  . note X = this
    1.18    {
    1.19      fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
    1.20 -    with x[OF this]
    1.21 -    have x: "space M = (\<Union>n. cball (x n) r)"
    1.22 +    with X(2)[OF this]
    1.23 +    have x: "space M = (\<Union>x\<in>X. cball x r)"
    1.24        by (auto simp add: sU) (metis dist_commute order_less_imp_le)
    1.25 -    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r))"
    1.26 +    let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"
    1.27 +    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M ?U"
    1.28        by (rule Lim_emeasure_incseq)
    1.29          (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
    1.30 -    also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
    1.31 -      unfolding x by force
    1.32 -    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
    1.33 +    also have "?U = space M"
    1.34 +    proof safe
    1.35 +      fix x from X(2)[OF open_ball[of x r]] `r > 0` obtain d where d: "d\<in>X" "d \<in> ball x r" by auto
    1.36 +      show "x \<in> ?U"
    1.37 +        using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
    1.38 +    qed (simp add: sU)
    1.39 +    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M (space M)" .
    1.40    } note M_space = this
    1.41    {
    1.42      fix e ::real and n :: nat assume "e > 0" "n > 0"
    1.43      hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
    1.44      from M_space[OF `1/n>0`]
    1.45 -    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
    1.46 +    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
    1.47        unfolding emeasure_eq_measure by simp
    1.48      from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
    1.49 -    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
    1.50 +    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
    1.51        e * 2 powr -n"
    1.52        by auto
    1.53 -    hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
    1.54 +    hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
    1.55        measure M (space M) - e * 2 powr -real n"
    1.56        by (auto simp: dist_real_def)
    1.57 -    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
    1.58 +    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
    1.59        measure M (space M) - e * 2 powr - real n" ..
    1.60    } note k=this
    1.61    hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
    1.62 -    measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
    1.63 +    measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
    1.64      by blast
    1.65    then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
    1.66 -    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
    1.67 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    1.68      apply atomize_elim unfolding bchoice_iff .
    1.69    hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
    1.70 -    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
    1.71 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    1.72      unfolding Ball_def by blast
    1.73    have approx_space:
    1.74      "\<And>e. e > 0 \<Longrightarrow>
    1.75 @@ -168,7 +173,7 @@
    1.76        (is "\<And>e. _ \<Longrightarrow> ?thesis e")
    1.77    proof -
    1.78      fix e :: real assume "e > 0"
    1.79 -    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
    1.80 +    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)"
    1.81      have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
    1.82      hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
    1.83      from k[OF `e > 0` zero_less_Suc]
    1.84 @@ -202,7 +207,7 @@
    1.85        show "complete K" using `closed K` by (simp add: complete_eq_closed)
    1.86        fix e'::real assume "0 < e'"
    1.87        from nat_approx_posE[OF this] guess n . note n = this
    1.88 -      let ?k = "x ` {0..k e (Suc n)}"
    1.89 +      let ?k = "from_nat_into X ` {0..k e (Suc n)}"
    1.90        have "finite ?k" by simp
    1.91        moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
    1.92        ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast