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