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