--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy Tue Oct 18 17:29:28 2016 +0200
@@ -0,0 +1,1392 @@
+(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr
+ License: BSD
+*)
+
+theory Function_Topology
+imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
+begin
+
+
+section {*Product topology*}
+
+text {*We want to define the product topology.
+
+The product topology on a product of topological spaces is generated by
+the sets which are products of open sets along finitely many coordinates, and the whole
+space along the other coordinates. This is the coarsest topology for which the projection
+to each factor is continuous.
+
+To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
+'a. The product is then @{term "PiE I X"}, the set of elements from 'i to 'a such that the $i$-th
+coordinate belongs to $X\;i$ for all $i \in I$.
+
+Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
+This means that type classes can not be used to define such a product if one wants to take the
+product of different topological spaces (as the type 'a can only be given one structure of
+topological space using type classes). On the other hand, one can define different topologies (as
+introduced in \verb+Topology_Euclidean_Space.thy+) on one type, and these topologies do not need to
+share the same maximal open set. Hence, one can form a product of topologies in this sense, and
+this works well. The big caveat is that it does not interact well with the main body of
+topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
+is not defined in this setting.
+
+As the product of different topological spaces is very important in several areas of
+mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
+and reformulate afterwards the consequences in terms of type classes (which are of course very
+handy for applications).
+
+Given this limitation, it looks to me that it would be very beneficial to revamp the theory
+of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
+type classes as consequences of more general statements in terms of topologies (but I am
+probably too naive here).
+
+Here is an example of a reformulation using topologies. Let
+\begin{verbatim}
+continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
+ \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
+\end{verbatim}
+be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
+the current \verb+continuous_on+ (with type classes) can be redefined as
+\begin{verbatim}
+continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
+\end{verbatim}
+
+In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
+for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
+the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
+
+I only develop the basics of the product topology in this theory. The most important missing piece
+is Tychonov theorem, stating that a product of compact spaces is always compact for the product
+topology, even when the product is not finite (or even countable).
+
+I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
+*}
+
+subsection {*Topology without type classes*}
+
+subsubsection {*The topology generated by some (open) subsets*}
+
+text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
+as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
+and is never a problem in proofs, so I prefer to write it down explicitly.
+
+We do not require UNIV to be an open set, as this will not be the case in applications. (We are
+thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)*}
+
+inductive generate_topology_on for S where
+Empty: "generate_topology_on S {}"
+|Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
+| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
+| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
+
+lemma istopology_generate_topology_on:
+ "istopology (generate_topology_on S)"
+unfolding istopology_def by (auto intro: generate_topology_on.intros)
+
+text {*The basic property of the topology generated by a set $S$ is that it is the
+smallest topology containing all the elements of $S$:*}
+
+lemma generate_topology_on_coarsest:
+ assumes "istopology T"
+ "\<And>s. s \<in> S \<Longrightarrow> T s"
+ "generate_topology_on S s0"
+ shows "T s0"
+using assms(3) apply (induct rule: generate_topology_on.induct)
+using assms(1) assms(2) unfolding istopology_def by auto
+
+definition topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+ where "topology_generated_by S = topology (generate_topology_on S)"
+
+lemma openin_topology_generated_by_iff:
+ "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
+using topology_inverse'[OF istopology_generate_topology_on[of S]]
+unfolding topology_generated_by_def by simp
+
+lemma openin_topology_generated_by:
+ "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
+using openin_topology_generated_by_iff by auto
+
+lemma topology_generated_by_topspace:
+ "topspace (topology_generated_by S) = (\<Union>S)"
+proof
+ {
+ fix s assume "openin (topology_generated_by S) s"
+ then have "generate_topology_on S s" by (rule openin_topology_generated_by)
+ then have "s \<subseteq> (\<Union>S)" by (induct, auto)
+ }
+ then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
+ unfolding topspace_def by auto
+next
+ have "generate_topology_on S (\<Union>S)"
+ using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
+ then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
+ unfolding topspace_def using openin_topology_generated_by_iff by auto
+qed
+
+lemma topology_generated_by_Basis:
+ "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
+by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
+
+subsubsection {*Continuity*}
+
+text {*We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.*}
+
+definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
+ \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
+
+lemma continuous_on_continuous_on_topo:
+ "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
+unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def
+topspace_euclidean_subtopology open_openin topspace_euclidean by fast
+
+lemma continuous_on_topo_UNIV:
+ "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
+using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
+
+lemma continuous_on_topo_open [intro]:
+ "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+unfolding continuous_on_topo_def by auto
+
+lemma continuous_on_topo_topspace [intro]:
+ "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
+unfolding continuous_on_topo_def by auto
+
+lemma continuous_on_generated_topo_iff:
+ "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
+ ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
+unfolding continuous_on_topo_def topology_generated_by_topspace
+proof (auto simp add: topology_generated_by_Basis)
+ assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
+ fix U assume "openin (topology_generated_by S) U"
+ then have "generate_topology_on S U" by (rule openin_topology_generated_by)
+ then show "openin T1 (f -` U \<inter> topspace T1)"
+ proof (induct)
+ fix a b
+ assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
+ have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
+ by auto
+ then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
+ next
+ fix K
+ assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
+ define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
+ have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
+ have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
+ moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
+ ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
+ qed (auto simp add: H)
+qed
+
+lemma continuous_on_generated_topo:
+ assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+ "f`(topspace T1) \<subseteq> (\<Union> S)"
+ shows "continuous_on_topo T1 (topology_generated_by S) f"
+using assms continuous_on_generated_topo_iff by blast
+
+lemma continuous_on_topo_compose:
+ assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
+ shows "continuous_on_topo T1 T3 (g o f)"
+using assms unfolding continuous_on_topo_def
+proof (auto)
+ fix U :: "'c set"
+ assume H: "openin T3 U"
+ have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
+ using H assms by blast
+ moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
+ using H assms continuous_on_topo_topspace by fastforce
+ ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
+ by simp
+qed (blast)
+
+lemma continuous_on_topo_preimage_topspace [intro]:
+ assumes "continuous_on_topo T1 T2 f"
+ shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
+using assms unfolding continuous_on_topo_def by auto
+
+
+subsubsection {*Pullback topology*}
+
+text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
+a special case of this notion, pulling back by the identity. We introduce the general notion as
+we will need it to define the strong operator topology on the space of continuous linear operators,
+by pulling back the product topology on the space of all functions.*}
+
+text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
+the set $A$.*}
+
+definition pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
+ where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+
+lemma istopology_pullback_topology:
+ "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+unfolding istopology_def proof (auto)
+ fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
+ then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
+ by (rule bchoice)
+ then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
+ by blast
+ define V where "V = (\<Union>S\<in>K. U S)"
+ have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
+ then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
+qed
+
+lemma openin_pullback_topology:
+ "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
+unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
+
+lemma topspace_pullback_topology:
+ "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
+by (auto simp add: topspace_def openin_pullback_topology)
+
+lemma continuous_on_topo_pullback [intro]:
+ assumes "continuous_on_topo T1 T2 g"
+ shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
+unfolding continuous_on_topo_def
+proof (auto)
+ fix U::"'b set" assume "openin T2 U"
+ then have "openin T1 (g-`U \<inter> topspace T1)"
+ using assms unfolding continuous_on_topo_def by auto
+ have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
+ unfolding topspace_pullback_topology by auto
+ also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
+ by auto
+ also have "openin (pullback_topology A f T1) (...)"
+ unfolding openin_pullback_topology using `openin T1 (g-\`U \<inter> topspace T1)` by auto
+ finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
+ by auto
+next
+ fix x assume "x \<in> topspace (pullback_topology A f T1)"
+ then have "f x \<in> topspace T1"
+ unfolding topspace_pullback_topology by auto
+ then show "g (f x) \<in> topspace T2"
+ using assms unfolding continuous_on_topo_def by auto
+qed
+
+lemma continuous_on_topo_pullback' [intro]:
+ assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
+ shows "continuous_on_topo T1 (pullback_topology A f T2) g"
+unfolding continuous_on_topo_def
+proof (auto)
+ fix U assume "openin (pullback_topology A f T2) U"
+ then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
+ unfolding openin_pullback_topology by auto
+ then obtain V where "openin T2 V" "U = f-`V \<inter> A"
+ by blast
+ then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
+ by blast
+ also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
+ by auto
+ also have "... = (f o g)-`V \<inter> topspace T1"
+ using assms(2) by auto
+ also have "openin T1 (...)"
+ using assms(1) `openin T2 V` by auto
+ finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
+next
+ fix x assume "x \<in> topspace T1"
+ have "(f o g) x \<in> topspace T2"
+ using assms(1) `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+ then have "g x \<in> f-`(topspace T2)"
+ unfolding comp_def by blast
+ moreover have "g x \<in> A" using assms(2) `x \<in> topspace T1` by blast
+ ultimately show "g x \<in> topspace (pullback_topology A f T2)"
+ unfolding topspace_pullback_topology by blast
+qed
+
+subsubsection {*Miscellaneous*}
+
+text {*The following could belong to \verb+Topology_Euclidean_Spaces.thy+, and will be needed
+below.*}
+lemma openin_INT [intro]:
+ assumes "finite I"
+ "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+ shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
+using assms by (induct, auto simp add: inf_sup_aci(2) openin_Int)
+
+lemma openin_INT2 [intro]:
+ assumes "finite I" "I \<noteq> {}"
+ "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
+ shows "openin T (\<Inter>i \<in> I. U i)"
+proof -
+ have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
+ using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
+ then show ?thesis
+ using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
+qed
+
+
+subsection {*The product topology*}
+
+text {*We can now define the product topology, as generated by
+the sets which are products of open sets along finitely many coordinates, and the whole
+space along the other coordinates. Equivalently, it is generated by sets which are one open
+set along one single coordinate, and the whole space along other coordinates. In fact, this is only
+equivalent for nonempty products, but for the empty product the first formulation is better
+(the second one gives an empty product space, while an empty product should have exactly one
+point, equal to \verb+undefined+ along all coordinates.
+
+So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
+*}
+
+definition product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
+ where "product_topology T I =
+ topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+
+text {*The total set of the product topology is the product of the total sets
+along each coordinate.*}
+
+lemma product_topology_topspace:
+ "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
+proof
+ show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
+ unfolding product_topology_def apply (simp only: topology_generated_by_topspace)
+ unfolding topspace_def by auto
+ have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+ using openin_topspace not_finite_existsD by auto
+ then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
+ unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
+qed
+
+lemma product_topology_basis:
+ assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
+ shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
+unfolding product_topology_def apply (rule topology_generated_by_Basis) using assms by auto
+
+lemma product_topology_open_contains_basis:
+ assumes "openin (product_topology T I) U"
+ "x \<in> U"
+ shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
+proof -
+ have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
+ using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
+ then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
+ proof induction
+ case (Int U V x)
+ then obtain XU XV where H:
+ "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
+ "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
+ by auto meson
+ define X where "X = (\<lambda>i. XU i \<inter> XV i)"
+ have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
+ unfolding X_def by (auto simp add: PiE_iff)
+ then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
+ moreover have "\<forall>i. openin (T i) (X i)"
+ unfolding X_def using H by auto
+ moreover have "finite {i. X i \<noteq> topspace (T i)}"
+ apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
+ unfolding X_def using H by auto
+ moreover have "x \<in> Pi\<^sub>E I X"
+ unfolding X_def using H by auto
+ ultimately show ?case
+ by auto
+ next
+ case (UN K x)
+ then obtain k where "k \<in> K" "x \<in> k" by auto
+ with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
+ by simp
+ then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
+ by blast
+ then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
+ using `k \<in> K` by auto
+ then show ?case
+ by auto
+ qed auto
+ then show ?thesis using `x \<in> U` by auto
+qed
+
+
+text {*The basic property of the product topology is the continuity of projections:*}
+
+lemma continuous_on_topo_product_coordinates [simp]:
+ assumes "i \<in> I"
+ shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
+proof -
+ {
+ fix U assume "openin (T i) U"
+ define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
+ then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
+ unfolding X_def using assms openin_subset[OF `openin (T i) U`]
+ by (auto simp add: PiE_iff, auto, metis subsetCE)
+ have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
+ unfolding X_def using `openin (T i) U` by auto
+ have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
+ unfolding product_topology_def
+ apply (rule topology_generated_by_Basis)
+ apply (subst *)
+ using ** by auto
+ }
+ then show ?thesis unfolding continuous_on_topo_def
+ by (auto simp add: assms product_topology_topspace PiE_iff)
+qed
+
+lemma continuous_on_topo_coordinatewise_then_product [intro]:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+ "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
+ shows "continuous_on_topo T1 (product_topology T I) f"
+unfolding product_topology_def
+proof (rule continuous_on_generated_topo)
+ fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+ then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
+ by blast
+ define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
+ have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
+ have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
+ using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
+ then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
+ using that unfolding J_def by auto
+ have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
+ by (subst H(1), auto simp add: PiE_iff assms)
+ also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
+ using * `J \<subseteq> I` by auto
+ also have "openin T1 (...)"
+ apply (rule openin_INT)
+ apply (simp add: `finite J`)
+ using H(2) assms(1) `J \<subseteq> I` by auto
+ ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
+next
+ show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+ apply (subst topology_generated_by_topspace[symmetric])
+ apply (subst product_topology_def[symmetric])
+ apply (simp only: product_topology_topspace)
+ apply (auto simp add: PiE_iff)
+ using assms unfolding continuous_on_topo_def by auto
+qed
+
+lemma continuous_on_topo_product_then_coordinatewise [intro]:
+ assumes "continuous_on_topo T1 (product_topology T I) f"
+ shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+ "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
+proof -
+ fix i assume "i \<in> I"
+ have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
+ also have "continuous_on_topo T1 (T i) (...)"
+ apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
+ using assms `i \<in> I` by auto
+ ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+ by simp
+next
+ fix i x assume "i \<notin> I" "x \<in> topspace T1"
+ have "f x \<in> topspace (product_topology T I)"
+ using assms `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+ then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
+ using product_topology_topspace by metis
+ then show "f x i = undefined"
+ using `i \<notin> I` by (auto simp add: PiE_iff extensional_def)
+qed
+
+lemma continuous_on_restrict:
+ assumes "J \<subseteq> I"
+ shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
+proof (rule continuous_on_topo_coordinatewise_then_product)
+ fix i assume "i \<in> J"
+ then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
+ then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
+ using `i \<in> J` `J \<subseteq> I` by auto
+next
+ fix i assume "i \<notin> J"
+ then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
+ unfolding restrict_def by auto
+qed
+
+
+subsubsection {*Powers of a single topological space as a topological space, using type classes*}
+
+instantiation "fun" :: (type, topological_space) topological_space
+begin
+
+definition open_fun_def:
+ "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+
+instance proof
+ have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
+ unfolding product_topology_topspace topspace_euclidean by auto
+ then show "open (UNIV::('a \<Rightarrow> 'b) set)"
+ unfolding open_fun_def by (metis openin_topspace)
+qed (auto simp add: open_fun_def)
+
+end
+
+lemma euclidean_product_topology:
+ "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
+by (metis open_openin topology_eq open_fun_def)
+
+lemma product_topology_basis':
+ fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
+ assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+ shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
+proof -
+ define J where "J = x`I"
+ define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
+ define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
+ have *: "open (X i)" for i
+ unfolding X_def V_def using assms by auto
+ have **: "finite {i. X i \<noteq> UNIV}"
+ unfolding X_def V_def J_def using assms(1) by auto
+ have "open (Pi\<^sub>E UNIV X)"
+ unfolding open_fun_def apply (rule product_topology_basis)
+ using * ** unfolding open_openin topspace_euclidean by auto
+ moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
+ apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
+ proof (auto)
+ fix f :: "'a \<Rightarrow> 'b" and i :: 'i
+ assume a1: "i \<in> I"
+ assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
+ have f3: "x i \<in> x`I"
+ using a1 by blast
+ have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
+ using a1 by blast
+ then show "f (x i) \<in> U i"
+ using f3 a2 by (meson Inter_iff)
+ qed
+ ultimately show ?thesis by simp
+qed
+
+text {*The results proved in the general situation of products of possibly different
+spaces have their counterparts in this simpler setting.*}
+
+lemma continuous_on_product_coordinates [simp]:
+ "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
+unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_product_coordinates, simp)
+
+lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
+ assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
+ shows "continuous_on UNIV f"
+using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_coordinatewise_then_product, simp)
+
+lemma continuous_on_product_then_coordinatewise:
+ assumes "continuous_on UNIV f"
+ shows "continuous_on UNIV (\<lambda>x. f x i)"
+using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
+by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
+
+lemma continuous_on_product_coordinatewise_iff:
+ "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
+by (auto intro: continuous_on_product_then_coordinatewise)
+
+subsubsection {*Topological countability for product spaces*}
+
+text {*The next two lemmas are useful to prove first or second countability
+of product spaces, but they have more to do with countability and could
+be put in the corresponding theory.*}
+
+lemma countable_nat_product_event_const:
+ fixes F::"'a set" and a::'a
+ assumes "a \<in> F" "countable F"
+ shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
+proof -
+ have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
+ \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
+ using infinite_nat_iff_unbounded_le by fastforce
+ have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
+ proof (induction N)
+ case 0
+ have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
+ using `a \<in> F` by auto
+ then show ?case by auto
+ next
+ case (Suc N)
+ define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
+ where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
+ have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+ proof (auto)
+ fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
+ define y where "y = (\<lambda>i. if i = N then a else x i)"
+ have "f (y, x N) = x"
+ unfolding f_def y_def by auto
+ moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
+ unfolding y_def using H `a \<in> F` by auto
+ ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+ by (metis (no_types, lifting) image_eqI)
+ qed
+ moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+ using Suc.IH assms(2) by auto
+ ultimately show ?case
+ by (meson countable_image countable_subset)
+ qed
+ then show ?thesis using countable_subset[OF *] by auto
+qed
+
+lemma countable_product_event_const:
+ fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
+ assumes "\<And>i. countable (F i)"
+ shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
+proof -
+ define G where "G = (\<Union>i. F i) \<union> {b}"
+ have "countable G" unfolding G_def using assms by auto
+ have "b \<in> G" unfolding G_def by auto
+ define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
+ have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
+ \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
+ proof (auto)
+ fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
+ define I where "I = {i. f i \<noteq> b}"
+ define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
+ have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
+ then have "finite {j. g j \<noteq> b}"
+ unfolding I_def using H(2) using finite_surj by blast
+ moreover have "g j \<in> G" for j
+ unfolding g_def G_def using H by auto
+ ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
+ by auto
+ moreover have "f = pi g"
+ unfolding pi_def g_def I_def using H by fastforce
+ ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
+ by auto
+ qed
+ then show ?thesis
+ using countable_nat_product_event_const[OF `b \<in> G` `countable G`]
+ by (meson countable_image countable_subset)
+qed
+
+instance "fun" :: (countable, first_countable_topology) first_countable_topology
+proof
+ fix x::"'a \<Rightarrow> 'b"
+ have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
+ apply (rule choice) using first_countable_basis by auto
+ then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
+ "\<And>x i. open (A x i)"
+ "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
+ by metis
+ text {*$B i$ is a countable basis of neighborhoods of $x_i$.*}
+ define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
+ have "countable (B i)" for i unfolding B_def by auto
+
+ define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
+ have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
+ unfolding K_def B_def by auto
+ then have "K \<noteq> {}" by auto
+ have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
+ apply (rule countable_product_event_const) using `\<And>i. countable (B i)` by auto
+ moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
+ unfolding K_def by auto
+ ultimately have "countable K" by auto
+ have "x \<in> k" if "k \<in> K" for k
+ using that unfolding K_def B_def apply auto using A(1) by auto
+ have "open k" if "k \<in> K" for k
+ using that unfolding open_fun_def K_def B_def apply (auto)
+ apply (rule product_topology_basis)
+ unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
+
+ have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
+ proof -
+ have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
+ using `open U \<and> x \<in> U` unfolding open_fun_def by auto
+ with product_topology_open_contains_basis[OF this]
+ have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+ unfolding topspace_euclidean open_openin by simp
+ then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+ "\<And>i. open (X i)"
+ "finite {i. X i \<noteq> UNIV}"
+ "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+ by auto
+ define I where "I = {i. X i \<noteq> UNIV}"
+ define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
+ have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
+ unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
+ have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
+ apply (cases "i \<in> I")
+ unfolding Y_def using * that apply (auto)
+ apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
+ unfolding B_def apply simp
+ unfolding I_def apply auto
+ done
+ have "{i. Y i \<noteq> UNIV} \<subseteq> I"
+ unfolding Y_def by auto
+ then have ***: "finite {i. Y i \<noteq> UNIV}"
+ unfolding I_def using H(3) rev_finite_subset by blast
+ have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
+ using ** *** by auto
+ then have "Pi\<^sub>E UNIV Y \<in> K"
+ unfolding K_def by auto
+
+ have "Y i \<subseteq> X i" for i
+ apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
+ then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
+ then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+ then show ?thesis using `Pi\<^sub>E UNIV Y \<in> K` by auto
+ qed
+
+ show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
+ apply (rule first_countableI[of K])
+ using `countable K` `\<And>k. k \<in> K \<Longrightarrow> x \<in> k` `\<And>k. k \<in> K \<Longrightarrow> open k` Inc by auto
+qed
+
+lemma product_topology_countable_basis:
+ shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
+ topological_basis K \<and> countable K \<and>
+ (\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
+proof -
+ obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
+ using ex_countable_basis by auto
+ then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
+ define B2 where "B2 = B \<union> {UNIV}"
+ have "countable B2"
+ unfolding B2_def using B by auto
+ have "open U" if "U \<in> B2" for U
+ using that unfolding B2_def using B topological_basis_open by auto
+
+ define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+ have i: "\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+ unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
+
+ have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+ apply (rule countable_product_event_const) using `countable B2` by auto
+ moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
+ unfolding K_def by auto
+ ultimately have ii: "countable K" by auto
+
+ have iii: "topological_basis K"
+ proof (rule topological_basisI)
+ fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
+ then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+ unfolding open_fun_def by auto
+ with product_topology_open_contains_basis[OF this `x \<in> U`]
+ have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+ unfolding topspace_euclidean open_openin by simp
+ then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+ "\<And>i. open (X i)"
+ "finite {i. X i \<noteq> UNIV}"
+ "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
+ by auto
+ then have "x i \<in> X i" for i by auto
+ define I where "I = {i. X i \<noteq> UNIV}"
+ define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
+ have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
+ unfolding B2_def using B `open (X i)` `x i \<in> X i` by (meson UnCI topological_basisE)
+ have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
+ using someI_ex[OF *]
+ apply (cases "i \<in> I")
+ unfolding Y_def using * apply (auto)
+ unfolding B2_def I_def by auto
+ have "{i. Y i \<noteq> UNIV} \<subseteq> I"
+ unfolding Y_def by auto
+ then have ***: "finite {i. Y i \<noteq> UNIV}"
+ unfolding I_def using H(3) rev_finite_subset by blast
+ have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
+ using ** *** by auto
+ then have "Pi\<^sub>E UNIV Y \<in> K"
+ unfolding K_def by auto
+
+ have "Y i \<subseteq> X i" for i
+ apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
+ then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
+ then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+
+ have "x \<in> Pi\<^sub>E UNIV Y"
+ using ** by auto
+
+ show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
+ using `Pi\<^sub>E UNIV Y \<in> K` `Pi\<^sub>E UNIV Y \<subseteq> U` `x \<in> Pi\<^sub>E UNIV Y` by auto
+ next
+ fix U assume "U \<in> K"
+ show "open U"
+ using `U \<in> K` unfolding open_fun_def K_def apply (auto)
+ apply (rule product_topology_basis)
+ using `\<And>V. V \<in> B2 \<Longrightarrow> open V` open_UNIV unfolding topspace_euclidean open_openin[symmetric]
+ by auto
+ qed
+
+ show ?thesis using i ii iii by auto
+qed
+
+instance "fun" :: (countable, second_countable_topology) second_countable_topology
+ apply standard
+ using product_topology_countable_basis topological_basis_imp_subbasis by auto
+
+
+subsection {*The strong operator topology on continuous linear operators*}
+
+text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
+operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
+
+However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
+$T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when 'b is the set
+of real numbers, since then this topology is compact.
+
+We can not implement it using type classes as there is already a topology, but at least we
+can define it as a topology.
+
+Note that there is yet another (common and useful) topology on operator spaces, the weak operator
+topology, defined analogously using the product topology, but where the target space is given the
+weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
+canonical embedding of a space into its bidual. We do not define it there, although it could also be
+defined analogously.
+*}
+
+definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
+where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
+
+lemma strong_operator_topology_topspace:
+ "topspace strong_operator_topology = UNIV"
+unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
+
+lemma strong_operator_topology_basis:
+ fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
+ assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+ shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
+proof -
+ have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
+ by (rule product_topology_basis'[OF assms])
+ moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
+ = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
+ by auto
+ ultimately show ?thesis
+ unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto
+qed
+
+lemma strong_operator_topology_continuous_evaluation:
+ "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+proof -
+ have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+ unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
+ using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+ then show ?thesis unfolding comp_def by simp
+qed
+
+lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+ "continuous_on_topo T strong_operator_topology f
+ \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+proof (auto)
+ fix x::"'b"
+ assume "continuous_on_topo T strong_operator_topology f"
+ with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
+ have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+ by simp
+ then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ unfolding comp_def by auto
+next
+ assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+ have "continuous_on_topo T euclidean (blinfun_apply o f)"
+ unfolding euclidean_product_topology
+ apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+ using * unfolding comp_def by auto
+ show "continuous_on_topo T strong_operator_topology f"
+ unfolding strong_operator_topology_def
+ apply (rule continuous_on_topo_pullback')
+ by (auto simp add: `continuous_on_topo T euclidean (blinfun_apply o f)`)
+qed
+
+lemma strong_operator_topology_weaker_than_euclidean:
+ "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+ auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+
+
+subsection {*Metrics on product spaces*}
+
+
+text {*In general, the product topology is not metrizable, unless the index set is countable.
+When the index set is countable, essentially any (convergent) combination of the metrics on the
+factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
+for instance.
+
+What is not completely trivial is that the distance thus defined induces the same topology
+as the product topology. This is what we have to prove to show that we have an instance
+of \verb+metric_space+.
+
+The proofs below would work verbatim for general countable products of metric spaces. However,
+since distances are only implemented in terms of type classes, we only develop the theory
+for countable products of the same space.*}
+
+instantiation "fun" :: (countable, metric_space) metric_space
+begin
+
+definition dist_fun_def:
+ "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+
+definition uniformity_fun_def:
+ "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
+
+text {*Except for the first one, the auxiliary lemmas below are only useful when proving the
+instance: once it is proved, they become trivial consequences of the general theory of metric
+spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
+to do this.*}
+
+lemma dist_fun_le_dist_first_terms:
+ "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+proof -
+ have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+ = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
+ by (rule suminf_cong, simp add: power_add)
+ also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
+ apply (rule suminf_mult)
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
+ apply (simp, rule suminf_le, simp)
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ also have "... = (1/2)^(Suc N) * 2"
+ using suminf_geometric[of "1/2"] by auto
+ also have "... = (1/2)^N"
+ by auto
+ finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"
+ by simp
+
+ define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
+ have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
+ unfolding M_def by (rule Max_ge, auto)
+ then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
+ have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
+ unfolding M_def apply (rule Max_ge) using that by auto
+ then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
+ using that by force
+ have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
+ (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
+ by (rule sum_mono, simp add: i)
+ also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
+ by (rule sum_distrib_left[symmetric])
+ also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
+ by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
+ also have "... = M * 2"
+ using suminf_geometric[of "1/2"] by auto
+ finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
+ by simp
+
+ have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+ unfolding dist_fun_def by simp
+ also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+ + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+ apply (rule suminf_split_initial_segment)
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ also have "... \<le> 2 * M + (1/2)^N"
+ using * ** by auto
+ finally show ?thesis unfolding M_def by simp
+qed
+
+lemma open_fun_contains_ball_aux:
+ assumes "open (U::(('a \<Rightarrow> 'b) set))"
+ "x \<in> U"
+ shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
+proof -
+ have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+ using open_fun_def assms by auto
+ obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
+ "\<And>i. openin euclidean (X i)"
+ "finite {i. X i \<noteq> topspace euclidean}"
+ "x \<in> Pi\<^sub>E UNIV X"
+ using product_topology_open_contains_basis[OF * `x \<in> U`] by auto
+ define I where "I = {i. X i \<noteq> topspace euclidean}"
+ have "finite I" unfolding I_def using H(3) by auto
+ {
+ fix i
+ have "x i \<in> X i" using `x \<in> U` H by auto
+ then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
+ using `openin euclidean (X i)` open_openin open_contains_ball by blast
+ then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
+ define f where "f = min e (1/2)"
+ have "f>0" "f<1" unfolding f_def using `e>0` by auto
+ moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using `ball (x i) e \<subseteq> X i` by auto
+ ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
+ } note * = this
+ have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
+ by (rule choice, auto simp add: *)
+ then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
+ by blast
+ define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
+ have "m > 0" if "I\<noteq>{}"
+ unfolding m_def apply (rule Min_grI) using `finite I` `I \<noteq> {}` `\<And>i. e i > 0` by auto
+ moreover have "{y. dist x y < m} \<subseteq> U"
+ proof (auto)
+ fix y assume "dist x y < m"
+ have "y i \<in> X i" if "i \<in> I" for i
+ proof -
+ have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ define n where "n = to_nat i"
+ have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
+ using `dist x y < m` unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
+ then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
+ using `n = to_nat i` by auto
+ also have "... \<le> (1/2)^(to_nat i) * e i"
+ unfolding m_def apply (rule Min_le) using `finite I` `i \<in> I` by auto
+ ultimately have "min (dist (x i) (y i)) 1 < e i"
+ by (auto simp add: divide_simps)
+ then have "dist (x i) (y i) < e i"
+ using `e i < 1` by auto
+ then show "y i \<in> X i" using `ball (x i) (e i) \<subseteq> X i` by auto
+ qed
+ then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+ then show "y \<in> U" using `Pi\<^sub>E UNIV X \<subseteq> U` by auto
+ qed
+ ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
+
+ have "U = UNIV" if "I = {}"
+ using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+ then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
+ then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
+qed
+
+lemma ball_fun_contains_open_aux:
+ fixes x::"('a \<Rightarrow> 'b)" and e::real
+ assumes "e>0"
+ shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
+proof -
+ have "\<exists>N::nat. 2^N > 8/e"
+ by (simp add: real_arch_pow)
+ then obtain N::nat where "2^N > 8/e" by auto
+ define f where "f = e/4"
+ have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
+ define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"
+ have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
+ unfolding X_def by auto
+ then have "finite {i. X i \<noteq> topspace euclidean}"
+ unfolding topspace_euclidean using finite_surj by blast
+ have "\<And>i. open (X i)"
+ unfolding X_def using metric_space_class.open_ball open_UNIV by auto
+ then have "\<And>i. openin euclidean (X i)"
+ using open_openin by auto
+ define U where "U = Pi\<^sub>E UNIV X"
+ have "open U"
+ unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
+ unfolding U_def using `\<And>i. openin euclidean (X i)` `finite {i. X i \<noteq> topspace euclidean}`
+ by auto
+ moreover have "x \<in> U"
+ unfolding U_def X_def by (auto simp add: PiE_iff)
+ moreover have "dist x y < e" if "y \<in> U" for y
+ proof -
+ have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
+ using `y \<in> U` unfolding U_def apply (auto simp add: PiE_iff)
+ unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
+ have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
+ apply (rule Max.boundedI) using * by auto
+
+ have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+ by (rule dist_fun_le_dist_first_terms)
+ also have "... \<le> 2 * f + e / 8"
+ apply (rule add_mono) using ** `2^N > 8/e` by(auto simp add: algebra_simps divide_simps)
+ also have "... \<le> e/2 + e/8"
+ unfolding f_def by auto
+ also have "... < e"
+ by auto
+ finally show "dist x y < e" by simp
+ qed
+ ultimately show ?thesis by auto
+qed
+
+lemma fun_open_ball_aux:
+ fixes U::"('a \<Rightarrow> 'b) set"
+ shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
+proof (auto)
+ assume "open U"
+ fix x assume "x \<in> U"
+ then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+ using open_fun_contains_ball_aux[OF `open U` `x \<in> U`] by auto
+next
+ assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+ define K where "K = {V. open V \<and> V \<subseteq> U}"
+ {
+ fix x assume "x \<in> U"
+ then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
+ then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
+ using ball_fun_contains_open_aux[OF `e>0`, of x] by auto
+ have "V \<in> K"
+ unfolding K_def using e(2) V(1) V(3) by auto
+ then have "x \<in> (\<Union>K)" using `x \<in> V` by auto
+ }
+ then have "(\<Union>K) = U"
+ unfolding K_def by auto
+ moreover have "open (\<Union>K)"
+ unfolding K_def by auto
+ ultimately show "open U" by simp
+qed
+
+instance proof
+ fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
+ proof
+ assume "x = y"
+ then show "dist x y = 0" unfolding dist_fun_def using `x = y` by auto
+ next
+ assume "dist x y = 0"
+ have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
+ using `dist x y = 0` unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
+ then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
+ by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
+ zero_eq_1_divide_iff zero_neq_numeral)
+ then have "x (from_nat n) = y (from_nat n)" for n
+ by auto
+ then have "x i = y i" for i
+ by (metis from_nat_to_nat)
+ then show "x = y"
+ by auto
+ qed
+next
+ text{*The proof of the triangular inequality is trivial, modulo the fact that we are dealing
+ with infinite series, hence we should justify the convergence at each step. In this
+ respect, the following simplification rule is extremely handy.*}
+ have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ fix x y z::"'a \<Rightarrow> 'b"
+ {
+ fix n
+ have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
+ dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
+ by (simp add: dist_triangle2)
+ have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
+ using zero_le_dist by blast
+ moreover
+ {
+ assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
+ then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
+ by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
+ }
+ ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
+ min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
+ using * by linarith
+ } note ineq = this
+ have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+ unfolding dist_fun_def by simp
+ also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
+ + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+ apply (rule suminf_le)
+ using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
+ le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
+ by (auto simp add: summable_add)
+ also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
+ + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+ by (rule suminf_add[symmetric], auto)
+ also have "... = dist x z + dist y z"
+ unfolding dist_fun_def by simp
+ finally show "dist x y \<le> dist x z + dist y z"
+ by simp
+next
+ text{*Finally, we show that the topology generated by the distance and the product
+ topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
+ except that the condition to prove is expressed with filters. To deal with this,
+ we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
+ \verb+Real_Vector_Spaces.thy+*}
+ fix U::"('a \<Rightarrow> 'b) set"
+ have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
+ unfolding uniformity_fun_def apply (subst eventually_INF_base)
+ by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
+ then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
+ unfolding fun_open_ball_aux by simp
+qed (simp add: uniformity_fun_def)
+
+end
+
+text {*Nice properties of spaces are preserved under countable products. In addition
+to first countability, second countability and metrizability, as we have seen above,
+completeness is also preserved, and therefore being Polish.*}
+
+instance "fun" :: (countable, complete_space) complete_space
+proof
+ fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
+ have "Cauchy (\<lambda>n. u n i)" for i
+ unfolding cauchy_def proof (intro impI allI)
+ fix e assume "e>(0::real)"
+ obtain k where "i = from_nat k"
+ using from_nat_to_nat[of i] by metis
+ have "(1/2)^k * min e 1 > 0" using `e>0` by auto
+ then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
+ using `Cauchy u` unfolding cauchy_def by blast
+ then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
+ by blast
+ have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+ proof (auto)
+ fix m n::nat assume "m \<ge> N" "n \<ge> N"
+ have "(1/2)^k * min (dist (u m i) (u n i)) 1
+ = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
+ using `i = from_nat k` by auto
+ also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
+ apply (rule sum_le_suminf)
+ by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+ also have "... = dist (u m) (u n)"
+ unfolding dist_fun_def by auto
+ also have "... < (1/2)^k * min e 1"
+ using C `m \<ge> N` `n \<ge> N` by auto
+ finally have "min (dist (u m i) (u n i)) 1 < min e 1"
+ by (auto simp add: algebra_simps divide_simps)
+ then show "dist (u m i) (u n i) < e" by auto
+ qed
+ then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+ by blast
+ qed
+ then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
+ using Cauchy_convergent convergent_def by auto
+ then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
+ using choice by force
+ then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
+ have "u \<longlonglongrightarrow> x"
+ proof (rule metric_LIMSEQ_I)
+ fix e assume [simp]: "e>(0::real)"
+ have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
+ by (rule metric_LIMSEQ_D, auto simp add: *)
+ have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
+ apply (rule choice) using i by auto
+ then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
+ by blast
+
+ have "\<exists>N::nat. 2^N > 4/e"
+ by (simp add: real_arch_pow)
+ then obtain N::nat where "2^N > 4/e" by auto
+ define L where "L = Max {K (from_nat n)|n. n \<le> N}"
+ have "dist (u k) x < e" if "k \<ge> L" for k
+ proof -
+ have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
+ proof -
+ have "K (from_nat n) \<le> L"
+ unfolding L_def apply (rule Max_ge) using `n \<le> N` by auto
+ then have "k \<ge> K (from_nat n)" using `k \<ge> L` by auto
+ then show ?thesis using K less_imp_le by auto
+ qed
+ have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
+ apply (rule Max.boundedI) using * by auto
+ have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
+ using dist_fun_le_dist_first_terms by auto
+ also have "... \<le> 2 * e/4 + e/4"
+ apply (rule add_mono)
+ using ** `2^N > 4/e` less_imp_le by (auto simp add: algebra_simps divide_simps)
+ also have "... < e" by auto
+ finally show ?thesis by simp
+ qed
+ then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
+ qed
+ then show "convergent u" using convergent_def by blast
+qed
+
+instance "fun" :: (countable, polish_space) polish_space
+by standard
+
+
+subsection {*Measurability*}
+
+text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
+generated by open sets in the product, and the product sigma algebra, countably generated by
+products of measurable sets along finitely many coordinates. The second one is defined and studied
+in \verb+Finite_Product_Measure.thy+.
+
+These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
+but there is a fundamental difference: open sets are generated by arbitrary unions, not only
+countable ones, so typically many open sets will not be measurable with respect to the product sigma
+algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
+only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
+the factor is countably generated).
+
+In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
+compare it with the product sigma algebra as explained above.
+*}
+
+lemma measurable_product_coordinates [measurable (raw)]:
+ "(\<lambda>x. x i) \<in> measurable borel borel"
+by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+
+lemma measurable_product_then_coordinatewise:
+ fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
+ assumes [measurable]: "f \<in> borel_measurable M"
+ shows "(\<lambda>x. f x i) \<in> borel_measurable M"
+proof -
+ have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
+ unfolding comp_def by auto
+ then show ?thesis by simp
+qed
+
+text {*To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+of the product sigma algebra that is more similar to the one we used above for the product
+topology.*}
+
+lemma sets_PiM_finite:
+ "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+ {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+proof
+ have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
+ proof (auto)
+ fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
+ then have *: "X i \<in> sets (M i)" for i by simp
+ define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
+ have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
+ define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
+ have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
+ unfolding Y_def apply (rule sets_PiM_I) using `finite J` `J \<subseteq> I` * by auto
+ moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
+ unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
+ by (auto simp add: PiE_iff, blast)
+ ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
+ qed
+ then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
+ \<subseteq> sets (Pi\<^sub>M I M)"
+ by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
+
+ have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
+ (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
+ if "i \<in> I" "A \<in> sets (M i)" for i A
+ proof -
+ define X where "X = (\<lambda>j. if j = i then A else space (M j))"
+ have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
+ unfolding X_def using sets.sets_into_space[OF `A \<in> sets (M i)`] `i \<in> I`
+ by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
+ moreover have "X j \<in> sets (M j)" for j
+ unfolding X_def using `A \<in> sets (M i)` by auto
+ moreover have "finite {j. X j \<noteq> space (M j)}"
+ unfolding X_def by simp
+ ultimately show ?thesis by auto
+ qed
+ show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+ unfolding sets_PiM_single
+ apply (rule sigma_sets_mono')
+ apply (auto simp add: PiE_iff *)
+ done
+qed
+
+lemma sets_PiM_subset_borel:
+ "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
+proof -
+ have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
+ proof -
+ define I where "I = {i. X i \<noteq> UNIV}"
+ have "finite I" unfolding I_def using that by simp
+ have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
+ unfolding I_def by auto
+ also have "... \<in> sets borel"
+ using that `finite I` by measurable
+ finally show ?thesis by simp
+ qed
+ then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
+ by auto
+ then show ?thesis unfolding sets_PiM_finite space_borel
+ by (simp add: * sets.sigma_sets_subset')
+qed
+
+lemma sets_PiM_equal_borel:
+ "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
+proof
+ obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
+ "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+ using product_topology_countable_basis by fast
+ have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
+ proof -
+ obtain X where H: "k = PiE UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+ using K(3)[OF `k \<in> K`] by blast
+ show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
+ qed
+ have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
+ proof -
+ obtain B where "B \<subseteq> K" "U = (\<Union>B)"
+ using `open U` `topological_basis K` by (metis topological_basis_def)
+ have "countable B" using `B \<subseteq> K` `countable K` countable_subset by blast
+ moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
+ using `B \<subseteq> K` * that by auto
+ ultimately show ?thesis unfolding `U = (\<Union>B)` by auto
+ qed
+ have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
+ apply (rule sets.sigma_sets_subset') using ** by auto
+ then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+ unfolding borel_def by auto
+qed (simp add: sets_PiM_subset_borel)
+
+lemma measurable_coordinatewise_then_product:
+ fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
+ assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
+ shows "f \<in> borel_measurable M"
+proof -
+ have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+ by (rule measurable_PiM_single', auto simp add: assms)
+ then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
+qed
+
+end