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