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