src/HOL/Multivariate_Analysis/Operator_Norm.thy
author wenzelm
Wed Sep 18 00:11:15 2013 +0200 (2013-09-18)
changeset 53688 63892cfef47f
parent 53253 220f306f5c4e
child 54263 c4159fe6fa46
permissions -rw-r--r--
tuned proofs;
wenzelm@41959
     1
(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy
huffman@36581
     2
    Author:     Amine Chaieb, University of Cambridge
huffman@36581
     3
*)
huffman@36581
     4
huffman@36581
     5
header {* Operator Norm *}
huffman@36581
     6
huffman@36581
     7
theory Operator_Norm
huffman@44133
     8
imports Linear_Algebra
huffman@36581
     9
begin
huffman@36581
    10
huffman@36581
    11
definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
huffman@36581
    12
huffman@36581
    13
lemma norm_bound_generalize:
wenzelm@53253
    14
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
huffman@36581
    15
  assumes lf: "linear f"
wenzelm@53253
    16
  shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)"
wenzelm@53253
    17
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@53253
    18
proof
wenzelm@53253
    19
  assume H: ?rhs
wenzelm@53253
    20
  {
wenzelm@53253
    21
    fix x :: "'a"
wenzelm@53253
    22
    assume x: "norm x = 1"
wenzelm@53688
    23
    from H[rule_format, of x] x have "norm (f x) \<le> b"
wenzelm@53688
    24
      by simp
wenzelm@53253
    25
  }
wenzelm@53253
    26
  then show ?lhs by blast
wenzelm@53253
    27
next
wenzelm@53253
    28
  assume H: ?lhs
wenzelm@53253
    29
  have bp: "b \<ge> 0"
wenzelm@53253
    30
    apply -
wenzelm@53253
    31
    apply (rule order_trans [OF norm_ge_zero])
wenzelm@53253
    32
    apply (rule H[rule_format, of "SOME x::'a. x \<in> Basis"])
wenzelm@53253
    33
    apply (auto intro: SOME_Basis norm_Basis)
wenzelm@53253
    34
    done
wenzelm@53253
    35
  {
wenzelm@53253
    36
    fix x :: "'a"
wenzelm@53253
    37
    {
wenzelm@53253
    38
      assume "x = 0"
wenzelm@53253
    39
      then have "norm (f x) \<le> b * norm x"
wenzelm@53253
    40
        by (simp add: linear_0[OF lf] bp)
wenzelm@53253
    41
    }
wenzelm@53253
    42
    moreover
wenzelm@53253
    43
    {
wenzelm@53253
    44
      assume x0: "x \<noteq> 0"
wenzelm@53688
    45
      then have n0: "norm x \<noteq> 0"
wenzelm@53688
    46
        by (metis norm_eq_zero)
wenzelm@53253
    47
      let ?c = "1/ norm x"
wenzelm@53688
    48
      have "norm (?c *\<^sub>R x) = 1"
wenzelm@53688
    49
        using x0 by (simp add: n0)
wenzelm@53688
    50
      with H have "norm (f (?c *\<^sub>R x)) \<le> b"
wenzelm@53688
    51
        by blast
wenzelm@53253
    52
      then have "?c * norm (f x) \<le> b"
wenzelm@53253
    53
        by (simp add: linear_cmul[OF lf])
wenzelm@53253
    54
      then have "norm (f x) \<le> b * norm x"
wenzelm@53688
    55
        using n0 norm_ge_zero[of x]
wenzelm@53688
    56
        by (auto simp add: field_simps)
wenzelm@53253
    57
    }
wenzelm@53688
    58
    ultimately have "norm (f x) \<le> b * norm x"
wenzelm@53688
    59
      by blast
wenzelm@53253
    60
  }
wenzelm@53253
    61
  then show ?rhs by blast
wenzelm@53253
    62
qed
huffman@36581
    63
huffman@36581
    64
lemma onorm:
hoelzl@37489
    65
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
huffman@36581
    66
  assumes lf: "linear f"
wenzelm@53253
    67
  shows "norm (f x) \<le> onorm f * norm x"
wenzelm@53253
    68
    and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
wenzelm@53253
    69
proof -
wenzelm@53253
    70
  let ?S = "{norm (f x) |x. norm x = 1}"
wenzelm@53253
    71
  have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
wenzelm@53253
    72
    by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
wenzelm@53688
    73
  then have Se: "?S \<noteq> {}"
wenzelm@53688
    74
    by auto
wenzelm@53253
    75
  from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
wenzelm@53688
    76
    unfolding norm_bound_generalize[OF lf, symmetric]
wenzelm@53688
    77
    by (auto simp add: setle_def)
wenzelm@53253
    78
  from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
wenzelm@53688
    79
  show "norm (f x) \<le> onorm f * norm x"
wenzelm@53253
    80
    apply -
wenzelm@53253
    81
    apply (rule spec[where x = x])
wenzelm@53253
    82
    unfolding norm_bound_generalize[OF lf, symmetric]
wenzelm@53253
    83
    apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
wenzelm@53253
    84
    done
wenzelm@53688
    85
  show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
wenzelm@53253
    86
    using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
wenzelm@53253
    87
    unfolding norm_bound_generalize[OF lf, symmetric]
wenzelm@53253
    88
    by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
huffman@36581
    89
qed
huffman@36581
    90
wenzelm@53253
    91
lemma onorm_pos_le:
wenzelm@53688
    92
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53688
    93
  assumes lf: "linear f"
