src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
author immler
Tue Dec 22 21:58:27 2015 +0100 (2015-12-22)
changeset 61915 e9812a95d108
child 61916 7950ae6d3266
permissions -rw-r--r--
theory for type of bounded linear functions; differentiation under the integral sign
     1 (*  Title:      HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
     2     Author:     Fabian Immler, TU M√ľnchen
     3 *)
     4 
     5 section {* Bounded Linear Function *}
     6 
     7 theory Bounded_Linear_Function
     8 imports
     9   Topology_Euclidean_Space
    10   Operator_Norm
    11 begin
    12 
    13 subsection {* Intro rules for @{term bounded_linear} *}
    14 
    15 named_theorems bounded_linear_intros
    16 
    17 lemma onorm_inner_left:
    18   assumes "bounded_linear r"
    19   shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
    20 proof (rule onorm_bound)
    21   fix x
    22   have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
    23     by (simp add: Cauchy_Schwarz_ineq2)
    24   also have "\<dots> \<le> onorm r * norm x * norm f"
    25     by (intro mult_right_mono onorm assms norm_ge_zero)
    26   finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
    27     by (simp add: ac_simps)
    28 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
    29 
    30 lemma onorm_inner_right:
    31   assumes "bounded_linear r"
    32   shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
    33   apply (subst inner_commute)
    34   apply (rule onorm_inner_left[OF assms, THEN order_trans])
    35   apply simp
    36   done
    37 
    38 lemmas [bounded_linear_intros] =
    39   bounded_linear_zero
    40   bounded_linear_add
    41   bounded_linear_const_mult
    42   bounded_linear_mult_const
    43   bounded_linear_scaleR_const
    44   bounded_linear_const_scaleR
    45   bounded_linear_ident
    46   bounded_linear_setsum
    47   bounded_linear_Pair
    48   bounded_linear_sub
    49   bounded_linear_fst_comp
    50   bounded_linear_snd_comp
    51   bounded_linear_inner_left_comp
    52   bounded_linear_inner_right_comp
    53 
    54 
    55 subsection \<open>declaration of derivative/continuous/tendsto introduction rules for bounded linear functions\<close>
    56 
    57 attribute_setup bounded_linear =
    58   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
    59     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
    60       [
    61         (@{thm bounded_linear.has_derivative}, "Deriv.derivative_intros"),
    62         (@{thm bounded_linear.tendsto}, "Topological_Spaces.tendsto_intros"),
    63         (@{thm bounded_linear.continuous}, "Topological_Spaces.continuous_intros"),
    64         (@{thm bounded_linear.continuous_on}, "Topological_Spaces.continuous_intros"),
    65         (@{thm bounded_linear.uniformly_continuous_on}, "Topological_Spaces.continuous_intros"),
    66         (@{thm bounded_linear_compose}, "Bounded_Linear_Function.bounded_linear_intros")
    67       ]))\<close>
    68 
    69 attribute_setup bounded_bilinear =
    70   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
    71     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
    72       [
    73         (@{thm bounded_bilinear.FDERIV}, "Deriv.derivative_intros"),
    74         (@{thm bounded_bilinear.tendsto}, "Topological_Spaces.tendsto_intros"),
    75         (@{thm bounded_bilinear.continuous}, "Topological_Spaces.continuous_intros"),
    76         (@{thm bounded_bilinear.continuous_on}, "Topological_Spaces.continuous_intros"),
    77         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
    78           "Bounded_Linear_Function.bounded_linear_intros"),
    79         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
    80           "Bounded_Linear_Function.bounded_linear_intros"),
    81         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
    82           "Topological_Spaces.continuous_intros"),
    83         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
    84           "Topological_Spaces.continuous_intros")
    85       ]))\<close>
    86 
    87 
    88 subsection \<open>type of bounded linear functions\<close>
    89 
    90 typedef (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
    91   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
    92   morphisms blinfun_apply Blinfun
    93   by (blast intro: bounded_linear_intros)
    94 
    95 declare [[coercion
    96     "blinfun_apply :: ('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'b"]]
    97 
    98 lemma bounded_linear_blinfun_apply[bounded_linear_intros]:
    99   "bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. blinfun_apply f (g x))"
   100   by (metis blinfun_apply mem_Collect_eq bounded_linear_compose)
   101 
   102 setup_lifting type_definition_blinfun
   103 
   104 lemma blinfun_eqI: "(\<And>i. blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
   105   by transfer auto
   106 
   107 lemma bounded_linear_Blinfun_apply: "bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f"
   108   by (auto simp: Blinfun_inverse)
   109 
   110 
   111 subsection \<open>type class instantiations\<close>
   112 
   113 instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
   114 begin
   115 
   116 lift_definition norm_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real" is onorm .
   117 
   118 lift_definition minus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   119   is "\<lambda>f g x. f x - g x"
   120   by (rule bounded_linear_sub)
   121 
   122 definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
   123   where "dist_blinfun a b = norm (a - b)"
   124 
   125 definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
   126   where "open_blinfun S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   127 
   128 lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
   129   by (rule bounded_linear_minus)
   130 
   131 lift_definition zero_blinfun :: "'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>x. 0"
   132   by (rule bounded_linear_zero)
   133 
   134 lift_definition plus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   135   is "\<lambda>f g x. f x + g x"
   136   by (metis bounded_linear_add)
   137 
   138 lift_definition 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"
   139   by (metis bounded_linear_compose bounded_linear_scaleR_right)
   140 
   141 definition sgn_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   142   where "sgn_blinfun x = scaleR (inverse (norm x)) x"
   143 
   144 instance
   145   apply standard
   146   unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
   147   apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
   148   done
   149 
   150 end
   151 
   152 lemma norm_blinfun_eqI:
   153   assumes "n \<le> norm (blinfun_apply f x) / norm x"
   154   assumes "\<And>x. norm (blinfun_apply f x) \<le> n * norm x"
   155   assumes "0 \<le> n"
   156   shows "norm f = n"
   157   by (auto simp: norm_blinfun_def
   158     intro!: antisym onorm_bound assms order_trans[OF _ le_onorm]
   159     bounded_linear_intros)
   160 
   161 lemma norm_blinfun: "norm (blinfun_apply f x) \<le> norm f * norm x"
   162   by transfer (rule onorm)
   163 
   164 lemma norm_blinfun_bound: "0 \<le> b \<Longrightarrow> (\<And>x. norm (blinfun_apply f x) \<le> b * norm x) \<Longrightarrow> norm f \<le> b"
   165   by transfer (rule onorm_bound)
   166 
   167 lemma bounded_bilinear_blinfun_apply[bounded_bilinear]: "bounded_bilinear blinfun_apply"
   168 proof
   169   fix f g::"'a \<Rightarrow>\<^sub>L 'b" and a b::'a and r::real
   170   show "(f + g) a = f a + g a" "(r *\<^sub>R f) a = r *\<^sub>R f a"
   171     by (transfer, simp)+
   172   interpret bounded_linear f for f::"'a \<Rightarrow>\<^sub>L 'b"
   173     by (auto intro!: bounded_linear_intros)
   174   show "f (a + b) = f a + f b" "f (r *\<^sub>R a) = r *\<^sub>R f a"
   175     by (simp_all add: add scaleR)
   176   show "\<exists>K. \<forall>a b. norm (blinfun_apply a b) \<le> norm a * norm b * K"
   177     by (auto intro!: exI[where x=1] norm_blinfun)
   178 qed
   179 
   180 interpretation blinfun: bounded_bilinear blinfun_apply
   181   by (rule bounded_bilinear_blinfun_apply)
   182 
   183 lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left
   184 
   185 
   186 context bounded_bilinear
   187 begin
   188 
   189 named_theorems bilinear_simps
   190 
   191 lemmas [bilinear_simps] =
   192   add_left
   193   add_right
   194   diff_left
   195   diff_right
   196   minus_left
   197   minus_right
   198   scaleR_left
   199   scaleR_right
   200   zero_left
   201   zero_right
   202   setsum_left
   203   setsum_right
   204 
   205 end
   206 
   207 
   208 instance blinfun :: (banach, banach) banach
   209 proof
   210   fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   211   assume "Cauchy X"
   212   {
   213     fix x::'a
   214     {
   215       fix x::'a
   216       assume "norm x \<le> 1"
   217       have "Cauchy (\<lambda>n. X n x)"
   218       proof (rule CauchyI)
   219         fix e::real
   220         assume "0 < e"
   221         from CauchyD[OF `Cauchy X` `0 < e`] obtain M
   222           where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
   223           by auto
   224         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
   225         proof (safe intro!: exI[where x=M])
   226           fix m n
   227           assume le: "M \<le> m" "M \<le> n"
   228           have "norm (X m x - X n x) = norm ((X m - X n) x)"
   229             by (simp add: blinfun.bilinear_simps)
   230           also have "\<dots> \<le> norm (X m - X n) * norm x"
   231              by (rule norm_blinfun)
   232           also have "\<dots> \<le> norm (X m - X n) * 1"
   233             using `norm x \<le> 1` norm_ge_zero by (rule mult_left_mono)
   234           also have "\<dots> = norm (X m - X n)" by simp
   235           also have "\<dots> < e" using le by fact
   236           finally show "norm (X m x - X n x) < e" .
   237         qed
   238       qed
   239       hence "convergent (\<lambda>n. X n x)"
   240         by (metis Cauchy_convergent_iff)
   241     } note convergent_norm1 = this
   242     def y \<equiv> "x /\<^sub>R norm x"
   243     have y: "norm y \<le> 1" and xy: "x = norm x *\<^sub>R y"
   244       by (simp_all add: y_def inverse_eq_divide)
   245     have "convergent (\<lambda>n. norm x *\<^sub>R X n y)"
   246       by (intro bounded_bilinear.convergent[OF bounded_bilinear_scaleR] convergent_const
   247         convergent_norm1 y)
   248     also have "(\<lambda>n. norm x *\<^sub>R X n y) = (\<lambda>n. X n x)"
   249       by (subst xy) (simp add: blinfun.bilinear_simps)
   250     finally have "convergent (\<lambda>n. X n x)" .
   251   }
   252   then obtain v where v: "\<And>x. (\<lambda>n. X n x) ----> v x"
   253     unfolding convergent_def
   254     by metis
   255 
   256   have "Cauchy (\<lambda>n. norm (X n))"
   257   proof (rule CauchyI)
   258     fix e::real
   259     assume "e > 0"
   260     from CauchyD[OF `Cauchy X` `0 < e`] obtain M
   261       where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
   262       by auto
   263     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
   264     proof (safe intro!: exI[where x=M])
   265       fix m n assume mn: "m \<ge> M" "n \<ge> M"
   266       have "norm (norm (X m) - norm (X n)) \<le> norm (X m - X n)"
   267         by (metis norm_triangle_ineq3 real_norm_def)
   268       also have "\<dots> < e" using mn by fact
   269       finally show "norm (norm (X m) - norm (X n)) < e" .
   270     qed
   271   qed
   272   then obtain K where K: "(\<lambda>n. norm (X n)) ----> K"
   273     unfolding Cauchy_convergent_iff convergent_def
   274     by metis
   275 
   276   have "bounded_linear v"
   277   proof
   278     fix x y and r::real
   279     from tendsto_add[OF v[of x] v [of y]] v[of "x + y", unfolded blinfun.bilinear_simps]
   280       tendsto_scaleR[OF tendsto_const[of r] v[of x]] v[of "r *\<^sub>R x", unfolded blinfun.bilinear_simps]
   281     show "v (x + y) = v x + v y" "v (r *\<^sub>R x) = r *\<^sub>R v x"
   282       by (metis (poly_guards_query) LIMSEQ_unique)+
   283     show "\<exists>K. \<forall>x. norm (v x) \<le> norm x * K"
   284     proof (safe intro!: exI[where x=K])
   285       fix x
   286       have "norm (v x) \<le> K * norm x"
   287         by (rule tendsto_le[OF _ tendsto_mult[OF K tendsto_const] tendsto_norm[OF v]])
   288           (auto simp: norm_blinfun)
   289       thus "norm (v x) \<le> norm x * K"
   290         by (simp add: ac_simps)
   291     qed
   292   qed
   293   hence Bv: "\<And>x. (\<lambda>n. X n x) ----> Blinfun v x"
   294     by (auto simp: bounded_linear_Blinfun_apply v)
   295 
   296   have "X ----> Blinfun v"
   297   proof (rule LIMSEQ_I)
   298     fix r::real assume "r > 0"
   299     def r' \<equiv> "r / 2"
   300     have "0 < r'" "r' < r" using `r > 0` by (simp_all add: r'_def)
   301     from CauchyD[OF `Cauchy X` `r' > 0`]
   302     obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
   303       by metis
   304     show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
   305     proof (safe intro!: exI[where x=M])
   306       fix n assume n: "M \<le> n"
   307       have "norm (X n - Blinfun v) \<le> r'"
   308       proof (rule norm_blinfun_bound)
   309         fix x
   310         have "eventually (\<lambda>m. m \<ge> M) sequentially"
   311           by (metis eventually_ge_at_top)
   312         hence ev_le: "eventually (\<lambda>m. norm (X n x - X m x) \<le> r' * norm x) sequentially"
   313         proof eventually_elim
   314           case (elim m)
   315           have "norm (X n x - X m x) = norm ((X n - X m) x)"
   316             by (simp add: blinfun.bilinear_simps)
   317           also have "\<dots> \<le> norm ((X n - X m)) * norm x"
   318             by (rule norm_blinfun)
   319           also have "\<dots> \<le> r' * norm x"
   320             using M[OF n elim] by (simp add: mult_right_mono)
   321           finally show ?case .
   322         qed
   323         have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) ----> norm (X n x - Blinfun v x)"
   324           by (auto intro!: tendsto_intros Bv)
   325         show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
   326           by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
   327       qed (simp add: `0 < r'` less_imp_le)
   328       thus "norm (X n - Blinfun v) < r"
   329         by (metis `r' < r` le_less_trans)
   330     qed
   331   qed
   332   thus "convergent X"
   333     by (rule convergentI)
   334 qed
   335 
   336 subsection {* On Euclidean Space *}
   337 
   338 lemma Zfun_setsum:
   339   assumes "finite s"
   340   assumes f: "\<And>i. i \<in> s \<Longrightarrow> Zfun (f i) F"
   341   shows "Zfun (\<lambda>x. setsum (\<lambda>i. f i x) s) F"
   342   using assms by induct (auto intro!: Zfun_zero Zfun_add)
   343 
   344 lemma norm_blinfun_euclidean_le:
   345   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
   346   shows "norm a \<le> setsum (\<lambda>x. norm (a x)) Basis"
   347   apply (rule norm_blinfun_bound)
   348    apply (simp add: setsum_nonneg)
   349   apply (subst euclidean_representation[symmetric, where 'a='a])
   350   apply (simp only: blinfun.bilinear_simps setsum_left_distrib)
   351   apply (rule order.trans[OF norm_setsum setsum_mono])
   352   apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
   353   done
   354 
   355 lemma tendsto_componentwise1:
   356   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::real_normed_vector"
   357     and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   358   assumes "(\<And>j. j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j) ---> a j) F)"
   359   shows "(b ---> a) F"
   360 proof -
   361   have "\<And>j. j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x j - a j)) F"
   362     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
   363   hence "Zfun (\<lambda>x. \<Sum>j\<in>Basis. norm (b x j - a j)) F"
   364     by (auto intro!: Zfun_setsum)
   365   thus ?thesis
   366     unfolding tendsto_Zfun_iff
   367     by (rule Zfun_le)
   368       (auto intro!: order_trans[OF norm_blinfun_euclidean_le] simp: blinfun.bilinear_simps)
   369 qed
   370 
   371 lift_definition
   372   blinfun_of_matrix::"('b::euclidean_space \<Rightarrow> 'a::euclidean_space \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   373   is "\<lambda>a x. \<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i"
   374   by (intro bounded_linear_intros)
   375 
   376 lemma blinfun_of_matrix_works:
   377   fixes f::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   378   shows "blinfun_of_matrix (\<lambda>i j. (f j) \<bullet> i) = f"
   379 proof (transfer, rule,  rule euclidean_eqI)
   380   fix f::"'a \<Rightarrow> 'b" and x::'a and b::'b assume "bounded_linear f" and b: "b \<in> Basis"
   381   then interpret bounded_linear f by simp
   382   have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
   383     = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
   384     using b
   385     by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: split_if intro!: setsum.cong)
   386   also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
   387     using b by (simp add: setsum.delta)
   388   also have "\<dots> = f x \<bullet> b"
   389     by (subst linear_componentwise[symmetric]) (unfold_locales, rule)
   390   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" .
   391 qed
   392 
   393 lemma blinfun_of_matrix_apply:
   394   "blinfun_of_matrix a x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)"
   395   by transfer simp
   396 
   397 lemma blinfun_of_matrix_minus: "blinfun_of_matrix x - blinfun_of_matrix y = blinfun_of_matrix (x - y)"
   398   by transfer (auto simp: algebra_simps setsum_subtractf)
   399 
   400 lemma norm_blinfun_of_matrix:
   401   "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
   402   apply (rule norm_blinfun_bound)
   403    apply (simp add: setsum_nonneg)
   404   apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
   405   apply (rule order_trans[OF norm_setsum setsum_mono])
   406   apply (rule order_trans[OF norm_setsum setsum_mono])
   407   apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm)
   408   done
   409 
   410 lemma tendsto_blinfun_of_matrix:
   411   assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n i j) ---> a i j) F"
   412   shows "((\<lambda>n. blinfun_of_matrix (b n)) ---> blinfun_of_matrix a) F"
   413 proof -
   414   have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
   415     using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
   416   hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
   417     by (auto intro!: Zfun_setsum)
   418   thus ?thesis
   419     unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
   420     by (rule Zfun_le) (auto intro!: order_trans[OF norm_blinfun_of_matrix])
   421 qed
   422 
   423 lemma tendsto_componentwise:
   424   fixes a::"'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   425     and b::"'c \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   426   shows "(\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> ((\<lambda>n. b n j \<bullet> i) ---> a j \<bullet> i) F) \<Longrightarrow> (b ---> a) F"
   427   apply (subst blinfun_of_matrix_works[of a, symmetric])
   428   apply (subst blinfun_of_matrix_works[of "b x" for x, symmetric, abs_def])
   429   by (rule tendsto_blinfun_of_matrix)
   430 
   431 lemma
   432   continuous_blinfun_componentwiseI:
   433   fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::euclidean_space"
   434   assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. (f x) j \<bullet> i)"
   435   shows "continuous F f"
   436   using assms by (auto simp: continuous_def intro!: tendsto_componentwise)
   437 
   438 lemma
   439   continuous_blinfun_componentwiseI1:
   440   fixes f:: "'b::t2_space \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'c::real_normed_vector"
   441   assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous F (\<lambda>x. f x i)"
   442   shows "continuous F f"
   443   using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
   444 
   445 lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
   446   by (auto intro!: bounded_linearI' bounded_linear_intros)
   447 
   448 lemma continuous_blinfun_matrix:
   449   fixes f:: "'b::t2_space \<Rightarrow> 'a::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
   450   assumes "continuous F f"
   451   shows "continuous F (\<lambda>x. (f x) j \<bullet> i)"
   452   by (rule bounded_linear.continuous[OF bounded_linear_blinfun_matrix assms])
   453 
   454 lemma continuous_on_blinfun_matrix:
   455   fixes f::"'a::t2_space \<Rightarrow> 'b::real_normed_vector \<Rightarrow>\<^sub>L 'c::real_inner"
   456   assumes "continuous_on S f"
   457   shows "continuous_on S (\<lambda>x. (f x) j \<bullet> i)"
   458   using assms
   459   by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)
   460 
   461 lemma mult_if_delta:
   462   "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
   463   by auto
   464 
   465 text {* TODO: generalize this and @{thm compact_lemma}?! *}
   466 lemma compact_blinfun_lemma:
   467   fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   468   assumes "bounded (range f)"
   469   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
   470     subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
   471 proof safe
   472   fix d :: "'a set"
   473   assume d: "d \<subseteq> Basis"
   474   with finite_Basis have "finite d"
   475     by (blast intro: finite_subset)
   476   from this d show "\<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists>r. subseq r \<and>
   477     (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
   478   proof (induct d)
   479     case empty
   480     then show ?case
   481       unfolding subseq_def by auto
   482   next
   483     case (insert k d)
   484     have k[intro]: "k \<in> Basis"
   485       using insert by auto
   486     have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
   487       using `bounded (range f)`
   488       by (auto intro!: bounded_linear_image bounded_linear_intros)
   489     obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
   490       and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
   491       using insert(3) using insert(4) by auto
   492     have f': "\<forall>n. f (r1 n) k \<in> (\<lambda>x. blinfun_apply x k) ` range f"
   493       by simp
   494     have "bounded (range (\<lambda>i. f (r1 i) k))"
   495       by (metis (lifting) bounded_subset f' image_subsetI s')
   496     then obtain l2 r2
   497       where r2: "subseq r2"
   498       and lr2: "((\<lambda>i. f (r1 (r2 i)) k) ---> l2) sequentially"
   499       using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"]
   500       by (auto simp: o_def)
   501     def r \<equiv> "r1 \<circ> r2"
   502     have r:"subseq r"
   503       using r1 and r2 unfolding r_def o_def subseq_def by auto
   504     moreover
   505     def l \<equiv> "blinfun_of_matrix (\<lambda>i j. if j = k then l2 \<bullet> i else l1 j \<bullet> i)::'a \<Rightarrow>\<^sub>L 'b"
   506     {
   507       fix e::real
   508       assume "e > 0"
   509       from lr1 `e > 0` have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
   510         by blast
   511       from lr2 `e > 0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
   512         by (rule tendstoD)
   513       from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
   514         by (rule eventually_subseq)
   515       have l2: "l k = l2"
   516         using insert.prems
   517         by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
   518           scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
   519       {
   520         fix i assume "i \<in> d"
   521         with insert have "i \<in> Basis" "i \<noteq> k" by auto
   522         hence l1: "l i = (l1 i)"
   523           by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
   524             scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
   525       } note l1 = this
   526       have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n)  i) (l  i) < e) sequentially"
   527         using N1' N2
   528         by eventually_elim (insert insert.prems, auto simp: r_def o_def l1 l2)
   529     }
   530     ultimately show ?case by auto
   531   qed
   532 qed
   533 
   534 lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
   535   apply (auto intro!: blinfun_eqI)
   536   apply (subst (2) euclidean_representation[symmetric, where 'a='a])
   537   apply (subst (1) euclidean_representation[symmetric, where 'a='a])
   538   apply (simp add: blinfun.bilinear_simps)
   539   done
   540 
   541 text {* TODO: generalize (via @{thm compact_cball})? *}
   542 instance blinfun :: (euclidean_space, euclidean_space) heine_borel
   543 proof
   544   fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   545   assume f: "bounded (range f)"
   546   then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"
   547     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
   548     using compact_blinfun_lemma [OF f] by blast
   549   {
   550     fix e::real
   551     let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
   552     assume "e > 0"
   553     hence "e / ?d > 0" by (simp add: DIM_positive)
   554     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
   555       by simp
   556     moreover
   557     {
   558       fix n
   559       assume n: "\<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d"
   560       have "norm (f (r n) - l) = norm (blinfun_of_matrix (\<lambda>i j. (f (r n) - l) j \<bullet> i))"
   561         unfolding blinfun_of_matrix_works ..
   562       also note norm_blinfun_of_matrix
   563       also have "(\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) <
   564         (\<Sum>i\<in>(Basis::'b set). e / real_of_nat DIM('b))"
   565       proof (rule setsum_strict_mono)
   566         fix i::'b assume i: "i \<in> Basis"
   567         have "(\<Sum>j::'a\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < (\<Sum>j::'a\<in>Basis. e / ?d)"
   568         proof (rule setsum_strict_mono)
   569           fix j::'a assume j: "j \<in> Basis"
   570           have "\<bar>(f (r n) - l) j \<bullet> i\<bar> \<le> norm ((f (r n) - l) j)"
   571             by (simp add: Basis_le_norm i)
   572           also have "\<dots> < e / ?d"
   573             using n i j by (auto simp: dist_norm blinfun.bilinear_simps)
   574           finally show "\<bar>(f (r n) - l) j \<bullet> i\<bar> < e / ?d" by simp
   575         qed simp_all
   576         also have "\<dots> \<le> e / real_of_nat DIM('b)"
   577           by simp
   578         finally show "(\<Sum>j\<in>Basis. \<bar>(f (r n) - l) j \<bullet> i\<bar>) < e / real_of_nat DIM('b)"
   579           by simp
   580       qed simp_all
   581       also have "\<dots> \<le> e" by simp
   582       finally have "dist (f (r n)) l < e"
   583         by (auto simp: dist_norm)
   584     }
   585     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
   586       using eventually_elim2 by force
   587   }
   588   then have *: "((f \<circ> r) ---> l) sequentially"
   589     unfolding o_def tendsto_iff by simp
   590   with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   591     by auto
   592 qed
   593 
   594 
   595 subsection \<open>concrete bounded linear functions\<close>
   596 
   597 lemma bounded_linear_bounded_bilinear_blinfun_applyI: --"TODO: transfer rule!"
   598   assumes n: "bounded_bilinear (\<lambda>i x. (blinfun_apply (f x) i))"
   599   shows "bounded_linear f"
   600 proof (unfold_locales, safe intro!: blinfun_eqI)
   601   fix i
   602   interpret bounded_bilinear "\<lambda>i x. f x i" by fact
   603   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
   604     by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)
   605   from _ nonneg_bounded show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
   606     by (rule ex_reg) (auto intro!: onorm_bound simp: norm_blinfun.rep_eq assms ac_simps)
   607 qed
   608 
   609 context bounded_bilinear
   610 begin
   611 
   612 lift_definition prod_left::"'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'c" is "(\<lambda>b a. prod a b)"
   613   by (rule bounded_linear_left)
   614 declare prod_left.rep_eq[simp]
   615 
   616 lemma bounded_linear_prod_left[bounded_linear]: "bounded_linear prod_left"
   617   by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_axioms)
   618 
   619 lift_definition prod_right::"'a \<Rightarrow> 'b \<Rightarrow>\<^sub>L 'c" is "(\<lambda>a b. prod a b)"
   620   by (rule bounded_linear_right)
   621 declare prod_right.rep_eq[simp]
   622 
   623 lemma bounded_linear_prod_right[bounded_linear]: "bounded_linear prod_right"
   624   by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: flip)
   625 
   626 end
   627 
   628 lift_definition id_blinfun::"'a::real_normed_vector \<Rightarrow>\<^sub>L 'a" is "\<lambda>x. x"
   629   by (rule bounded_linear_ident)
   630 
   631 lemmas blinfun_apply_id_blinfun[simp] = id_blinfun.rep_eq
   632 
   633 lemma norm_blinfun_id[simp]:
   634   "norm (id_blinfun::'a::{real_normed_vector, perfect_space} \<Rightarrow>\<^sub>L 'a) = 1"
   635   by transfer (auto simp: onorm_id)
   636 
   637 lemma norm_blinfun_id_le:
   638   "norm (id_blinfun::'a::real_normed_vector \<Rightarrow>\<^sub>L 'a) \<le> 1"
   639   by transfer (auto simp: onorm_id_le)
   640 
   641 
   642 lift_definition fst_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'a" is fst
   643   by (rule bounded_linear_fst)
   644 
   645 lemma blinfun_apply_fst_blinfun[simp]: "blinfun_apply fst_blinfun = fst"
   646   by transfer (rule refl)
   647 
   648 
   649 lift_definition snd_blinfun::"('a::real_normed_vector \<times> 'b::real_normed_vector) \<Rightarrow>\<^sub>L 'b" is snd
   650   by (rule bounded_linear_snd)
   651 
   652 lemma blinfun_apply_snd_blinfun[simp]: "blinfun_apply snd_blinfun = snd"
   653   by transfer (rule refl)
   654 
   655 
   656 lift_definition blinfun_compose::
   657   "'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
   658     'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
   659     'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "op o"
   660   parametric comp_transfer
   661   unfolding o_def
   662   by (rule bounded_linear_compose)
   663 
   664 lemma blinfun_apply_blinfun_compose[simp]: "(a o\<^sub>L b) c = a (b c)"
   665   by (simp add: blinfun_compose.rep_eq)
   666 
   667 lemma norm_blinfun_compose:
   668   "norm (f o\<^sub>L g) \<le> norm f * norm g"
   669   by transfer (rule onorm_compose)
   670 
   671 lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear op o\<^sub>L"
   672   by unfold_locales
   673     (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
   674 
   675 
   676 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
   677   by (rule bounded_linear_inner_right)
   678 declare blinfun_inner_right.rep_eq[simp]
   679 
   680 lemma bounded_linear_blinfun_inner_right[bounded_linear]: "bounded_linear blinfun_inner_right"
   681   by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
   682     (auto simp: bounded_bilinear.flip[OF bounded_bilinear_inner])
   683 
   684 
   685 lift_definition blinfun_inner_left::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "\<lambda>x y. y \<bullet> x"
   686   by (rule bounded_linear_inner_left)
   687 declare blinfun_inner_left.rep_eq[simp]
   688 
   689 lemma bounded_linear_blinfun_inner_left[bounded_linear]: "bounded_linear blinfun_inner_left"
   690   by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_inner)
   691 
   692 
   693 lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
   694   by (rule bounded_linear_scaleR_right)
   695 declare blinfun_scaleR_right.rep_eq[simp]
   696 
   697 lemma bounded_linear_blinfun_scaleR_right[bounded_linear]: "bounded_linear blinfun_scaleR_right"
   698   by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
   699     (auto simp: bounded_bilinear.flip[OF bounded_bilinear_scaleR])
   700 
   701 
   702 lift_definition blinfun_scaleR_left::"'a::real_normed_vector \<Rightarrow> real \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y *\<^sub>R x"
   703   by (rule bounded_linear_scaleR_left)
   704 lemmas [simp] = blinfun_scaleR_left.rep_eq
   705 
   706 lemma bounded_linear_blinfun_scaleR_left[bounded_linear]: "bounded_linear blinfun_scaleR_left"
   707   by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_scaleR)
   708 
   709 
   710 lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
   711   by (rule bounded_linear_mult_right)
   712 declare blinfun_mult_right.rep_eq[simp]
   713 
   714 lemma bounded_linear_blinfun_mult_right[bounded_linear]: "bounded_linear blinfun_mult_right"
   715   by (rule bounded_linear_bounded_bilinear_blinfun_applyI)
   716     (auto simp: bounded_bilinear.flip[OF bounded_bilinear_mult])
   717 
   718 
   719 lift_definition blinfun_mult_left::"'a::real_normed_algebra \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a" is "\<lambda>x y. y * x"
   720   by (rule bounded_linear_mult_left)
   721 lemmas [simp] = blinfun_mult_left.rep_eq
   722 
   723 lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
   724   by (rule bounded_linear_bounded_bilinear_blinfun_applyI) (auto simp: bounded_bilinear_mult)
   725 
   726 end