src/HOL/Multivariate_Analysis/Operator_Norm.thy
author hoelzl
Mon Jun 21 19:33:51 2010 +0200 (2010-06-21)
changeset 37489 44e42d392c6e
parent 36593 fb69c8cd27bd
child 38642 8fa437809c67
permissions -rw-r--r--
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
huffman@36581
     1
(*  Title:      Library/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@36581
     8
imports Euclidean_Space
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:
hoelzl@37489
    14
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
huffman@36581
    15
  assumes lf: "linear f"
huffman@36581
    16
  shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")
huffman@36581
    17
proof-
huffman@36581
    18
  {assume H: ?rhs
hoelzl@37489
    19
    {fix x :: "'a" assume x: "norm x = 1"
huffman@36581
    20
      from H[rule_format, of x] x have "norm (f x) \<le> b" by simp}
huffman@36581
    21
    then have ?lhs by blast }
huffman@36581
    22
huffman@36581
    23
  moreover
huffman@36581
    24
  {assume H: ?lhs
hoelzl@37489
    25
    have bp: "b \<ge> 0" apply-apply(rule order_trans [OF norm_ge_zero])
hoelzl@37489
    26
      apply(rule H[rule_format, of "basis 0::'a"]) by auto 
hoelzl@37489
    27
    {fix x :: "'a"
huffman@36581
    28
      {assume "x = 0"
huffman@36581
    29
        then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
huffman@36581
    30
      moreover
huffman@36581
    31
      {assume x0: "x \<noteq> 0"
huffman@36581
    32
        hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
huffman@36581
    33
        let ?c = "1/ norm x"
huffman@36593
    34
        have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0)
huffman@36593
    35
        with H have "norm (f (?c *\<^sub>R x)) \<le> b" by blast
huffman@36581
    36
        hence "?c * norm (f x) \<le> b"
huffman@36581
    37
          by (simp add: linear_cmul[OF lf])
huffman@36581
    38
        hence "norm (f x) \<le> b * norm x"
huffman@36581
    39
          using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
huffman@36581
    40
      ultimately have "norm (f x) \<le> b * norm x" by blast}
huffman@36581
    41
    then have ?rhs by blast}
huffman@36581
    42
  ultimately show ?thesis by blast
huffman@36581
    43
qed
hoelzl@37489
    44
 
huffman@36581
    45
lemma onorm:
hoelzl@37489
    46
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
huffman@36581
    47
  assumes lf: "linear f"
huffman@36581
    48
  shows "norm (f x) <= onorm f * norm x"
huffman@36581
    49
  and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
huffman@36581
    50
proof-
huffman@36581
    51
  {
huffman@36581
    52
    let ?S = "{norm (f x) |x. norm x = 1}"
hoelzl@37489
    53
    have "norm (f (basis 0)) \<in> ?S" unfolding mem_Collect_eq
hoelzl@37489
    54
      apply(rule_tac x="basis 0" in exI) by auto
hoelzl@37489
    55
    hence Se: "?S \<noteq> {}" by auto
huffman@36581
    56
    from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
huffman@36581
    57
      unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
huffman@36581
    58
    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
huffman@36581
    59
      show "norm (f x) <= onorm f * norm x"
huffman@36581
    60
        apply -
huffman@36581
    61
        apply (rule spec[where x = x])
huffman@36581
    62
        unfolding norm_bound_generalize[OF lf, symmetric]
huffman@36581
    63
        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
huffman@36581
    64
    {
huffman@36581
    65
      show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
huffman@36581
    66
        using Sup[OF Se b, unfolded onorm_def[symmetric]]
huffman@36581
    67
        unfolding norm_bound_generalize[OF lf, symmetric]
huffman@36581
    68
        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
huffman@36581
    69
  }
huffman@36581
    70
qed
huffman@36581
    71
hoelzl@37489
    72
lemma onorm_pos_le: assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" shows "0 <= onorm f"
hoelzl@37489
    73
  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 0"]] 
hoelzl@37489
    74
  using DIM_positive[where 'a='n] by auto
huffman@36581
    75
hoelzl@37489
    76
lemma onorm_eq_0: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
huffman@36581
    77
  shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
huffman@36581
    78
  using onorm[OF lf]
huffman@36581
    79
  apply (auto simp add: onorm_pos_le)
huffman@36581
    80
  apply atomize
huffman@36581
    81
  apply (erule allE[where x="0::real"])
huffman@36581
    82
  using onorm_pos_le[OF lf]
huffman@36581
    83
  apply arith
huffman@36581
    84
  done
huffman@36581
    85
hoelzl@37489
    86
lemma onorm_const: "onorm(\<lambda>x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y"
huffman@36581
    87
proof-
hoelzl@37489
    88
  let ?f = "\<lambda>x::'a. (y::'b)"
huffman@36581
    89
  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
hoelzl@37489
    90
    apply safe apply(rule_tac x="basis 0" in exI) by auto
huffman@36581
    91
  show ?thesis
huffman@36581
    92
    unfolding onorm_def th
huffman@36581
    93
    apply (rule Sup_unique) by (simp_all  add: setle_def)
huffman@36581
    94
qed
huffman@36581
    95
hoelzl@37489
    96
lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
huffman@36581
    97
  shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"
huffman@36581
    98
  unfolding onorm_eq_0[OF lf, symmetric]
huffman@36581
    99
  using onorm_pos_le[OF lf] by arith
huffman@36581
   100
huffman@36581
   101
lemma onorm_compose:
hoelzl@37489
   102
  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
hoelzl@37489
   103
  and lg: "linear (g::'k::euclidean_space \<Rightarrow> 'n::euclidean_space)"
huffman@36581
   104
  shows "onorm (f o g) <= onorm f * onorm g"
huffman@36581
   105
  apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
huffman@36581
   106
  unfolding o_def
huffman@36581
   107
  apply (subst mult_assoc)
huffman@36581
   108
  apply (rule order_trans)
huffman@36581
   109
  apply (rule onorm(1)[OF lf])
huffman@36581
   110
  apply (rule mult_mono1)
huffman@36581
   111
  apply (rule onorm(1)[OF lg])
huffman@36581
   112
  apply (rule onorm_pos_le[OF lf])
huffman@36581
   113
  done
huffman@36581
   114
hoelzl@37489
   115
lemma onorm_neg_lemma: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
huffman@36581
   116
  shows "onorm (\<lambda>x. - f x) \<le> onorm f"
huffman@36581
   117
  using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
huffman@36581
   118
  unfolding norm_minus_cancel by metis
huffman@36581
   119
hoelzl@37489
   120
lemma onorm_neg: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
huffman@36581
   121
  shows "onorm (\<lambda>x. - f x) = onorm f"
huffman@36581
   122
  using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
huffman@36581
   123
  by simp
huffman@36581
   124
huffman@36581
   125
lemma onorm_triangle:
hoelzl@37489
   126
  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" and lg: "linear g"
huffman@36581
   127
  shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
huffman@36581
   128
  apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
huffman@36581
   129
  apply (rule order_trans)
huffman@36581
   130
  apply (rule norm_triangle_ineq)
huffman@36581
   131
  apply (simp add: distrib)
huffman@36581
   132
  apply (rule add_mono)
huffman@36581
   133
  apply (rule onorm(1)[OF lf])
huffman@36581
   134
  apply (rule onorm(1)[OF lg])
huffman@36581
   135
  done
huffman@36581
   136
hoelzl@37489
   137
lemma onorm_triangle_le: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e
huffman@36581
   138
  \<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"
huffman@36581
   139
  apply (rule order_trans)
huffman@36581
   140
  apply (rule onorm_triangle)
huffman@36581
   141
  apply assumption+
huffman@36581
   142
  done
huffman@36581
   143
hoelzl@37489
   144
lemma onorm_triangle_lt: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e
huffman@36581
   145
  ==> onorm(\<lambda>x. f x + g x) < e"
huffman@36581
   146
  apply (rule order_le_less_trans)
huffman@36581
   147
  apply (rule onorm_triangle)
huffman@36581
   148
  by assumption+
huffman@36581
   149
huffman@36581
   150
end