src/HOL/Analysis/Bounded_Linear_Function.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 70065 cc89a395b5a3
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/Bounded_Linear_Function.thy
     2     Author:     Fabian Immler, TU M√ľnchen
     3 *)
     4 
     5 section \<open>Bounded Linear Function\<close>
     6 
     7 theory Bounded_Linear_Function
     8 imports
     9   Topology_Euclidean_Space
    10   Operator_Norm
    11   Uniform_Limit
    12   Function_Topology
    13 
    14 begin
    15 
    16 lemma onorm_componentwise:
    17   assumes "bounded_linear f"
    18   shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
    19 proof -
    20   {
    21     fix i::'a
    22     assume "i \<in> Basis"
    23     hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
    24       by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
    25     also have "\<dots> \<le>  norm i * norm (f i)"
    26       by (rule mult_right_mono)
    27         (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
    28     finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
    29       by simp
    30   } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
    31     by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
    32       sum_mono bounded_linear_inner_left)
    33   also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
    34     by (simp add: linear_sum bounded_linear.linear assms linear_simps)
    35   also have "\<dots> = f"
    36     by (simp add: euclidean_representation)
    37   finally show ?thesis .
    38 qed
    39 
    40 lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
    41 
    42 subsection%unimportant \<open>Intro rules for \<^term>\<open>bounded_linear\<close>\<close>
    43 
    44 named_theorems bounded_linear_intros
    45 
    46 lemma onorm_inner_left:
    47   assumes "bounded_linear r"
    48   shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
    49 proof (rule onorm_bound)
    50   fix x
    51   have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
    52     by (simp add: Cauchy_Schwarz_ineq2)
    53   also have "\<dots> \<le> onorm r * norm x * norm f"
    54     by (intro mult_right_mono onorm assms norm_ge_zero)
    55   finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
    56     by (simp add: ac_simps)
    57 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
    58 
    59 lemma onorm_inner_right:
    60   assumes "bounded_linear r"
    61   shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
    62   apply (subst inner_commute)
    63   apply (rule onorm_inner_left[OF assms, THEN order_trans])
    64   apply simp
    65   done
    66 
    67 lemmas [bounded_linear_intros] =
    68   bounded_linear_zero
    69   bounded_linear_add
    70   bounded_linear_const_mult
    71   bounded_linear_mult_const
    72   bounded_linear_scaleR_const
    73   bounded_linear_const_scaleR
    74   bounded_linear_ident
    75   bounded_linear_sum
    76   bounded_linear_Pair
    77   bounded_linear_sub
    78   bounded_linear_fst_comp
    79   bounded_linear_snd_comp
    80   bounded_linear_inner_left_comp
    81   bounded_linear_inner_right_comp
    82 
    83 
    84 subsection%unimportant \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
    85 
    86 attribute_setup bounded_linear =
    87   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
    88     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
    89       [
    90         (@{thm bounded_linear.has_derivative}, \<^named_theorems>\<open>derivative_intros\<close>),
    91         (@{thm bounded_linear.tendsto}, \<^named_theorems>\<open>tendsto_intros\<close>),
    92         (@{thm bounded_linear.continuous}, \<^named_theorems>\<open>continuous_intros\<close>),
    93         (@{thm bounded_linear.continuous_on}, \<^named_theorems>\<open>continuous_intros\<close>),
    94         (@{thm bounded_linear.uniformly_continuous_on}, \<^named_theorems>\<open>continuous_intros\<close>),
    95         (@{thm bounded_linear_compose}, \<^named_theorems>\<open>bounded_linear_intros\<close>)
    96       ]))\<close>
    97 
    98 attribute_setup bounded_bilinear =
    99   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
   100     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
   101       [
   102         (@{thm bounded_bilinear.FDERIV}, \<^named_theorems>\<open>derivative_intros\<close>),
   103         (@{thm bounded_bilinear.tendsto}, \<^named_theorems>\<open>tendsto_intros\<close>),
   104         (@{thm bounded_bilinear.continuous}, \<^named_theorems>\<open>continuous_intros\<close>),
   105         (@{thm bounded_bilinear.continuous_on}, \<^named_theorems>\<open>continuous_intros\<close>),
   106         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
   107           \<^named_theorems>\<open>bounded_linear_intros\<close>),
   108         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
   109           \<^named_theorems>\<open>bounded_linear_intros\<close>),
   110         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
   111           \<^named_theorems>\<open>continuous_intros\<close>),
   112         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
   113           \<^named_theorems>\<open>continuous_intros\<close>)
   114       ]))\<close>
   115 
   116 
   117 subsection \<open>Type of bounded linear functions\<close>
   118 
   119 typedef%important (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
   120   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
   121   morphisms blinfun_apply Blinfun
   122   by (blast intro: bounded_linear_intros)
   123 
   124 declare [[coercion
   125     "blinfun_apply :: ('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b"]]
   126 
   127 lemma bounded_linear_blinfun_apply[bounded_linear_intros]:
   128   "bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. blinfun_apply f (g x))"
   129   by (metis blinfun_apply mem_Collect_eq bounded_linear_compose)
   130 
   131 setup_lifting type_definition_blinfun
   132 
   133 lemma blinfun_eqI: "(\<And>i. blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
   134   by transfer auto
   135 
   136 lemma bounded_linear_Blinfun_apply: "bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f"
   137   by (auto simp: Blinfun_inverse)
   138 
   139 
   140 subsection \<open>Type class instantiations\<close>
   141 
   142 instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
   143 begin
   144 
   145 lift_definition%important norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
   146 
   147 lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   148   is "\<lambda>f g x. f x - g x"
   149   by (rule bounded_linear_sub)
   150 
   151 definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
   152   where "dist_blinfun a b = norm (a - b)"
   153 
   154 definition [code del]:
   155   "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
   156 
   157 definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
   158   where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   159 
   160 lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
   161   by (rule bounded_linear_minus)
   162 
   163 lift_definition%important zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
   164   by (rule bounded_linear_zero)
   165 
   166 lift_definition%important plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   167   is "\<lambda>f g x. f x + g x"
   168   by (metis bounded_linear_add)
   169 
   170 lift_definition%important scaleR_blinfun::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>r f x. r *\<^sub>R f x"
   171   by (metis bounded_linear_compose bounded_linear_scaleR_right)
   172 
   173 definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   174   where "sgn_blinfun x = scaleR (inverse (norm x)) x"
   175 
   176 instance
   177   apply standard
   178   unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
   179   apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
   180   done
   181 
   182 end
   183 
   184 declare uniformity_Abort[where 'a="('a :: real_normed_vector) \<Rightarrow>\<^sub>L ('b :: real_normed_vector)", code]
   185 
   186 lemma norm_blinfun_eqI:
   187   assumes "n \<le> norm (blinfun_apply f x) / norm x"
   188   assumes "\<And>x. norm (blinfun_apply f x) \<le> n * norm x"
   189   assumes "0 \<le> n"
   190   shows "norm f = n"
   191   by (auto simp: norm_blinfun_def
   192     intro!: antisym onorm_bound assms order_trans[OF _ le_onorm]
   193     bounded_linear_intros)
   194 
   195 lemma norm_blinfun: "norm (blinfun_apply f x) \<le> norm f * norm x"
   196   by transfer (rule onorm)
   197 
   198 lemma norm_blinfun_bound: "0 \<le> b \<Longrightarrow> (\<And>x. norm (blinfun_apply f x) \<le> b * norm x) \<Longrightarrow> norm f \<le> b"
   199   by transfer (rule onorm_bound)
   200 
   201 lemma bounded_bilinear_blinfun_apply[bounded_bilinear]: "bounded_bilinear blinfun_apply"
   202 proof
   203   fix f g::"'a \<Rightarrow>\<^sub>L 'b" and a b::'a and r::real
   204   show "(f + g) a = f a + g a" "(r *\<^sub>R f) a = r *\<^sub>R f a"
   205     by (transfer, simp)+
   206   interpret bounded_linear f for f::"'a \<Rightarrow>\<^sub>L 'b"
   207     by (auto intro!: bounded_linear_intros)
   208   show "f (a + b) = f a + f b" "f (r *\<^sub>R a) = r *\<^sub>R f a"
   209     by (simp_all add: add scaleR)
   210   show "\<exists>K. \<forall>a b. norm (blinfun_apply a b) \<le> norm a * norm b * K"
   211     by (auto intro!: exI[where x=1] norm_blinfun)
   212 qed
   213 
   214 interpretation blinfun: bounded_bilinear blinfun_apply
   215   by (rule bounded_bilinear_blinfun_apply)
   216 
   217 lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left
   218 
   219 
   220 context bounded_bilinear
   221 begin
   222 
   223 named_theorems bilinear_simps
   224 
   225 lemmas [bilinear_simps] =
   226   add_left
   227   add_right
   228   diff_left
   229   diff_right
   230   minus_left
   231   minus_right
   232   scaleR_left
   233   scaleR_right
   234   zero_left
   235   zero_right
   236   sum_left
   237   sum_right
   238 
   239 end
   240 
   241 
   242 instance blinfun :: (real_normed_vector, banach) banach
   243 proof
   244   fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   245   assume "Cauchy X"
   246   {
   247     fix x::'a
   248     {
   249       fix x::'a
   250       assume "norm x \<le> 1"
   251       have "Cauchy (\<lambda>n. X n x)"
   252       proof (rule CauchyI)
   253         fix e::real
   254         assume "0 < e"
   255         from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
   256           where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
   257           by auto
   258         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
   259         proof (safe intro!: exI[where x=M])
   260           fix m n
   261           assume le: "M \<le> m" "M \<le> n"
   262           have "norm (X m x - X n x) = norm ((X m - X n) x)"
   263             by (simp add: blinfun.bilinear_simps)
   264           also have "\<dots> \<le> norm (X m - X n) * norm x"
   265              by (rule norm_blinfun)
   266           also have "\<dots> \<le> norm (X m - X n) * 1"
   267             using \<open>norm x \<le> 1\<close> norm_ge_zero by (rule mult_left_mono)
   268           also have "\<dots> = norm (X m - X n)" by simp
   269           also have "\<dots> < e" using le by fact
   270           finally show "norm (X m x - X n x) < e" .
   271         qed
   272       qed
   273       hence "convergent (\<lambda>n. X n x)"
   274         by (metis Cauchy_convergent_iff)
   275     } note convergent_norm1 = this
   276     define y where "y = x /\<^sub>R norm x"
   277     have y: "norm y \<le> 1" and xy: "x = norm x *\<^sub>R y"
   278       by (simp_all add: y_def inverse_eq_divide)
   279     have "convergent (\<lambda>n. norm x *\<^sub>R X n y)"
   280       by (intro bounded_bilinear.convergent[OF bounded_bilinear_scaleR] convergent_const
   281         convergent_norm1 y)
   282     also have "(\<lambda>n. norm x *\<^sub>R X n y) = (\<lambda>n. X n x)"
   283       by (subst xy) (simp add: blinfun.bilinear_simps)
   284     finally have "convergent (\<lambda>n. X n x)" .
   285   }
   286   then obtain v where v: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> v x"
   287     unfolding convergent_def
   288     by metis
   289 
   290   have "Cauchy (\<lambda>n. norm (X n))"
   291   proof (rule CauchyI)
   292     fix e::real
   293     assume "e > 0"
   294     from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
   295       where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
   296       by auto
   297     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
   298     proof (safe intro!: exI[where x=M])
   299       fix m n assume mn: "m \<ge> M" "n \<ge> M"
   300       have "norm (norm (X m) - norm (X n)) \<le> norm (X m - X n)"
   301         by (metis norm_triangle_ineq3 real_norm_def)
   302       also have "\<dots> < e" using mn by fact
   303       finally show "norm (norm (X m) - norm (X n)) < e" .
   304     qed
   305   qed
   306   then obtain K where K: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow> K"
   307     unfolding Cauchy_convergent_iff convergent_def
   308     by metis
   309 
   310   have "bounded_linear v"
   311   proof
   312     fix x y and r::real
   313     from tendsto_add[OF v[of x] v [of y]] v[of "x + y", unfolded blinfun.bilinear_simps]
   314       tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *\<^sub>R x", unfolded blinfun.bilinear_simps]
   315     show "v (x + y) = v x + v y" "v (r *\<^sub>R x) = r *\<^sub>R v x"
   316       by (metis (poly_guards_query) LIMSEQ_unique)+
   317     show "\<exists>K. \<forall>x. norm (v x) \<le> norm x * K"
   318     proof (safe intro!: exI[where x=K])
   319       fix x
   320       have "norm (v x) \<le> K * norm x"
   321         by (rule tendsto_le[OF _ tendsto_mult[OF K tendsto_const] tendsto_norm[OF v]])
   322           (auto simp: norm_blinfun)
   323       thus "norm (v x) \<le> norm x * K"
   324         by (simp add: ac_simps)
   325     qed
   326   qed
   327   hence Bv: "\<And>x. (\<lambda>n. X n x) \<longlonglongrightarrow> Blinfun v x"
   328     by (auto simp: bounded_linear_Blinfun_apply v)
   329 
   330   have "X \<longlonglongrightarrow> Blinfun v"
   331   proof (rule LIMSEQ_I)
   332     fix r::real assume "r > 0"
   333     define r' where "r' = r / 2"
   334     have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
   335     from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
   336     obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
   337       by metis
   338     show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
   339     proof (safe intro!: exI[where x=M])
   340       fix n assume n: "M \<le> n"
   341       have "norm (X n - Blinfun v) \<le> r'"
   342       proof (rule norm_blinfun_bound)
   343         fix x
   344         have "eventually (\<lambda>m. m \<ge> M) sequentially"
   345           by (metis eventually_ge_at_top)
   346         hence ev_le: "eventually (\<lambda>m. norm (X n x - X m x) \<le> r' * norm x) sequentially"
   347         proof eventually_elim
   348           case (elim m)
   349           have "norm (X n x - X m x) = norm ((X n - X m) x)"
   350             by (simp add: blinfun.bilinear_simps)
   351           also have "\<dots> \<le> norm ((X n - X m)) * norm x"
   352             by (rule norm_blinfun)
   353           also have "\<dots> \<le> r' * norm x"
   354             using M[OF n elim] by (simp add: mult_right_mono)
   355           finally show ?case .
   356         qed
   357         have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
   358           by (auto intro!: tendsto_intros Bv)
   359         show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
   360           by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
   361       qed (simp add: \<open>0 < r'\<close> less_imp_le)
   362       thus "norm (X n - Blinfun v) < r"
   363         by (metis \<open>r' < r\<close> le_less_trans)
   364     qed
   365   qed
   366   thus "convergent X"
   367     by (rule convergentI)
   368 qed
   369 
   370 subsection%unimportant \<open>On Euclidean Space\<close>
   371 
   372 lemma Zfun_sum:
   373   assumes "finite s"
   374   assumes f: "\<And>i. i \<in> s \<Longrightarrow> Zfun (f i) F"
   375   shows "Zfun (\<lambda>x. sum (\<lambda>i. f i x) s) F"
   376   using assms by induct (auto intro!: Zfun_zero Zfun_add)
   377 
   378 lemma norm_blinfun_euclidean_le:
   379   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
   380   shows "norm a \<le> sum (\<lambda>x. norm (a x)) Basis"
   381   apply (rule norm_blinfun_bound)
   382    apply (simp add: sum_nonneg)
   383   apply (subst euclidean_representation[symmetric, where 'a='a])
   384   apply (simp only: blinfun.bilinear_simps sum_distrib_right)
   385   apply (rule order.trans[OF norm_sum sum_mono])
   386   apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
   387   done
   388 
   389 lemma tendsto_componentwise1:
   390   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
   391     and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   392   assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) \<longlongrightarrow> a j) F)"
   393   shows "(b \<longlongrightarrow> a) F"
   394 proof -
   395   have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x j - a j)) F"
   396     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
   397   hence "Zfun (\<lambda>x. \<Sum>j\<in>Basis. norm (b x j - a j)) F"
   398     by (auto intro!: Zfun_sum)
   399   thus ?thesis
   400     unfolding tendsto_Zfun_iff
   401     by (rule Zfun_le)
   402       (auto intro!: order_trans[OF norm_blinfun_euclidean_le] simp: blinfun.bilinear_simps)
   403 qed
   404 
   405 lift_definition
   406   blinfun_of_matrix::"('b::euclidean_space \<Rightarrow> 'a::euclidean_space \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   407   is "\<lambda>a x. \<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i"
   408   by (intro bounded_linear_intros)
   409 
   410 lemma blinfun_of_matrix_works:
   411   fixes f::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   412   shows "blinfun_of_matrix (\<lambda>i j. (f j) \<bullet> i) = f"
   413 proof (transfer, rule,  rule euclidean_eqI)
   414   fix f::"'a \<Rightarrow> 'b" and x::'a and b::'b assume "bounded_linear f" and b: "b \<in> Basis"
   415   then interpret bounded_linear f by simp
   416   have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
   417     = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
   418     using b
   419     by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
   420   also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
   421     using b by (simp add: sum.delta)
   422   also have "\<dots> = f x \<bullet> b"
   423     by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms)
   424   finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" .
   425 qed
   426 
   427 lemma blinfun_of_matrix_apply:
   428   "blinfun_of_matrix a x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)"
   429   by transfer simp
   430 
   431 lemma blinfun_of_matrix_minus: "blinfun_of_matrix x - blinfun_of_matrix y = blinfun_of_matrix (x - y)"
   432   by transfer (auto simp: algebra_simps sum_subtractf)
   433 
   434 lemma norm_blinfun_of_matrix:
   435   "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
   436   apply (rule norm_blinfun_bound)
   437    apply (simp add: sum_nonneg)
   438   apply (simp only: blinfun_of_matrix_apply sum_distrib_right)
   439   apply (rule order_trans[OF norm_sum sum_mono])
   440   apply (rule order_trans[OF norm_sum sum_mono])
   441   apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
   442   done
   443 
   444 lemma tendsto_blinfun_of_matrix:
   445   assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) \<longlongrightarrow> a i j) F"
   446   shows "((\<lambda>n. blinfun_of_matrix (b n)) \<longlongrightarrow> blinfun_of_matrix a) F"
   447 proof -
   448   have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
   449     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
   450   hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
   451     by (auto intro!: Zfun_sum)
   452   thus ?thesis
   453     unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
   454     by (rule Zfun_le) (auto intro!: order_trans[OF norm_blinfun_of_matrix])
   455 qed
   456 
   457 lemma tendsto_componentwise:
   458   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   459     and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   460   shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) \<longlongrightarrow> a j \<bullet> i) F) \<Longrightarrow> (b \<longlongrightarrow> a) F"
   461   apply (subst blinfun_of_matrix_works[of a, symmetric])
   462   apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
   463   by (rule tendsto_blinfun_of_matrix)
   464 
   465 lemma
   466   continuous_blinfun_componentwiseI:
   467   fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::euclidean_space"
   468   assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. (f x) j \<bullet> i)"
   469   shows "continuous F f"
   470   using assms by (auto simp: continuous_def intro!: tendsto_componentwise)
   471 
   472 lemma
   473   continuous_blinfun_componentwiseI1:
   474   fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector"
   475   assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. f x i)"
   476   shows "continuous F f"
   477   using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
   478 
   479 lemma
   480   continuous_on_blinfun_componentwise:
   481   fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
   482   assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
   483   shows "continuous_on s f"
   484   using assms
   485   by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
   486     simp: continuous_on_eq_continuous_within continuous_def)
   487 
   488 lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
   489   by (auto intro!: bounded_linearI' bounded_linear_intros)
   490 
   491 lemma continuous_blinfun_matrix:
   492   fixes f:: "'b::t2_space \<Rightarrow> 'a::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
   493   assumes "continuous F f"
   494   shows "continuous F (\<lambda>x. (f x) j \<bullet> i)"
   495   by (rule bounded_linear.continuous[OF bounded_linear_blinfun_matrix assms])
   496 
   497 lemma continuous_on_blinfun_matrix:
   498   fixes f::"'a::t2_space \<Rightarrow> 'b::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
   499   assumes "continuous_on S f"
   500   shows "continuous_on S (\<lambda>x. (f x) j \<bullet> i)"
   501   using assms
   502   by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)
   503 
   504 lemma continuous_on_blinfun_of_matrix[continuous_intros]:
   505   assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>s. g s i j)"
   506   shows "continuous_on S (\<lambda>s. blinfun_of_matrix (g s))"
   507   using assms
   508   by (auto simp: continuous_on intro!: tendsto_blinfun_of_matrix)
   509 
   510 lemma mult_if_delta:
   511   "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
   512   by auto
   513 
   514 lemma compact_blinfun_lemma:
   515   fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   516   assumes "bounded (range f)"
   517   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r::nat\<Rightarrow>nat.
   518     strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
   519   by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
   520    (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
   521     simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta sum.delta'
   522       scaleR_sum_left[symmetric])
   523 
   524 lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
   525   apply (auto intro!: blinfun_eqI)
   526   apply (subst (2) euclidean_representation[symmetric, where 'a='a])
   527   apply (subst (1) euclidean_representation[symmetric, where 'a='a])
   528   apply (simp add: blinfun.bilinear_simps)
   529   done
   530 
   531 lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)"
   532   by (intro blinfun_euclidean_eqI)
   533      (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
   534       if_distribR sum.delta' euclidean_representation
   535       cong: if_cong)
   536 
   537 text \<open>TODO: generalize (via \<open>compact_cball\<close>)?\<close>
   538 instance blinfun :: (euclidean_space, euclidean_space) heine_borel
   539 proof
   540   fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   541   assume f: "bounded (range f)"
   542   then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "strict_mono r"
   543     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
   544     using compact_blinfun_lemma [OF f] by blast
   545   {
   546     fix e::real
   547     let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
   548     assume "e > 0"
   549     hence "e / ?d > 0" by (simp add: DIM_positive)
   550     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
   551       by simp
   552     moreover
   553     {
   554       fix n
   555       assume n: "\<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d"
   556       have "norm (f (r n) - l) = norm (blinfun_of_matrix (\<lambda>i j. (f (r n) - l) j \<bullet> i))"
   557         unfolding blinfun_of_matrix_works ..
   558       also note norm_blinfun_of_matrix
   559       also have "(\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) <
   560         (\<Sum>i\<in>(Basis::'b set). e / real_of_nat DIM('b))"
   561       proof (rule sum_strict_mono)
   562         fix i::'b assume i: "i \<in> Basis"
   563         have "(\<Sum>j::'a\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < (\<Sum>j::'a\<in>Basis. e / ?d)"
   564         proof (rule sum_strict_mono)
   565           fix j::'a assume j: "j \<in> Basis"
   566           have "\<bar>(f (r n) - l) j \<bullet> i\<bar> \<le> norm ((f (r n) - l) j)"
   567             by (simp add: Basis_le_norm i)
   568           also have "\<dots> < e / ?d"
   569             using n i j by (auto simp: dist_norm blinfun.bilinear_simps)
   570           finally show "\<bar>(f (r n) - l) j \<bullet> i\<bar> < e / ?d" by simp
   571         qed simp_all
   572         also have "\<dots> \<le> e / real_of_nat DIM('b)"
   573           by simp
   574         finally show "(\<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < e / real_of_nat DIM('b)"
   575           by simp
   576       qed simp_all
   577       also have "\<dots> \<le> e" by simp
   578       finally have "dist (f (r n)) l < e"
   579         by (auto simp: dist_norm)
   580     }
   581     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
   582       using eventually_elim2 by force
   583   }
   584   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
   585     unfolding o_def tendsto_iff by simp
   586   with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
   587     by auto
   588 qed
   589 
   590 
   591 subsection%unimportant \<open>concrete bounded linear functions\<close>
   592 
   593 lemma transfer_bounded_bilinear_bounded_linearI:
   594   assumes "g = (\<lambda>i x. (blinfun_apply (f i) x))"
   595   shows "bounded_bilinear g = bounded_linear f"
   596 proof
   597   assume "bounded_bilinear g"
   598   then interpret bounded_bilinear f by (simp add: assms)
   599   show "bounded_linear f"
   600   proof (unfold_locales, safe intro!: blinfun_eqI)
   601     fix i
   602     show "f (x + y) i = (f x + f y) i" "f (r *\<^sub>R x) i = (r *\<^sub>R f x) i" for r x y
   603       by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
   604     from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
   605       by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq ac_simps)
   606   qed
   607 qed (auto simp: assms intro!: blinfun.comp)
   608 
   609 lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
   610   "(rel_fun (rel_fun (=) (pcr_blinfun (=) (=))) (=)) bounded_bilinear bounded_linear"
   611   by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
   612     intro!: transfer_bounded_bilinear_bounded_linearI)
   613 
   614 context bounded_bilinear
   615 begin
   616 
   617 lift_definition prod_left::"'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'c" is "(\<lambda>b a. prod a b)"
   618   by (rule bounded_linear_left)
   619 declare prod_left.rep_eq[simp]
   620 
   621 lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
   622   by transfer (rule flip)
   623 
   624 lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
   625   by (rule bounded_linear_right)
   626 declare prod_right.rep_eq[simp]
   627 
   628 lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
   629   by transfer (rule bounded_bilinear_axioms)
   630 
   631 end
   632 
   633 lift_definition id_blinfun::"'a::real_normed_vector \<Rightarrow>\<^sub>L 'a" is "\<lambda>x. x"
   634   by (rule bounded_linear_ident)
   635 
   636 lemmas blinfun_apply_id_blinfun[simp] = id_blinfun.rep_eq
   637 
   638 lemma norm_blinfun_id[simp]:
   639   "norm (id_blinfun::'a::{real_normed_vector, perfect_space} \<Rightarrow>\<^sub>L 'a) = 1"
   640   by transfer (auto simp: onorm_id)
   641 
   642 lemma norm_blinfun_id_le:
   643   "norm (id_blinfun::'a::real_normed_vector \<Rightarrow>\<^sub>L 'a) \<le> 1"
   644   by transfer (auto simp: onorm_id_le)
   645 
   646 
   647 lift_definition fst_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'a" is fst
   648   by (rule bounded_linear_fst)
   649 
   650 lemma blinfun_apply_fst_blinfun[simp]: "blinfun_apply fst_blinfun = fst"
   651   by transfer (rule refl)
   652 
   653 
   654 lift_definition snd_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'b" is snd
   655   by (rule bounded_linear_snd)
   656 
   657 lemma blinfun_apply_snd_blinfun[simp]: "blinfun_apply snd_blinfun = snd"
   658   by transfer (rule refl)
   659 
   660 
   661 lift_definition blinfun_compose::
   662   "'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
   663     'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
   664     'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "(o)"
   665   parametric comp_transfer
   666   unfolding o_def
   667   by (rule bounded_linear_compose)
   668 
   669 lemma blinfun_apply_blinfun_compose[simp]: "(a o\<^sub>L b) c = a (b c)"
   670   by (simp add: blinfun_compose.rep_eq)
   671 
   672 lemma norm_blinfun_compose:
   673   "norm (f o\<^sub>L g) \<le> norm f * norm g"
   674   by transfer (rule onorm_compose)
   675 
   676 lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear (o\<^sub>L)"
   677   by unfold_locales
   678     (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
   679 
   680 lemma blinfun_compose_zero[simp]:
   681   "blinfun_compose 0 = (\<lambda>_. 0)"
   682   "blinfun_compose x 0 = 0"
   683   by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
   684 
   685 
   686 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "(\<bullet>)"
   687   by (rule bounded_linear_inner_right)
   688 declare blinfun_inner_right.rep_eq[simp]
   689 
   690 lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
   691   by transfer (rule bounded_bilinear_inner)
   692 
   693 
   694 lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
   695   by (rule bounded_linear_inner_left)
   696 declare blinfun_inner_left.rep_eq[simp]
   697 
   698 lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
   699   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
   700 
   701 
   702 lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "(*\<^sub>R)"
   703   by (rule bounded_linear_scaleR_right)
   704 declare blinfun_scaleR_right.rep_eq[simp]
   705 
   706 lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
   707   by transfer (rule bounded_bilinear_scaleR)
   708 
   709 
   710 lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
   711   by (rule bounded_linear_scaleR_left)
   712 lemmas [simp] = blinfun_scaleR_left.rep_eq
   713 
   714 lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
   715   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
   716 
   717 
   718 lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "(*)"
   719   by (rule bounded_linear_mult_right)
   720 declare blinfun_mult_right.rep_eq[simp]
   721 
   722 lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
   723   by transfer (rule bounded_bilinear_mult)
   724 
   725 
   726 lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
   727   by (rule bounded_linear_mult_left)
   728 lemmas [simp] = blinfun_mult_left.rep_eq
   729 
   730 lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
   731   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
   732 
   733 lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
   734   bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
   735   bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
   736   bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
   737 
   738 
   739 subsection \<open>The strong operator topology on continuous linear operators\<close>
   740 
   741 text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
   742 operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
   743 (the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
   744 
   745 However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
   746 \<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
   747 where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
   748 of real numbers, since then this topology is compact.
   749 
   750 We can not implement it using type classes as there is already a topology, but at least we
   751 can define it as a topology.
   752 
   753 Note that there is yet another (common and useful) topology on operator spaces, the weak operator
   754 topology, defined analogously using the product topology, but where the target space is given the
   755 weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
   756 canonical embedding of a space into its bidual. We do not define it there, although it could also be
   757 defined analogously.
   758 \<close>
   759 
   760 definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
   761 where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
   762 
   763 lemma strong_operator_topology_topspace:
   764   "topspace strong_operator_topology = UNIV"
   765 unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
   766 
   767 lemma strong_operator_topology_basis:
   768   fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
   769   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   770   shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
   771 proof -
   772   have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
   773     by (rule product_topology_basis'[OF assms])
   774   moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
   775                 = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
   776     by auto
   777   ultimately show ?thesis
   778     unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
   779 qed
   780 
   781 lemma strong_operator_topology_continuous_evaluation:
   782   "continuous_map strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
   783 proof -
   784   have "continuous_map strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
   785     unfolding strong_operator_topology_def apply (rule continuous_map_pullback)
   786     using continuous_on_product_coordinates by fastforce
   787   then show ?thesis unfolding comp_def by simp
   788 qed
   789 
   790 lemma continuous_on_strong_operator_topo_iff_coordinatewise:
   791   "continuous_map T strong_operator_topology f
   792     \<longleftrightarrow> (\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x))"
   793 proof (auto)
   794   fix x::"'b"
   795   assume "continuous_map T strong_operator_topology f"
   796   with continuous_map_compose[OF this strong_operator_topology_continuous_evaluation]
   797   have "continuous_map T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
   798     by simp
   799   then show "continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
   800     unfolding comp_def by auto
   801 next
   802   assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
   803   have "continuous_map T euclidean (blinfun_apply o f)"
   804     unfolding euclidean_product_topology
   805     apply (rule continuous_map_coordinatewise_then_product, auto)
   806     using * unfolding comp_def by auto
   807   show "continuous_map T strong_operator_topology f"
   808     unfolding strong_operator_topology_def
   809     apply (rule continuous_map_pullback')
   810     by (auto simp add: \<open>continuous_map T euclidean (blinfun_apply o f)\<close>)
   811 qed
   812 
   813 lemma strong_operator_topology_weaker_than_euclidean:
   814   "continuous_map euclidean strong_operator_topology (\<lambda>f. f)"
   815   by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
   816     auto simp add: linear_continuous_on)
   817 
   818 
   819 
   820 end