Up to index of Isabelle/HOL/HOL-Multivariate_Analysis/HOL-Probability/Stochastic_Processes
theory Polish_Space(* Author: Fabian Immler <immler@in.tum.de> *)
theory Polish_Space
imports Auxiliarities
begin
section {* Topological Formalizations Leading to Polish Spaces *}
subsection {* Characterization of Compact Sets *}
lemma pos_approach_nat:
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)) ≤ 1 / (1/e)"
by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
also have "… = e" by simp
finally show "∃n. 1 / real (Suc n) < e" ..
qed
text {* TODO: move to Topology-Euclidean-Space *}
lemma compact_eq_totally_bounded:
shows "compact s <-> complete s ∧ (∀e>0. ∃k. finite k ∧ s ⊆ (\<Union>((λx. ball x e) ` k)))"
proof (safe intro!: compact_imp_complete)
fix e::real
def f ≡ "(λx::'a. ball x e) ` UNIV"
assume "0 < e" "compact s"
hence "(∀t∈f. open t) ∧ s ⊆ \<Union>f --> (∃f'⊆f. finite f' ∧ s ⊆ \<Union>f')"
by (simp add: compact_eq_heine_borel)
moreover
have d0: "!!x::'a. dist x x < e" using `0 < e` by simp
hence "(∀t∈f. open t) ∧ s ⊆ \<Union>f" by (auto simp: f_def intro!: d0)
ultimately have "(∃f'⊆f. finite f' ∧ s ⊆ \<Union>f')" ..
then guess K .. note K = this
have "∀K'∈K. ∃k. K' = ball k e" using K by (auto simp: f_def)
then obtain k where "!!K'. K' ∈ K ==> K' = ball (k K') e" unfolding bchoice_iff by blast
thus "∃k. finite k ∧ s ⊆ \<Union>(λx. ball x e) ` k" using K
by (intro exI[where x="k ` K"]) (auto simp: f_def)
next
assume assms: "complete s" "∀e>0. ∃k. finite k ∧ s ⊆ \<Union>(λx. ball x e) ` k"
show "compact s"
proof cases
assume "s = {}" thus "compact s" by simp
next
assume "s ≠ {}"
show ?thesis
unfolding compact_def
proof safe
fix f::"nat => _" assume "∀n. f n ∈ s" hence f: "!!n. f n ∈ s" by simp
from assms have "∀e. ∃k. e>0 --> finite k ∧ s ⊆ (\<Union>((λx. ball x e) ` k))" by simp
then obtain K where
K: "!!e. e > 0 ==> finite (K e) ∧ s ⊆ (\<Union>((λx. ball x e) ` (K e)))"
unfolding choice_iff by blast
{
fix e::real and f' have f': "!!n::nat. (f o f') n ∈ s" using f by auto
assume "e > 0"
from K[OF this] have K: "finite (K e)" "s ⊆ (\<Union>((λx. ball x e) ` (K e)))"
by simp_all
have "∃k∈(K e). ∃r. subseq r ∧ (∀i. (f o f' o r) i ∈ ball k e)"
proof (rule ccontr)
from K have "finite (K e)" "K e ≠ {}" "s ⊆ (\<Union>((λx. ball x e) ` (K e)))"
using `s ≠ {}`
by auto
moreover
assume "¬ (∃k∈K e. ∃r. subseq r ∧ (∀i. (f o f' o r) i ∈ ball k e))"
hence "!!r k. k ∈ K e ==> subseq r ==> (∃i. (f o f' o r) i ∉ ball k e)" by simp
ultimately
show False using f'
proof (induct arbitrary: s f f' rule: finite_ne_induct)
case (singleton x)
have "∃i. (f o f' o id) i ∉ 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>((λx. ball x e) ` (insert x A)))"
using insert by (intro infinite_super[OF _ inf_ms]) auto
also have "((f o f') -` \<Union>((λx. ball x e) ` (insert x A))) =
{m. (f o f') m ∈ ball x e} ∪ {m. (f o f') m ∈ \<Union>((λx. ball x e) ` A)}" by auto
finally have "infinite …" .
moreover assume "finite {m. (f o f') m ∈ ball x e}"
ultimately have inf: "infinite {m. (f o f') m ∈ \<Union>((λx. ball x e) ` A)}" by blast
hence "A ≠ {}" by auto then obtain k where "k ∈ A" by auto
def r ≡ "enumerate {m. (f o f') m ∈ \<Union>((λx. ball x e) ` A)}"
have r_mono: "!!n m. n < m ==> 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: "!!n. r n ∈ {m. (f o f') m ∈ \<Union>((λx. ball x e) ` A)}"
using enumerate_in_set[OF inf] by (simp add: r_def)
show False
proof (rule insert)
show "\<Union>(λx. ball x e) ` A ⊆ \<Union>(λx. ball x e) ` A" by simp
fix k s assume "k ∈ A" "subseq s"
thus "∃i. (f o f' o r o s) i ∉ ball k e" using `subseq r`
by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
next
fix n show "(f o f' o r) n ∈ \<Union>(λx. ball x e) ` A" using r_in_set by auto
qed
next
assume inf: "infinite {m. (f o f') m ∈ ball x e}"
def r ≡ "enumerate {m. (f o f') m ∈ ball x e}"
have r_mono: "!!n m. n < m ==> 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) ∉ ball x e" by auto
moreover
have r_in_set: "!!n. r n ∈ {m. (f o f') m ∈ ball x e}"
using enumerate_in_set[OF inf] by (simp add: r_def)
hence "(f o f') (r i) ∈ ball x e" by simp
ultimately show False by simp
qed
qed
qed
}
hence "∀f'. ∀e > 0. (∃k∈K e. ∃r. subseq r ∧ (∀i. (f o f' o r) i ∈ ball k e))" by simp
hence "∀f'. ∀e. (∃k. e > 0 --> (k ∈ K e ∧ (∃r. subseq r ∧ (∀i. (f o f' o r) i ∈ ball k e))))"
by (simp add: Bex_def)
then obtain k where k: "∀f'. ∀e > 0. (k f' e ∈ K e ∧
(∃r. subseq r ∧ (∀i. (f o f' o r) i ∈ ball (k f' e) e)))"
unfolding choice_iff by atomize_elim
let ?P = "λn s x. (∀i. (f o s o x) i ∈ ball (k s (1/real (Suc n))) (1/real (Suc n)))"
interpret subseqs ?P using k
by unfold_locales simp
from `complete s` have limI: "!!f. (!!n. f n ∈ s) ==> Cauchy f ==> (∃l∈s. f ----> l)"
by (simp add: complete_def)
have "∃l∈s. (f o diagseq) ----> l"
proof (intro limI metric_CauchyI)
fix e::real assume "0 < e" hence "0 < e / 2" by auto
from pos_approach_nat[OF this] guess n . note n = this
show "∃M. ∀m≥M. ∀n≥M. dist ((f o diagseq) m) ((f o diagseq) n) < e"
proof (rule exI[where x="Suc n"], safe)
fix m mm assume "Suc n ≤ m" "Suc n ≤ mm"
let ?e = "1 / real (Suc n)"
let ?k = "(k (seqseq n) ?e)"
from reducer_reduces[of n]
have "!!i. (f o seqseq (Suc n)) i ∈ ball ?k ?e" unfolding seqseq_reducer by simp
moreover
note diagseq_sub[OF `Suc n ≤ m`] diagseq_sub[OF `Suc n ≤ mm`]
ultimately have "{(f o diagseq) m, (f o diagseq) mm} ⊆ ball ?k ?e" by auto
also have "… ⊆ ball ?k (e / 2)" using n by (intro subset_ball) simp
finally
have "dist ?k ((f o diagseq) m) + dist ?k ((f o diagseq) mm) < e / 2 + e /2"
by (intro add_strict_mono) auto
hence "dist ((f o diagseq) m) ?k + dist ((f o diagseq) mm) ?k < e"
by (simp add: dist_commute)
moreover have "dist ((f o diagseq) m) ((f o diagseq) mm) ≤
dist ((f o diagseq) m) ?k + dist ((f o diagseq) mm) ?k"
by (rule dist_triangle2)
ultimately show "dist ((f o diagseq) m) ((f o diagseq) mm) < e"
by simp
qed
next
fix n show "(f o diagseq) n ∈ s" using f by simp
qed
thus "∃l∈s. ∃r. subseq r ∧ (f o r) ----> l" using subseq_diagseq by auto
qed
qed
qed
subsection {* Infimum Distance *}
definition "infdist x A = Inf {dist x a|a. a ∈ A}"
lemma infdist_nonneg:
assumes "A ≠ {}"
shows "0 ≤ infdist x A"
using assms by (auto simp add: infdist_def)
lemma infdist_le:
assumes "a ∈ A"
assumes "d = dist x a"
shows "infdist x A ≤ d"
using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
lemma infdist_zero[simp]:
assumes "a ∈ A" shows "infdist a A = 0"
proof -
from infdist_le[OF assms, of "dist a a"] have "infdist a A ≤ 0" by auto
with infdist_nonneg[of A a] assms show "infdist a A = 0" by auto
qed
lemma infdist_triangle:
assumes "A ≠ {}"
shows "infdist x A ≤ infdist y A + dist x y"
proof -
from assms obtain a where "a ∈ A" by auto
have "infdist x A ≤ Inf {dist x y + dist y a |a. a ∈ A}"
proof
from assms show "{dist x y + dist y a |a. a ∈ A} ≠ {}" by simp
fix d assume "d ∈ {dist x y + dist y a |a. a ∈ A}"
then obtain a where d: "d = dist x y + dist y a" "a ∈ A" by auto
show "infdist x A ≤ d"
unfolding infdist_def
proof (rule Inf_lower2)
show "dist x a ∈ {dist x a |a. a ∈ A}" using `a ∈ A` by auto
show "dist x a ≤ d" unfolding d by (rule dist_triangle)
fix d assume "d ∈ {dist x a |a. a ∈ A}"
then obtain a where "a ∈ A" "d = dist x a" by auto
thus "infdist x A ≤ d" by (rule infdist_le)
qed
qed
also have "… = dist x y + infdist y A"
proof (rule Inf_eq, safe)
fix a assume "a ∈ A"
thus "dist x y + infdist y A ≤ dist x y + dist y a" by (auto intro: infdist_le)
next
fix i assume inf: "!!d. d ∈ {dist x y + dist y a |a. a ∈ A} ==> i ≤ d"
hence "i - dist x y ≤ infdist y A" unfolding infdist_def using `a ∈ A`
by (intro Inf_greatest) (auto simp: field_simps)
thus "i ≤ dist x y + infdist y A" by simp
qed
finally show ?thesis by simp
qed
lemma
in_closure_iff_infdist_zero:
assumes "A ≠ {}"
shows "x ∈ closure A <-> infdist x A = 0"
proof
assume "x ∈ closure A"
show "infdist x A = 0"
proof (rule ccontr)
assume "infdist x A ≠ 0"
with infdist_nonneg[OF `A ≠ {}`, of x] have "infdist x A > 0" by auto
hence "ball x (infdist x A) ∩ closure A = {}" apply auto
by (metis `0 < infdist x A` `x ∈ closure A` closure_approachable dist_commute
eucl_less_not_refl euclidean_trans(2) infdist_le)
hence "x ∉ closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
thus False using `x ∈ closure A` by simp
qed
next
assume x: "infdist x A = 0"
then obtain a where "a ∈ A" by atomize_elim (metis all_not_in_conv assms)
show "x ∈ closure A" unfolding closure_approachable
proof (safe, rule ccontr)
fix e::real assume "0 < e"
assume "¬ (∃y∈A. dist y x < e)"
hence "infdist x A ≥ e" using `a ∈ 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 ≠ {}"
shows "x ∈ A <-> infdist x A = 0"
proof -
have "x ∈ closure A <-> infdist x A = 0"
by (rule in_closure_iff_infdist_zero) fact
with assms show ?thesis by simp
qed
lemma continuous_infdist:
assumes "A ≠ {}"
shows "continuous (at x) (λx. infdist x A)"
unfolding continuous_at_eps_delta
proof safe
fix e ::real assume "0 < e"
moreover {
fix y
from infdist_triangle[OF `A ≠ {}`, of x y] infdist_triangle[OF `A ≠ {}`, of y x]
have "dist (infdist y A) (infdist x A) ≤ dist y x" by (simp add: dist_commute dist_real_def)
also assume "dist y x < e"
finally have "dist (infdist y A) (infdist x A) < e" .
} ultimately show "∃d>0. ∀x'. dist x' x < d --> dist (infdist x' A) (infdist x A) < e" by blast
qed
subsection {* Topological Basis *}
context topological_space
begin
definition "topological_basis B =
((∀b∈B. open b) ∧ (∀x. open x --> (∃B'. B' ⊆ B ∧ Union B' = x)))"
lemma topological_basis_iff:
assumes "!!B'. B' ∈ B ==> open B'"
shows "topological_basis B <-> (∀O'. open O' --> (∀x∈O'. ∃B'∈B. x ∈ B' ∧ B' ⊆ O'))"
(is "_ <-> ?rhs")
proof safe
fix O' and x::'a
assume H: "topological_basis B" "open O'" "x ∈ O'"
hence "(∃B'⊆B. \<Union>B' = O')" by (simp add: topological_basis_def)
then obtain B' where "B' ⊆ B" "O' = \<Union>B'" by auto
thus "∃B'∈B. x ∈ B' ∧ B' ⊆ 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 "∀x∈O'. f x ∈ B ∧ x ∈ f x ∧ f x ⊆ O'"
by (force intro: bchoice simp: Bex_def)
thus "∃B'⊆B. \<Union>B' = O'"
by (auto intro: exI[where x="{f x |x. x ∈ O'}"])
qed
qed
lemma topological_basisI:
assumes "!!B'. B' ∈ B ==> open B'"
assumes "!!O' x. open O' ==> x ∈ O' ==> ∃B'∈B. x ∈ B' ∧ B' ⊆ 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 ∈ O'"
obtains B' where "B' ∈ B" "x ∈ B'" "B' ⊆ O'"
proof atomize_elim
from assms have "!!B'. B'∈B ==> open B'" by (simp add: topological_basis_def)
with topological_basis_iff assms
show "∃B'. B' ∈ B ∧ x ∈ B' ∧ B' ⊆ O'" using assms by (simp add: Bex_def)
qed
end
subsection {* Enumerable Basis *}
class enumerable_basis = topological_space +
assumes ex_enum_basis: "∃f::nat => 'a set. topological_basis (range f)"
begin
definition enum_basis'::"nat => '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 => 'a set"
where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
lemma
open_enum_basis:
assumes "B ∈ 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 ∈ 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 "∃B'∈range enum_basis. x ∈ B' ∧ B' ⊆ O'" by blast
qed
lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
lemma open_enumerable_basis_ex:
assumes "open X"
shows "∃N. X = (\<Union>n∈N. enum_basis n)"
proof -
from enumerable_basis assms obtain B' where "B' ⊆ range enum_basis" "X = Union B'"
unfolding topological_basis_def by blast
hence "Union B' = (\<Union>n∈{n. enum_basis n ∈ 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∈N. enum_basis n)"
using assms open_enumerable_basis_ex by (atomize_elim) simp
text {* Construction of an Increasing Sequence Approximating Open Sets *}
lemma empty_basisI[intro]: "{} ∈ 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 ∈ range enum_basis" "B ∈ range enum_basis"
shows "A ∪ B ∈ range enum_basis"
proof -
from assms obtain a b where "A ∪ B = enum_basis a ∪ enum_basis b" by auto
also have "… = 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 "∃S. incseq S ∧ (\<Union>j. S j) = X ∧ range S ⊆ range enum_basis"
proof -
from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n∈N. enum_basis n)" by auto
hence X: "X = (\<Union>n. if n ∈ N then enum_basis n else {})" by (auto split: split_if_asm)
def S ≡ "nat_rec (if 0 ∈ N then enum_basis 0 else {})
(λn S. if (Suc n) ∈ N then S ∪ enum_basis (Suc n) else S)"
have S_simps[simp]:
"S 0 = (if 0 ∈ N then enum_basis 0 else {})"
"!!n. S (Suc n) = (if (Suc n) ∈ N then S n ∪ 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 ∈ N" "x ∈ enum_basis n"
hence "x ∈ S n" by (cases n) auto
thus "x ∈ (\<Union>j. S j)" by auto
next
fix x j
assume "x ∈ S j"
thus "x ∈ UNION N enum_basis" by (induct j) (auto split: split_if_asm)
qed
moreover have "range S ⊆ range enum_basis"
proof safe
fix j show "S j ∈ 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 ⊆ range enum_basis"
using open_imp_Union_of_incseq assms by atomize_elim
end
lemma borel_eq_sigma_enum_basis:
"sets borel = sigma_sets (space borel) (range enum_basis)"
apply (simp add: borel_def)
proof (intro 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 ∈ N then enum_basis n else {})" by (auto split: split_if_asm)
also have "… ∈ sigma_sets UNIV (range enum_basis)" by (rule Union) auto
finally show "x ∈ sigma_sets UNIV (range enum_basis)" .
next
fix n
have "open (enum_basis n)" by (rule open_enum_basis) simp
thus "enum_basis n ∈ sigma_sets UNIV (Collect open)" by auto
qed
lemma countable_dense_set:
shows "∃x::nat => _. ∀(y::'a::enumerable_basis set). open y --> y ≠ {} --> (∃n. x n ∈ y)"
proof -
def x ≡ "λn. (SOME x::'a. x ∈ enum_basis n)"
have x: "!!n. enum_basis n ≠ ({}::'a set) ==> x n ∈ enum_basis n" unfolding x_def
by (rule someI_ex) auto
have "∀y. open y --> y ≠ {} --> (∃n. x n ∈ y)"
proof (intro allI impI)
fix y::"'a set" assume "open y" "y ≠ {}"
from open_enumerable_basisE[OF `open y`] guess N . note N = this
obtain n where n: "n ∈ N" "enum_basis n ≠ ({}::'a set)"
proof (atomize_elim, rule ccontr, clarsimp)
assume "∀n. n ∈ N --> enum_basis n = ({}::'a set)"
hence "(\<Union>n∈N. enum_basis n) = (\<Union>n∈N. {}::'a set)"
by (intro UN_cong) auto
hence "y = {}" unfolding N by simp
with `y ≠ {}` show False by auto
qed
with x N n have "x n ∈ y" by auto
thus "∃n. x n ∈ y" ..
qed
thus ?thesis by blast
qed
lemma countable_dense_setE:
obtains x :: "nat => _"
where "!!(y::'a::enumerable_basis set). open y ==> y ≠ {} ==> ∃n. x n ∈ y"
using countable_dense_set by blast
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
text {*
TODO:
Rules in @{text "Topology_Euclidean_Space"} should be proved in the
@{text "ordered_euclidean_space"} locale!
Then we can use subclass instead of instance.
*}
instance ordered_euclidean_space ⊆ polish_space
proof
def to_cube ≡ "λ(a, b). {Chi (real_of_rat o op ! a)<..<Chi (real_of_rat o op ! b)}::'a set"
def enum ≡ "λ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 × rat list")
(simp add: open_interval to_cube_def)
qed
moreover have "(∀x. open x --> (∃B'⊆range enum. \<Union>B' = x))"
proof safe
fix x::"'a set" assume "open x"
def lists ≡ "{(a, b) |a b. to_cube (a, b) ⊆ 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 ⊆ range enum"
proof
fix x assume "x ∈ to_cube ` lists"
then obtain l where "l ∈ lists" "x = to_cube l" by auto
hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
thus "x ∈ range enum" by simp
qed
ultimately
show "∃B'⊆range enum. \<Union>B' = x" by blast
qed
ultimately
show "∃f::nat=>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
qed
instantiation nat::topological_space
begin
definition open_nat::"nat set => bool"
where "open_nat s = True"
instance proof qed (auto simp: open_nat_def)
end
instantiation nat::metric_space
begin
definition dist_nat::"nat => nat => 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=>nat" assume "Cauchy X"
hence "∃n. ∀m≥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::polish_space
proof
have "topological_basis (range (λn::nat. {n}))"
by (intro topological_basisI) (auto simp: open_nat_def)
thus "∃f::nat=>nat set. topological_basis (range f)" by blast
qed
subsection {* Regularity of Measures *}
lemma ereal_approx_SUP:
fixes x::ereal
assumes A_notempty: "A ≠ {}"
assumes f_bound: "!!i. i ∈ A ==> f i ≤ x"
assumes f_fin: "!!i. i ∈ A ==> f i ≠ ∞"
assumes f_nonneg: "!!i. 0 ≤ f i"
assumes approx: "!!e. (e::real) > 0 ==> ∃i ∈ A. x ≤ f i + e"
shows "x = (SUP i : A. f i)"
proof (subst eq_commute, rule ereal_SUPI)
show "!!i. i ∈ A ==> f i ≤ x" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(!!i::'a. i ∈ A ==> f i ≤ y)"
with A_notempty f_nonneg have "y ≥ 0" by auto (metis order_trans)
show "x ≤ y"
proof (rule ccontr)
assume "¬ x ≤ y" hence "x > y" by simp
hence y_fin: "¦y¦ ≠ ∞" using `y ≥ 0` by auto
have x_fin: "¦x¦ ≠ ∞" using `x > y` f_fin approx[where e = 1] by auto
def e ≡ "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 ∈ A" "x ≤ 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 ≤ 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 ≠ {}"
assumes f_bound: "!!i. i ∈ A ==> x ≤ f i"
assumes f_fin: "!!i. i ∈ A ==> f i ≠ ∞"
assumes f_nonneg: "!!i. 0 ≤ f i"
assumes approx: "!!e. (e::real) > 0 ==> ∃i ∈ A. f i ≤ x + e"
shows "x = (INF i : A. f i)"
proof (subst eq_commute, rule ereal_INFI)
show "!!i. i ∈ A ==> x ≤ f i" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(!!i::'a. i ∈ A ==> y ≤ f i)"
with A_notempty f_fin have "y ≠ ∞" by force
show "y ≤ x"
proof (rule ccontr)
assume "¬ y ≤ x" hence "y > x" by simp hence "y ≠ - ∞" by auto
hence y_fin: "¦y¦ ≠ ∞" using `y ≠ ∞` by auto
have x_fin: "¦x¦ ≠ ∞" 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 ≡ "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 ∈ A" "x + e ≥ f i" by blast
note i(2)
also note e(1)
finally have "y > f i" .
moreover have "y ≤ 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 "¦x¦ ≠ ∞"
shows "∃i ∈ A. f i < x + e"
proof (rule ccontr, clarsimp)
assume "∀i∈A. ¬ f i < x + e"
moreover
from INF have "!!y. (!!i. i ∈ A ==> y ≤ f i) ==> y ≤ 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 "¦x¦ ≠ ∞"
shows "∃i ∈ A. x ≤ f i + e"
proof (rule ccontr, clarsimp)
assume "∀i∈A. ¬ x ≤ f i + e"
moreover
from SUP have "!!y. (!!i. i ∈ A ==> f i ≤ y) ==> y ≥ x" by (auto intro: SUP_least)
ultimately
have "(SUP i : A. f i) = x - e" using `e > 0` `¦x¦ ≠ ∞`
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::polish_space measure"
assumes sb: "sets M = sets borel"
assumes "emeasure M (space M) ≠ ∞"
assumes "B ∈ sets borel"
shows inner_regular: "emeasure M B =
(SUP K : {K. K ⊆ B ∧ compact K}. emeasure M K)" (is "?inner B")
and outer_regular: "emeasure M B =
(INF U : {U. B ⊆ U ∧ 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: "!!A. A ∈ sets M ==>
(!!e. e > 0 ==> ∃K. K ⊆ A ∧ compact K ∧ emeasure M A ≤ emeasure M K + ereal e) ==> ?inner A"
by (rule ereal_approx_SUP)
(force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
have approx_outer: "!!A. A ∈ sets M ==>
(!!e. e > 0 ==> ∃B. A ⊆ B ∧ open B ∧ emeasure M B ≤ emeasure M A + ereal e) ==> ?outer A"
by (rule ereal_approx_INF)
(force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
from countable_dense_setE guess x::"nat => 'a" . note x = this
{
fix r::real assume "r > 0" hence "!!y. open (ball y r)" "!!y. ball y r ≠ {}" 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 "(λk. emeasure M (\<Union>n∈{0..k}. cball (x n) r)) ----> M (\<Union>k. (\<Union>n∈{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∈{0..k}. cball (x n) r)) = space M"
unfolding x by force
finally have "(λk. M (\<Union>n∈{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 "(λk. measure M (\<Union>i∈{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∈{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
e * 2 powr -n"
by auto
hence "measure M (\<Union>i∈{0..k}. cball (x i) (1/real n)) ≥
measure M (space M) - e * 2 powr -real n"
by (auto simp: dist_real_def)
hence "∃k. measure M (\<Union>i∈{0..k}. cball (x i) (1/real n)) ≥
measure M (space M) - e * 2 powr - real n" ..
} note k=this
hence "∀e∈{0<..}. ∀(n::nat)∈{0<..}. ∃k.
measure M (\<Union>i∈{0..k}. cball (x i) (1/real n)) ≥ measure M (space M) - e * 2 powr - real n"
by blast
then obtain k where k: "∀e∈{0<..}. ∀n∈{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
≤ measure M (\<Union>i∈{0..k e n}. cball (x i) (1 / n))"
apply atomize_elim unfolding bchoice_iff .
hence k: "!!e n. e > 0 ==> n > 0 ==> measure M (space M) - e * 2 powr - n
≤ measure M (\<Union>i∈{0..k e n}. cball (x i) (1 / n))"
unfolding Ball_def by blast
have approx_space:
"!!e. e > 0 ==>
∃K ∈ {K. K ⊆ space M ∧ compact K}. emeasure M (space M) ≤ emeasure M K + ereal e"
(is "!!e. _ ==> ?thesis e")
proof -
fix e :: real assume "e > 0"
def B ≡ "λn. \<Union>i∈{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
have "!!n. closed (B n)" by (auto simp: B_def closed_cball)
hence [simp]: "!!n. B n ∈ sets M" by (simp add: sb)
from k[OF `e > 0` zero_less_Suc]
have "!!n. measure M (space M) - measure M (B n) ≤ e * 2 powr - real (Suc n)"
by (simp add: algebra_simps B_def finite_measure_compl)
hence B_compl_le: "!!n::nat. measure M (space M - B n) ≤ e * 2 powr - real (Suc n)"
by (simp add: finite_measure_compl)
def K ≡ "\<Inter>n. B n"
from `closed (B _)` have "closed K" by (auto simp: K_def)
hence [simp]: "K ∈ 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 "… = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
also have "… ≤ (∑n. emeasure M (space M - B n))"
by (rule emeasure_subadditive_countably) (auto simp: summable_def)
also have "… ≤ (∑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 "… ≤ (∑n. ereal (e * (1 / 2) ^ Suc n))"
by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
also have "… = (∑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 "… = ereal e * (∑n. ((1 / 2) ^ Suc n))"
by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
also have "… = e" unfolding suminf_half_series_ereal by simp
finally have "measure M (space M) ≤ measure M K + e" by simp
hence "emeasure M (space M) ≤ 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 pos_approach_nat[OF this] guess n . note n = this
let ?k = "x ` {0..k e (Suc n)}"
have "finite ?k" by simp
moreover have "K ⊆ \<Union>(λx. ball x e') ` ?k" unfolding K_def B_def using n by force
ultimately show "∃k. finite k ∧ K ⊆ \<Union>(λx. ball x e') ` k" by blast
qed
ultimately
show "?thesis e " by (auto simp: sU)
qed
have closed_in_D: "!!A. closed A ==> ?inner A ∧ ?outer A"
proof
fix A::"'a set" assume "closed A" hence "A ∈ sets borel" by (simp add: compact_imp_closed)
hence [simp]: "A ∈ 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 ⊆ space M" "compact K" "emeasure M (space M) ≤ emeasure M K + e"
by (auto simp: emeasure_eq_measure)
hence [simp]: "K ∈ sets M" by (simp add: sb compact_imp_closed)
have "M A - M (A ∩ K) = M (A ∪ K) - M K" by (simp add: emeasure_eq_measure measure_union)
also have "… ≤ M (space M) - M K"
by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
also have "… ≤ e" using K by (simp add: emeasure_eq_measure)
finally have "emeasure M A ≤ emeasure M (A ∩ K) + ereal e" by (simp add: emeasure_eq_measure)
moreover have "A ∩ K ⊆ A" "compact (A ∩ K)" using `closed A` `compact K` by auto
ultimately show "∃K ⊆ A. compact K ∧ emeasure M A ≤ emeasure M K + ereal e"
by blast
qed simp
show "?outer A"
proof cases
assume "A ≠ {}"
let ?G = "λd. {x. infdist x A < d}"
{
fix d
have "?G d = (λx. infdist x A) -` {..<d}" by auto
also have "open …" using continuous_infdist[OF `A ≠ {}`]
by (intro continuous_open_vimage) auto
finally have "open (?G d)" .
} note open_G = this
from in_closed_iff_infdist_zero[OF `closed A` `A ≠ {}`]
have "A = {x. infdist x A = 0}" by auto
also have "… = (\<Inter>i. ?G (1/real (Suc i)))"
proof (auto, rule ccontr)
fix x
assume "infdist x A ≠ 0"
hence pos: "infdist x A > 0" using infdist_nonneg[OF `A ≠ {}`, of x] by simp
from pos_approach_nat[OF this] guess n .
moreover
assume "∀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 … = (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)) ∈ sets M" by (simp add: sb)
next
show "decseq (λ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 "… ≥ (INF U:{U. A ⊆ U ∧ open U}. emeasure M U)"
proof (intro INF_mono)
fix m
have "?G (1 / real (Suc m)) ∈ {U. A ⊆ U ∧ open U}" using open_G by auto
moreover have "M (?G (1 / real (Suc m))) ≤ M (?G (1 / real (Suc m)))" by simp
ultimately show "∃U∈{U. A ⊆ U ∧ open U}.
emeasure M U ≤ emeasure M {x. infdist x A < 1 / real (Suc m)}"
by blast
qed
moreover
have "emeasure M A ≤ (INF U:{U. A ⊆ U ∧ 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 ∈ sets M. ?inner B ∧ ?outer B}"
interpret dynkin: dynkin_system "space M" ?D
proof (rule dynkin_systemI)
have "{U::'a set. space M ⊆ U ∧ 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 "∃K∈{K. K ⊆ space M ∧ compact K}. emeasure M (space M) ≤ 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 ∈ ?D" by (simp add: sU sb)
next
fix B assume "B ∈ ?D" thus "B ⊆ space M" by (simp add: sU)
from `B ∈ ?D` have [simp]: "B ∈ sets M" and "?inner B" "?outer B" by auto
hence inner: "emeasure M B = (SUP K:{K. K ⊆ B ∧ compact K}. emeasure M K)"
and outer: "emeasure M B = (INF U:{U. B ⊆ U ∧ 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 "… = (INF K:{K. K ⊆ B ∧ compact K}. M (space M) - M K)"
unfolding inner by (subst INFI_ereal_cminus) force+
also have "… = (INF U:{U. U ⊆ B ∧ compact U}. M (space M - U))"
by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
also have "… ≥ (INF U:{U. U ⊆ B ∧ closed U}. M (space M - U))"
by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
also have "(INF U:{U. U ⊆ B ∧ closed U}. M (space M - U)) =
(INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U)"
by (subst INF_image[of "λu. space M - u", symmetric])
(rule INF_cong, auto simp add: sU intro!: INF_cong)
finally have
"(INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U) ≤ emeasure M (space M - B)" .
moreover have
"(INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U) ≥ 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 "… = (SUP U: {U. B ⊆ U ∧ open U}. M (space M) - M U)"
unfolding outer by (subst SUPR_ereal_cminus) auto
also have "… = (SUP U:{U. B ⊆ U ∧ open U}. M (space M - U))"
by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
also have "… = (SUP K:{K. K ⊆ space M - B ∧ closed K}. emeasure M K)"
by (subst SUP_image[of "λu. space M - u", symmetric])
(rule SUP_cong, auto simp: sU)
also have "… = (SUP K:{K. K ⊆ space M - B ∧ compact K}. emeasure M K)"
proof (safe intro!: antisym SUP_least)
fix K assume "closed K" "K ⊆ space M - B"
from closed_in_D[OF `closed K`]
have K_inner: "emeasure M K = (SUP K:{Ka. Ka ⊆ K ∧ compact Ka}. emeasure M K)" by simp
show "emeasure M K ≤ (SUP K:{K. K ⊆ space M - B ∧ compact K}. emeasure M K)"
unfolding K_inner using `K ⊆ 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 ∈ ?D" by auto
next
fix D :: "nat => _"
assume "range D ⊆ ?D" hence "range D ⊆ sets M" by auto
moreover assume "disjoint_family D"
ultimately have M[symmetric]: "(∑i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
also have "(λn. ∑i∈{0..<n}. M (D i)) ----> (∑i. M (D i))"
by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
finally have measure_LIMSEQ: "(λn. ∑i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
by (simp add: emeasure_eq_measure)
have "(\<Union>i. D i) ∈ sets M" using `range D ⊆ 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 "∃no. ∀n≥no. ¦(∑i = 0..<n. measure M (D i)) -measure M (\<Union>x. D x)¦ < e/2"
by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
hence "∃n0. ¦(∑i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)¦ < e/2" by auto
then obtain n0 where n0: "¦(∑i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)¦ < e/2"
unfolding choice_iff by blast
have "ereal (∑i = 0..<n0. measure M (D i)) = (∑i = 0..<n0. M (D i))"
by (auto simp add: emeasure_eq_measure)
also have "… = (∑i<n0. M (D i))" by (rule setsum_cong) auto
also have "… ≤ (∑i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
also have "… = M (\<Union>i. D i)" by (simp add: M)
also have "… = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
finally have n0: "measure M (\<Union>i. D i) - (∑i = 0..<n0. measure M (D i)) < e/2"
using n0 by auto
have "∀i. ∃K. K ⊆ D i ∧ compact K ∧ emeasure M (D i) ≤ 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 ⊆ (D i) ∧ compact K}. emeasure M K)"
using `range D ⊆ ?D` by blast
from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
show "∃K. K ⊆ D i ∧ compact K ∧ emeasure M (D i) ≤ emeasure M K + e/(2*Suc n0)"
by (auto simp: emeasure_eq_measure)
qed
then obtain K where K: "!!i. K i ⊆ D i" "!!i. compact (K i)"
"!!i. emeasure M (D i) ≤ emeasure M (K i) + e/(2*Suc n0)"
unfolding choice_iff by blast
let ?K = "\<Union>i∈{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 = (∑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) < (∑i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
also have "(∑i = 0..<n0. measure M (D i)) ≤ (∑i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
also have "… = (∑i = 0..<n0. measure M (K i)) + (∑i = 0..<n0. e/(2*Suc n0))"
by (simp add: setsum.distrib)
also have "… ≤ (∑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) < (∑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 ⊆ (\<Union>i. D i)" using K by auto
moreover
have "compact ?K" using K by auto
ultimately
have "?K⊆(\<Union>i. D i) ∧ compact ?K ∧ emeasure M (\<Union>i. D i) ≤ emeasure M ?K + ereal e" by simp
thus "∃K⊆\<Union>i. D i. compact K ∧ emeasure M (\<Union>i. D i) ≤ emeasure M K + ereal e" ..
qed
moreover have "?outer (\<Union>i. D i)"
proof (rule approx_outer[OF `(\<Union>i. D i) ∈ sets M`])
fix e::real assume "e > 0"
have "∀i::nat. ∃U. D i ⊆ U ∧ open U ∧ 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) ⊆ U ∧ open U}. emeasure M U)"
using `range D ⊆ ?D` by blast
from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
show "∃U. D i ⊆ U ∧ open U ∧ e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
by (auto simp: emeasure_eq_measure)
qed
then obtain U where U: "!!i. D i ⊆ U i" "!!i. open (U i)"
"!!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) ∈ sets M`
by (subst emeasure_Diff) (auto simp: sb)
also have "… ≤ M (\<Union>i. U i - D i)" using U `range D ⊆ sets M`
by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
also have "… ≤ (∑i. M (U i - D i))" using U `range D ⊆ sets M`
by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
also have "… ≤ (∑i. ereal e/(2 powr Suc i))" using U `range D ⊆ 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 "… ≤ (∑n. ereal (e * (1 / 2) ^ Suc n))"
by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
also have "… = (∑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 "… = ereal e * (∑n. ((1 / 2) ^ Suc n))"
by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
also have "… = e" unfolding suminf_half_series_ereal by simp
finally
have "emeasure M ?U ≤ emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
moreover
have "(\<Union>i. D i) ⊆ ?U" using U by auto
moreover
have "open ?U" using U by auto
ultimately
have "(\<Union>i. D i) ⊆ ?U ∧ open ?U ∧ emeasure M ?U ≤ emeasure M (\<Union>i. D i) + ereal e" by simp
thus "∃B. (\<Union>i. D i) ⊆ B ∧ open B ∧ emeasure M B ≤ emeasure M (\<Union>i. D i) + ereal e" ..
qed
ultimately show "(\<Union>i. D i) ∈ ?D" by safe
qed
have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_def_closed sU)
also have "… = dynkin (space M) (Collect closed)"
proof (rule sigma_eq_dynkin)
show "Collect closed ⊆ 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 "… ⊆ ?D" using closed_in_D
by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
finally have "sets borel ⊆ ?D" .
moreover have "?D ⊆ 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