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
```