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