diff -r 66c4567664b5 -r eddcc7c726f3 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Mar 18 15:35:34 2019 +0000
@@ -9,6 +9,8 @@
   Topology_Euclidean_Space
   Operator_Norm
   Uniform_Limit
+  Function_Topology
+
 begin
 
 lemma onorm_componentwise:
@@ -733,4 +735,86 @@
   bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
   bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
 
+
+subsection \<open>The strong operator topology on continuous linear operators\<close>
+
+text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
+operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
+
+However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
+\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> 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.
+\<close>
+
+definition%important 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 by (subst openin_pullback_topology) 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: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
+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)
+
+
+
 end