regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Thu Nov 15 10:49:58 2012 +0100
@@ -0,0 +1,111 @@
+(* Author: Fabian Immler, TUM *)
+
+header {* Sequence of Properties on Subsequences *}
+
+theory Diagonal_Subsequence
+imports SEQ
+begin
+
+locale subseqs =
+ fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
+ assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
+begin
+
+primrec seqseq where
+ "seqseq 0 = id"
+| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
+
+lemma seqseq_ex:
+ shows "subseq (seqseq n) \<and>
+ (\<exists>r'. seqseq (Suc n) = seqseq n o r' \<and> subseq r' \<and> P n (seqseq n o r'))"
+proof (induct n)
+ case 0
+ let ?P = "\<lambda>r'. subseq r' \<and> P 0 r'"
+ let ?r = "Eps ?P"
+ have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def)
+ thus ?case by (auto simp: subseq_def)
+next
+ case (Suc n)
+ then obtain r' where
+ Suc': "seqseq (Suc n) = seqseq n \<circ> r'" "subseq (seqseq n)" "subseq r'"
+ "P n (seqseq n o r')"
+ by blast
+ let ?P = "\<lambda>r'a. subseq (r'a ) \<and> P (Suc n) (seqseq n o r' o r'a)"
+ let ?r = "Eps ?P"
+ have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc'
+ by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc)
+ moreover have "seqseq (Suc (Suc n)) = seqseq n \<circ> r' \<circ> ?r"
+ by (subst seqseq.simps) (simp only: Suc' o_assoc)
+ moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`]
+ ultimately show ?case unfolding Suc' by (auto simp: o_def)
+qed
+
+lemma subseq_seqseq:
+ shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto
+
+definition reducer where "reducer n = (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
+
+lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n o reducer n)"
+ unfolding atomize_conj unfolding reducer_def using subseq_seqseq
+ by (rule someI_ex[OF ex_subseq])
+
+lemma seqseq_reducer[simp]:
+ "seqseq (Suc n) = seqseq n o reducer n"
+ by (simp add: reducer_def)
+
+declare seqseq.simps(2)[simp del]
+
+definition diagseq where "diagseq i = seqseq i i"
+
+lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
+ unfolding diagseq_def seqseq_reducer o_def
+ by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer)
+
+lemma subseq_diagseq: "subseq diagseq"
+ using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
+
+primrec fold_reduce where
+ "fold_reduce n 0 = id"
+| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)"
+
+lemma subseq_fold_reduce: "subseq (fold_reduce n k)"
+proof (induct k)
+ case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def)
+qed (simp add: subseq_def)
+
+lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
+ by (induct k) simp_all
+
+lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
+ by (induct n) (simp_all)
+
+lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
+ using seqseq_fold_reduce by (simp add: diagseq_def)
+
+lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
+ by (induct n) simp_all
+
+lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
+proof -
+ have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
+ by (simp add: diagseq_fold_reduce)
+ also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)"
+ unfolding fold_reduce_add seqseq_fold_reduce ..
+ finally show ?thesis .
+qed
+
+lemma diagseq_sub:
+ assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
+ using diagseq_add[of m "n - m"] assms by simp
+
+lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
+ unfolding subseq_Suc_iff fold_reduce.simps o_def
+ by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble
+ subseq_reducer)
+
+lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))"
+ by (auto simp: o_def diagseq_add)
+
+end
+
+end
--- a/src/HOL/Library/Library.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Library/Library.thy Thu Nov 15 10:49:58 2012 +0100
@@ -13,6 +13,7 @@
Convex
Countable
Debug
+ Diagonal_Subsequence
Dlist
Eval_Witness
Extended_Nat
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 15 10:49:58 2012 +0100
@@ -7,9 +7,210 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
+imports
+ SEQ
+ "~~/src/HOL/Library/Diagonal_Subsequence"
+ "~~/src/HOL/Library/Countable"
+ Linear_Algebra
+ "~~/src/HOL/Library/Glbs"
+ Norm_Arith
+begin
+
+subsection {* Topological Basis *}
+
+context topological_space
+begin
+
+definition "topological_basis B =
+ ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
+
+lemma topological_basis_iff:
+ assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
+ 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'))"
+ (is "_ \<longleftrightarrow> ?rhs")
+proof safe
+ fix O' and x::'a
+ assume H: "topological_basis B" "open O'" "x \<in> O'"
+ hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
+ then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
+ thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
+next
+ assume H: ?rhs
+ show "topological_basis B" using assms unfolding topological_basis_def
+ proof safe
+ fix O'::"'a set" assume "open O'"
+ with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
+ by (force intro: bchoice simp: Bex_def)
+ thus "\<exists>B'\<subseteq>B. \<Union>B' = O'"
+ by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
+ qed
+qed
+
+lemma topological_basisI:
+ assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
+ assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
+ shows "topological_basis B"
+ using assms by (subst topological_basis_iff) auto
+
+lemma topological_basisE:
+ fixes O'
+ assumes "topological_basis B"
+ assumes "open O'"
+ assumes "x \<in> O'"
+ obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
+proof atomize_elim
+ from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" by (simp add: topological_basis_def)
+ with topological_basis_iff assms
+ show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def)
+qed
+
+end
+
+subsection {* Enumerable Basis *}
+
+class enumerable_basis = topological_space +
+ assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a set. topological_basis (range f)"
begin
+definition enum_basis'::"nat \<Rightarrow> 'a set"
+ where "enum_basis' = Eps (topological_basis o range)"
+
+lemma enumerable_basis': "topological_basis (range enum_basis')"
+ using ex_enum_basis
+ unfolding enum_basis'_def o_def
+ by (rule someI_ex)
+
+lemmas enumerable_basisE' = topological_basisE[OF enumerable_basis']
+
+text {* Extend enumeration of basis, such that it is closed under (finite) Union *}
+
+definition enum_basis::"nat \<Rightarrow> 'a set"
+ where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
+
+lemma
+ open_enum_basis:
+ assumes "B \<in> range enum_basis"
+ shows "open B"
+ using assms enumerable_basis'
+ by (force simp add: topological_basis_def enum_basis_def)
+
+lemma enumerable_basis: "topological_basis (range enum_basis)"
+proof (rule topological_basisI[OF open_enum_basis])
+ fix O' x assume "open O'" "x \<in> O'"
+ from topological_basisE[OF enumerable_basis' this] guess B' . note B' = this
+ moreover then obtain n where "B' = enum_basis' n" by auto
+ moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
+ ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
+qed
+
+lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
+
+lemma open_enumerable_basis_ex:
+ assumes "open X"
+ shows "\<exists>N. X = (\<Union>n\<in>N. enum_basis n)"
+proof -
+ from enumerable_basis assms obtain B' where "B' \<subseteq> range enum_basis" "X = Union B'"
+ unfolding topological_basis_def by blast
+ hence "Union B' = (\<Union>n\<in>{n. enum_basis n \<in> B'}. enum_basis n)" by auto
+ with `X = Union B'` show ?thesis by blast
+qed
+
+lemma open_enumerable_basisE:
+ assumes "open X"
+ obtains N where "X = (\<Union>n\<in>N. enum_basis n)"
+ using assms open_enumerable_basis_ex by (atomize_elim) simp
+
+lemma countable_dense_set:
+ shows "\<exists>x::nat \<Rightarrow> _. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+proof -
+ def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> enum_basis n)"
+ have x: "\<And>n. enum_basis n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> enum_basis n" unfolding x_def
+ by (rule someI_ex) auto
+ have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+ proof (intro allI impI)
+ fix y::"'a set" assume "open y" "y \<noteq> {}"
+ from open_enumerable_basisE[OF `open y`] guess N . note N = this
+ obtain n where n: "n \<in> N" "enum_basis n \<noteq> ({}::'a set)"
+ proof (atomize_elim, rule ccontr, clarsimp)
+ assume "\<forall>n. n \<in> N \<longrightarrow> enum_basis n = ({}::'a set)"
+ hence "(\<Union>n\<in>N. enum_basis n) = (\<Union>n\<in>N. {}::'a set)"
+ by (intro UN_cong) auto
+ hence "y = {}" unfolding N by simp
+ with `y \<noteq> {}` show False by auto
+ qed
+ with x N n have "x n \<in> y" by auto
+ thus "\<exists>n. x n \<in> y" ..
+ qed
+ thus ?thesis by blast
+qed
+
+lemma countable_dense_setE:
+ obtains x :: "nat \<Rightarrow> _"
+ where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
+ using countable_dense_set by blast
+
+text {* Construction of an Increasing Sequence Approximating Open Sets *}
+
+lemma empty_basisI[intro]: "{} \<in> range enum_basis"
+proof
+ show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
+qed rule
+
+lemma union_basisI[intro]:
+ assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
+ shows "A \<union> B \<in> range enum_basis"
+proof -
+ from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
+ also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
+ by (simp add: enum_basis_def)
+ finally show ?thesis by simp
+qed
+
+lemma open_imp_Union_of_incseq:
+ assumes "open X"
+ shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
+proof -
+ from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
+ hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
+ def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
+ (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
+ have S_simps[simp]:
+ "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
+ "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
+ by (simp_all add: S_def)
+ have "incseq S" by (rule incseq_SucI) auto
+ moreover
+ have "(\<Union>j. S j) = X" unfolding N
+ proof safe
+ fix x n assume "n \<in> N" "x \<in> enum_basis n"
+ hence "x \<in> S n" by (cases n) auto
+ thus "x \<in> (\<Union>j. S j)" by auto
+ next
+ fix x j
+ assume "x \<in> S j"
+ thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
+ qed
+ moreover have "range S \<subseteq> range enum_basis"
+ proof safe
+ fix j show "S j \<in> range enum_basis" by (induct j) auto
+ qed
+ ultimately show ?thesis by auto
+qed
+
+lemma open_incseqE:
+ assumes "open X"
+ obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
+ using open_imp_Union_of_incseq assms by atomize_elim
+
+end
+
+subsection {* Polish spaces *}
+
+text {* Textbooks define Polish spaces as completely metrizable.
+ We assume the topology to be complete for a given metric. *}
+
+class polish_space = complete_space + enumerable_basis
+
subsection {* General notion of a topology as a value *}
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))"
@@ -377,6 +578,86 @@
lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
+lemma rational_boxes:
+ fixes x :: "'a\<Colon>ordered_euclidean_space"
+ assumes "0 < e"
+ 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"
+proof -
+ def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
+ then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
+ have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
+ proof
+ fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
+ show "?th i" by auto
+ qed
+ from choice[OF this] guess a .. note a = this
+ have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
+ proof
+ fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
+ show "?th i" by auto
+ qed
+ from choice[OF this] guess b .. note b = this
+ { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
+ have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
+ unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+ also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
+ proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
+ fix i assume i: "i \<in> {..<DIM('a)}"
+ have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
+ moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
+ moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
+ ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
+ then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
+ unfolding e'_def by (auto simp: dist_real_def)
+ then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
+ by (rule power_strict_mono) auto
+ then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
+ by (simp add: power_divide)
+ qed auto
+ also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
+ finally have "dist x y < e" . }
+ with a b show ?thesis
+ apply (rule_tac exI[of _ "Chi a"])
+ apply (rule_tac exI[of _ "Chi b"])
+ using eucl_less[where 'a='a] by auto
+qed
+
+lemma ex_rat_list:
+ fixes x :: "'a\<Colon>ordered_euclidean_space"
+ assumes "\<And> i. x $$ i \<in> \<rat>"
+ shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
+proof -
+ have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
+ from choice[OF this] guess r ..
+ then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
+qed
+
+lemma open_UNION:
+ fixes M :: "'a\<Colon>ordered_euclidean_space set"
+ assumes "open M"
+ shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
+ (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
+ (is "M = UNION ?idx ?box")
+proof safe
+ fix x assume "x \<in> M"
+ obtain e where e: "e > 0" "ball x e \<subseteq> M"
+ using openE[OF assms `x \<in> M`] by auto
+ 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"
+ using rational_boxes[OF e(1)] by blast
+ then obtain p q where pq: "length p = DIM ('a)"
+ "length q = DIM ('a)"
+ "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
+ using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
+ hence p: "Chi (of_rat \<circ> op ! p) = a"
+ using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
+ unfolding o_def by auto
+ from pq have q: "Chi (of_rat \<circ> op ! q) = b"
+ using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
+ unfolding o_def by auto
+ have "x \<in> ?box (p, q)"
+ using p q ab by auto
+ thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
+qed auto
subsection{* Connectedness *}
@@ -803,7 +1084,6 @@
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
-
subsection {* Filters and the ``eventually true'' quantifier *}
definition
@@ -1361,6 +1641,121 @@
shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
by (metis closure_closed closure_approachable)
+subsection {* Infimum Distance *}
+
+definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
+
+lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
+ by (simp add: infdist_def)
+
+lemma infdist_nonneg:
+ shows "0 \<le> infdist x A"
+ using assms by (auto simp add: infdist_def)
+
+lemma infdist_le:
+ assumes "a \<in> A"
+ assumes "d = dist x a"
+ shows "infdist x A \<le> d"
+ using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
+
+lemma infdist_zero[simp]:
+ assumes "a \<in> A" shows "infdist a A = 0"
+proof -
+ from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0" by auto
+ with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto
+qed
+
+lemma infdist_triangle:
+ shows "infdist x A \<le> infdist y A + dist x y"
+proof cases
+ assume "A = {}" thus ?thesis by (simp add: infdist_def)
+next
+ assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
+ have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
+ proof
+ from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
+ fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
+ then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
+ show "infdist x A \<le> d"
+ unfolding infdist_notempty[OF `A \<noteq> {}`]
+ proof (rule Inf_lower2)
+ show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
+ show "dist x a \<le> d" unfolding d by (rule dist_triangle)
+ fix d assume "d \<in> {dist x a |a. a \<in> A}"
+ then obtain a where "a \<in> A" "d = dist x a" by auto
+ thus "infdist x A \<le> d" by (rule infdist_le)
+ qed
+ qed
+ also have "\<dots> = dist x y + infdist y A"
+ proof (rule Inf_eq, safe)
+ fix a assume "a \<in> A"
+ thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
+ next
+ fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
+ hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
+ by (intro Inf_greatest) (auto simp: field_simps)
+ thus "i \<le> dist x y + infdist y A" by simp
+ qed
+ finally show ?thesis by simp
+qed
+
+lemma
+ in_closure_iff_infdist_zero:
+ assumes "A \<noteq> {}"
+ shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+proof
+ assume "x \<in> closure A"
+ show "infdist x A = 0"
+ proof (rule ccontr)
+ assume "infdist x A \<noteq> 0"
+ with infdist_nonneg[of x A] have "infdist x A > 0" by auto
+ hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
+ by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
+ eucl_less_not_refl euclidean_trans(2) infdist_le)
+ hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
+ thus False using `x \<in> closure A` by simp
+ qed
+next
+ assume x: "infdist x A = 0"
+ then obtain a where "a \<in> A" by atomize_elim (metis all_not_in_conv assms)
+ show "x \<in> closure A" unfolding closure_approachable
+ proof (safe, rule ccontr)
+ fix e::real assume "0 < e"
+ assume "\<not> (\<exists>y\<in>A. dist y x < e)"
+ hence "infdist x A \<ge> e" using `a \<in> A`
+ unfolding infdist_def
+ by (force intro: Inf_greatest simp: dist_commute)
+ with x `0 < e` show False by auto
+ qed
+qed
+
+lemma
+ in_closed_iff_infdist_zero:
+ assumes "closed A" "A \<noteq> {}"
+ shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
+proof -
+ have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+ by (rule in_closure_iff_infdist_zero) fact
+ with assms show ?thesis by simp
+qed
+
+lemma tendsto_infdist [tendsto_intros]:
+ assumes f: "(f ---> l) F"
+ shows "((\<lambda>x. infdist (f x) A) ---> infdist l A) F"
+proof (rule tendstoI)
+ fix e ::real assume "0 < e"
+ from tendstoD[OF f this]
+ show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
+ proof (eventually_elim)
+ fix x
+ from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
+ have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
+ by (simp add: dist_commute dist_real_def)
+ also assume "dist (f x) l < e"
+ finally show "dist (infdist (f x) A) (infdist l A) < e" .
+ qed
+qed
+
text{* Some other lemmas about sequences. *}
lemma sequentially_offset:
@@ -2696,6 +3091,157 @@
assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
qed
+lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
+ by metis
+
+lemma nat_approx_posE:
+ fixes e::real
+ assumes "0 < e"
+ obtains n::nat where "1 / (Suc n) < e"
+proof atomize_elim
+ have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
+ by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
+ also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
+ by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
+ also have "\<dots> = e" by simp
+ finally show "\<exists>n. 1 / real (Suc n) < e" ..
+qed
+
+lemma compact_eq_totally_bounded:
+ shows "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+proof (safe intro!: compact_imp_complete)
+ fix e::real
+ def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
+ assume "0 < e" "compact s"
+ hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
+ by (simp add: compact_eq_heine_borel)
+ moreover
+ have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
+ hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
+ ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
+ then guess K .. note K = this
+ have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
+ then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
+ thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
+ by (intro exI[where x="k ` K"]) (auto simp: f_def)
+next
+ assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
+ show "compact s"
+ proof cases
+ assume "s = {}" thus "compact s" by (simp add: compact_def)
+ next
+ assume "s \<noteq> {}"
+ show ?thesis
+ unfolding compact_def
+ proof safe
+ fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
+ from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
+ then obtain K where
+ K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+ unfolding choice_iff by blast
+ {
+ fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
+ assume "e > 0"
+ from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+ by simp_all
+ have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
+ proof (rule ccontr)
+ from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
+ using `s \<noteq> {}`
+ by auto
+ moreover
+ assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
+ 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
+ ultimately
+ show False using f'
+ proof (induct arbitrary: s f f' rule: finite_ne_induct)
+ case (singleton x)
+ have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
+ thus ?case using singleton by (auto simp: ball_def)
+ next
+ case (insert x A)
+ show ?case
+ proof cases
+ have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
+ have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
+ using insert by (intro infinite_super[OF _ inf_ms]) auto
+ also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
+ {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
+ finally have "infinite \<dots>" .
+ moreover assume "finite {m. (f o f') m \<in> ball x e}"
+ ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
+ hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
+ def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
+ have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
+ using enumerate_mono[OF _ inf] by (simp add: r_def)
+ hence "subseq r" by (simp add: subseq_def)
+ have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
+ using enumerate_in_set[OF inf] by (simp add: r_def)
+ show False
+ proof (rule insert)
+ show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
+ fix k s assume "k \<in> A" "subseq s"
+ thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
+ by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
+ next
+ fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
+ qed
+ next
+ assume inf: "infinite {m. (f o f') m \<in> ball x e}"
+ def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
+ have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
+ using enumerate_mono[OF _ inf] by (simp add: r_def)
+ hence "subseq r" by (simp add: subseq_def)
+ from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
+ moreover
+ have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
+ using enumerate_in_set[OF inf] by (simp add: r_def)
+ hence "(f o f') (r i) \<in> ball x e" by simp
+ ultimately show False by simp
+ qed
+ qed
+ qed
+ }
+ 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
+ let ?e = "\<lambda>n. 1 / real (Suc n)"
+ let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
+ interpret subseqs ?P using ex by unfold_locales force
+ from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
+ by (simp add: complete_def)
+ have "\<exists>l\<in>s. (f o diagseq) ----> l"
+ proof (intro limI metric_CauchyI)
+ fix e::real assume "0 < e" hence "0 < e / 2" by auto
+ from nat_approx_posE[OF this] guess n . note n = this
+ show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
+ proof (rule exI[where x="Suc n"], safe)
+ fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
+ let ?e = "1 / real (Suc n)"
+ from reducer_reduces[of n] obtain k where
+ "k\<in>K ?e" "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
+ unfolding seqseq_reducer by auto
+ moreover
+ note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
+ ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
+ also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
+ finally
+ have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
+ by (intro add_strict_mono) auto
+ hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
+ by (simp add: dist_commute)
+ moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
+ dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
+ by (rule dist_triangle2)
+ ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
+ by simp
+ qed
+ next
+ fix n show "(f o diagseq) n \<in> s" using f by simp
+ qed
+ thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
+ qed
+ qed
+qed
+
lemma compact_eq_bounded_closed:
fixes s :: "'a::heine_borel set"
shows "compact s \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs")
@@ -2738,9 +3284,6 @@
unfolding compact_def
by simp
-lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
- unfolding subseq_def by simp (* TODO: move somewhere else *)
-
lemma compact_union [intro]:
assumes "compact s" and "compact t"
shows "compact (s \<union> t)"
@@ -2771,6 +3314,13 @@
qed
qed
+lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
+ by (induct set: finite) auto
+
+lemma compact_UN [intro]:
+ "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
+ unfolding SUP_def by (rule compact_Union) auto
+
lemma compact_inter_closed [intro]:
assumes "compact s" and "closed t"
shows "compact (s \<inter> t)"
@@ -3294,6 +3844,11 @@
shows "continuous F (\<lambda>x. dist (f x) (g x))"
using assms unfolding continuous_def by (rule tendsto_dist)
+lemma continuous_infdist:
+ assumes "continuous F f"
+ shows "continuous F (\<lambda>x. infdist (f x) A)"
+ using assms unfolding continuous_def by (rule tendsto_infdist)
+
lemma continuous_norm:
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
unfolding continuous_def by (rule tendsto_norm)
@@ -4886,6 +5441,39 @@
thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed
+instance ordered_euclidean_space \<subseteq> enumerable_basis
+proof
+ def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
+ def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
+ have "Ball (range enum) open" unfolding enum_def
+ proof safe
+ fix n show "open (to_cube (from_nat n))"
+ by (cases "from_nat n::rat list \<times> rat list")
+ (simp add: open_interval to_cube_def)
+ qed
+ moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
+ proof safe
+ fix x::"'a set" assume "open x"
+ def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
+ from open_UNION[OF `open x`]
+ have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
+ by simp
+ moreover have "to_cube ` lists \<subseteq> range enum"
+ proof
+ fix x assume "x \<in> to_cube ` lists"
+ then obtain l where "l \<in> lists" "x = to_cube l" by auto
+ hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
+ thus "x \<in> range enum" by simp
+ qed
+ ultimately
+ show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
+ qed
+ ultimately
+ show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
+qed
+
+instance ordered_euclidean_space \<subseteq> polish_space ..
+
text {* Intervals in general, including infinite and mixtures of open and closed. *}
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
--- a/src/HOL/Probability/Borel_Space.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Thu Nov 15 10:49:58 2012 +0100
@@ -173,87 +173,6 @@
subsection "Borel space equals sigma algebras over intervals"
-lemma rational_boxes:
- fixes x :: "'a\<Colon>ordered_euclidean_space"
- assumes "0 < e"
- 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"
-proof -
- def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
- then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
- have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
- proof
- fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
- show "?th i" by auto
- qed
- from choice[OF this] guess a .. note a = this
- have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
- proof
- fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
- show "?th i" by auto
- qed
- from choice[OF this] guess b .. note b = this
- { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
- have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
- unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
- also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
- proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
- fix i assume i: "i \<in> {..<DIM('a)}"
- have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
- moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
- moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
- ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
- then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
- unfolding e'_def by (auto simp: dist_real_def)
- then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
- by (rule power_strict_mono) auto
- then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
- by (simp add: power_divide)
- qed auto
- also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
- finally have "dist x y < e" . }
- with a b show ?thesis
- apply (rule_tac exI[of _ "Chi a"])
- apply (rule_tac exI[of _ "Chi b"])
- using eucl_less[where 'a='a] by auto
-qed
-
-lemma ex_rat_list:
- fixes x :: "'a\<Colon>ordered_euclidean_space"
- assumes "\<And> i. x $$ i \<in> \<rat>"
- shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
-proof -
- have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
- from choice[OF this] guess r ..
- then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
-qed
-
-lemma open_UNION:
- fixes M :: "'a\<Colon>ordered_euclidean_space set"
- assumes "open M"
- shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
- (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
- (is "M = UNION ?idx ?box")
-proof safe
- fix x assume "x \<in> M"
- obtain e where e: "e > 0" "ball x e \<subseteq> M"
- using openE[OF assms `x \<in> M`] by auto
- 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"
- using rational_boxes[OF e(1)] by blast
- then obtain p q where pq: "length p = DIM ('a)"
- "length q = DIM ('a)"
- "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
- using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
- hence p: "Chi (of_rat \<circ> op ! p) = a"
- using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
- unfolding o_def by auto
- from pq have q: "Chi (of_rat \<circ> op ! q) = b"
- using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
- unfolding o_def by auto
- have "x \<in> ?box (p, q)"
- using p q ab by auto
- thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
-qed auto
-
lemma borel_sigma_sets_subset:
"A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
using sigma_sets_subset[of A borel] by simp
@@ -519,6 +438,39 @@
by (auto intro: sigma_sets.intros)
qed auto
+lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
+ unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+ fix x :: "'a set" assume "open x"
+ hence "x = UNIV - (UNIV - x)" by auto
+ also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
+ by (rule sigma_sets.Compl)
+ (auto intro!: sigma_sets.Basic simp: `open x`)
+ finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
+next
+ fix x :: "'a set" assume "closed x"
+ hence "x = UNIV - (UNIV - x)" by auto
+ also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
+ by (rule sigma_sets.Compl)
+ (auto intro!: sigma_sets.Basic simp: `closed x`)
+ finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
+qed simp_all
+
+lemma borel_eq_enum_basis:
+ "borel = sigma UNIV (range enum_basis)"
+ unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI, safe)
+ fix x::"'a set" assume "open x"
+ from open_enumerable_basisE[OF this] guess N .
+ hence x: "x = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
+ also have "\<dots> \<in> sigma_sets UNIV (range enum_basis)" by (rule Union) auto
+ finally show "x \<in> sigma_sets UNIV (range enum_basis)" .
+next
+ fix n
+ have "open (enum_basis n)" by (rule open_enum_basis) simp
+ thus "enum_basis n \<in> sigma_sets UNIV (Collect open)" by auto
+qed simp_all
+
lemma borel_measurable_halfspacesI:
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
assumes F: "borel = sigma UNIV (range F)"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 10:49:58 2012 +0100
@@ -1161,9 +1161,6 @@
by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
qed
-lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
- by metis
-
lemma sigma_prod_algebra_sigma_eq:
fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
assumes "finite I"
--- a/src/HOL/Probability/Independent_Family.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Thu Nov 15 10:49:58 2012 +0100
@@ -8,20 +8,6 @@
imports Probability_Measure Infinite_Product_Measure
begin
-lemma INT_decseq_offset:
- assumes "decseq F"
- shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
-proof safe
- fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
- show "x \<in> F i"
- proof cases
- from x have "x \<in> F n" by auto
- also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
- unfolding decseq_def by simp
- finally show ?thesis .
- qed (insert x, simp)
-qed auto
-
definition (in prob_space)
"indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
(\<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))))"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 15 10:49:58 2012 +0100
@@ -8,69 +8,6 @@
imports Probability_Measure Caratheodory Projective_Family
begin
-lemma (in product_prob_space) distr_restrict:
- assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
- 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")
-proof (rule measure_eqI_generator_eq)
- have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
- interpret J: finite_product_prob_space M J proof qed fact
- interpret K: finite_product_prob_space M K proof qed fact
-
- let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
- let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
- let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
- show "Int_stable ?J"
- by (rule Int_stable_PiE)
- show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
- using `finite J` by (auto intro!: prod_algebraI_finite)
- { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
- show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
- show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
- using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
-
- fix X assume "X \<in> ?J"
- 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
- with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
- by simp
-
- have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
- using E by (simp add: J.measure_times)
- also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
- by simp
- also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
- using `finite K` `J \<subseteq> K`
- by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
- 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))"
- using E by (simp add: K.measure_times)
- 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))"
- using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm)
- finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
- using X `J \<subseteq> K` apply (subst emeasure_distr)
- by (auto intro!: measurable_restrict_subset simp: space_PiM)
-qed
-
-lemma (in product_prob_space) emeasure_prod_emb[simp]:
- assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
- shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
- by (subst distr_restrict[OF L])
- (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
-
-sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
-proof
- fix J::"'i set" assume "finite J"
- interpret f: finite_product_prob_space M J proof qed fact
- show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
- show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
- (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
- (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
- by (auto simp add: sigma_finite_measure_def)
- show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
-qed simp_all
-
-lemma (in product_prob_space) PiP_PiM_finite[simp]:
- assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
- using assms by (simp add: PiP_finite)
-
lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
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)"
--- a/src/HOL/Probability/Measure_Space.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Thu Nov 15 10:49:58 2012 +0100
@@ -169,6 +169,27 @@
finally show "f x \<le> f y" by simp
qed
+lemma (in ring_of_sets) subadditive:
+ assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S"
+ shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))"
+using S
+proof (induct S)
+ case empty thus ?case using f by (auto simp: positive_def)
+next
+ case (insert x F)
+ 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+
+ have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
+ have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
+ hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
+ by simp
+ also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
+ using f(2) by (rule additiveD) (insert in_M, auto)
+ also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
+ using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
+ also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
+ 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
+qed
+
lemma (in ring_of_sets) countably_additive_additive:
assumes posf: "positive M f" and ca: "countably_additive M f"
shows "additive M f"
--- a/src/HOL/Probability/Probability.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Probability.thy Thu Nov 15 10:49:58 2012 +0100
@@ -3,6 +3,7 @@
Complete_Measure
Probability_Measure
Infinite_Product_Measure
+ Regularity
Independent_Family
Information
begin
--- a/src/HOL/Probability/Projective_Family.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Thu Nov 15 10:49:58 2012 +0100
@@ -9,6 +9,53 @@
imports Finite_Product_Measure Probability_Measure
begin
+lemma (in product_prob_space) distr_restrict:
+ assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
+ 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")
+proof (rule measure_eqI_generator_eq)
+ have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
+ interpret J: finite_product_prob_space M J proof qed fact
+ interpret K: finite_product_prob_space M K proof qed fact
+
+ let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
+ let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
+ let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
+ show "Int_stable ?J"
+ by (rule Int_stable_PiE)
+ show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
+ using `finite J` by (auto intro!: prod_algebraI_finite)
+ { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
+ show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+ show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
+ using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
+
+ fix X assume "X \<in> ?J"
+ 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
+ with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
+ by simp
+
+ have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
+ using E by (simp add: J.measure_times)
+ also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
+ by simp
+ also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
+ using `finite K` `J \<subseteq> K`
+ by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
+ 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))"
+ using E by (simp add: K.measure_times)
+ 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))"
+ using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm)
+ finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
+ using X `J \<subseteq> K` apply (subst emeasure_distr)
+ by (auto intro!: measurable_restrict_subset simp: space_PiM)
+qed
+
+lemma (in product_prob_space) emeasure_prod_emb[simp]:
+ assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
+ shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
+ by (subst distr_restrict[OF L])
+ (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
+
definition
PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
"PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
@@ -297,4 +344,20 @@
end
+sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
+proof
+ fix J::"'i set" assume "finite J"
+ interpret f: finite_product_prob_space M J proof qed fact
+ show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
+ show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
+ (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
+ (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
+ by (auto simp add: sigma_finite_measure_def)
+ show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
+qed simp_all
+
+lemma (in product_prob_space) PiP_PiM_finite[simp]:
+ assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
+ using assms by (simp add: PiP_finite)
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Regularity.thy Thu Nov 15 10:49:58 2012 +0100
@@ -0,0 +1,516 @@
+(* Title: HOL/Probability/Projective_Family.thy
+ Author: Fabian Immler, TU München
+*)
+
+theory Regularity
+imports Measure_Space Borel_Space
+begin
+
+instantiation nat::topological_space
+begin
+
+definition open_nat::"nat set \<Rightarrow> bool"
+ where "open_nat s = True"
+
+instance proof qed (auto simp: open_nat_def)
+end
+
+instantiation nat::metric_space
+begin
+
+definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
+ where "dist_nat n m = (if n = m then 0 else 1)"
+
+instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
+end
+
+instance nat::complete_space
+proof
+ fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
+ hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
+ by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
+ then guess n ..
+ thus "convergent X"
+ apply (intro convergentI[where L="X n"] tendstoI)
+ unfolding eventually_sequentially dist_nat_def
+ apply (intro exI[where x=n])
+ apply (intro allI)
+ apply (drule_tac x=na in spec)
+ apply simp
+ done
+qed
+
+instance nat::enumerable_basis
+proof
+ have "topological_basis (range (\<lambda>n::nat. {n}))"
+ by (intro topological_basisI) (auto simp: open_nat_def)
+ thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
+qed
+
+subsection {* Regularity of Measures *}
+
+lemma ereal_approx_SUP:
+ fixes x::ereal
+ assumes A_notempty: "A \<noteq> {}"
+ assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
+ assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
+ assumes f_nonneg: "\<And>i. 0 \<le> f i"
+ assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
+ shows "x = (SUP i : A. f i)"
+proof (subst eq_commute, rule ereal_SUPI)
+ show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
+next
+ fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
+ with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
+ show "x \<le> y"
+ proof (rule ccontr)
+ assume "\<not> x \<le> y" hence "x > y" by simp
+ hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<ge> 0` by auto
+ have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
+ def e \<equiv> "real ((x - y) / 2)"
+ have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
+ note e(1)
+ also from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
+ note i(2)
+ finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
+ moreover have "f i \<le> y" by (rule f_le_y) fact
+ ultimately show False by simp
+ qed
+qed
+
+lemma ereal_approx_INF:
+ fixes x::ereal
+ assumes A_notempty: "A \<noteq> {}"
+ assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
+ assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
+ assumes f_nonneg: "\<And>i. 0 \<le> f i"
+ assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
+ shows "x = (INF i : A. f i)"
+proof (subst eq_commute, rule ereal_INFI)
+ show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
+next
+ fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
+ with A_notempty f_fin have "y \<noteq> \<infinity>" by force
+ show "y \<le> x"
+ proof (rule ccontr)
+ assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
+ hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
+ have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
+ apply auto by (metis ereal_infty_less_eq(2) f_le_y)
+ def e \<equiv> "real ((y - x) / 2)"
+ have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
+ from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
+ note i(2)
+ also note e(1)
+ finally have "y > f i" .
+ moreover have "y \<le> f i" by (rule f_le_y) fact
+ ultimately show False by simp
+ qed
+qed
+
+lemma INF_approx_ereal:
+ fixes x::ereal and e::real
+ assumes "e > 0"
+ assumes INF: "x = (INF i : A. f i)"
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ shows "\<exists>i \<in> A. f i < x + e"
+proof (rule ccontr, clarsimp)
+ assume "\<forall>i\<in>A. \<not> f i < x + e"
+ moreover
+ from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
+ ultimately
+ have "(INF i : A. f i) = x + e" using `e > 0`
+ by (intro ereal_INFI)
+ (force, metis add.comm_neutral add_left_mono ereal_less(1)
+ linorder_not_le not_less_iff_gr_or_eq)
+ thus False using assms by auto
+qed
+
+lemma SUP_approx_ereal:
+ fixes x::ereal and e::real
+ assumes "e > 0"
+ assumes SUP: "x = (SUP i : A. f i)"
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ shows "\<exists>i \<in> A. x \<le> f i + e"
+proof (rule ccontr, clarsimp)
+ assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
+ moreover
+ from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
+ ultimately
+ have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
+ by (intro ereal_SUPI)
+ (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
+ metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
+ thus False using assms by auto
+qed
+
+lemma
+ fixes M::"'a::{enumerable_basis, complete_space} measure"
+ assumes sb: "sets M = sets borel"
+ assumes "emeasure M (space M) \<noteq> \<infinity>"
+ assumes "B \<in> sets borel"
+ shows inner_regular: "emeasure M B =
+ (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
+ and outer_regular: "emeasure M B =
+ (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
+proof -
+ have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
+ hence sU: "space M = UNIV" by simp
+ interpret finite_measure M by rule fact
+ have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
+ (\<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"
+ by (rule ereal_approx_SUP)
+ (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
+ have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
+ (\<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"
+ by (rule ereal_approx_INF)
+ (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
+ from countable_dense_setE guess x::"nat \<Rightarrow> 'a" . note x = this
+ {
+ fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
+ with x[OF this]
+ have x: "space M = (\<Union>n. cball (x n) r)"
+ by (auto simp add: sU) (metis dist_commute order_less_imp_le)
+ 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))"
+ by (rule Lim_emeasure_incseq)
+ (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
+ also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
+ unfolding x by force
+ finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
+ } note M_space = this
+ {
+ fix e ::real and n :: nat assume "e > 0" "n > 0"
+ hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
+ from M_space[OF `1/n>0`]
+ have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
+ unfolding emeasure_eq_measure by simp
+ from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
+ obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
+ e * 2 powr -n"
+ by auto
+ hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+ measure M (space M) - e * 2 powr -real n"
+ by (auto simp: dist_real_def)
+ hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+ measure M (space M) - e * 2 powr - real n" ..
+ } note k=this
+ hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
+ measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
+ by blast
+ then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
+ \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+ apply atomize_elim unfolding bchoice_iff .
+ hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
+ \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+ unfolding Ball_def by blast
+ have approx_space:
+ "\<And>e. e > 0 \<Longrightarrow>
+ \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
+ (is "\<And>e. _ \<Longrightarrow> ?thesis e")
+ proof -
+ fix e :: real assume "e > 0"
+ def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
+ have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
+ hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
+ from k[OF `e > 0` zero_less_Suc]
+ have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
+ by (simp add: algebra_simps B_def finite_measure_compl)
+ hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
+ by (simp add: finite_measure_compl)
+ def K \<equiv> "\<Inter>n. B n"
+ from `closed (B _)` have "closed K" by (auto simp: K_def)
+ hence [simp]: "K \<in> sets M" by (simp add: sb)
+ have "measure M (space M) - measure M K = measure M (space M - K)"
+ by (simp add: finite_measure_compl)
+ also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
+ also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
+ by (rule emeasure_subadditive_countably) (auto simp: summable_def)
+ also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
+ using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
+ also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
+ by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+ also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
+ unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
+ by simp
+ also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
+ by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
+ also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
+ finally have "measure M (space M) \<le> measure M K + e" by simp
+ hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
+ moreover have "compact K"
+ unfolding compact_eq_totally_bounded
+ proof safe
+ show "complete K" using `closed K` by (simp add: complete_eq_closed)
+ fix e'::real assume "0 < e'"
+ from nat_approx_posE[OF this] guess n . note n = this
+ let ?k = "x ` {0..k e (Suc n)}"
+ have "finite ?k" by simp
+ moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
+ ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
+ qed
+ ultimately
+ show "?thesis e " by (auto simp: sU)
+ qed
+ have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
+ proof
+ fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
+ hence [simp]: "A \<in> sets M" by (simp add: sb)
+ show "?inner A"
+ proof (rule approx_inner)
+ fix e::real assume "e > 0"
+ from approx_space[OF this] obtain K where
+ K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
+ by (auto simp: emeasure_eq_measure)
+ hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
+ have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
+ by (simp add: emeasure_eq_measure)
+ also have "\<dots> = measure M (A - A \<inter> K)"
+ by (subst finite_measure_Diff) auto
+ also have "A - A \<inter> K = A \<union> K - K" by auto
+ also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
+ by (subst finite_measure_Diff) auto
+ also have "\<dots> \<le> measure M (space M) - measure M K"
+ by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
+ also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
+ finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
+ by (simp add: emeasure_eq_measure algebra_simps)
+ moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
+ ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
+ by blast
+ qed simp
+ show "?outer A"
+ proof cases
+ assume "A \<noteq> {}"
+ let ?G = "\<lambda>d. {x. infdist x A < d}"
+ {
+ fix d
+ have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
+ also have "open \<dots>"
+ by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
+ finally have "open (?G d)" .
+ } note open_G = this
+ from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
+ have "A = {x. infdist x A = 0}" by auto
+ also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
+ proof (auto, rule ccontr)
+ fix x
+ assume "infdist x A \<noteq> 0"
+ hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
+ from nat_approx_posE[OF this] guess n .
+ moreover
+ assume "\<forall>i. infdist x A < 1 / real (Suc i)"
+ hence "infdist x A < 1 / real (Suc n)" by auto
+ ultimately show False by simp
+ qed
+ also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
+ proof (rule INF_emeasure_decseq[symmetric], safe)
+ fix i::nat
+ from open_G[of "1 / real (Suc i)"]
+ show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
+ next
+ show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
+ by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
+ simp: decseq_def le_eq_less_or_eq)
+ qed simp
+ finally
+ have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
+ moreover
+ have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+ proof (intro INF_mono)
+ fix m
+ have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
+ moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
+ ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
+ emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
+ by blast
+ qed
+ moreover
+ have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+ by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
+ ultimately show ?thesis by simp
+ qed (auto intro!: ereal_INFI)
+ qed
+ let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
+ interpret dynkin: dynkin_system "space M" ?D
+ proof (rule dynkin_systemI)
+ have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
+ hence "?outer (space M)" by (simp add: min_def INF_def)
+ moreover
+ have "?inner (space M)"
+ proof (rule ereal_approx_SUP)
+ fix e::real assume "0 < e"
+ thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
+ by (rule approx_space)
+ qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
+ ultimately show "space M \<in> ?D" by (simp add: sU sb)
+ next
+ fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
+ from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
+ hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
+ and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
+ have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
+ also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"
+ unfolding inner by (subst INFI_ereal_cminus) force+
+ also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
+ by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+ also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
+ by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
+ also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
+ (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
+ by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
+ (rule INF_cong, auto simp add: sU intro!: INF_cong)
+ finally have
+ "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
+ moreover have
+ "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
+ by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
+ ultimately have "?outer (space M - B)" by simp
+ moreover
+ {
+ have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
+ also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"
+ unfolding outer by (subst SUPR_ereal_cminus) auto
+ also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
+ by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+ also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
+ by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
+ (rule SUP_cong, auto simp: sU)
+ also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+ proof (safe intro!: antisym SUP_least)
+ fix K assume "closed K" "K \<subseteq> space M - B"
+ from closed_in_D[OF `closed K`]
+ have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
+ show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+ unfolding K_inner using `K \<subseteq> space M - B`
+ by (auto intro!: SUP_upper SUP_least)
+ qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
+ finally have "?inner (space M - B)" .
+ } hence "?inner (space M - B)" .
+ ultimately show "space M - B \<in> ?D" by auto
+ next
+ fix D :: "nat \<Rightarrow> _"
+ assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
+ moreover assume "disjoint_family D"
+ ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
+ also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
+ by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
+ finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
+ by (simp add: emeasure_eq_measure)
+ have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
+ moreover
+ hence "?inner (\<Union>i. D i)"
+ proof (rule approx_inner)
+ fix e::real assume "e > 0"
+ with measure_LIMSEQ
+ 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"
+ by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
+ hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
+ then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
+ unfolding choice_iff by blast
+ have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
+ by (auto simp add: emeasure_eq_measure)
+ also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
+ also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
+ also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
+ also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
+ finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
+ using n0 by auto
+ 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)"
+ proof
+ fix i
+ from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
+ have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
+ using `range D \<subseteq> ?D` by blast
+ from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
+ show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
+ by (auto simp: emeasure_eq_measure)
+ qed
+ then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
+ "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
+ unfolding choice_iff by blast
+ let ?K = "\<Union>i\<in>{0..<n0}. K i"
+ have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
+ unfolding disjoint_family_on_def by blast
+ hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
+ by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
+ have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
+ also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
+ using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
+ also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
+ by (simp add: setsum.distrib)
+ also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) + e / 2" using `0 < e`
+ by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
+ finally
+ have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
+ by auto
+ hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
+ moreover
+ have "?K \<subseteq> (\<Union>i. D i)" using K by auto
+ moreover
+ have "compact ?K" using K by auto
+ ultimately
+ 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
+ thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
+ qed
+ moreover have "?outer (\<Union>i. D i)"
+ proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
+ fix e::real assume "e > 0"
+ 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)"
+ proof
+ fix i::nat
+ from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
+ have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
+ using `range D \<subseteq> ?D` by blast
+ from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
+ show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
+ by (auto simp: emeasure_eq_measure)
+ qed
+ then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
+ "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
+ unfolding choice_iff by blast
+ let ?U = "\<Union>i. U i"
+ have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U `(\<Union>i. D i) \<in> sets M`
+ by (subst emeasure_Diff) (auto simp: sb)
+ also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U `range D \<subseteq> sets M`
+ by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
+ also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U `range D \<subseteq> sets M`
+ by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
+ also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
+ by (intro suminf_le_pos, subst emeasure_Diff)
+ (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
+ also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
+ by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+ also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
+ unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
+ by simp
+ also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
+ by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
+ also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
+ finally
+ have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
+ moreover
+ have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
+ moreover
+ have "open ?U" using U by auto
+ ultimately
+ 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
+ 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" ..
+ qed
+ ultimately show "(\<Union>i. D i) \<in> ?D" by safe
+ qed
+ have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
+ also have "\<dots> = dynkin (space M) (Collect closed)"
+ proof (rule sigma_eq_dynkin)
+ show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
+ show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
+ qed
+ also have "\<dots> \<subseteq> ?D" using closed_in_D
+ by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
+ finally have "sets borel \<subseteq> ?D" .
+ moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
+ ultimately have "sets borel = ?D" by simp
+ with assms show "?inner B" and "?outer B" by auto
+qed
+
+end
+
--- a/src/HOL/SEQ.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/SEQ.thy Thu Nov 15 10:49:58 2012 +0100
@@ -171,6 +171,12 @@
thus ?case by arith
qed
+lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
+ unfolding subseq_def by simp
+
+lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
+ using assms by (auto simp: subseq_def)
+
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X"
by (simp add: incseq_def monoseq_def)
@@ -181,6 +187,20 @@
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
by (simp add: decseq_def incseq_def)
+lemma INT_decseq_offset:
+ assumes "decseq F"
+ shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
+proof safe
+ fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
+ show "x \<in> F i"
+ proof cases
+ from x have "x \<in> F n" by auto
+ also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
+ unfolding decseq_def by simp
+ finally show ?thesis .
+ qed (insert x, simp)
+qed auto
+
subsection {* Defintions of limits *}
abbreviation (in topological_space)