--- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 13 17:41:27 2013 +0100
@@ -3368,4 +3368,80 @@
foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
+lemma dist_less_imp_nth_equal:
+ assumes "dist f g < inverse (2 ^ i)"
+ assumes "j \<le> i"
+ shows "f $ j = g $ j"
+proof cases
+ assume "f \<noteq> g"
+ hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
+ with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+ by (simp add: split_if_asm dist_fps_def)
+ moreover
+ from fps_eq_least_unique[OF `f \<noteq> g`]
+ obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
+ moreover hence "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
+ by (auto simp add: leastP_def setge_def)
+ ultimately show ?thesis using `j \<le> i` by simp
+qed simp
+
+lemma nth_equal_imp_dist_less:
+ assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j"
+ shows "dist f g < inverse (2 ^ i)"
+proof cases
+ assume "f \<noteq> g"
+ hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
+ with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
+ by (simp add: split_if_asm dist_fps_def)
+ moreover
+ from fps_eq_least_unique[OF `f \<noteq> g`]
+ obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
+ with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+ by (metis (full_types) leastPD1 not_le)
+ ultimately show ?thesis by simp
+qed simp
+
+lemma dist_less_eq_nth_equal:
+ shows "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
+ using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
+
+instance fps :: (comm_ring_1) complete_space
+proof
+ fix X::"nat \<Rightarrow> 'a fps"
+ assume "Cauchy X"
+ {
+ fix i
+ have "0 < inverse ((2::real)^i)" by simp
+ from metric_CauchyD[OF `Cauchy X` this] dist_less_imp_nth_equal
+ have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" by blast
+ }
+ then obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis
+ hence "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis
+ show "convergent X"
+ proof (rule convergentI)
+ show "X ----> Abs_fps (\<lambda>i. X (M i) $ i)"
+ unfolding tendsto_iff
+ proof safe
+ fix e::real assume "0 < e"
+ with LIMSEQ_inverse_realpow_zero[of 2, simplified, simplified filterlim_iff,
+ THEN spec, of "\<lambda>x. x < e"]
+ have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
+ by safe (auto simp: eventually_nhds)
+ then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
+ have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
+ thus "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially"
+ proof eventually_elim
+ fix x assume "M i \<le> x"
+ moreover
+ have "\<And>j. j \<le> i \<Longrightarrow> X (M i) $ j = X (M j) $ j"
+ using M by (metis nat_le_linear)
+ ultimately have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)"
+ using M by (force simp: dist_less_eq_nth_equal)
+ also note `inverse (2 ^ i) < e`
+ finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" .
+ qed
+ qed
+ qed
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 13 17:41:27 2013 +0100
@@ -170,99 +170,6 @@
where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
using countable_dense_exists by blast
-text {* Construction of an increasing sequence approximating open sets,
- therefore basis which is closed under union. *}
-
-definition union_closed_basis::"'a set set" where
- "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
-
-lemma basis_union_closed_basis: "topological_basis union_closed_basis"
-proof (rule topological_basisI)
- fix O' and x::'a assume "open O'" "x \<in> O'"
- from topological_basisE[OF is_basis this] guess B' . note B' = this
- thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def
- by (auto intro!: bexI[where x="[B']"])
-next
- fix B' assume "B' \<in> union_closed_basis"
- thus "open B'"
- using topological_basis_open[OF is_basis]
- by (auto simp: union_closed_basis_def)
-qed
-
-lemma countable_union_closed_basis: "countable union_closed_basis"
- unfolding union_closed_basis_def using countable_basis by simp
-
-lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
-
-lemma union_closed_basis_ex:
- assumes X: "X \<in> union_closed_basis"
- shows "\<exists>B'. finite B' \<and> X = \<Union>B' \<and> B' \<subseteq> B"
-proof -
- from X obtain l where "\<And>x. x\<in>set l \<Longrightarrow> x\<in>B" "X = \<Union>set l" by (auto simp: union_closed_basis_def)
- thus ?thesis by auto
-qed
-
-lemma union_closed_basisE:
- assumes "X \<in> union_closed_basis"
- obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast
-
-lemma union_closed_basisI:
- assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B"
- shows "X \<in> union_closed_basis"
-proof -
- from finite_list[OF `finite B'`] guess l ..
- thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l])
-qed
-
-lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
- by (rule union_closed_basisI[of "{}"]) auto
-
-lemma union_basisI[intro]:
- assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis"
- shows "X \<union> Y \<in> union_closed_basis"
- using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE)
-
-lemma open_imp_Union_of_incseq:
- assumes "open X"
- shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis"
-proof -
- from open_countable_basis_ex[OF `open X`]
- obtain B' where B': "B'\<subseteq>B" "X = \<Union>B'" by auto
- from this(1) countable_basis have "countable B'" by (rule countable_subset)
- show ?thesis
- proof cases
- assume "B' \<noteq> {}"
- def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i"
- have S:"\<And>n. S n = \<Union>{from_nat_into B' i|i. i\<in>{0..n}}" unfolding S_def by force
- have "incseq S" by (force simp: S_def incseq_Suc_iff)
- moreover
- have "(\<Union>j. S j) = X" unfolding B'
- proof safe
- fix x X assume "X \<in> B'" "x \<in> X"
- then obtain n where "X = from_nat_into B' n"
- by (metis `countable B'` from_nat_into_surj)
- also have "\<dots> \<subseteq> S n" by (auto simp: S_def)
- finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto
- next
- fix x n
- assume "x \<in> S n"
- also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)"
- by (simp add: S_def)
- also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto
- also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into)
- finally show "x \<in> \<Union>B'" .
- qed
- moreover have "range S \<subseteq> union_closed_basis" using B'
- by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`)
- ultimately show ?thesis by auto
- qed (auto simp: B')
-qed
-
-lemma open_incseqE:
- assumes "open X"
- obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis"
- using open_imp_Union_of_incseq assms by atomize_elim
-
end
class first_countable_topology = topological_space +
@@ -304,6 +211,31 @@
using first_countable_basis[of x]
by atomize_elim auto
+lemma (in first_countable_topology) first_countable_basis_Int_stableE:
+ obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
+ "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
+proof atomize_elim
+ from first_countable_basisE[of x] guess A' . note A' = this
+ def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
+ thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
+ (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
+ proof (safe intro!: exI[where x=A])
+ show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite)
+ fix a assume "a \<in> A"
+ thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
+ next
+ let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N"
+ fix a b assume "a \<in> A" "b \<in> A"
+ then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
+ thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
+ next
+ fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
+ thus "\<exists>a\<in>A. a \<subseteq> S" using a A'
+ by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
+ qed
+qed
+
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
proof
fix x :: "'a \<times> 'b"
@@ -794,7 +726,7 @@
finally show "y \<in> ball x e" by (auto simp: ball_def)
qed (insert a b, auto simp: box_def)
qed
-
+
lemma open_UNION_box:
fixes M :: "'a\<Colon>euclidean_space set"
assumes "open M"
@@ -3704,7 +3636,7 @@
text{* Cauchy-type criteria for uniform convergence. *}
-lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows
+lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space" shows
"(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
(\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs")
proof(rule)
@@ -3738,7 +3670,7 @@
qed
lemma uniformly_cauchy_imp_uniformly_convergent:
- fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel"
+ fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
"\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
@@ -5796,7 +5728,7 @@
show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
qed
-instance ordered_euclidean_space \<subseteq> polish_space ..
+instance euclidean_space \<subseteq> polish_space ..
text {* Intervals in general, including infinite and mixtures of open and closed. *}
--- a/src/HOL/Probability/Borel_Space.thy Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Feb 13 17:41:27 2013 +0100
@@ -149,10 +149,6 @@
thus "b \<in> sigma_sets UNIV (Collect open)" by auto
qed simp_all
-lemma borel_eq_union_closed_basis:
- "borel = sigma UNIV union_closed_basis"
- by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
-
lemma borel_measurable_Pair[measurable (raw)]:
fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
assumes f[measurable]: "f \<in> borel_measurable M"
--- a/src/HOL/Probability/Fin_Map.thy Wed Feb 13 16:30:34 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Wed Feb 13 17:41:27 2013 +0100
@@ -76,9 +76,8 @@
lemma finmap_of_eq_iff[simp]:
assumes "finite i" "finite j"
- shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> restrict m i = restrict n i"
- using assms
- apply (auto simp: finmap_eq_iff restrict_def) by metis
+ shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> (\<forall>k\<in>i. m k= n k)"
+ using assms by (auto simp: finmap_eq_iff)
lemma finmap_of_inj_on_extensional_finite:
assumes "finite K"
@@ -94,17 +93,6 @@
show "x = y" using assms by (simp add: extensional_restrict)
qed
-lemma finmap_choice:
- assumes *: "\<And>i. i \<in> I \<Longrightarrow> \<exists>x. P i x" and I: "finite I"
- shows "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. P i (fm i))"
-proof -
- have "\<exists>f. \<forall>i\<in>I. P i (f i)"
- unfolding bchoice_iff[symmetric] using * by auto
- then guess f ..
- with I show ?thesis
- by (intro exI[of _ "finmap_of I f"]) auto
-qed
-
subsection {* Product set of Finite Maps *}
text {* This is @{term Pi} for Finite Maps, most of this is copied *}
@@ -163,128 +151,19 @@
apply auto
done
-subsection {* Metric Space of Finite Maps *}
-
-instantiation finmap :: (type, metric_space) metric_space
-begin
+subsection {* Topological Space of Finite Maps *}
-definition dist_finmap where
- "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
- card ((domain P - domain Q) \<union> (domain Q - domain P))"
-
-lemma dist_finmap_extend:
- assumes "finite X"
- shows "dist P Q = (\<Sum>i\<in>domain P \<union> domain Q \<union> X. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)) +
- card ((domain P - domain Q) \<union> (domain Q - domain P))"
- unfolding dist_finmap_def add_right_cancel
- using assms extensional_arb[of "(P)\<^isub>F"] extensional_arb[of "(Q)\<^isub>F" "domain Q"]
- by (intro setsum_mono_zero_cong_left) auto
+instantiation finmap :: (type, topological_space) topological_space
+begin
definition open_finmap :: "('a \<Rightarrow>\<^isub>F 'b) set \<Rightarrow> bool" where
- "open_finmap S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-
-lemma add_eq_zero_iff[simp]:
- fixes a b::real
- assumes "a \<ge> 0" "b \<ge> 0"
- shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
-using assms by auto
-
-lemma dist_le_1_imp_domain_eq:
- assumes "dist P Q < 1"
- shows "domain P = domain Q"
-proof -
- have "0 \<le> (\<Sum>i\<in>domain P \<union> domain Q. dist (P i) (Q i))"
- by (simp add: setsum_nonneg)
- with assms have "card (domain P - domain Q \<union> (domain Q - domain P)) = 0"
- unfolding dist_finmap_def by arith
- thus "domain P = domain Q" by auto
-qed
-
-lemma dist_proj:
- shows "dist ((x)\<^isub>F i) ((y)\<^isub>F i) \<le> dist x y"
-proof -
- have "dist (x i) (y i) = (\<Sum>i\<in>{i}. dist (x i) (y i))" by simp
- also have "\<dots> \<le> (\<Sum>i\<in>domain x \<union> domain y \<union> {i}. dist (x i) (y i))"
- by (intro setsum_mono2) auto
- also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_extend[of "{i}"])
- finally show ?thesis by simp
-qed
+ "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
-lemma open_Pi'I:
- assumes open_component: "\<And>i. i \<in> I \<Longrightarrow> open (A i)"
- shows "open (Pi' I A)"
-proof (subst open_finmap_def, safe)
- fix x assume x: "x \<in> Pi' I A"
- hence dim_x: "domain x = I" by (simp add: Pi'_def)
- hence [simp]: "finite I" unfolding dim_x[symmetric] by simp
- have "\<exists>ei. \<forall>i\<in>I. 0 < ei i \<and> (\<forall>y. dist y (x i) < ei i \<longrightarrow> y \<in> A i)"
- proof (safe intro!: bchoice)
- fix i assume i: "i \<in> I"
- moreover with open_component have "open (A i)" by simp
- moreover have "x i \<in> A i" using x i
- by (auto simp: proj_def)
- ultimately show "\<exists>e>0. \<forall>y. dist y (x i) < e \<longrightarrow> y \<in> A i"
- using x by (auto simp: open_dist Ball_def)
- qed
- then guess ei .. note ei = this
- def es \<equiv> "ei ` I"
- def e \<equiv> "if es = {} then 0.5 else min 0.5 (Min es)"
- from ei have "e > 0" using x
- by (auto simp add: e_def es_def Pi'_def Ball_def)
- moreover have "\<forall>y. dist y x < e \<longrightarrow> y \<in> Pi' I A"
- proof (intro allI impI)
- fix y
- assume "dist y x < e"
- also have "\<dots> < 1" by (auto simp: e_def)
- finally have "domain y = domain x" by (rule dist_le_1_imp_domain_eq)
- with dim_x have dims: "domain y = domain x" "domain x = I" by auto
- show "y \<in> Pi' I A"
- proof
- show "domain y = I" using dims by simp
- next
- fix i
- assume "i \<in> I"
- have "dist (y i) (x i) \<le> dist y x" using dims `i \<in> I`
- by (auto intro: dist_proj)
- also have "\<dots> < e" using `dist y x < e` dims
- by (simp add: dist_finmap_def)
- also have "e \<le> Min (ei ` I)" using dims `i \<in> I`
- by (auto simp: e_def es_def)
- also have "\<dots> \<le> ei i" using `i \<in> I` by (simp add: e_def)
- finally have "dist (y i) (x i) < ei i" .
- with ei `i \<in> I` show "y i \<in> A i" by simp
- qed
- qed
- ultimately
- show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> Pi' I A" by blast
-qed
+lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
+ by (auto intro: generate_topology.Basis simp: open_finmap_def)
-instance
-proof
- fix S::"('a \<Rightarrow>\<^isub>F 'b) set"
- show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
- unfolding open_finmap_def ..
-next
- fix P Q::"'a \<Rightarrow>\<^isub>F 'b"
- show "dist P Q = 0 \<longleftrightarrow> P = Q"
- by (auto simp: finmap_eq_iff dist_finmap_def setsum_nonneg setsum_nonneg_eq_0_iff)
-next
- fix P Q R::"'a \<Rightarrow>\<^isub>F 'b"
- let ?symdiff = "\<lambda>a b. domain a - domain b \<union> (domain b - domain a)"
- def E \<equiv> "domain P \<union> domain Q \<union> domain R"
- hence "finite E" by (simp add: E_def)
- have "card (?symdiff P Q) \<le> card (?symdiff P R \<union> ?symdiff Q R)"
- by (auto intro: card_mono)
- also have "\<dots> \<le> card (?symdiff P R) + card (?symdiff Q R)"
- by (subst card_Un_Int) auto
- finally have "dist P Q \<le> (\<Sum>i\<in>E. dist (P i) (R i) + dist (Q i) (R i)) +
- real (card (?symdiff P R) + card (?symdiff Q R))"
- unfolding dist_finmap_extend[OF `finite E`]
- by (intro add_mono) (auto simp: E_def intro: setsum_mono dist_triangle_le)
- also have "\<dots> \<le> dist P R + dist Q R"
- unfolding dist_finmap_extend[OF `finite E`] by (simp add: ac_simps E_def setsum_addf[symmetric])
- finally show "dist P Q \<le> dist P R + dist Q R" by simp
-qed
+instance using topological_space_generate_topology
+ by intro_classes (auto simp: open_finmap_def class.topological_space_def)
end
@@ -310,69 +189,268 @@
lemma closed_restricted_space:
shows "closed {m. P (domain m)}"
-proof -
- have "{m. P (domain m)} = - (\<Union>i \<in> - Collect P. {m. domain m = i})" by auto
- also have "closed \<dots>"
- proof (rule, rule, rule, cases)
- fix i::"'a set"
- assume "finite i"
- hence "{m. domain m = i} = Pi' i (\<lambda>_. UNIV)" by (auto simp: Pi'_def)
- also have "open \<dots>" by (auto intro: open_Pi'I simp: `finite i`)
- finally show "open {m. domain m = i}" .
- next
- fix i::"'a set"
- assume "\<not> finite i" hence "{m. domain m = i} = {}" by auto
- also have "open \<dots>" by simp
- finally show "open {m. domain m = i}" .
- qed
- finally show ?thesis .
+ using open_restricted_space[of "\<lambda>x. \<not> P x"]
+ unfolding closed_def by (rule back_subst) auto
+
+lemma tendsto_proj: "((\<lambda>x. x) ---> a) F \<Longrightarrow> ((\<lambda>x. (x)\<^isub>F i) ---> (a)\<^isub>F i) F"
+ unfolding tendsto_def
+proof safe
+ fix S::"'b set"
+ let ?S = "Pi' (domain a) (\<lambda>x. if x = i then S else UNIV)"
+ assume "open S" hence "open ?S" by (auto intro!: open_Pi'I)
+ moreover assume "\<forall>S. open S \<longrightarrow> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F" "a i \<in> S"
+ ultimately have "eventually (\<lambda>x. x \<in> ?S) F" by auto
+ thus "eventually (\<lambda>x. (x)\<^isub>F i \<in> S) F"
+ by eventually_elim (insert `a i \<in> S`, force simp: Pi'_iff split: split_if_asm)
qed
lemma continuous_proj:
shows "continuous_on s (\<lambda>x. (x)\<^isub>F i)"
- unfolding continuous_on_topological
-proof safe
- fix x B assume "x \<in> s" "open B" "x i \<in> B"
- let ?A = "Pi' (domain x) (\<lambda>j. if i = j then B else UNIV)"
- have "open ?A" using `open B` by (auto intro: open_Pi'I)
- moreover have "x \<in> ?A" using `x i \<in> B` by auto
- moreover have "(\<forall>y\<in>s. y \<in> ?A \<longrightarrow> y i \<in> B)"
- proof (cases, safe)
- fix y assume "y \<in> s"
- assume "i \<notin> domain x" hence "undefined \<in> B" using `x i \<in> B`
- by simp
- moreover
- assume "y \<in> ?A" hence "domain y = domain x" by (simp add: Pi'_def)
- hence "y i = undefined" using `i \<notin> domain x` by simp
- ultimately
- show "y i \<in> B" by simp
- qed force
- ultimately
- show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> y i \<in> B)" by blast
+ unfolding continuous_on_def
+ by (safe intro!: tendsto_proj tendsto_ident_at_within)
+
+instance finmap :: (type, first_countable_topology) first_countable_topology
+proof
+ fix x::"'a\<Rightarrow>\<^isub>F'b"
+ have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
+ (\<forall>S. open S \<and> x i \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" (is "\<forall>i. ?th i")
+ proof
+ fix i from first_countable_basis_Int_stableE[of "x i"] guess A .
+ thus "?th i" by (intro exI[where x=A]) simp
+ qed
+ then guess A unfolding choice_iff .. note A = this
+ hence open_sub: "\<And>i S. i\<in>domain x \<Longrightarrow> open (S i) \<Longrightarrow> x i\<in>(S i) \<Longrightarrow> (\<exists>a\<in>A i. a\<subseteq>(S i))" by auto
+ have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
+ let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^isub>E (domain x) A)"
+ show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+ proof (rule exI[where x="?A"], safe)
+ show "countable ?A" using A by (simp add: countable_PiE)
+ next
+ fix S::"('a \<Rightarrow>\<^isub>F 'b) set" assume "open S" "x \<in> S"
+ thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_finmap_def
+ proof (induct rule: generate_topology.induct)
+ case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty)
+ next
+ case (Int a b)
+ then obtain f g where
+ "f \<in> Pi\<^isub>E (domain x) A" "Pi' (domain x) f \<subseteq> a" "g \<in> Pi\<^isub>E (domain x) A" "Pi' (domain x) g \<subseteq> b"
+ by auto
+ thus ?case using A
+ by (auto simp: Pi'_iff PiE_iff extensional_def Int_stable_def
+ intro!: bexI[where x="\<lambda>i. f i \<inter> g i"])
+ next
+ case (UN B)
+ then obtain b where "x \<in> b" "b \<in> B" by auto
+ hence "\<exists>a\<in>?A. a \<subseteq> b" using UN by simp
+ thus ?case using `b \<in> B` by blast
+ next
+ case (Basis s)
+ then obtain a b where xs: "x\<in> Pi' a b" "s = Pi' a b" "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
+ have "\<forall>i. \<exists>a. (i \<in> domain x \<and> open (b i) \<and> (x)\<^isub>F i \<in> b i) \<longrightarrow> (a\<in>A i \<and> a \<subseteq> b i)"
+ using open_sub[of _ b] by auto
+ then obtain b'
+ where "\<And>i. i \<in> domain x \<Longrightarrow> open (b i) \<Longrightarrow> (x)\<^isub>F i \<in> b i \<Longrightarrow> (b' i \<in>A i \<and> b' i \<subseteq> b i)"
+ unfolding choice_iff by auto
+ with xs have "\<And>i. i \<in> a \<Longrightarrow> (b' i \<in>A i \<and> b' i \<subseteq> b i)" "Pi' a b' \<subseteq> Pi' a b"
+ by (auto simp: Pi'_iff intro!: Pi'_mono)
+ thus ?case using xs
+ by (intro bexI[where x="Pi' a b'"])
+ (auto simp: Pi'_iff intro!: image_eqI[where x="restrict b' (domain x)"])
+ qed
+ qed (insert A,auto simp: PiE_iff intro!: open_Pi'I)
+qed
+
+subsection {* Metric Space of Finite Maps *}
+
+instantiation finmap :: (type, metric_space) metric_space
+begin
+
+definition dist_finmap where
+ "dist P Q = Max (range (\<lambda>i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i))) + (if domain P = domain Q then 0 else 1)"
+
+lemma add_eq_zero_iff[simp]:
+ fixes a b::real
+ assumes "a \<ge> 0" "b \<ge> 0"
+ shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
+using assms by auto
+
+lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^isub>F ` S)"
+ by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
+
+lemma finite_proj_image: "finite ((P)\<^isub>F ` S)"
+ by (cases "\<exists>x. x \<notin> domain P") (auto intro: finite_proj_image' finite_subset[where B="domain P"])
+
+lemma finite_proj_diag: "finite ((\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S)"
+proof -
+ have "(\<lambda>i. d ((P)\<^isub>F i) ((Q)\<^isub>F i)) ` S = (\<lambda>(i, j). d i j) ` ((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S)" by auto
+ moreover have "((\<lambda>i. ((P)\<^isub>F i, (Q)\<^isub>F i)) ` S) \<subseteq> (\<lambda>i. (P)\<^isub>F i) ` S \<times> (\<lambda>i. (Q)\<^isub>F i) ` S" by auto
+ moreover have "finite \<dots>" using finite_proj_image[of P S] finite_proj_image[of Q S]
+ by (intro finite_cartesian_product) simp_all
+ ultimately show ?thesis by (simp add: finite_subset)
+qed
+
+lemma dist_le_1_imp_domain_eq:
+ shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
+ by (simp add: dist_finmap_def finite_proj_diag split: split_if_asm)
+
+lemma dist_proj:
+ shows "dist ((x)\<^isub>F i) ((y)\<^isub>F i) \<le> dist x y"
+proof -
+ have "dist (x i) (y i) \<le> Max (range (\<lambda>i. dist (x i) (y i)))"
+ by (simp add: Max_ge_iff finite_proj_diag)
+ also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_def)
+ finally show ?thesis .
qed
-subsection {* Complete Space of Finite Maps *}
+lemma dist_finmap_lessI:
+ assumes "domain P = domain Q"
+ assumes "0 < e"
+ assumes "\<And>i. i \<in> domain P \<Longrightarrow> dist (P i) (Q i) < e"
+ shows "dist P Q < e"
+proof -
+ have "dist P Q = Max (range (\<lambda>i. dist (P i) (Q i)))"
+ using assms by (simp add: dist_finmap_def finite_proj_diag)
+ also have "\<dots> < e"
+ proof (subst Max_less_iff, safe)
+ fix i
+ show "dist ((P)\<^isub>F i) ((Q)\<^isub>F i) < e" using assms
+ by (cases "i \<in> domain P") simp_all
+ qed (simp add: finite_proj_diag)
+ finally show ?thesis .
+qed
-lemma tendsto_dist_zero:
- assumes "(\<lambda>i. dist (f i) g) ----> 0"
- shows "f ----> g"
- using assms by (auto simp: tendsto_iff dist_real_def)
+instance
+proof
+ fix S::"('a \<Rightarrow>\<^isub>F 'b) set"
+ show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
+ proof
+ assume "open S"
+ thus ?od
+ unfolding open_finmap_def
+ proof (induct rule: generate_topology.induct)
+ case UNIV thus ?case by (auto intro: zero_less_one)
+ next
+ case (Int a b)
+ show ?case
+ proof safe
+ fix x assume x: "x \<in> a" "x \<in> b"
+ with Int x obtain e1 e2 where
+ "e1>0" "\<forall>y. dist y x < e1 \<longrightarrow> y \<in> a" "e2>0" "\<forall>y. dist y x < e2 \<longrightarrow> y \<in> b" by force
+ thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> a \<inter> b"
+ by (auto intro!: exI[where x="min e1 e2"])
+ qed
+ next
+ case (UN K)
+ show ?case
+ proof safe
+ fix x X assume "x \<in> X" "X \<in> K"
+ moreover with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
+ ultimately show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
+ qed
+ next
+ case (Basis s) then obtain a b where s: "s = Pi' a b" and b: "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
+ show ?case
+ proof safe
+ fix x assume "x \<in> s"
+ hence [simp]: "finite a" and a_dom: "a = domain x" using s by (auto simp: Pi'_iff)
+ obtain es where es: "\<forall>i \<in> a. es i > 0 \<and> (\<forall>y. dist y (proj x i) < es i \<longrightarrow> y \<in> b i)"
+ using b `x \<in> s` by atomize_elim (intro bchoice, auto simp: open_dist s)
+ hence in_b: "\<And>i y. i \<in> a \<Longrightarrow> dist y (proj x i) < es i \<Longrightarrow> y \<in> b i" by auto
+ show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s"
+ proof (cases, rule, safe)
+ assume "a \<noteq> {}"
+ show "0 < min 1 (Min (es ` a))" using es by (auto simp: `a \<noteq> {}`)
+ fix y assume d: "dist y x < min 1 (Min (es ` a))"
+ show "y \<in> s" unfolding s
+ proof
+ show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom)
+ fix i assume "i \<in> a"
+ moreover
+ hence "dist ((y)\<^isub>F i) ((x)\<^isub>F i) < es i" using d
+ by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj])
+ ultimately
+ show "y i \<in> b i" by (rule in_b)
+ qed
+ next
+ assume "\<not>a \<noteq> {}"
+ thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> s"
+ using s `x \<in> s` by (auto simp: Pi'_def dist_le_1_imp_domain_eq intro!: exI[where x=1])
+ qed
+ qed
+ qed
+ next
+ assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+ then obtain e where e_pos: "\<And>x. x \<in> S \<Longrightarrow> e x > 0" and
+ e_in: "\<And>x y . x \<in> S \<Longrightarrow> dist y x < e x \<Longrightarrow> y \<in> S"
+ unfolding bchoice_iff
+ by auto
+ have S_eq: "S = \<Union>{Pi' a b| a b. \<exists>x\<in>S. domain x = a \<and> b = (\<lambda>i. ball (x i) (e x))}"
+ proof safe
+ fix x assume "x \<in> S"
+ thus "x \<in> \<Union>{Pi' a b| a b. \<exists>x\<in>S. domain x = a \<and> b = (\<lambda>i. ball (x i) (e x))}"
+ using e_pos by (auto intro!: exI[where x="Pi' (domain x) (\<lambda>i. ball (x i) (e x))"])
+ next
+ fix x y
+ assume "y \<in> S"
+ moreover
+ assume "x \<in> (\<Pi>' i\<in>domain y. ball (y i) (e y))"
+ hence "dist x y < e y" using e_pos `y \<in> S`
+ by (auto simp: dist_finmap_def Pi'_iff finite_proj_diag dist_commute)
+ ultimately show "x \<in> S" by (rule e_in)
+ qed
+ also have "open \<dots>"
+ unfolding open_finmap_def
+ by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
+ finally show "open S" .
+ qed
+next
+ fix P Q::"'a \<Rightarrow>\<^isub>F 'b"
+ have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
+ by (metis Max.in_idem Max_in max_def min_max.sup.commute order_refl)
+ show "dist P Q = 0 \<longleftrightarrow> P = Q"
+ by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+ intro!: Max_eqI image_eqI[where x=undefined])
+next
+ fix P Q R::"'a \<Rightarrow>\<^isub>F 'b"
+ let ?dists = "\<lambda>P Q i. dist ((P)\<^isub>F i) ((Q)\<^isub>F i)"
+ let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R"
+ let ?dom = "\<lambda>P Q. (if domain P = domain Q then 0 else 1::real)"
+ have "dist P Q = Max (range ?dpq) + ?dom P Q"
+ by (simp add: dist_finmap_def)
+ also obtain t where "t \<in> range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag)
+ then obtain i where "Max (range ?dpq) = ?dpq i" by auto
+ also have "?dpq i \<le> ?dpr i + ?dqr i" by (rule dist_triangle2)
+ also have "?dpr i \<le> Max (range ?dpr)" by (simp add: finite_proj_diag)
+ also have "?dqr i \<le> Max (range ?dqr)" by (simp add: finite_proj_diag)
+ also have "?dom P Q \<le> ?dom P R + ?dom Q R" by simp
+ finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps)
+qed
-lemma tendsto_dist_zero':
- assumes "(\<lambda>i. dist (f i) g) ----> x"
- assumes "0 = x"
- shows "f ----> g"
- using assms tendsto_dist_zero by simp
+end
+
+subsection {* Complete Space of Finite Maps *}
lemma tendsto_finmap:
fixes f::"nat \<Rightarrow> ('i \<Rightarrow>\<^isub>F ('a::metric_space))"
assumes ind_f: "\<And>n. domain (f n) = domain g"
assumes proj_g: "\<And>i. i \<in> domain g \<Longrightarrow> (\<lambda>n. (f n) i) ----> g i"
shows "f ----> g"
- apply (rule tendsto_dist_zero')
- unfolding dist_finmap_def assms
- apply (rule tendsto_intros proj_g | simp)+
- done
+ unfolding tendsto_iff
+proof safe
+ fix e::real assume "0 < e"
+ let ?dists = "\<lambda>x i. dist ((f x)\<^isub>F i) ((g)\<^isub>F i)"
+ have "eventually (\<lambda>x. \<forall>i\<in>domain g. ?dists x i < e) sequentially"
+ using finite_domain[of g] proj_g
+ proof induct
+ case (insert i G)
+ with `0 < e` have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff)
+ moreover
+ from insert have "eventually (\<lambda>x. \<forall>i\<in>G. dist ((f x)\<^isub>F i) ((g)\<^isub>F i) < e) sequentially" by simp
+ ultimately show ?case by eventually_elim auto
+ qed simp
+ thus "eventually (\<lambda>x. dist (f x) g < e) sequentially"
+ by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f `0 < e`)
+qed
instance finmap :: (type, complete_space) complete_space
proof
@@ -412,123 +490,114 @@
have "P ----> Q"
proof (rule metric_LIMSEQ_I)
fix e::real assume "0 < e"
- def e' \<equiv> "min 1 (e / (card d + 1))"
- hence "0 < e'" using `0 < e` by (auto simp: e'_def intro: divide_pos_pos)
- have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e'"
+ have "\<exists>ni. \<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e"
proof (safe intro!: bchoice)
fix i assume "i \<in> d"
- from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e'`]
- show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e'" .
+ from p[OF `i \<in> d`, THEN metric_LIMSEQ_D, OF `0 < e`]
+ show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" .
qed then guess ni .. note ni = this
def N \<equiv> "max Nd (Max (ni ` d))"
show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e"
proof (safe intro!: exI[where x="N"])
fix n assume "N \<le> n"
- hence "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
+ hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse)
- hence "dist (P n) Q = (\<Sum>i\<in>d. dist ((P n) i) (Q i))" by (simp add: dist_finmap_def)
- also have "\<dots> \<le> (\<Sum>i\<in>d. e')"
- proof (intro setsum_mono less_imp_le)
- fix i assume "i \<in> d"
- hence "ni i \<le> Max (ni ` d)" by simp
+ show "dist (P n) Q < e"
+ proof (rule dist_finmap_lessI[OF dom(3) `0 < e`])
+ fix i
+ assume "i \<in> domain (P n)"
+ hence "ni i \<le> Max (ni ` d)" using dom by simp
also have "\<dots> \<le> N" by (simp add: N_def)
- also have "\<dots> \<le> n" using `N \<le> n` .
- finally
- show "dist ((P n) i) (Q i) < e'"
- using ni `i \<in> d` by (auto simp: p_def q N_def)
+ finally show "dist ((P n)\<^isub>F i) ((Q)\<^isub>F i) < e" using ni `i \<in> domain (P n)` `N \<le> n` dom
+ by (auto simp: p_def q N_def less_imp_le)
qed
- also have "\<dots> = card d * e'" by (simp add: real_eq_of_nat)
- also have "\<dots> < e" using `0 < e` by (simp add: e'_def field_simps min_def)
- finally show "dist (P n) Q < e" .
qed
qed
thus "convergent P" by (auto simp: convergent_def)
qed
-subsection {* Polish Space of Finite Maps *}
+subsection {* Second Countable Space of Finite Maps *}
-instantiation finmap :: (countable, polish_space) polish_space
+instantiation finmap :: (countable, second_countable_topology) second_countable_topology
begin
+definition basis_proj::"'b set set"
+ where "basis_proj = (SOME B. countable B \<and> topological_basis B)"
+
+lemma countable_basis_proj: "countable basis_proj" and basis_proj: "topological_basis basis_proj"
+ unfolding basis_proj_def by (intro is_basis countable_basis)+
+
definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
- where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
+ where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> basis_proj)}"
lemma in_basis_finmapI:
- assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
+ assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> basis_proj"
shows "Pi' I S \<in> basis_finmap"
using assms unfolding basis_finmap_def by auto
-lemma in_basis_finmapE:
- assumes "x \<in> basis_finmap"
- obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
- using assms unfolding basis_finmap_def by auto
-
lemma basis_finmap_eq:
- "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
+ assumes "basis_proj \<noteq> {}"
+ shows "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into basis_proj ((f)\<^isub>F i))) `
(UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
unfolding basis_finmap_def
proof safe
fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
- assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
- hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
- by (force simp: Pi'_def countable_union_closed_basis)
+ assume "finite I" "\<forall>i\<in>I. S i \<in> basis_proj"
+ hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on basis_proj (S x)))"
+ by (force simp: Pi'_def countable_basis_proj)
thus "Pi' I S \<in> range ?f" by simp
-qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
+next
+ fix x and f::"'a \<Rightarrow>\<^isub>F nat"
+ show "\<exists>I S. (\<Pi>' i\<in>domain f. from_nat_into local.basis_proj ((f)\<^isub>F i)) = Pi' I S \<and>
+ finite I \<and> (\<forall>i\<in>I. S i \<in> local.basis_proj)"
+ using assms by (auto intro: from_nat_into)
+qed
+
+lemma basis_finmap_eq_empty: "basis_proj = {} \<Longrightarrow> basis_finmap = {Pi' {} undefined}"
+ by (auto simp: Pi'_iff basis_finmap_def)
lemma countable_basis_finmap: "countable basis_finmap"
- unfolding basis_finmap_eq by simp
+ by (cases "basis_proj = {}") (auto simp: basis_finmap_eq basis_finmap_eq_empty)
lemma finmap_topological_basis:
"topological_basis basis_finmap"
proof (subst topological_basis_iff, safe)
fix B' assume "B' \<in> basis_finmap"
thus "open B'"
- by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
+ by (auto intro!: open_Pi'I topological_basis_open[OF basis_proj]
simp: topological_basis_def basis_finmap_def Let_def)
next
fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
- assume "open O'" "x \<in> O'"
- then obtain e where e: "e > 0" "\<And>y. dist y x < e \<Longrightarrow> y \<in> O'" unfolding open_dist by blast
- def e' \<equiv> "e / (card (domain x) + 1)"
-
+ assume O': "open O'" "x \<in> O'"
+ then obtain a where a:
+ "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> O'" "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
+ unfolding open_finmap_def
+ proof (atomize_elim, induct rule: generate_topology.induct)
+ case (Int a b)
+ let ?p="\<lambda>a f. x \<in> Pi' (domain x) f \<and> Pi' (domain x) f \<subseteq> a \<and> (\<forall>i. i \<in> domain x \<longrightarrow> open (f i))"
+ from Int obtain f g where "?p a f" "?p b g" by auto
+ thus ?case by (force intro!: exI[where x="\<lambda>i. f i \<inter> g i"] simp: Pi'_def)
+ next
+ case (UN k)
+ then obtain kk a where "x \<in> kk" "kk \<in> k" "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> kk"
+ "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
+ by force
+ thus ?case by blast
+ qed (auto simp: Pi'_def)
have "\<exists>B.
- (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> ball (x i) e' \<and> B i \<in> union_closed_basis)"
+ (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> basis_proj)"
proof (rule bchoice, safe)
fix i assume "i \<in> domain x"
- have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
- by (auto simp add: e'_def intro!: divide_pos_pos)
- from topological_basisE[OF basis_union_closed_basis this] guess b' .
- thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
+ hence "open (a i)" "x i \<in> a i" using a by auto
+ from topological_basisE[OF basis_proj this] guess b' .
+ thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto
qed
then guess B .. note B = this
def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
- hence "B' \<in> basis_finmap" unfolding B'_def using B
- by (intro in_basis_finmapI) auto
- moreover have "x \<in> B'" unfolding B'_def using B by auto
- moreover have "B' \<subseteq> O'"
- proof
- fix y assume "y \<in> B'" with B have "domain y = domain x" unfolding B'_def
- by (simp add: Pi'_def)
- show "y \<in> O'"
- proof (rule e)
- have "dist y x = (\<Sum>i \<in> domain x. dist (y i) (x i))"
- using `domain y = domain x` by (simp add: dist_finmap_def)
- also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
- proof (rule setsum_mono)
- fix i assume "i \<in> domain x"
- with `y \<in> B'` B have "y i \<in> B i"
- by (simp add: Pi'_def B'_def)
- hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
- by force
- thus "dist (y i) (x i) \<le> e'" by (simp add: dist_commute)
- qed
- also have "\<dots> = card (domain x) * e'" by (simp add: real_eq_of_nat)
- also have "\<dots> < e" using e by (simp add: e'_def field_simps)
- finally show "dist y x < e" .
- qed
- qed
- ultimately
- show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
+ have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def)
+ also note `\<dots> \<subseteq> O'`
+ finally show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" using B
+ by (auto intro!: bexI[where x=B'] Pi'_mono in_basis_finmapI simp: B'_def)
qed
lemma range_enum_basis_finmap_imp_open:
@@ -540,6 +609,11 @@
end
+subsection {* Polish Space of Finite Maps *}
+
+instance finmap :: (countable, polish_space) polish_space proof qed
+
+
subsection {* Product Measurable Space of Finite Maps *}
definition "PiF I M \<equiv>
@@ -942,9 +1016,8 @@
text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
lemma sigma_fprod_algebra_sigma_eq:
- fixes E :: "'i \<Rightarrow> 'a set set"
+ fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
assumes [simp]: "finite I" "I \<noteq> {}"
- assumes S_mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
@@ -953,6 +1026,9 @@
shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P"
proof
let ?P = "sigma (space (Pi\<^isub>F {I} M)) P"
+ from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
+ then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
+ by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: `finite I`)
have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>F {I} M))"
using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq)
then have space_P: "space ?P = (\<Pi>' i\<in>I. space (M i))"
@@ -975,15 +1051,20 @@
using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)"
by (intro Pi'_cong) (simp_all add: S_union)
- also have "\<dots> = (\<Union>n. \<Pi>' j\<in>I. if i = j then A else S j n)"
- using S_mono
- by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
+ also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
+ using T
+ apply auto
+ apply (simp_all add: Pi'_iff bchoice_iff)
+ apply (erule conjE exE)+
+ apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
+ apply (auto simp: bij_betw_def)
+ done
also have "\<dots> \<in> sets ?P"
proof (safe intro!: sets.countable_UN)
- fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
+ fix xs show "(\<Pi>' j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
using A S_in_E
by (simp add: P_closed)
- (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j n"])
+ (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
qed
finally show "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space ?P \<in> sets ?P"
using P_closed by simp
@@ -1003,76 +1084,28 @@
by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
qed
-lemma sets_PiF_eq_sigma_union_closed_basis_single:
- assumes "I \<noteq> {}"
- assumes [simp]: "finite I"
- shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
- {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
-proof -
- from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
- show ?thesis
- proof (rule sigma_fprod_algebra_sigma_eq)
- show "finite I" by simp
- show "I \<noteq> {}" by fact
- show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
- using S by simp_all
- show "union_closed_basis \<subseteq> Pow (space borel)" by simp
- show "sets borel = sigma_sets (space borel) union_closed_basis"
- by (simp add: borel_eq_union_closed_basis)
- qed
-qed
-
-text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
-
-lemma sets_PiM_eq_sigma_union_closed_basis:
- assumes "I \<noteq> {}"
- assumes [simp]: "finite I"
- shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
- {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
-proof -
- from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
- show ?thesis
- proof (rule sigma_prod_algebra_sigma_eq)
- show "finite I" by simp note[[show_types]]
- fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
- using S by simp_all
- show "union_closed_basis \<subseteq> Pow (space borel)" by simp
- show "sets borel = sigma_sets (space borel) union_closed_basis"
- by (simp add: borel_eq_union_closed_basis)
- qed
-qed
-
lemma product_open_generates_sets_PiF_single:
assumes "I \<noteq> {}"
assumes [simp]: "finite I"
shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
proof -
- from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
+ from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
show ?thesis
proof (rule sigma_fprod_algebra_sigma_eq)
show "finite I" by simp
show "I \<noteq> {}" by fact
- show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
- using S by (auto simp: open_union_closed_basis)
- show "Collect open \<subseteq> Pow (space borel)" by simp
- show "sets borel = sigma_sets (space borel) (Collect open)"
- by (simp add: borel_def)
- qed
-qed
-
-lemma product_open_generates_sets_PiM:
- assumes "I \<noteq> {}"
- assumes [simp]: "finite I"
- shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
- sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
-proof -
- from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
- show ?thesis
- proof (rule sigma_prod_algebra_sigma_eq)
- show "finite I" by simp note[[show_types]]
- fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
- using S by (auto simp: open_union_closed_basis)
+ def S'\<equiv>"from_nat_into S"
+ show "(\<Union>j. S' j) = space borel"
+ using S
+ apply (auto simp add: from_nat_into countable_basis_proj S'_def basis_proj_def)
+ apply (metis (lifting, mono_tags) UNIV_I UnionE basis_proj_def countable_basis_proj countable_subset from_nat_into_surj)
+ done
+ show "range S' \<subseteq> Collect open"
+ using S
+ apply (auto simp add: from_nat_into countable_basis_proj S'_def)
+ apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
+ done
show "Collect open \<subseteq> Pow (space borel)" by simp
show "sets borel = sigma_sets (space borel) (Collect open)"
by (simp add: borel_def)
@@ -1099,7 +1132,7 @@
proof
fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
- by (auto simp: basis_finmap_def open_union_closed_basis)
+ by (auto simp: basis_finmap_def topological_basis_open[OF basis_proj])
thus "x \<in> sets ?s" by auto
qed
qed