src/HOL/Analysis/Operator_Norm.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69607 7cd977863194
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Operator_Norm.thy
huffman@36581
     2
    Author:     Amine Chaieb, University of Cambridge
huffman@56223
     3
    Author:     Brian Huffman
huffman@36581
     4
*)
huffman@36581
     5
nipkow@69518
     6
section \<open>Operator Norm\<close>
huffman@36581
     7
huffman@36581
     8
theory Operator_Norm
huffman@56319
     9
imports Complex_Main
huffman@36581
    10
begin
huffman@36581
    11
wenzelm@61808
    12
text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
huffman@56223
    13
wenzelm@69607
    14
text%important \<open>%whitespace\<close>
nipkow@69518
    15
definition%important
nipkow@69518
    16
onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" where
nipkow@69518
    17
"onorm f = (SUP x. norm (f x) / norm x)"
huffman@56223
    18
nipkow@69518
    19
proposition onorm_bound:
huffman@56223
    20
  assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
huffman@56223
    21
  shows "onorm f \<le> b"
huffman@56223
    22
  unfolding onorm_def
nipkow@69518
    23
proof (rule cSUP_least)
huffman@56223
    24
  fix x
huffman@56223
    25
  show "norm (f x) / norm x \<le> b"
huffman@56223
    26
    using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
huffman@56223
    27
qed simp
huffman@56223
    28
wenzelm@60420
    29
text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>
huffman@36581
    30
nipkow@69518
    31
lemma onorm_le:
huffman@56223
    32
  fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
huffman@56223
    33
  assumes "\<And>x. norm (f x) \<le> b * norm x"
huffman@56223
    34
  shows "onorm f \<le> b"
nipkow@69518
    35
proof (rule onorm_bound [OF _ assms])
huffman@56223
    36
  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
huffman@56223
    37
  then obtain a :: 'a where "a \<noteq> 0" by fast
huffman@56223
    38
  have "0 \<le> b * norm a"
huffman@56223
    39
    by (rule order_trans [OF norm_ge_zero assms])
wenzelm@60420
    40
  with \<open>a \<noteq> 0\<close> show "0 \<le> b"
huffman@56223
    41
    by (simp add: zero_le_mult_iff)
huffman@56223
    42
qed
huffman@56223
    43
nipkow@69518
    44
lemma le_onorm:
huffman@56223
    45
  assumes "bounded_linear f"
huffman@56223
    46
  shows "norm (f x) / norm x \<le> onorm f"
nipkow@69518
    47
proof -
huffman@56223
    48
  interpret f: bounded_linear f by fact
huffman@56223
    49
  obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
huffman@56223
    50
    using f.nonneg_bounded by auto
huffman@56223
    51
  then have "\<forall>x. norm (f x) / norm x \<le> b"
huffman@56223
    52
    by (clarify, case_tac "x = 0",
haftmann@57512
    53
      simp_all add: f.zero pos_divide_le_eq mult.commute)
huffman@56223
    54
  then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))"
huffman@56223
    55
    unfolding bdd_above_def by fast
huffman@56223
    56
  with UNIV_I show ?thesis
huffman@56223
    57
    unfolding onorm_def by (rule cSUP_upper)
wenzelm@53253
    58
qed
huffman@36581
    59
nipkow@69518
    60
lemma onorm:
huffman@56223
    61
  assumes "bounded_linear f"
wenzelm@53253
    62
  shows "norm (f x) \<le> onorm f * norm x"
nipkow@69518
    63
proof -
huffman@56223
    64
  interpret f: bounded_linear f by fact
huffman@56223
    65
  show ?thesis
huffman@56223
    66
  proof (cases)
huffman@56223
    67
    assume "x = 0"
huffman@56223
    68
    then show ?thesis by (simp add: f.zero)
huffman@56223
    69
  next
huffman@56223
    70
    assume "x \<noteq> 0"
huffman@56223
    71
    have "norm (f x) / norm x \<le> onorm f"
huffman@56223
    72
      by (rule le_onorm [OF assms])
huffman@56223
    73
    then show "norm (f x) \<le> onorm f * norm x"
wenzelm@60420
    74
      by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>)
huffman@56223
    75
  qed
huffman@36581
    76
qed
huffman@36581
    77
nipkow@69518
    78
lemma onorm_pos_le:
huffman@56223
    79
  assumes f: "bounded_linear f"
wenzelm@53253
    80
  shows "0 \<le> onorm f"
huffman@56223
    81
  using le_onorm [OF f, where x=0] by simp
