src/HOL/Multivariate_Analysis/Operator_Norm.thy
author huffman
Wed Mar 19 20:50:24 2014 -0700 (2014-03-19)
changeset 56223 7696903b9e61
parent 54263 c4159fe6fa46
child 56319 3bc95e0fa651
permissions -rw-r--r--
generalize theory of operator norms to work with class real_normed_vector
wenzelm@41959
     1
(*  Title:      HOL/Multivariate_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
huffman@36581
     6
header {* Operator Norm *}
huffman@36581
     7
huffman@36581
     8
theory Operator_Norm
huffman@44133
     9
imports Linear_Algebra
huffman@36581
    10
begin
huffman@36581
    11
huffman@56223
    12
text {* This formulation yields zero if @{text 'a} is the trivial vector space. *}
huffman@56223
    13
huffman@56223
    14
definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real"
huffman@56223
    15
  where "onorm f = (SUP x. norm (f x) / norm x)"
huffman@56223
    16
huffman@56223
    17
lemma onorm_bound:
huffman@56223
    18
  assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
huffman@56223
    19
  shows "onorm f \<le> b"
huffman@56223
    20
  unfolding onorm_def
huffman@56223
    21
proof (rule cSUP_least)
huffman@56223
    22
  fix x
huffman@56223
    23
  show "norm (f x) / norm x \<le> b"
huffman@56223
    24
    using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
huffman@56223
    25
qed simp
huffman@56223
    26
huffman@56223
    27
text {* In non-trivial vector spaces, the first assumption is redundant. *}
huffman@36581
    28
huffman@56223
    29
lemma onorm_le:
huffman@56223
    30
  fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
huffman@56223
    31
  assumes "\<And>x. norm (f x) \<le> b * norm x"
huffman@56223
    32
  shows "onorm f \<le> b"
huffman@56223
    33
proof (rule onorm_bound [OF _ assms])
huffman@56223
    34
  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
huffman@56223
    35
  then obtain a :: 'a where "a \<noteq> 0" by fast
huffman@56223
    36
  have "0 \<le> b * norm a"
huffman@56223
    37
    by (rule order_trans [OF norm_ge_zero assms])
huffman@56223
    38
  with `a \<noteq> 0` show "0 \<le> b"
huffman@56223
    39
    by (simp add: zero_le_mult_iff)
huffman@56223
    40
qed
huffman@56223
    41
huffman@56223
    42
lemma le_onorm:
huffman@56223
    43
  assumes "bounded_linear f"
huffman@56223
    44
  shows "norm (f x) / norm x \<le> onorm f"
huffman@56223
    45
proof -
huffman@56223
    46
  interpret f: bounded_linear f by fact
huffman@56223
    47
  obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
huffman@56223
    48
    using f.nonneg_bounded by auto
huffman@56223
    49
  then have "\<forall>x. norm (f x) / norm x \<le> b"
huffman@56223
    50
    by (clarify, case_tac "x = 0",
huffman@56223
    51
      simp_all add: f.zero pos_divide_le_eq mult_commute)
huffman@56223
    52
  then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))"
huffman@56223
    53
    unfolding bdd_above_def by fast
huffman@56223
    54
  with UNIV_I show ?thesis
huffman@56223
    55
    unfolding onorm_def by (rule cSUP_upper)
wenzelm@53253
    56
qed
huffman@36581
    57
huffman@36581
    58
lemma onorm:
huffman@56223
    59
  assumes "bounded_linear f"
wenzelm@53253
    60
  shows "norm (f x) \<le> onorm f * norm x"
wenzelm@53253
    61
proof -
huffman@56223
    62
  interpret f: bounded_linear f by fact
huffman@56223
    63
  show ?thesis
huffman@56223
    64
  proof (cases)
huffman@56223
    65
    assume "x = 0"
huffman@56223
    66
    then show ?thesis by (simp add: f.zero)
huffman@56223
    67
  next
huffman@56223
    68
    assume "x \<noteq> 0"
huffman@56223
    69
    have "norm (f x) / norm x \<le> onorm f"
huffman@56223
    70
      by (rule le_onorm [OF assms])
huffman@56223
    71
    then show "norm (f x) \<le> onorm f * norm x"
huffman@56223
    72
      by (simp add: pos_divide_le_eq `x \<noteq> 0`)
huffman@56223
    73
  qed
huffman@36581
    74
qed
huffman@36581
    75
wenzelm@53253
    76
lemma onorm_pos_le:
huffman@56223
    77
  assumes f: "bounded_linear f"
wenzelm@53253
    78
  shows "0 \<le> onorm f"
huffman@56223
    79
  using le_onorm [OF f, where x=0] by simp
huffman@56223
    80
huffman@56223
    81
lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
huffman@56223
    82
proof (rule order_antisym)
huffman@56223
    83
  show "onorm (\<lambda>x. 0) \<le> 0"
huffman@56223
    84
    by (simp add: onorm_bound)
huffman@56223
    85
  show "0 \<le> onorm (\<lambda>x. 0)"
huffman@56223
    86
    using bounded_linear_zero by (rule onorm_pos_le)
huffman@56223
    87
qed
huffman@36581
    88
wenzelm@53253
    89
lemma onorm_eq_0:
huffman@56223
    90
  assumes f: "bounded_linear f"
huffman@36581
    91
  shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
huffman@56223
    92
  using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
huffman@36581
    93
wenzelm@53253
    94
lemma onorm_pos_lt:
huffman@56223
    95
  assumes f: "bounded_linear f"
wenzelm@53688
    96
  shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
huffman@56223
    97
  by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
huffman@36581
    98
huffman@36581
    99
lemma onorm_compose:
huffman@56223
   100
  assumes f: "bounded_linear f"
huffman@56223
   101
  assumes g: "bounded_linear g"
wenzelm@53688
   102
  shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
huffman@56223
   103
proof (rule onorm_bound)
huffman@56223
   104
  show "0 \<le> onorm f * onorm g"
huffman@56223
   105
    by (intro mult_nonneg_nonneg onorm_pos_le f g)
huffman@56223
   106
next
huffman@56223
   107
  fix x
huffman@56223
   108
  have "norm (f (g x)) \<le> onorm f * norm (g x)"
huffman@56223
   109
    by (rule onorm [OF f])
huffman@56223
   110
  also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)"