wenzelm@53253
    94
  shows "0 \<le> onorm f"
wenzelm@53253
    95
  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
hoelzl@50526
    96
  by (simp add: SOME_Basis)
huffman@36581
    97
wenzelm@53253
    98
lemma onorm_eq_0:
wenzelm@53688
    99
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53688
   100
  assumes lf: "linear f"
huffman@36581
   101
  shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
huffman@36581
   102
  using onorm[OF lf]
huffman@36581
   103
  apply (auto simp add: onorm_pos_le)
huffman@36581
   104
  apply atomize
huffman@36581
   105
  apply (erule allE[where x="0::real"])
huffman@36581
   106
  using onorm_pos_le[OF lf]
huffman@36581
   107
  apply arith
huffman@36581
   108
  done
huffman@36581
   109
wenzelm@53688
   110
lemma onorm_const:
wenzelm@53688
   111
  "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
wenzelm@53253
   112
proof -
wenzelm@53688
   113
  let ?f = "\<lambda>x::'a. y::'b"
huffman@36581
   114
  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
hoelzl@50526
   115
    by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
huffman@36581
   116
  show ?thesis
huffman@36581
   117
    unfolding onorm_def th
wenzelm@53253
   118
    apply (rule cSup_unique)
wenzelm@53253
   119
    apply (simp_all  add: setle_def)
wenzelm@53253
   120
    done
huffman@36581
   121
qed
huffman@36581
   122
wenzelm@53253
   123
lemma onorm_pos_lt:
wenzelm@53688
   124
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53688
   125
  assumes lf: "linear f"
wenzelm@53688
   126
  shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
huffman@36581
   127
  unfolding onorm_eq_0[OF lf, symmetric]
huffman@36581
   128
  using onorm_pos_le[OF lf] by arith
huffman@36581
   129
huffman@36581
   130
lemma onorm_compose:
wenzelm@53688
   131
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53688
   132
    and g :: "'k::euclidean_space \<Rightarrow> 'n::euclidean_space"
wenzelm@53688
   133
  assumes lf: "linear f"
wenzelm@53688
   134
    and lg: "linear g"
wenzelm@53688
   135
  shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
wenzelm@53253
   136
    apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
wenzelm@53253
   137
    unfolding o_def
wenzelm@53253
   138
    apply (subst mult_assoc)
wenzelm@53253
   139
    apply (rule order_trans)
wenzelm@53253
   140
    apply (rule onorm(1)[OF lf])
wenzelm@53253
   141
    apply (rule mult_left_mono)
wenzelm@53253
   142
    apply (rule onorm(1)[OF lg])
wenzelm@53253
   143
    apply (rule onorm_pos_le[OF lf])
wenzelm@53253
   144
    done
huffman@36581
   145
wenzelm@53253
   146
lemma onorm_neg_lemma:
wenzelm@53688
   147
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53688
   148
  assumes lf: "linear f"
huffman@36581
   149
  shows "onorm (\<lambda>x. - f x) \<le> onorm f"
huffman@36581
   150
  using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
huffman@36581
   151
  unfolding norm_minus_cancel by metis
huffman@36581
   152
wenzelm@53253
   153
lemma onorm_neg:
wenzelm@53688
   154
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53688
   155
  assumes lf: "linear f"
huffman@36581
   156
  shows "onorm (\<lambda>x. - f x) = onorm f"
huffman@36581
   157
  using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
huffman@36581
   158
  by simp
huffman@36581
   159
huffman@36581
   160
lemma onorm_triangle:
wenzelm@53688
   161
  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53688
   162
  assumes lf: "linear f"
wenzelm@53253
   163
    and lg: "linear g"
wenzelm@53253
   164
  shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
huffman@36581
   165
  apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
huffman@36581
   166
  apply (rule order_trans)
huffman@36581
   167
  apply (rule norm_triangle_ineq)
huffman@36581
   168
  apply (simp add: distrib)
huffman@36581
   169
  apply (rule add_mono)
huffman@36581
   170
  apply (rule onorm(1)[OF lf])
huffman@36581
   171
  apply (rule onorm(1)[OF lg])
huffman@36581
   172
  done
huffman@36581
   173
wenzelm@53253
   174
lemma onorm_triangle_le:
wenzelm@53688
   175
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53688
   176
  assumes "linear f"
wenzelm@53688
   177
    and "linear g"
wenzelm@53688
   178
    and "onorm f + onorm g \<le> e"
wenzelm@53688
   179
  shows "onorm (\<lambda>x. f x + g x) \<le> e"
huffman@36581
   180
  apply (rule order_trans)
huffman@36581
   181
  apply (rule onorm_triangle)
wenzelm@53688
   182
  apply (rule assms)+
huffman@36581
   183
  done
huffman@36581
   184
wenzelm@53253
   185
lemma onorm_triangle_lt:
wenzelm@53688
   186
  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53688
   187
  assumes "linear f"
wenzelm@53688
   188
    and "linear g"
wenzelm@53688
   189
    and "onorm f + onorm g < e"
wenzelm@53688
   190
  shows "onorm (\<lambda>x. f x + g x) < e"
huffman@36581
   191
  apply (rule order_le_less_trans)
huffman@36581
   192
  apply (rule onorm_triangle)
wenzelm@53688
   193
  apply (rule assms)+
wenzelm@53253
   194
  done
huffman@36581
   195
huffman@36581
   196
end