1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy Thu Nov 15 10:49:58 2012 +0100
1.3 @@ -0,0 +1,111 @@
1.4 +(* Author: Fabian Immler, TUM *)
1.5 +
1.6 +header {* Sequence of Properties on Subsequences *}
1.7 +
1.8 +theory Diagonal_Subsequence
1.9 +imports SEQ
1.10 +begin
1.11 +
1.12 +locale subseqs =
1.13 + fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
1.14 + assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
1.15 +begin
1.16 +
1.17 +primrec seqseq where
1.18 + "seqseq 0 = id"
1.19 +| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
1.20 +
1.21 +lemma seqseq_ex:
1.22 + shows "subseq (seqseq n) \<and>
1.23 + (\<exists>r'. seqseq (Suc n) = seqseq n o r' \<and> subseq r' \<and> P n (seqseq n o r'))"
1.24 +proof (induct n)
1.25 + case 0
1.26 + let ?P = "\<lambda>r'. subseq r' \<and> P 0 r'"
1.27 + let ?r = "Eps ?P"
1.28 + have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def)
1.29 + thus ?case by (auto simp: subseq_def)
1.30 +next
1.31 + case (Suc n)
1.32 + then obtain r' where
1.33 + Suc': "seqseq (Suc n) = seqseq n \<circ> r'" "subseq (seqseq n)" "subseq r'"
1.34 + "P n (seqseq n o r')"
1.35 + by blast
1.36 + let ?P = "\<lambda>r'a. subseq (r'a ) \<and> P (Suc n) (seqseq n o r' o r'a)"
1.37 + let ?r = "Eps ?P"
1.38 + have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc'
1.39 + by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc)
1.40 + moreover have "seqseq (Suc (Suc n)) = seqseq n \<circ> r' \<circ> ?r"
1.41 + by (subst seqseq.simps) (simp only: Suc' o_assoc)
1.42 + moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`]
1.43 + ultimately show ?case unfolding Suc' by (auto simp: o_def)
1.44 +qed
1.45 +
1.46 +lemma subseq_seqseq:
1.47 + shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto
1.48 +
1.49 +definition reducer where "reducer n = (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
1.50 +
1.51 +lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n o reducer n)"
1.52 + unfolding atomize_conj unfolding reducer_def using subseq_seqseq
1.53 + by (rule someI_ex[OF ex_subseq])
1.54 +
1.55 +lemma seqseq_reducer[simp]:
1.56 + "seqseq (Suc n) = seqseq n o reducer n"
1.57 + by (simp add: reducer_def)
1.58 +
1.59 +declare seqseq.simps(2)[simp del]
1.60 +
1.61 +definition diagseq where "diagseq i = seqseq i i"
1.62 +
1.63 +lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
1.64 + unfolding diagseq_def seqseq_reducer o_def
1.65 + by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer)
1.66 +
1.67 +lemma subseq_diagseq: "subseq diagseq"
1.68 + using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
1.69 +
1.70 +primrec fold_reduce where
1.71 + "fold_reduce n 0 = id"
1.72 +| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)"
1.73 +
1.74 +lemma subseq_fold_reduce: "subseq (fold_reduce n k)"
1.75 +proof (induct k)
1.76 + case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def)
1.77 +qed (simp add: subseq_def)
1.78 +
1.79 +lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
1.80 + by (induct k) simp_all
1.81 +
1.82 +lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
1.83 + by (induct n) (simp_all)
1.84 +
1.85 +lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
1.86 + using seqseq_fold_reduce by (simp add: diagseq_def)
1.87 +
1.88 +lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
1.89 + by (induct n) simp_all
1.90 +
1.91 +lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
1.92 +proof -
1.93 + have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
1.94 + by (simp add: diagseq_fold_reduce)
1.95 + also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)"
1.96 + unfolding fold_reduce_add seqseq_fold_reduce ..
1.97 + finally show ?thesis .
1.98 +qed
1.99 +
1.100 +lemma diagseq_sub:
1.101 + assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
1.102 + using diagseq_add[of m "n - m"] assms by simp
1.103 +
1.104 +lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
1.105 + unfolding subseq_Suc_iff fold_reduce.simps o_def
1.106 + by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble
1.107 + subseq_reducer)
1.108 +
1.109 +lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))"
1.110 + by (auto simp: o_def diagseq_add)
1.111 +
1.112 +end
1.113 +
1.114 +end
2.1 --- a/src/HOL/Library/Library.thy Thu Nov 15 14:04:23 2012 +0100
2.2 +++ b/src/HOL/Library/Library.thy Thu Nov 15 10:49:58 2012 +0100
2.3 @@ -13,6 +13,7 @@
2.4 Convex
2.5 Countable
2.6 Debug
2.7 + Diagonal_Subsequence
2.8 Dlist
2.9 Eval_Witness
2.10 Extended_Nat
3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 15 14:04:23 2012 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 15 10:49:58 2012 +0100
3.3 @@ -7,9 +7,210 @@
3.4 header {* Elementary topology in Euclidean space. *}
3.5
3.6 theory Topology_Euclidean_Space
3.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
3.8 +imports
3.9 + SEQ
3.10 + "~~/src/HOL/Library/Diagonal_Subsequence"
3.11 + "~~/src/HOL/Library/Countable"
3.12 + Linear_Algebra
3.13 + "~~/src/HOL/Library/Glbs"
3.14 + Norm_Arith
3.15 begin
3.16
3.17 +subsection {* Topological Basis *}
3.18 +
3.19 +context topological_space
3.20 +begin
3.21 +
3.22 +definition "topological_basis B =
3.23 + ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
3.24 +
3.25 +lemma topological_basis_iff:
3.26 + assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
3.27 + shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
3.28 + (is "_ \<longleftrightarrow> ?rhs")
3.29 +proof safe
3.30 + fix O' and x::'a
3.31 + assume H: "topological_basis B" "open O'" "x \<in> O'"
3.32 + hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
3.33 + then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
3.34 + thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
3.35 +next
3.36 + assume H: ?rhs
3.37 + show "topological_basis B" using assms unfolding topological_basis_def
3.38 + proof safe
3.39 + fix O'::"'a set" assume "open O'"
3.40 + with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
3.41 + by (force intro: bchoice simp: Bex_def)
3.42 + thus "\<exists>B'\<subseteq>B. \<Union>B' = O'"
3.43 + by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
3.44 + qed
3.45 +qed
3.46 +
3.47 +lemma topological_basisI:
3.48 + assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
3.49 + assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
3.50 + shows "topological_basis B"
3.51 + using assms by (subst topological_basis_iff) auto
3.52 +
3.53 +lemma topological_basisE:
3.54 + fixes O'
3.55 + assumes "topological_basis B"
3.56 + assumes "open O'"
3.57 + assumes "x \<in> O'"
3.58 + obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
3.59 +proof atomize_elim
3.60 + from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" by (simp add: topological_basis_def)
3.61 + with topological_basis_iff assms
3.62 + show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def)
3.63 +qed
3.64 +
3.65 +end
3.66 +
3.67 +subsection {* Enumerable Basis *}
3.68 +
3.69 +class enumerable_basis = topological_space +
3.70 + assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a set. topological_basis (range f)"
3.71 +begin
3.72 +
3.73 +definition enum_basis'::"nat \<Rightarrow> 'a set"
3.74 + where "enum_basis' = Eps (topological_basis o range)"
3.75 +
3.76 +lemma enumerable_basis': "topological_basis (range enum_basis')"
3.77 + using ex_enum_basis
3.78 + unfolding enum_basis'_def o_def
3.79 + by (rule someI_ex)
3.80 +
3.81 +lemmas enumerable_basisE' = topological_basisE[OF enumerable_basis']
3.82 +
3.83 +text {* Extend enumeration of basis, such that it is closed under (finite) Union *}
3.84 +
3.85 +definition enum_basis::"nat \<Rightarrow> 'a set"
3.86 + where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
3.87 +
3.88 +lemma
3.89 + open_enum_basis:
3.90 + assumes "B \<in> range enum_basis"
3.91 + shows "open B"
3.92 + using assms enumerable_basis'
3.93 + by (force simp add: topological_basis_def enum_basis_def)
3.94 +
3.95 +lemma enumerable_basis: "topological_basis (range enum_basis)"
3.96 +proof (rule topological_basisI[OF open_enum_basis])
3.97 + fix O' x assume "open O'" "x \<in> O'"
3.98 + from topological_basisE[OF enumerable_basis' this] guess B' . note B' = this
3.99 + moreover then obtain n where "B' = enum_basis' n" by auto
3.100 + moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
3.101 + ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
3.102 +qed
3.103 +
3.104 +lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
3.105 +
3.106 +lemma open_enumerable_basis_ex:
3.107 + assumes "open X"
3.108 + shows "\<exists>N. X = (\<Union>n\<in>N. enum_basis n)"
3.109 +proof -
3.110 + from enumerable_basis assms obtain B' where "B' \<subseteq> range enum_basis" "X = Union B'"
3.111 + unfolding topological_basis_def by blast
3.112 + hence "Union B' = (\<Union>n\<in>{n. enum_basis n \<in> B'}. enum_basis n)" by auto
3.113 + with `X = Union B'` show ?thesis by blast
3.114 +qed
3.115 +
3.116 +lemma open_enumerable_basisE:
3.117 + assumes "open X"
3.118 + obtains N where "X = (\<Union>n\<in>N. enum_basis n)"
3.119 + using assms open_enumerable_basis_ex by (atomize_elim) simp
3.120 +
3.121 +lemma countable_dense_set:
3.122 + shows "\<exists>x::nat \<Rightarrow> _. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
3.123 +proof -
3.124 + def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> enum_basis n)"
3.125 + have x: "\<And>n. enum_basis n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> enum_basis n" unfolding x_def
3.126 + by (rule someI_ex) auto
3.127 + have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
3.128 + proof (intro allI impI)
3.129 + fix y::"'a set" assume "open y" "y \<noteq> {}"
3.130 + from open_enumerable_basisE[OF `open y`] guess N . note N = this
3.131 + obtain n where n: "n \<in> N" "enum_basis n \<noteq> ({}::'a set)"
3.132 + proof (atomize_elim, rule ccontr, clarsimp)
3.133 + assume "\<forall>n. n \<in> N \<longrightarrow> enum_basis n = ({}::'a set)"
3.134 + hence "(\<Union>n\<in>N. enum_basis n) = (\<Union>n\<in>N. {}::'a set)"
3.135 + by (intro UN_cong) auto
3.136 + hence "y = {}" unfolding N by simp
3.137 + with `y \<noteq> {}` show False by auto
3.138 + qed
3.139 + with x N n have "x n \<in> y" by auto
3.140 + thus "\<exists>n. x n \<in> y" ..
3.141 + qed
3.142 + thus ?thesis by blast
3.143 +qed
3.144 +
3.145 +lemma countable_dense_setE:
3.146 + obtains x :: "nat \<Rightarrow> _"
3.147 + where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
3.148 + using countable_dense_set by blast
3.149 +
3.150 +text {* Construction of an Increasing Sequence Approximating Open Sets *}
3.151 +
3.152 +lemma empty_basisI[intro]: "{} \<in> range enum_basis"
3.153 +proof
3.154 + show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
3.155 +qed rule
3.156 +
3.157 +lemma union_basisI[intro]:
3.158 + assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
3.159 + shows "A \<union> B \<in> range enum_basis"
3.160 +proof -
3.161 + from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
3.162 + also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
3.163 + by (simp add: enum_basis_def)
3.164 + finally show ?thesis by simp
3.165 +qed
3.166 +
3.167 +lemma open_imp_Union_of_incseq:
3.168 + assumes "open X"
3.169 + shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
3.170 +proof -
3.171 + from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
3.172 + hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
3.173 + def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
3.174 + (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
3.175 + have S_simps[simp]:
3.176 + "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
3.177 + "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
3.178 + by (simp_all add: S_def)
3.179 + have "incseq S" by (rule incseq_SucI) auto
3.180 + moreover
3.181 + have "(\<Union>j. S j) = X" unfolding N
3.182 + proof safe
3.183 + fix x n assume "n \<in> N" "x \<in> enum_basis n"
3.184 + hence "x \<in> S n" by (cases n) auto
3.185 + thus "x \<in> (\<Union>j. S j)" by auto
3.186 + next
3.187 + fix x j
3.188 + assume "x \<in> S j"
3.189 + thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
3.190 + qed
3.191 + moreover have "range S \<subseteq> range enum_basis"
3.192 + proof safe
3.193 + fix j show "S j \<in> range enum_basis" by (induct j) auto
3.194 + qed
3.195 + ultimately show ?thesis by auto
3.196 +qed
3.197 +
3.198 +lemma open_incseqE:
3.199 + assumes "open X"
3.200 + obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
3.201 + using open_imp_Union_of_incseq assms by atomize_elim
3.202 +
3.203 +end
3.204 +
3.205 +subsection {* Polish spaces *}
3.206 +
3.207 +text {* Textbooks define Polish spaces as completely metrizable.
3.208 + We assume the topology to be complete for a given metric. *}
3.209 +
3.210 +class polish_space = complete_space + enumerable_basis
3.211 +
3.212 subsection {* General notion of a topology as a value *}
3.213
3.214 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
3.215 @@ -377,6 +578,86 @@
3.216
3.217 lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
3.218
3.219 +lemma rational_boxes:
3.220 + fixes x :: "'a\<Colon>ordered_euclidean_space"
3.221 + assumes "0 < e"
3.222 + shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
3.223 +proof -
3.224 + def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
3.225 + then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
3.226 + have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
3.227 + proof
3.228 + fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
3.229 + show "?th i" by auto
3.230 + qed
3.231 + from choice[OF this] guess a .. note a = this
3.232 + have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
3.233 + proof
3.234 + fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
3.235 + show "?th i" by auto
3.236 + qed
3.237 + from choice[OF this] guess b .. note b = this
3.238 + { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
3.239 + have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
3.240 + unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
3.241 + also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
3.242 + proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
3.243 + fix i assume i: "i \<in> {..<DIM('a)}"
3.244 + have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
3.245 + moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
3.246 + moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
3.247 + ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
3.248 + then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
3.249 + unfolding e'_def by (auto simp: dist_real_def)
3.250 + then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
3.251 + by (rule power_strict_mono) auto
3.252 + then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
3.253 + by (simp add: power_divide)
3.254 + qed auto
3.255 + also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
3.256 + finally have "dist x y < e" . }
3.257 + with a b show ?thesis
3.258 + apply (rule_tac exI[of _ "Chi a"])
3.259 + apply (rule_tac exI[of _ "Chi b"])
3.260 + using eucl_less[where 'a='a] by auto
3.261 +qed
3.262 +
3.263 +lemma ex_rat_list:
3.264 + fixes x :: "'a\<Colon>ordered_euclidean_space"
3.265 + assumes "\<And> i. x $$ i \<in> \<rat>"
3.266 + shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
3.267 +proof -
3.268 + have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
3.269 + from choice[OF this] guess r ..
3.270 + then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
3.271 +qed
3.272 +
3.273 +lemma open_UNION:
3.274 + fixes M :: "'a\<Colon>ordered_euclidean_space set"
3.275 + assumes "open M"
3.276 + shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
3.277 + (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
3.278 + (is "M = UNION ?idx ?box")
3.279 +proof safe
3.280 + fix x assume "x \<in> M"
3.281 + obtain e where e: "e > 0" "ball x e \<subseteq> M"
3.282 + using openE[OF assms `x \<in> M`] by auto
3.283 + then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
3.284 + using rational_boxes[OF e(1)] by blast
3.285 + then obtain p q where pq: "length p = DIM ('a)"
3.286 + "length q = DIM ('a)"
3.287 + "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
3.288 + using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
3.289 + hence p: "Chi (of_rat \<circ> op ! p) = a"
3.290 + using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
3.291 + unfolding o_def by auto
3.292 + from pq have q: "Chi (of_rat \<circ> op ! q) = b"
3.293 + using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
3.294 + unfolding o_def by auto
3.295 + have "x \<in> ?box (p, q)"
3.296 + using p q ab by auto
3.297 + thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
3.298 +qed auto
3.299
3.300 subsection{* Connectedness *}
3.301
3.302 @@ -803,7 +1084,6 @@
3.303 using frontier_complement frontier_subset_eq[of "- S"]
3.304 unfolding open_closed by auto
3.305
3.306 -
3.307 subsection {* Filters and the ``eventually true'' quantifier *}
3.308
3.309 definition
3.310 @@ -1361,6 +1641,121 @@
3.311 shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
3.312 by (metis closure_closed closure_approachable)
3.313
3.314 +subsection {* Infimum Distance *}
3.315 +
3.316 +definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
3.317 +
3.318 +lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
3.319 + by (simp add: infdist_def)
3.320 +
3.321 +lemma infdist_nonneg:
3.322 + shows "0 \<le> infdist x A"
3.323 + using assms by (auto simp add: infdist_def)
3.324 +
3.325 +lemma infdist_le:
3.326 + assumes "a \<in> A"
3.327 + assumes "d = dist x a"
3.328 + shows "infdist x A \<le> d"
3.329 + using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
3.330 +
3.331 +lemma infdist_zero[simp]:
3.332 + assumes "a \<in> A" shows "infdist a A = 0"
3.333 +proof -
3.334 + from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0" by auto
3.335 + with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto
3.336 +qed
3.337 +
3.338 +lemma infdist_triangle:
3.339 + shows "infdist x A \<le> infdist y A + dist x y"
3.340 +proof cases
3.341 + assume "A = {}" thus ?thesis by (simp add: infdist_def)
3.342 +next
3.343 + assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
3.344 + have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
3.345 + proof
3.346 + from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
3.347 + fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
3.348 + then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
3.349 + show "infdist x A \<le> d"
3.350 + unfolding infdist_notempty[OF `A \<noteq> {}`]
3.351 + proof (rule Inf_lower2)
3.352 + show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
3.353 + show "dist x a \<le> d" unfolding d by (rule dist_triangle)
3.354 + fix d assume "d \<in> {dist x a |a. a \<in> A}"
3.355 + then obtain a where "a \<in> A" "d = dist x a" by auto
3.356 + thus "infdist x A \<le> d" by (rule infdist_le)
3.357 + qed
3.358 + qed
3.359 + also have "\<dots> = dist x y + infdist y A"
3.360 + proof (rule Inf_eq, safe)
3.361 + fix a assume "a \<in> A"
3.362 + thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
3.363 + next
3.364 + fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
3.365 + hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
3.366 + by (intro Inf_greatest) (auto simp: field_simps)
3.367 + thus "i \<le> dist x y + infdist y A" by simp
3.368 + qed
3.369 + finally show ?thesis by simp
3.370 +qed
3.371 +
3.372 +lemma
3.373 + in_closure_iff_infdist_zero:
3.374 + assumes "A \<noteq> {}"
3.375 + shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
3.376 +proof
3.377 + assume "x \<in> closure A"
3.378 + show "infdist x A = 0"
3.379 + proof (rule ccontr)
3.380 + assume "infdist x A \<noteq> 0"
3.381 + with infdist_nonneg[of x A] have "infdist x A > 0" by auto
3.382 + hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
3.383 + by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
3.384 + eucl_less_not_refl euclidean_trans(2) infdist_le)
3.385 + hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
3.386 + thus False using `x \<in> closure A` by simp
3.387 + qed
3.388 +next
3.389 + assume x: "infdist x A = 0"
3.390 + then obtain a where "a \<in> A" by atomize_elim (metis all_not_in_conv assms)
3.391 + show "x \<in> closure A" unfolding closure_approachable
3.392 + proof (safe, rule ccontr)
3.393 + fix e::real assume "0 < e"
3.394 + assume "\<not> (\<exists>y\<in>A. dist y x < e)"
3.395 + hence "infdist x A \<ge> e" using `a \<in> A`
3.396 + unfolding infdist_def
3.397 + by (force intro: Inf_greatest simp: dist_commute)
3.398 + with x `0 < e` show False by auto
3.399 + qed
3.400 +qed
3.401 +
3.402 +lemma
3.403 + in_closed_iff_infdist_zero:
3.404 + assumes "closed A" "A \<noteq> {}"
3.405 + shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
3.406 +proof -
3.407 + have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
3.408 + by (rule in_closure_iff_infdist_zero) fact
3.409 + with assms show ?thesis by simp
3.410 +qed
3.411 +
3.412 +lemma tendsto_infdist [tendsto_intros]:
3.413 + assumes f: "(f ---> l) F"
3.414 + shows "((\<lambda>x. infdist (f x) A) ---> infdist l A) F"
3.415 +proof (rule tendstoI)
3.416 + fix e ::real assume "0 < e"
3.417 + from tendstoD[OF f this]
3.418 + show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
3.419 + proof (eventually_elim)
3.420 + fix x
3.421 + from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
3.422 + have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
3.423 + by (simp add: dist_commute dist_real_def)
3.424 + also assume "dist (f x) l < e"
3.425 + finally show "dist (infdist (f x) A) (infdist l A) < e" .
3.426 + qed
3.427 +qed
3.428 +
3.429 text{* Some other lemmas about sequences. *}
3.430
3.431 lemma sequentially_offset:
3.432 @@ -2696,6 +3091,157 @@
3.433 assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
3.434 qed
3.435
3.436 +lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
3.437 + by metis
3.438 +
3.439 +lemma nat_approx_posE:
3.440 + fixes e::real
3.441 + assumes "0 < e"
3.442 + obtains n::nat where "1 / (Suc n) < e"
3.443 +proof atomize_elim
3.444 + have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
3.445 + by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
3.446 + also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
3.447 + by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
3.448 + also have "\<dots> = e" by simp
3.449 + finally show "\<exists>n. 1 / real (Suc n) < e" ..
3.450 +qed
3.451 +
3.452 +lemma compact_eq_totally_bounded:
3.453 + shows "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
3.454 +proof (safe intro!: compact_imp_complete)
3.455 + fix e::real
3.456 + def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
3.457 + assume "0 < e" "compact s"
3.458 + hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
3.459 + by (simp add: compact_eq_heine_borel)
3.460 + moreover
3.461 + have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
3.462 + hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
3.463 + ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
3.464 + then guess K .. note K = this
3.465 + have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
3.466 + then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
3.467 + thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
3.468 + by (intro exI[where x="k ` K"]) (auto simp: f_def)
3.469 +next
3.470 + assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
3.471 + show "compact s"
3.472 + proof cases
3.473 + assume "s = {}" thus "compact s" by (simp add: compact_def)
3.474 + next
3.475 + assume "s \<noteq> {}"
3.476 + show ?thesis
3.477 + unfolding compact_def
3.478 + proof safe
3.479 + fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
3.480 + from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
3.481 + then obtain K where
3.482 + K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
3.483 + unfolding choice_iff by blast
3.484 + {
3.485 + fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
3.486 + assume "e > 0"
3.487 + from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
3.488 + by simp_all
3.489 + have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
3.490 + proof (rule ccontr)
3.491 + from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
3.492 + using `s \<noteq> {}`
3.493 + by auto
3.494 + moreover
3.495 + assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
3.496 + hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
3.497 + ultimately
3.498 + show False using f'
3.499 + proof (induct arbitrary: s f f' rule: finite_ne_induct)
3.500 + case (singleton x)
3.501 + have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
3.502 + thus ?case using singleton by (auto simp: ball_def)
3.503 + next
3.504 + case (insert x A)
3.505 + show ?case
3.506 + proof cases
3.507 + have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
3.508 + have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
3.509 + using insert by (intro infinite_super[OF _ inf_ms]) auto
3.510 + also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
3.511 + {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
3.512 + finally have "infinite \<dots>" .
3.513 + moreover assume "finite {m. (f o f') m \<in> ball x e}"
3.514 + ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
3.515 + hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
3.516 + def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
3.517 + have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
3.518 + using enumerate_mono[OF _ inf] by (simp add: r_def)
3.519 + hence "subseq r" by (simp add: subseq_def)
3.520 + have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
3.521 + using enumerate_in_set[OF inf] by (simp add: r_def)
3.522 + show False
3.523 + proof (rule insert)
3.524 + show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
3.525 + fix k s assume "k \<in> A" "subseq s"
3.526 + thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
3.527 + by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
3.528 + next
3.529 + fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
3.530 + qed
3.531 + next
3.532 + assume inf: "infinite {m. (f o f') m \<in> ball x e}"
3.533 + def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
3.534 + have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
3.535 + using enumerate_mono[OF _ inf] by (simp add: r_def)
3.536 + hence "subseq r" by (simp add: subseq_def)
3.537 + from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
3.538 + moreover
3.539 + have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
3.540 + using enumerate_in_set[OF inf] by (simp add: r_def)
3.541 + hence "(f o f') (r i) \<in> ball x e" by simp
3.542 + ultimately show False by simp
3.543 + qed
3.544 + qed
3.545 + qed
3.546 + }
3.547 + hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
3.548 + let ?e = "\<lambda>n. 1 / real (Suc n)"
3.549 + let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
3.550 + interpret subseqs ?P using ex by unfold_locales force
3.551 + from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
3.552 + by (simp add: complete_def)
3.553 + have "\<exists>l\<in>s. (f o diagseq) ----> l"
3.554 + proof (intro limI metric_CauchyI)
3.555 + fix e::real assume "0 < e" hence "0 < e / 2" by auto
3.556 + from nat_approx_posE[OF this] guess n . note n = this
3.557 + show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
3.558 + proof (rule exI[where x="Suc n"], safe)
3.559 + fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
3.560 + let ?e = "1 / real (Suc n)"
3.561 + from reducer_reduces[of n] obtain k where
3.562 + "k\<in>K ?e" "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
3.563 + unfolding seqseq_reducer by auto
3.564 + moreover
3.565 + note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
3.566 + ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
3.567 + also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
3.568 + finally
3.569 + have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
3.570 + by (intro add_strict_mono) auto
3.571 + hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
3.572 + by (simp add: dist_commute)
3.573 + moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
3.574 + dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
3.575 + by (rule dist_triangle2)
3.576 + ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
3.577 + by simp
3.578 + qed
3.579 + next
3.580 + fix n show "(f o diagseq) n \<in> s" using f by simp
3.581 + qed
3.582 + thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
3.583 + qed
3.584 + qed
3.585 +qed
3.586 +
3.587 lemma compact_eq_bounded_closed:
3.588 fixes s :: "'a::heine_borel set"
3.589 shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs")
3.590 @@ -2738,9 +3284,6 @@
3.591 unfolding compact_def
3.592 by simp
3.593
3.594 -lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
3.595 - unfolding subseq_def by simp (* TODO: move somewhere else *)
3.596 -
3.597 lemma compact_union [intro]:
3.598 assumes "compact s" and "compact t"
3.599 shows "compact (s \<union> t)"
3.600 @@ -2771,6 +3314,13 @@
3.601 qed
3.602 qed
3.603
3.604 +lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
3.605 + by (induct set: finite) auto
3.606 +
3.607 +lemma compact_UN [intro]:
3.608 + "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
3.609 + unfolding SUP_def by (rule compact_Union) auto
3.610 +
3.611 lemma compact_inter_closed [intro]:
3.612 assumes "compact s" and "closed t"
3.613 shows "compact (s \<inter> t)"
3.614 @@ -3294,6 +3844,11 @@
3.615 shows "continuous F (\<lambda>x. dist (f x) (g x))"
3.616 using assms unfolding continuous_def by (rule tendsto_dist)
3.617
3.618 +lemma continuous_infdist:
3.619 + assumes "continuous F f"
3.620 + shows "continuous F (\<lambda>x. infdist (f x) A)"
3.621 + using assms unfolding continuous_def by (rule tendsto_infdist)
3.622 +
3.623 lemma continuous_norm:
3.624 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
3.625 unfolding continuous_def by (rule tendsto_norm)
3.626 @@ -4886,6 +5441,39 @@
3.627 thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
3.628 qed
3.629
3.630 +instance ordered_euclidean_space \<subseteq> enumerable_basis
3.631 +proof
3.632 + def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
3.633 + def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
3.634 + have "Ball (range enum) open" unfolding enum_def
3.635 + proof safe
3.636 + fix n show "open (to_cube (from_nat n))"
3.637 + by (cases "from_nat n::rat list \<times> rat list")
3.638 + (simp add: open_interval to_cube_def)
3.639 + qed
3.640 + moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
3.641 + proof safe
3.642 + fix x::"'a set" assume "open x"
3.643 + def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
3.644 + from open_UNION[OF `open x`]
3.645 + have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
3.646 + by simp
3.647 + moreover have "to_cube ` lists \<subseteq> range enum"
3.648 + proof
3.649 + fix x assume "x \<in> to_cube ` lists"
3.650 + then obtain l where "l \<in> lists" "x = to_cube l" by auto
3.651 + hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
3.652 + thus "x \<in> range enum" by simp
3.653 + qed
3.654 + ultimately
3.655 + show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
3.656 + qed
3.657 + ultimately
3.658 + show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
3.659 +qed
3.660 +
3.661 +instance ordered_euclidean_space \<subseteq> polish_space ..
3.662 +
3.663 text {* Intervals in general, including infinite and mixtures of open and closed. *}
3.664
3.665 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
4.1 --- a/src/HOL/Probability/Borel_Space.thy Thu Nov 15 14:04:23 2012 +0100
4.2 +++ b/src/HOL/Probability/Borel_Space.thy Thu Nov 15 10:49:58 2012 +0100
4.3 @@ -173,87 +173,6 @@
4.4
4.5 subsection "Borel space equals sigma algebras over intervals"
4.6
4.7 -lemma rational_boxes:
4.8 - fixes x :: "'a\<Colon>ordered_euclidean_space"
4.9 - assumes "0 < e"
4.10 - shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
4.11 -proof -
4.12 - def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
4.13 - then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
4.14 - have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
4.15 - proof
4.16 - fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
4.17 - show "?th i" by auto
4.18 - qed
4.19 - from choice[OF this] guess a .. note a = this
4.20 - have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
4.21 - proof
4.22 - fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
4.23 - show "?th i" by auto
4.24 - qed
4.25 - from choice[OF this] guess b .. note b = this
4.26 - { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
4.27 - have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
4.28 - unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
4.29 - also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
4.30 - proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
4.31 - fix i assume i: "i \<in> {..<DIM('a)}"
4.32 - have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
4.33 - moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
4.34 - moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
4.35 - ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
4.36 - then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
4.37 - unfolding e'_def by (auto simp: dist_real_def)
4.38 - then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
4.39 - by (rule power_strict_mono) auto
4.40 - then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
4.41 - by (simp add: power_divide)
4.42 - qed auto
4.43 - also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
4.44 - finally have "dist x y < e" . }
4.45 - with a b show ?thesis
4.46 - apply (rule_tac exI[of _ "Chi a"])
4.47 - apply (rule_tac exI[of _ "Chi b"])
4.48 - using eucl_less[where 'a='a] by auto
4.49 -qed
4.50 -
4.51 -lemma ex_rat_list:
4.52 - fixes x :: "'a\<Colon>ordered_euclidean_space"
4.53 - assumes "\<And> i. x $$ i \<in> \<rat>"
4.54 - shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
4.55 -proof -
4.56 - have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
4.57 - from choice[OF this] guess r ..
4.58 - then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
4.59 -qed
4.60 -
4.61 -lemma open_UNION:
4.62 - fixes M :: "'a\<Colon>ordered_euclidean_space set"
4.63 - assumes "open M"
4.64 - shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
4.65 - (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
4.66 - (is "M = UNION ?idx ?box")
4.67 -proof safe
4.68 - fix x assume "x \<in> M"
4.69 - obtain e where e: "e > 0" "ball x e \<subseteq> M"
4.70 - using openE[OF assms `x \<in> M`] by auto
4.71 - then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
4.72 - using rational_boxes[OF e(1)] by blast
4.73 - then obtain p q where pq: "length p = DIM ('a)"
4.74 - "length q = DIM ('a)"
4.75 - "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
4.76 - using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
4.77 - hence p: "Chi (of_rat \<circ> op ! p) = a"
4.78 - using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
4.79 - unfolding o_def by auto
4.80 - from pq have q: "Chi (of_rat \<circ> op ! q) = b"
4.81 - using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
4.82 - unfolding o_def by auto
4.83 - have "x \<in> ?box (p, q)"
4.84 - using p q ab by auto
4.85 - thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
4.86 -qed auto
4.87 -
4.88 lemma borel_sigma_sets_subset:
4.89 "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
4.90 using sigma_sets_subset[of A borel] by simp
4.91 @@ -519,6 +438,39 @@
4.92 by (auto intro: sigma_sets.intros)
4.93 qed auto
4.94
4.95 +lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
4.96 + unfolding borel_def
4.97 +proof (intro sigma_eqI sigma_sets_eqI, safe)
4.98 + fix x :: "'a set" assume "open x"
4.99 + hence "x = UNIV - (UNIV - x)" by auto
4.100 + also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
4.101 + by (rule sigma_sets.Compl)
4.102 + (auto intro!: sigma_sets.Basic simp: `open x`)
4.103 + finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
4.104 +next
4.105 + fix x :: "'a set" assume "closed x"
4.106 + hence "x = UNIV - (UNIV - x)" by auto
4.107 + also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
4.108 + by (rule sigma_sets.Compl)
4.109 + (auto intro!: sigma_sets.Basic simp: `closed x`)
4.110 + finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
4.111 +qed simp_all
4.112 +
4.113 +lemma borel_eq_enum_basis:
4.114 + "borel = sigma UNIV (range enum_basis)"
4.115 + unfolding borel_def
4.116 +proof (intro sigma_eqI sigma_sets_eqI, safe)
4.117 + fix x::"'a set" assume "open x"
4.118 + from open_enumerable_basisE[OF this] guess N .
4.119 + hence x: "x = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
4.120 + also have "\<dots> \<in> sigma_sets UNIV (range enum_basis)" by (rule Union) auto
4.121 + finally show "x \<in> sigma_sets UNIV (range enum_basis)" .
4.122 +next
4.123 + fix n
4.124 + have "open (enum_basis n)" by (rule open_enum_basis) simp
4.125 + thus "enum_basis n \<in> sigma_sets UNIV (Collect open)" by auto
4.126 +qed simp_all
4.127 +
4.128 lemma borel_measurable_halfspacesI:
4.129 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
4.130 assumes F: "borel = sigma UNIV (range F)"
5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 14:04:23 2012 +0100
5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 10:49:58 2012 +0100
5.3 @@ -1161,9 +1161,6 @@
5.4 by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
5.5 qed
5.6
5.7 -lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
5.8 - by metis
5.9 -
5.10 lemma sigma_prod_algebra_sigma_eq:
5.11 fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
5.12 assumes "finite I"
6.1 --- a/src/HOL/Probability/Independent_Family.thy Thu Nov 15 14:04:23 2012 +0100
6.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu Nov 15 10:49:58 2012 +0100
6.3 @@ -8,20 +8,6 @@
6.4 imports Probability_Measure Infinite_Product_Measure
6.5 begin
6.6
6.7 -lemma INT_decseq_offset:
6.8 - assumes "decseq F"
6.9 - shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
6.10 -proof safe
6.11 - fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
6.12 - show "x \<in> F i"
6.13 - proof cases
6.14 - from x have "x \<in> F n" by auto
6.15 - also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
6.16 - unfolding decseq_def by simp
6.17 - finally show ?thesis .
6.18 - qed (insert x, simp)
6.19 -qed auto
6.20 -
6.21 definition (in prob_space)
6.22 "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
6.23 (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
7.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 15 14:04:23 2012 +0100
7.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 15 10:49:58 2012 +0100
7.3 @@ -8,69 +8,6 @@
7.4 imports Probability_Measure Caratheodory Projective_Family
7.5 begin
7.6
7.7 -lemma (in product_prob_space) distr_restrict:
7.8 - assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
7.9 - shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
7.10 -proof (rule measure_eqI_generator_eq)
7.11 - have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
7.12 - interpret J: finite_product_prob_space M J proof qed fact
7.13 - interpret K: finite_product_prob_space M K proof qed fact
7.14 -
7.15 - let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
7.16 - let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
7.17 - let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
7.18 - show "Int_stable ?J"
7.19 - by (rule Int_stable_PiE)
7.20 - show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
7.21 - using `finite J` by (auto intro!: prod_algebraI_finite)
7.22 - { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
7.23 - show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
7.24 - show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
7.25 - using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
7.26 -
7.27 - fix X assume "X \<in> ?J"
7.28 - then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
7.29 - with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
7.30 - by simp
7.31 -
7.32 - have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
7.33 - using E by (simp add: J.measure_times)
7.34 - also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
7.35 - by simp
7.36 - also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
7.37 - using `finite K` `J \<subseteq> K`
7.38 - by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
7.39 - also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
7.40 - using E by (simp add: K.measure_times)
7.41 - also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
7.42 - using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm)
7.43 - finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
7.44 - using X `J \<subseteq> K` apply (subst emeasure_distr)
7.45 - by (auto intro!: measurable_restrict_subset simp: space_PiM)
7.46 -qed
7.47 -
7.48 -lemma (in product_prob_space) emeasure_prod_emb[simp]:
7.49 - assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
7.50 - shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
7.51 - by (subst distr_restrict[OF L])
7.52 - (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
7.53 -
7.54 -sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
7.55 -proof
7.56 - fix J::"'i set" assume "finite J"
7.57 - interpret f: finite_product_prob_space M J proof qed fact
7.58 - show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
7.59 - show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
7.60 - (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
7.61 - (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
7.62 - by (auto simp add: sigma_finite_measure_def)
7.63 - show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
7.64 -qed simp_all
7.65 -
7.66 -lemma (in product_prob_space) PiP_PiM_finite[simp]:
7.67 - assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
7.68 - using assms by (simp add: PiP_finite)
7.69 -
7.70 lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
7.71 assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
7.72 shows "emeasure (Pi\<^isub>M I M) (emb I J (Pi\<^isub>E J X)) = emeasure (Pi\<^isub>M J M) (Pi\<^isub>E J X)"
8.1 --- a/src/HOL/Probability/Measure_Space.thy Thu Nov 15 14:04:23 2012 +0100
8.2 +++ b/src/HOL/Probability/Measure_Space.thy Thu Nov 15 10:49:58 2012 +0100
8.3 @@ -169,6 +169,27 @@
8.4 finally show "f x \<le> f y" by simp
8.5 qed
8.6
8.7 +lemma (in ring_of_sets) subadditive:
8.8 + assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S"
8.9 + shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))"
8.10 +using S
8.11 +proof (induct S)
8.12 + case empty thus ?case using f by (auto simp: positive_def)
8.13 +next
8.14 + case (insert x F)
8.15 + hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
8.16 + have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
8.17 + have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
8.18 + hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
8.19 + by simp
8.20 + also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
8.21 + using f(2) by (rule additiveD) (insert in_M, auto)
8.22 + also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
8.23 + using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
8.24 + also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
8.25 + finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
8.26 +qed
8.27 +
8.28 lemma (in ring_of_sets) countably_additive_additive:
8.29 assumes posf: "positive M f" and ca: "countably_additive M f"
8.30 shows "additive M f"
9.1 --- a/src/HOL/Probability/Probability.thy Thu Nov 15 14:04:23 2012 +0100
9.2 +++ b/src/HOL/Probability/Probability.thy Thu Nov 15 10:49:58 2012 +0100
9.3 @@ -3,6 +3,7 @@
9.4 Complete_Measure
9.5 Probability_Measure
9.6 Infinite_Product_Measure
9.7 + Regularity
9.8 Independent_Family
9.9 Information
9.10 begin
10.1 --- a/src/HOL/Probability/Projective_Family.thy Thu Nov 15 14:04:23 2012 +0100
10.2 +++ b/src/HOL/Probability/Projective_Family.thy Thu Nov 15 10:49:58 2012 +0100
10.3 @@ -9,6 +9,53 @@
10.4 imports Finite_Product_Measure Probability_Measure
10.5 begin
10.6
10.7 +lemma (in product_prob_space) distr_restrict:
10.8 + assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
10.9 + shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
10.10 +proof (rule measure_eqI_generator_eq)
10.11 + have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
10.12 + interpret J: finite_product_prob_space M J proof qed fact
10.13 + interpret K: finite_product_prob_space M K proof qed fact
10.14 +
10.15 + let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
10.16 + let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
10.17 + let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
10.18 + show "Int_stable ?J"
10.19 + by (rule Int_stable_PiE)
10.20 + show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
10.21 + using `finite J` by (auto intro!: prod_algebraI_finite)
10.22 + { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
10.23 + show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
10.24 + show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
10.25 + using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
10.26 +
10.27 + fix X assume "X \<in> ?J"
10.28 + then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
10.29 + with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
10.30 + by simp
10.31 +
10.32 + have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
10.33 + using E by (simp add: J.measure_times)
10.34 + also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
10.35 + by simp
10.36 + also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
10.37 + using `finite K` `J \<subseteq> K`
10.38 + by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
10.39 + also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
10.40 + using E by (simp add: K.measure_times)
10.41 + also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
10.42 + using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm)
10.43 + finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
10.44 + using X `J \<subseteq> K` apply (subst emeasure_distr)
10.45 + by (auto intro!: measurable_restrict_subset simp: space_PiM)
10.46 +qed
10.47 +
10.48 +lemma (in product_prob_space) emeasure_prod_emb[simp]:
10.49 + assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
10.50 + shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
10.51 + by (subst distr_restrict[OF L])
10.52 + (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
10.53 +
10.54 definition
10.55 PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
10.56 "PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
10.57 @@ -297,4 +344,20 @@
10.58
10.59 end
10.60
10.61 +sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
10.62 +proof
10.63 + fix J::"'i set" assume "finite J"
10.64 + interpret f: finite_product_prob_space M J proof qed fact
10.65 + show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
10.66 + show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
10.67 + (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
10.68 + (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
10.69 + by (auto simp add: sigma_finite_measure_def)
10.70 + show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
10.71 +qed simp_all
10.72 +
10.73 +lemma (in product_prob_space) PiP_PiM_finite[simp]:
10.74 + assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
10.75 + using assms by (simp add: PiP_finite)
10.76 +
10.77 end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/Probability/Regularity.thy Thu Nov 15 10:49:58 2012 +0100
11.3 @@ -0,0 +1,516 @@
11.4 +(* Title: HOL/Probability/Projective_Family.thy
11.5 + Author: Fabian Immler, TU München
11.6 +*)
11.7 +
11.8 +theory Regularity
11.9 +imports Measure_Space Borel_Space
11.10 +begin
11.11 +
11.12 +instantiation nat::topological_space
11.13 +begin
11.14 +
11.15 +definition open_nat::"nat set \<Rightarrow> bool"
11.16 + where "open_nat s = True"
11.17 +
11.18 +instance proof qed (auto simp: open_nat_def)
11.19 +end
11.20 +
11.21 +instantiation nat::metric_space
11.22 +begin
11.23 +
11.24 +definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
11.25 + where "dist_nat n m = (if n = m then 0 else 1)"
11.26 +
11.27 +instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
11.28 +end
11.29 +
11.30 +instance nat::complete_space
11.31 +proof
11.32 + fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
11.33 + hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
11.34 + by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
11.35 + then guess n ..
11.36 + thus "convergent X"
11.37 + apply (intro convergentI[where L="X n"] tendstoI)
11.38 + unfolding eventually_sequentially dist_nat_def
11.39 + apply (intro exI[where x=n])
11.40 + apply (intro allI)
11.41 + apply (drule_tac x=na in spec)
11.42 + apply simp
11.43 + done
11.44 +qed
11.45 +
11.46 +instance nat::enumerable_basis
11.47 +proof
11.48 + have "topological_basis (range (\<lambda>n::nat. {n}))"
11.49 + by (intro topological_basisI) (auto simp: open_nat_def)
11.50 + thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
11.51 +qed
11.52 +
11.53 +subsection {* Regularity of Measures *}
11.54 +
11.55 +lemma ereal_approx_SUP:
11.56 + fixes x::ereal
11.57 + assumes A_notempty: "A \<noteq> {}"
11.58 + assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
11.59 + assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
11.60 + assumes f_nonneg: "\<And>i. 0 \<le> f i"
11.61 + assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
11.62 + shows "x = (SUP i : A. f i)"
11.63 +proof (subst eq_commute, rule ereal_SUPI)
11.64 + show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
11.65 +next
11.66 + fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
11.67 + with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
11.68 + show "x \<le> y"
11.69 + proof (rule ccontr)
11.70 + assume "\<not> x \<le> y" hence "x > y" by simp
11.71 + hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<ge> 0` by auto
11.72 + have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
11.73 + def e \<equiv> "real ((x - y) / 2)"
11.74 + have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
11.75 + note e(1)
11.76 + also from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
11.77 + note i(2)
11.78 + finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
11.79 + moreover have "f i \<le> y" by (rule f_le_y) fact
11.80 + ultimately show False by simp
11.81 + qed
11.82 +qed
11.83 +
11.84 +lemma ereal_approx_INF:
11.85 + fixes x::ereal
11.86 + assumes A_notempty: "A \<noteq> {}"
11.87 + assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
11.88 + assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
11.89 + assumes f_nonneg: "\<And>i. 0 \<le> f i"
11.90 + assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
11.91 + shows "x = (INF i : A. f i)"
11.92 +proof (subst eq_commute, rule ereal_INFI)
11.93 + show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
11.94 +next
11.95 + fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
11.96 + with A_notempty f_fin have "y \<noteq> \<infinity>" by force
11.97 + show "y \<le> x"
11.98 + proof (rule ccontr)
11.99 + assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
11.100 + hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
11.101 + have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
11.102 + apply auto by (metis ereal_infty_less_eq(2) f_le_y)
11.103 + def e \<equiv> "real ((y - x) / 2)"
11.104 + have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
11.105 + from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
11.106 + note i(2)
11.107 + also note e(1)
11.108 + finally have "y > f i" .
11.109 + moreover have "y \<le> f i" by (rule f_le_y) fact
11.110 + ultimately show False by simp
11.111 + qed
11.112 +qed
11.113 +
11.114 +lemma INF_approx_ereal:
11.115 + fixes x::ereal and e::real
11.116 + assumes "e > 0"
11.117 + assumes INF: "x = (INF i : A. f i)"
11.118 + assumes "\<bar>x\<bar> \<noteq> \<infinity>"
11.119 + shows "\<exists>i \<in> A. f i < x + e"
11.120 +proof (rule ccontr, clarsimp)
11.121 + assume "\<forall>i\<in>A. \<not> f i < x + e"
11.122 + moreover
11.123 + from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
11.124 + ultimately
11.125 + have "(INF i : A. f i) = x + e" using `e > 0`
11.126 + by (intro ereal_INFI)
11.127 + (force, metis add.comm_neutral add_left_mono ereal_less(1)
11.128 + linorder_not_le not_less_iff_gr_or_eq)
11.129 + thus False using assms by auto
11.130 +qed
11.131 +
11.132 +lemma SUP_approx_ereal:
11.133 + fixes x::ereal and e::real
11.134 + assumes "e > 0"
11.135 + assumes SUP: "x = (SUP i : A. f i)"
11.136 + assumes "\<bar>x\<bar> \<noteq> \<infinity>"
11.137 + shows "\<exists>i \<in> A. x \<le> f i + e"
11.138 +proof (rule ccontr, clarsimp)
11.139 + assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
11.140 + moreover
11.141 + from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
11.142 + ultimately
11.143 + have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
11.144 + by (intro ereal_SUPI)
11.145 + (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
11.146 + metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
11.147 + thus False using assms by auto
11.148 +qed
11.149 +
11.150 +lemma
11.151 + fixes M::"'a::{enumerable_basis, complete_space} measure"
11.152 + assumes sb: "sets M = sets borel"
11.153 + assumes "emeasure M (space M) \<noteq> \<infinity>"
11.154 + assumes "B \<in> sets borel"
11.155 + shows inner_regular: "emeasure M B =
11.156 + (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
11.157 + and outer_regular: "emeasure M B =
11.158 + (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
11.159 +proof -
11.160 + have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
11.161 + hence sU: "space M = UNIV" by simp
11.162 + interpret finite_measure M by rule fact
11.163 + have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
11.164 + (\<And>e. e > 0 \<Longrightarrow> \<exists>K. K \<subseteq> A \<and> compact K \<and> emeasure M A \<le> emeasure M K + ereal e) \<Longrightarrow> ?inner A"
11.165 + by (rule ereal_approx_SUP)
11.166 + (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
11.167 + have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
11.168 + (\<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"
11.169 + by (rule ereal_approx_INF)
11.170 + (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
11.171 + from countable_dense_setE guess x::"nat \<Rightarrow> 'a" . note x = this
11.172 + {
11.173 + fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
11.174 + with x[OF this]
11.175 + have x: "space M = (\<Union>n. cball (x n) r)"
11.176 + by (auto simp add: sU) (metis dist_commute order_less_imp_le)
11.177 + 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))"
11.178 + by (rule Lim_emeasure_incseq)
11.179 + (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
11.180 + also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
11.181 + unfolding x by force
11.182 + finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
11.183 + } note M_space = this
11.184 + {
11.185 + fix e ::real and n :: nat assume "e > 0" "n > 0"
11.186 + hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
11.187 + from M_space[OF `1/n>0`]
11.188 + have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
11.189 + unfolding emeasure_eq_measure by simp
11.190 + from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
11.191 + obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
11.192 + e * 2 powr -n"
11.193 + by auto
11.194 + hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
11.195 + measure M (space M) - e * 2 powr -real n"
11.196 + by (auto simp: dist_real_def)
11.197 + hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
11.198 + measure M (space M) - e * 2 powr - real n" ..
11.199 + } note k=this
11.200 + hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
11.201 + measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
11.202 + by blast
11.203 + then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
11.204 + \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
11.205 + apply atomize_elim unfolding bchoice_iff .
11.206 + hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
11.207 + \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
11.208 + unfolding Ball_def by blast
11.209 + have approx_space:
11.210 + "\<And>e. e > 0 \<Longrightarrow>
11.211 + \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
11.212 + (is "\<And>e. _ \<Longrightarrow> ?thesis e")
11.213 + proof -
11.214 + fix e :: real assume "e > 0"
11.215 + def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
11.216 + have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
11.217 + hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
11.218 + from k[OF `e > 0` zero_less_Suc]
11.219 + have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
11.220 + by (simp add: algebra_simps B_def finite_measure_compl)
11.221 + hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
11.222 + by (simp add: finite_measure_compl)
11.223 + def K \<equiv> "\<Inter>n. B n"
11.224 + from `closed (B _)` have "closed K" by (auto simp: K_def)
11.225 + hence [simp]: "K \<in> sets M" by (simp add: sb)
11.226 + have "measure M (space M) - measure M K = measure M (space M - K)"
11.227 + by (simp add: finite_measure_compl)
11.228 + also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
11.229 + also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
11.230 + by (rule emeasure_subadditive_countably) (auto simp: summable_def)
11.231 + also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
11.232 + using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
11.233 + also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
11.234 + by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
11.235 + also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
11.236 + unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
11.237 + by simp
11.238 + also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
11.239 + by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
11.240 + also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
11.241 + finally have "measure M (space M) \<le> measure M K + e" by simp
11.242 + hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
11.243 + moreover have "compact K"
11.244 + unfolding compact_eq_totally_bounded
11.245 + proof safe
11.246 + show "complete K" using `closed K` by (simp add: complete_eq_closed)
11.247 + fix e'::real assume "0 < e'"
11.248 + from nat_approx_posE[OF this] guess n . note n = this
11.249 + let ?k = "x ` {0..k e (Suc n)}"
11.250 + have "finite ?k" by simp
11.251 + moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
11.252 + ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
11.253 + qed
11.254 + ultimately
11.255 + show "?thesis e " by (auto simp: sU)
11.256 + qed
11.257 + have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
11.258 + proof
11.259 + fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
11.260 + hence [simp]: "A \<in> sets M" by (simp add: sb)
11.261 + show "?inner A"
11.262 + proof (rule approx_inner)
11.263 + fix e::real assume "e > 0"
11.264 + from approx_space[OF this] obtain K where
11.265 + K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
11.266 + by (auto simp: emeasure_eq_measure)
11.267 + hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
11.268 + have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
11.269 + by (simp add: emeasure_eq_measure)
11.270 + also have "\<dots> = measure M (A - A \<inter> K)"
11.271 + by (subst finite_measure_Diff) auto
11.272 + also have "A - A \<inter> K = A \<union> K - K" by auto
11.273 + also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
11.274 + by (subst finite_measure_Diff) auto
11.275 + also have "\<dots> \<le> measure M (space M) - measure M K"
11.276 + by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
11.277 + also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
11.278 + finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
11.279 + by (simp add: emeasure_eq_measure algebra_simps)
11.280 + moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
11.281 + ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
11.282 + by blast
11.283 + qed simp
11.284 + show "?outer A"
11.285 + proof cases
11.286 + assume "A \<noteq> {}"
11.287 + let ?G = "\<lambda>d. {x. infdist x A < d}"
11.288 + {
11.289 + fix d
11.290 + have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
11.291 + also have "open \<dots>"
11.292 + by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
11.293 + finally have "open (?G d)" .
11.294 + } note open_G = this
11.295 + from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
11.296 + have "A = {x. infdist x A = 0}" by auto
11.297 + also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
11.298 + proof (auto, rule ccontr)
11.299 + fix x
11.300 + assume "infdist x A \<noteq> 0"
11.301 + hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
11.302 + from nat_approx_posE[OF this] guess n .
11.303 + moreover
11.304 + assume "\<forall>i. infdist x A < 1 / real (Suc i)"
11.305 + hence "infdist x A < 1 / real (Suc n)" by auto
11.306 + ultimately show False by simp
11.307 + qed
11.308 + also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
11.309 + proof (rule INF_emeasure_decseq[symmetric], safe)
11.310 + fix i::nat
11.311 + from open_G[of "1 / real (Suc i)"]
11.312 + show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
11.313 + next
11.314 + show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
11.315 + by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
11.316 + simp: decseq_def le_eq_less_or_eq)
11.317 + qed simp
11.318 + finally
11.319 + have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
11.320 + moreover
11.321 + have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
11.322 + proof (intro INF_mono)
11.323 + fix m
11.324 + have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
11.325 + moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
11.326 + ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
11.327 + emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
11.328 + by blast
11.329 + qed
11.330 + moreover
11.331 + have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
11.332 + by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
11.333 + ultimately show ?thesis by simp
11.334 + qed (auto intro!: ereal_INFI)
11.335 + qed
11.336 + let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
11.337 + interpret dynkin: dynkin_system "space M" ?D
11.338 + proof (rule dynkin_systemI)
11.339 + have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
11.340 + hence "?outer (space M)" by (simp add: min_def INF_def)
11.341 + moreover
11.342 + have "?inner (space M)"
11.343 + proof (rule ereal_approx_SUP)
11.344 + fix e::real assume "0 < e"
11.345 + thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
11.346 + by (rule approx_space)
11.347 + qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
11.348 + ultimately show "space M \<in> ?D" by (simp add: sU sb)
11.349 + next
11.350 + fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
11.351 + from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
11.352 + hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
11.353 + and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
11.354 + have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
11.355 + also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"
11.356 + unfolding inner by (subst INFI_ereal_cminus) force+
11.357 + also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
11.358 + by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
11.359 + also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
11.360 + by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
11.361 + also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
11.362 + (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
11.363 + by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
11.364 + (rule INF_cong, auto simp add: sU intro!: INF_cong)
11.365 + finally have
11.366 + "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
11.367 + moreover have
11.368 + "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
11.369 + by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
11.370 + ultimately have "?outer (space M - B)" by simp
11.371 + moreover
11.372 + {
11.373 + have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
11.374 + also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"
11.375 + unfolding outer by (subst SUPR_ereal_cminus) auto
11.376 + also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
11.377 + by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
11.378 + also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
11.379 + by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
11.380 + (rule SUP_cong, auto simp: sU)
11.381 + also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
11.382 + proof (safe intro!: antisym SUP_least)
11.383 + fix K assume "closed K" "K \<subseteq> space M - B"
11.384 + from closed_in_D[OF `closed K`]
11.385 + have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
11.386 + show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
11.387 + unfolding K_inner using `K \<subseteq> space M - B`
11.388 + by (auto intro!: SUP_upper SUP_least)
11.389 + qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
11.390 + finally have "?inner (space M - B)" .
11.391 + } hence "?inner (space M - B)" .
11.392 + ultimately show "space M - B \<in> ?D" by auto
11.393 + next
11.394 + fix D :: "nat \<Rightarrow> _"
11.395 + assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
11.396 + moreover assume "disjoint_family D"
11.397 + ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
11.398 + also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
11.399 + by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
11.400 + finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
11.401 + by (simp add: emeasure_eq_measure)
11.402 + have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
11.403 + moreover
11.404 + hence "?inner (\<Union>i. D i)"
11.405 + proof (rule approx_inner)
11.406 + fix e::real assume "e > 0"
11.407 + with measure_LIMSEQ
11.408 + have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i = 0..<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
11.409 + by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
11.410 + hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
11.411 + then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
11.412 + unfolding choice_iff by blast
11.413 + have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
11.414 + by (auto simp add: emeasure_eq_measure)
11.415 + also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
11.416 + also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
11.417 + also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
11.418 + also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
11.419 + finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
11.420 + using n0 by auto
11.421 + have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
11.422 + proof
11.423 + fix i
11.424 + from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
11.425 + have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
11.426 + using `range D \<subseteq> ?D` by blast
11.427 + from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
11.428 + show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
11.429 + by (auto simp: emeasure_eq_measure)
11.430 + qed
11.431 + then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
11.432 + "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
11.433 + unfolding choice_iff by blast
11.434 + let ?K = "\<Union>i\<in>{0..<n0}. K i"
11.435 + have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
11.436 + unfolding disjoint_family_on_def by blast
11.437 + hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
11.438 + by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
11.439 + have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
11.440 + also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
11.441 + using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
11.442 + also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
11.443 + by (simp add: setsum.distrib)
11.444 + also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) + e / 2" using `0 < e`
11.445 + by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
11.446 + finally
11.447 + have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
11.448 + by auto
11.449 + hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
11.450 + moreover
11.451 + have "?K \<subseteq> (\<Union>i. D i)" using K by auto
11.452 + moreover
11.453 + have "compact ?K" using K by auto
11.454 + ultimately
11.455 + have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp
11.456 + thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
11.457 + qed
11.458 + moreover have "?outer (\<Union>i. D i)"
11.459 + proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
11.460 + fix e::real assume "e > 0"
11.461 + have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
11.462 + proof
11.463 + fix i::nat
11.464 + from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
11.465 + have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
11.466 + using `range D \<subseteq> ?D` by blast
11.467 + from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
11.468 + show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
11.469 + by (auto simp: emeasure_eq_measure)
11.470 + qed
11.471 + then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
11.472 + "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
11.473 + unfolding choice_iff by blast
11.474 + let ?U = "\<Union>i. U i"
11.475 + have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U `(\<Union>i. D i) \<in> sets M`
11.476 + by (subst emeasure_Diff) (auto simp: sb)
11.477 + also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U `range D \<subseteq> sets M`
11.478 + by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
11.479 + also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U `range D \<subseteq> sets M`
11.480 + by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
11.481 + also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
11.482 + by (intro suminf_le_pos, subst emeasure_Diff)
11.483 + (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
11.484 + also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
11.485 + by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
11.486 + also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
11.487 + unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
11.488 + by simp
11.489 + also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
11.490 + by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
11.491 + also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
11.492 + finally
11.493 + have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
11.494 + moreover
11.495 + have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
11.496 + moreover
11.497 + have "open ?U" using U by auto
11.498 + ultimately
11.499 + have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp
11.500 + thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" ..
11.501 + qed
11.502 + ultimately show "(\<Union>i. D i) \<in> ?D" by safe
11.503 + qed
11.504 + have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
11.505 + also have "\<dots> = dynkin (space M) (Collect closed)"
11.506 + proof (rule sigma_eq_dynkin)
11.507 + show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
11.508 + show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
11.509 + qed
11.510 + also have "\<dots> \<subseteq> ?D" using closed_in_D
11.511 + by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
11.512 + finally have "sets borel \<subseteq> ?D" .
11.513 + moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
11.514 + ultimately have "sets borel = ?D" by simp
11.515 + with assms show "?inner B" and "?outer B" by auto
11.516 +qed
11.517 +
11.518 +end
11.519 +
12.1 --- a/src/HOL/SEQ.thy Thu Nov 15 14:04:23 2012 +0100
12.2 +++ b/src/HOL/SEQ.thy Thu Nov 15 10:49:58 2012 +0100
12.3 @@ -171,6 +171,12 @@
12.4 thus ?case by arith
12.5 qed
12.6
12.7 +lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
12.8 + unfolding subseq_def by simp
12.9 +
12.10 +lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
12.11 + using assms by (auto simp: subseq_def)
12.12 +
12.13 lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X"
12.14 by (simp add: incseq_def monoseq_def)
12.15
12.16 @@ -181,6 +187,20 @@
12.17 fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
12.18 by (simp add: decseq_def incseq_def)
12.19
12.20 +lemma INT_decseq_offset:
12.21 + assumes "decseq F"
12.22 + shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
12.23 +proof safe
12.24 + fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
12.25 + show "x \<in> F i"
12.26 + proof cases
12.27 + from x have "x \<in> F n" by auto
12.28 + also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
12.29 + unfolding decseq_def by simp
12.30 + finally show ?thesis .
12.31 + qed (insert x, simp)
12.32 +qed auto
12.33 +
12.34 subsection {* Defintions of limits *}
12.35
12.36 abbreviation (in topological_space)