huffman@56223
   111
    by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
huffman@56223
   112
  finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x"
huffman@56223
   113
    by (simp add: mult_assoc)
huffman@56223
   114
qed
huffman@36581
   115
huffman@56223
   116
lemma onorm_scaleR_lemma:
huffman@56223
   117
  assumes f: "bounded_linear f"
huffman@56223
   118
  shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   119
proof (rule onorm_bound)
huffman@56223
   120
  show "0 \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   121
    by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
huffman@56223
   122
next
huffman@56223
   123
  fix x
huffman@56223
   124
  have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)"
huffman@56223
   125
    by (intro mult_left_mono onorm abs_ge_zero f)
huffman@56223
   126
  then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x"
huffman@56223
   127
    by (simp only: norm_scaleR mult_assoc)
huffman@56223
   128
qed
huffman@56223
   129
huffman@56223
   130
lemma onorm_scaleR:
huffman@56223
   131
  assumes f: "bounded_linear f"
huffman@56223
   132
  shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
huffman@56223
   133
proof (cases "r = 0")
huffman@56223
   134
  assume "r \<noteq> 0"
huffman@56223
   135
  show ?thesis
huffman@56223
   136
  proof (rule order_antisym)
huffman@56223
   137
    show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
huffman@56223
   138
      using f by (rule onorm_scaleR_lemma)
huffman@56223
   139
  next
huffman@56223
   140
    have "bounded_linear (\<lambda>x. r *\<^sub>R f x)"
huffman@56223
   141
      using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
huffman@56223
   142
    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
   143
      by (rule onorm_scaleR_lemma)
huffman@56223
   144
    with `r \<noteq> 0` show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
huffman@56223
   145
      by (simp add: inverse_eq_divide pos_le_divide_eq mult_commute)
huffman@56223
   146
  qed
huffman@56223
   147
qed (simp add: onorm_zero)
huffman@36581
   148
wenzelm@53253
   149
lemma onorm_neg:
huffman@36581
   150
  shows "onorm (\<lambda>x. - f x) = onorm f"
huffman@56223
   151
  unfolding onorm_def by simp
huffman@36581
   152
huffman@36581
   153
lemma onorm_triangle:
huffman@56223
   154
  assumes f: "bounded_linear f"
huffman@56223
   155
  assumes g: "bounded_linear g"
wenzelm@53253
   156
  shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
huffman@56223
   157
proof (rule onorm_bound)
huffman@56223
   158
  show "0 \<le> onorm f + onorm g"
huffman@56223
   159
    by (intro add_nonneg_nonneg onorm_pos_le f g)
huffman@56223
   160
next
huffman@56223
   161
  fix x
huffman@56223
   162
  have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
huffman@56223
   163
    by (rule norm_triangle_ineq)
huffman@56223
   164
  also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x"
huffman@56223
   165
    by (intro add_mono onorm f g)
huffman@56223
   166
  finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x"
huffman@56223
   167
    by (simp only: distrib_right)
huffman@56223
   168
qed
huffman@36581
   169
wenzelm@53253
   170
lemma onorm_triangle_le:
huffman@56223
   171
  assumes "bounded_linear f"
huffman@56223
   172
  assumes "bounded_linear g"
huffman@56223
   173
  assumes "onorm f + onorm g \<le> e"
wenzelm@53688
   174
  shows "onorm (\<lambda>x. f x + g x) \<le> e"
huffman@56223
   175
  using assms by (rule onorm_triangle [THEN order_trans])
huffman@36581
   176
wenzelm@53253
   177
lemma onorm_triangle_lt:
huffman@56223
   178
  assumes "bounded_linear f"
huffman@56223
   179
  assumes "bounded_linear g"
huffman@56223
   180
  assumes "onorm f + onorm g < e"
wenzelm@53688
   181
  shows "onorm (\<lambda>x. f x + g x) < e"
huffman@56223
   182
  using assms by (rule onorm_triangle [THEN order_le_less_trans])
huffman@36581
   183
huffman@36581
   184
end