src/HOL/Analysis/Operator_Norm.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69518 bf88364c9e94 child 69607 7cd977863194 permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Title:      HOL/Analysis/Operator_Norm.thy
```
```     2     Author:     Amine Chaieb, University of Cambridge
```
```     3     Author:     Brian Huffman
```
```     4 *)
```
```     5
```
```     6 section \<open>Operator Norm\<close>
```
```     7
```
```     8 theory Operator_Norm
```
```     9 imports Complex_Main
```
```    10 begin
```
```    11
```
```    12 text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
```
```    13
```
```    14 definition%important
```
```    15 onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" where
```
```    16 "onorm f = (SUP x. norm (f x) / norm x)"
```
```    17
```
```    18 proposition onorm_bound:
```
```    19   assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
```
```    20   shows "onorm f \<le> b"
```
```    21   unfolding onorm_def
```
```    22 proof (rule cSUP_least)
```
```    23   fix x
```
```    24   show "norm (f x) / norm x \<le> b"
```
```    25     using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
```
```    26 qed simp
```
```    27
```
```    28 text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>
```
```    29
```
```    30 lemma onorm_le:
```
```    31   fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
```
```    32   assumes "\<And>x. norm (f x) \<le> b * norm x"
```
```    33   shows "onorm f \<le> b"
```
```    34 proof (rule onorm_bound [OF _ assms])
```
```    35   have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
```
```    36   then obtain a :: 'a where "a \<noteq> 0" by fast
```
```    37   have "0 \<le> b * norm a"
```
```    38     by (rule order_trans [OF norm_ge_zero assms])
```
```    39   with \<open>a \<noteq> 0\<close> show "0 \<le> b"
```
```    40     by (simp add: zero_le_mult_iff)
```
```    41 qed
```
```    42
```
```    43 lemma le_onorm:
```
```    44   assumes "bounded_linear f"
```
```    45   shows "norm (f x) / norm x \<le> onorm f"
```
```    46 proof -
```
```    47   interpret f: bounded_linear f by fact
```
```    48   obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
```
```    49     using f.nonneg_bounded by auto
```
```    50   then have "\<forall>x. norm (f x) / norm x \<le> b"
```
```    51     by (clarify, case_tac "x = 0",
```
```    52       simp_all add: f.zero pos_divide_le_eq mult.commute)
```
```    53   then have "bdd_above (range (\<lambda>x. norm (f x) / norm x))"
```
```    54     unfolding bdd_above_def by fast
```
```    55   with UNIV_I show ?thesis
```
```    56     unfolding onorm_def by (rule cSUP_upper)
```
```    57 qed
```
```    58
```
```    59 lemma onorm:
```
```    60   assumes "bounded_linear f"
```
```    61   shows "norm (f x) \<le> onorm f * norm x"
```
```    62 proof -
```
```    63   interpret f: bounded_linear f by fact
```
```    64   show ?thesis
```
```    65   proof (cases)
```
```    66     assume "x = 0"
```
```    67     then show ?thesis by (simp add: f.zero)
```
```    68   next
```
```    69     assume "x \<noteq> 0"
```
```    70     have "norm (f x) / norm x \<le> onorm f"
```
```    71       by (rule le_onorm [OF assms])
```
```    72     then show "norm (f x) \<le> onorm f * norm x"
```
```    73       by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>)
```
```    74   qed
```
```    75 qed
```
```    76
```
```    77 lemma onorm_pos_le:
```
```    78   assumes f: "bounded_linear f"
```
```    79   shows "0 \<le> onorm f"
```
```    80   using le_onorm [OF f, where x=0] by simp
```
```    81
```
```    82 lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
```
```    83 proof (rule order_antisym)
```
```    84   show "onorm (\<lambda>x. 0) \<le> 0"
```
```    85     by (simp add: onorm_bound)
```
```    86   show "0 \<le> onorm (\<lambda>x. 0)"
```
```    87     using bounded_linear_zero by (rule onorm_pos_le)
```
```    88 qed
```
```    89
```
```    90 lemma onorm_eq_0:
```
```    91   assumes f: "bounded_linear f"
```
```    92   shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
```
```    93   using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
```
```    94
```
```    95 lemma onorm_pos_lt:
```
```    96   assumes f: "bounded_linear f"
```
```    97   shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
```
```    98   by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
```
```    99
```
```   100 lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
```
```   101   by (rule onorm_bound) simp_all
```
```   102
```
```   103 lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
```
```   104 proof (rule antisym[OF onorm_id_le])
```
```   105   have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
```
```   106   then obtain x :: 'a where "x \<noteq> 0" by fast
```
```   107   hence "1 \<le> norm x / norm x"
```
```   108     by simp
```
```   109   also have "\<dots> \<le> onorm (\<lambda>x::'a. x)"
```
```   110     by (rule le_onorm) (rule bounded_linear_ident)
```
```   111   finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
```
```   112 qed
```
```   113
```
```   114 lemma onorm_compose:
```
```   115   assumes f: "bounded_linear f"
```
```   116   assumes g: "bounded_linear g"
```
```   117   shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
```
```   118 proof (rule onorm_bound)
```
```   119   show "0 \<le> onorm f * onorm g"
```
```   120     by (intro mult_nonneg_nonneg onorm_pos_le f g)
```
```   121 next
```
```   122   fix x
```
```   123   have "norm (f (g x)) \<le> onorm f * norm (g x)"
```
```   124     by (rule onorm [OF f])
```
```   125   also have "onorm f * norm (g x) \<le> onorm f * (onorm g * norm x)"
```
```   126     by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
```
```   127   finally show "norm ((f \<circ> g) x) \<le> onorm f * onorm g * norm x"
```
```   128     by (simp add: mult.assoc)
```
```   129 qed
```
```   130
```
```   131 lemma onorm_scaleR_lemma:
```
```   132   assumes f: "bounded_linear f"
```
```   133   shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
```
```   134 proof (rule onorm_bound)
```
```   135   show "0 \<le> \<bar>r\<bar> * onorm f"
```
```   136     by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
```
```   137 next
```
```   138   fix x
```
```   139   have "\<bar>r\<bar> * norm (f x) \<le> \<bar>r\<bar> * (onorm f * norm x)"
```
```   140     by (intro mult_left_mono onorm abs_ge_zero f)
```
```   141   then show "norm (r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f * norm x"
```
```   142     by (simp only: norm_scaleR mult.assoc)
```
```   143 qed
```
```   144
```
```   145 lemma onorm_scaleR:
```
```   146   assumes f: "bounded_linear f"
```
```   147   shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
```
```   148 proof (cases "r = 0")
```
```   149   assume "r \<noteq> 0"
```
```   150   show ?thesis
```
```   151   proof (rule order_antisym)
```
```   152     show "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
```
```   153       using f by (rule onorm_scaleR_lemma)
```
```   154   next
```
```   155     have "bounded_linear (\<lambda>x. r *\<^sub>R f x)"
```
```   156       using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
```
```   157     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)"
```
```   158       by (rule onorm_scaleR_lemma)
```
```   159     with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
```
```   160       by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
```
```   161   qed
```
```   162 qed (simp add: onorm_zero)
```
```   163
```
```   164 lemma onorm_scaleR_left_lemma:
```
```   165   assumes r: "bounded_linear r"
```
```   166   shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
```
```   167 proof (rule onorm_bound)
```
```   168   fix x
```
```   169   have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
```
```   170     by simp
```
```   171   also have "\<dots> \<le> onorm r * norm x * norm f"
```
```   172     by (intro mult_right_mono onorm r norm_ge_zero)
```
```   173   finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x"
```
```   174     by (simp add: ac_simps)
```
```   175 qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
```
```   176
```
```   177 lemma onorm_scaleR_left:
```
```   178   assumes f: "bounded_linear r"
```
```   179   shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
```
```   180 proof (cases "f = 0")
```
```   181   assume "f \<noteq> 0"
```
```   182   show ?thesis
```
```   183   proof (rule order_antisym)
```
```   184     show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
```
```   185       using f by (rule onorm_scaleR_left_lemma)
```
```   186   next
```
```   187     have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)"
```
```   188       by (metis bounded_linear_scaleR_const f)
```
```   189     have "bounded_linear (\<lambda>x. r x * norm f)"
```
```   190       by (metis bounded_linear_mult_const f)
```
```   191     from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
```
```   192     have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
```
```   193       using \<open>f \<noteq> 0\<close>
```
```   194       by (simp add: inverse_eq_divide)
```
```   195     also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
```
```   196       by (rule onorm_bound)
```
```   197         (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
```
```   198     finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
```
```   199       using \<open>f \<noteq> 0\<close>
```
```   200       by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
```
```   201   qed
```
```   202 qed (simp add: onorm_zero)
```
```   203
```
```   204 lemma onorm_neg:
```
```   205   shows "onorm (\<lambda>x. - f x) = onorm f"
```
```   206   unfolding onorm_def by simp
```
```   207
```
```   208 lemma onorm_triangle:
```
```   209   assumes f: "bounded_linear f"
```
```   210   assumes g: "bounded_linear g"
```
```   211   shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
```
```   212 proof (rule onorm_bound)
```
```   213   show "0 \<le> onorm f + onorm g"
```
```   214     by (intro add_nonneg_nonneg onorm_pos_le f g)
```
```   215 next
```
```   216   fix x
```
```   217   have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
```
```   218     by (rule norm_triangle_ineq)
```
```   219   also have "norm (f x) + norm (g x) \<le> onorm f * norm x + onorm g * norm x"
```
```   220     by (intro add_mono onorm f g)
```
```   221   finally show "norm (f x + g x) \<le> (onorm f + onorm g) * norm x"
```
```   222     by (simp only: distrib_right)
```
```   223 qed
```
```   224
```
```   225 lemma onorm_triangle_le:
```
```   226   assumes "bounded_linear f"
```
```   227   assumes "bounded_linear g"
```
```   228   assumes "onorm f + onorm g \<le> e"
```
```   229   shows "onorm (\<lambda>x. f x + g x) \<le> e"
```
```   230   using assms by (rule onorm_triangle [THEN order_trans])
```
```   231
```
```   232 lemma onorm_triangle_lt:
```
```   233   assumes "bounded_linear f"
```
```   234   assumes "bounded_linear g"
```
```   235   assumes "onorm f + onorm g < e"
```
```   236   shows "onorm (\<lambda>x. f x + g x) < e"
```
```   237   using assms by (rule onorm_triangle [THEN order_le_less_trans])
```
```   238
```
```   239 lemma onorm_sum:
```
```   240   assumes "finite S"
```
```   241   assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
```
```   242   shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
```
```   243   using assms
```
```   244   by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
```
```   245
```
```   246 lemmas onorm_sum_le = onorm_sum[THEN order_trans]
```
```   247
```
```   248 end
```