huffman@56223
    82
nipkow@69518
    83
lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
huffman@56223
    84
proof (rule order_antisym)
huffman@56223
    85
  show "onorm (\<lambda>x. 0) \<le> 0"
huffman@56223
    86
    by (simp add: onorm_bound)
huffman@56223
    87
  show "0 \<le> onorm (\<lambda>x. 0)"
huffman@56223
    88
    using bounded_linear_zero by (rule onorm_pos_le)
huffman@56223
    89
qed
huffman@36581
    90
nipkow@69518
    91
lemma onorm_eq_0:
huffman@56223
    92
  assumes f: "bounded_linear f"
huffman@36581
    93
  shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
huffman@56223
    94
  using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
huffman@36581
    95
nipkow@69518
    96
lemma onorm_pos_lt:
huffman@56223
    97
  assumes f: "bounded_linear f"
wenzelm@53688
    98
  shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
huffman@56223
    99
  by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
huffman@36581
   100
nipkow@69518
   101
lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
immler@61915
   102
  by (rule onorm_bound) simp_all
immler@61915
   103
nipkow@69518
   104
lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
immler@61915
   105
proof (rule antisym[OF onorm_id_le])
immler@61915
   106
  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
immler@61915
   107
  then obtain x :: 'a where "x \<noteq> 0" by fast
immler@61915
   108
  hence "1 \<le> norm x / norm x"
immler@61915
   109
    by simp
immler@61915
   110
  also have "\<dots> \<le> onorm (\<lambda>x::'a. x)"
immler@61915
   111
    by (rule le_onorm) (rule bounded_linear_ident)
immler@61915
   112
  finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
immler@61915
   113
qed
immler@61915
   114
nipkow@69518
   115
lemma onorm_compose:
huffman@56223
   116
  assumes f: "bounded_linear f"
huffman@56223
   117
  assumes g: "bounded_linear g"
wenzelm@53688
   118
  shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
nipkow@69518
   119
proof (rule onorm_bound)
huffman@56223
   120
  show "0 \<le> onorm f * onorm g"
huffman@56223
   121
    by (intro mult_nonneg_nonneg onorm_pos_le f g)
huffman@56223
   122
next
huffman@56223
   123
  fix x
huffman@56223
   124
  have "norm (f (g x)) \<le> onorm f * norm (g x)"
huffman@56223
   125
    by (rule onorm [OF f])
huffman@56223
   126
  also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)"
huffman@56223
   127
    by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
huffman@56223
   128
  finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x"
haftmann@57512
   129
    by (simp add: mult.assoc)
huffman@56223
   130
qed
huffman@36581
   131
nipkow@69518
   132
lemma onorm_scaleR_lemma:
huffman@56223
   133
  assumes f: "bounded_linear f"
huffman@56223
   134
  shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   135
proof (rule onorm_bound)
huffman@56223
   136
  show "0 \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   137
    by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
huffman@56223
   138
next
huffman@56223
   139
  fix x
huffman@56223
   140
  have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)"
huffman@56223
   141
    by (intro mult_left_mono onorm abs_ge_zero f)
huffman@56223
   142
  then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x"
haftmann@57512
   143
    by (simp only: norm_scaleR mult.assoc)
huffman@56223
   144
qed
huffman@56223
   145
nipkow@69518
   146
lemma onorm_scaleR:
huffman@56223
   147
  assumes f: "bounded_linear f"
huffman@56223
   148
  shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
nipkow@69518
   149
proof (cases "r = 0")
huffman@56223
   150
  assume "r \<noteq> 0"
huffman@56223
   151
  show ?thesis
huffman@56223
   152
  proof (rule order_antisym)
huffman@56223
   153
    show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   154
      using f by (rule onorm_scaleR_lemma)
huffman@56223
   155
  next
huffman@56223
   156
    have "bounded_linear (\<lambda>x. r *\<^sub>R f x)"
huffman@56223
   157
      using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
huffman@56223
   158
    then have "onorm (\<lambda>x. inverse r *\<^sub>R r *\<^sub>R f x) \<le> \<bar>inverse r\<bar> * onorm (\<lambda>x. r *\<^sub>R f x)"
huffman@56223
   159
      by (rule onorm_scaleR_lemma)
wenzelm@60420
   160
    with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
haftmann@57512
   161
      by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
huffman@56223
   162
  qed
huffman@56223
   163
qed (simp add: onorm_zero)
huffman@36581
   164
nipkow@69518
   165
