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
```