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
```