lemma onorm_scaleR_left_lemma:
immler@61915
   166
  assumes r: "bounded_linear r"
immler@61915
   167
  shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
immler@61915
   168
proof (rule onorm_bound)
immler@61915
   169
  fix x
immler@61915
   170
  have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
immler@61915
   171
    by simp
immler@61915
   172
  also have "\<dots> \<le> onorm r * norm x * norm f"
immler@61915
   173
    by (intro mult_right_mono onorm r norm_ge_zero)
immler@61915
   174
  finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x"
immler@61915
   175
    by (simp add: ac_simps)
immler@61915
   176
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
immler@61915
   177
nipkow@69518
   178
lemma onorm_scaleR_left:
immler@61915
   179
  assumes f: "bounded_linear r"
immler@61915
   180
  shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
nipkow@69518
   181
proof (cases "f = 0")
immler@61915
   182
  assume "f \<noteq> 0"
immler@61915
   183
  show ?thesis
immler@61915
   184
  proof (rule order_antisym)
immler@61915
   185
    show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
immler@61915
   186
      using f by (rule onorm_scaleR_left_lemma)
immler@61915
   187
  next
immler@61915
   188
    have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)"
immler@61915
   189
      by (metis bounded_linear_scaleR_const f)
immler@61915
   190
    have "bounded_linear (\<lambda>x. r x * norm f)"
immler@61915
   191
      by (metis bounded_linear_mult_const f)
immler@61915
   192
    from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
immler@61915
   193
    have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
wenzelm@61975
   194
      using \<open>f \<noteq> 0\<close>
immler@61915
   195
      by (simp add: inverse_eq_divide)
immler@61915
   196
    also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
immler@61915
   197
      by (rule onorm_bound)
immler@61915
   198
        (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
immler@61915
   199
    finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
wenzelm@61975
   200
      using \<open>f \<noteq> 0\<close>
immler@61915
   201
      by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
immler@61915
   202
  qed
immler@61915
   203
qed (simp add: onorm_zero)
immler@61915
   204
nipkow@69518
   205
lemma onorm_neg:
huffman@36581
   206
  shows "onorm (\<lambda>x. - f x) = onorm f"
huffman@56223
   207
  unfolding onorm_def by simp
huffman@36581
   208
nipkow@69518
   209
lemma onorm_triangle:
huffman@56223
   210
  assumes f: "bounded_linear f"
huffman@56223
   211
  assumes g: "bounded_linear g"
wenzelm@53253
   212
  shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
nipkow@69518
   213
proof (rule onorm_bound)
huffman@56223
   214
  show "0 \<le> onorm f + onorm g"
huffman@56223
   215
    by (intro add_nonneg_nonneg onorm_pos_le f g)
huffman@56223
   216
next
huffman@56223
   217
  fix x
huffman@56223
   218
  have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
huffman@56223
   219
    by (rule norm_triangle_ineq)
huffman@56223
   220
  also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x"
huffman@56223
   221
    by (intro add_mono onorm f g)
huffman@56223
   222
  finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x"
huffman@56223
   223
    by (simp only: distrib_right)
huffman@56223
   224
qed
huffman@36581
   225
nipkow@69518
   226
lemma onorm_triangle_le:
huffman@56223
   227
  assumes "bounded_linear f"
huffman@56223
   228
  assumes "bounded_linear g"
huffman@56223
   229
  assumes "onorm f + onorm g \<le> e"
wenzelm@53688
   230
  shows "onorm (\<lambda>x. f x + g x) \<le> e"
nipkow@69518
   231
  using assms by (rule onorm_triangle [THEN order_trans])
huffman@36581
   232
nipkow@69518
   233
lemma onorm_triangle_lt:
huffman@56223
   234
  assumes "bounded_linear f"
huffman@56223
   235
  assumes "bounded_linear g"
huffman@56223
   236
  assumes "onorm f + onorm g < e"
wenzelm@53688
   237
  shows "onorm (\<lambda>x. f x + g x) < e"
huffman@56223
   238
  using assms by (rule onorm_triangle [THEN order_le_less_trans])
huffman@36581
   239
nipkow@69518
   240
lemma onorm_sum:
immler@67685
   241
  assumes "finite S"
immler@67685
   242
  assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
immler@67685
   243
  shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
nipkow@69518
   244
  using assms
nipkow@69518
   245
  by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
immler@67685
   246
immler@67685
   247
lemmas onorm_sum_le = onorm_sum[THEN order_trans]
immler@67685
   248
huffman@36581
   249
end