src/HOL/Multivariate_Analysis/Operator_Norm.thy
 author wenzelm Wed Dec 30 11:37:29 2015 +0100 (2015-12-30) changeset 61975 b4b11391c676 parent 61915 e9812a95d108 permissions -rw-r--r--
isabelle update_cartouches -c -t;
 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` wenzelm@60420 ` 6` ```section \Operator Norm\ ``` huffman@36581 ` 7` huffman@36581 ` 8` ```theory Operator_Norm ``` huffman@56319 ` 9` ```imports Complex_Main ``` huffman@36581 ` 10` ```begin ``` huffman@36581 ` 11` wenzelm@61808 ` 12` ```text \This formulation yields zero if \'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` wenzelm@60420 ` 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]) ``` wenzelm@60420 ` 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", ``` haftmann@57512 ` 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" ``` wenzelm@60420 ` 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` immler@61915 ` 99` ```lemma onorm_id_le: "onorm (\x. x) \ 1" ``` immler@61915 ` 100` ``` by (rule onorm_bound) simp_all ``` immler@61915 ` 101` immler@61915 ` 102` ```lemma onorm_id: "onorm (\x. x::'a::{real_normed_vector, perfect_space}) = 1" ``` immler@61915 ` 103` ```proof (rule antisym[OF onorm_id_le]) ``` immler@61915 ` 104` ``` have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV) ``` immler@61915 ` 105` ``` then obtain x :: 'a where "x \ 0" by fast ``` immler@61915 ` 106` ``` hence "1 \ norm x / norm x" ``` immler@61915 ` 107` ``` by simp ``` immler@61915 ` 108` ``` also have "\ \ onorm (\x::'a. x)" ``` immler@61915 ` 109` ``` by (rule le_onorm) (rule bounded_linear_ident) ``` immler@61915 ` 110` ``` finally show "1 \ onorm (\x::'a. x)" . ``` immler@61915 ` 111` ```qed ``` immler@61915 ` 112` huffman@36581 ` 113` ```lemma onorm_compose: ``` huffman@56223 ` 114` ``` assumes f: "bounded_linear f" ``` huffman@56223 ` 115` ``` assumes g: "bounded_linear g" ``` wenzelm@53688 ` 116` ``` shows "onorm (f \ g) \ onorm f * onorm g" ``` huffman@56223 ` 117` ```proof (rule onorm_bound) ``` huffman@56223 ` 118` ``` show "0 \ onorm f * onorm g" ``` huffman@56223 ` 119` ``` by (intro mult_nonneg_nonneg onorm_pos_le f g) ``` huffman@56223 ` 120` ```next ``` huffman@56223 ` 121` ``` fix x ``` huffman@56223 ` 122` ``` have "norm (f (g x)) \ onorm f * norm (g x)" ``` huffman@56223 ` 123` ``` by (rule onorm [OF f]) ``` huffman@56223 ` 124` ``` also have "onorm f * norm (g x) \ onorm f * (onorm g * norm x)" ``` huffman@56223 ` 125` ``` by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]]) ``` huffman@56223 ` 126` ``` finally show "norm ((f \ g) x) \ onorm f * onorm g * norm x" ``` haftmann@57512 ` 127` ``` by (simp add: mult.assoc) ``` huffman@56223 ` 128` ```qed ``` huffman@36581 ` 129` huffman@56223 ` 130` ```lemma onorm_scaleR_lemma: ``` 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 (rule onorm_bound) ``` huffman@56223 ` 134` ``` show "0 \ \r\ * onorm f" ``` huffman@56223 ` 135` ``` by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f) ``` huffman@56223 ` 136` ```next ``` huffman@56223 ` 137` ``` fix x ``` huffman@56223 ` 138` ``` have "\r\ * norm (f x) \ \r\ * (onorm f * norm x)" ``` huffman@56223 ` 139` ``` by (intro mult_left_mono onorm abs_ge_zero f) ``` huffman@56223 ` 140` ``` then show "norm (r *\<^sub>R f x) \ \r\ * onorm f * norm x" ``` haftmann@57512 ` 141` ``` by (simp only: norm_scaleR mult.assoc) ``` huffman@56223 ` 142` ```qed ``` huffman@56223 ` 143` huffman@56223 ` 144` ```lemma onorm_scaleR: ``` huffman@56223 ` 145` ``` assumes f: "bounded_linear f" ``` huffman@56223 ` 146` ``` shows "onorm (\x. r *\<^sub>R f x) = \r\ * onorm f" ``` huffman@56223 ` 147` ```proof (cases "r = 0") ``` huffman@56223 ` 148` ``` assume "r \ 0" ``` huffman@56223 ` 149` ``` show ?thesis ``` huffman@56223 ` 150` ``` proof (rule order_antisym) ``` huffman@56223 ` 151` ``` show "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f" ``` huffman@56223 ` 152` ``` using f by (rule onorm_scaleR_lemma) ``` huffman@56223 ` 153` ``` next ``` huffman@56223 ` 154` ``` have "bounded_linear (\x. r *\<^sub>R f x)" ``` huffman@56223 ` 155` ``` using bounded_linear_scaleR_right f by (rule bounded_linear_compose) ``` huffman@56223 ` 156` ``` then have "onorm (\x. inverse r *\<^sub>R r *\<^sub>R f x) \ \inverse r\ * onorm (\x. r *\<^sub>R f x)" ``` huffman@56223 ` 157` ``` by (rule onorm_scaleR_lemma) ``` wenzelm@60420 ` 158` ``` with \r \ 0\ show "\r\ * onorm f \ onorm (\x. r *\<^sub>R f x)" ``` haftmann@57512 ` 159` ``` by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) ``` huffman@56223 ` 160` ``` qed ``` huffman@56223 ` 161` ```qed (simp add: onorm_zero) ``` huffman@36581 ` 162` immler@61915 ` 163` ```lemma onorm_scaleR_left_lemma: ``` immler@61915 ` 164` ``` assumes r: "bounded_linear r" ``` immler@61915 ` 165` ``` shows "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f" ``` immler@61915 ` 166` ```proof (rule onorm_bound) ``` immler@61915 ` 167` ``` fix x ``` immler@61915 ` 168` ``` have "norm (r x *\<^sub>R f) = norm (r x) * norm f" ``` immler@61915 ` 169` ``` by simp ``` immler@61915 ` 170` ``` also have "\ \ onorm r * norm x * norm f" ``` immler@61915 ` 171` ``` by (intro mult_right_mono onorm r norm_ge_zero) ``` immler@61915 ` 172` ``` finally show "norm (r x *\<^sub>R f) \ onorm r * norm f * norm x" ``` immler@61915 ` 173` ``` by (simp add: ac_simps) ``` immler@61915 ` 174` ```qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r) ``` immler@61915 ` 175` immler@61915 ` 176` ```lemma onorm_scaleR_left: ``` immler@61915 ` 177` ``` assumes f: "bounded_linear r" ``` immler@61915 ` 178` ``` shows "onorm (\x. r x *\<^sub>R f) = onorm r * norm f" ``` immler@61915 ` 179` ```proof (cases "f = 0") ``` immler@61915 ` 180` ``` assume "f \ 0" ``` immler@61915 ` 181` ``` show ?thesis ``` immler@61915 ` 182` ``` proof (rule order_antisym) ``` immler@61915 ` 183` ``` show "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f" ``` immler@61915 ` 184` ``` using f by (rule onorm_scaleR_left_lemma) ``` immler@61915 ` 185` ``` next ``` immler@61915 ` 186` ``` have bl1: "bounded_linear (\x. r x *\<^sub>R f)" ``` immler@61915 ` 187` ``` by (metis bounded_linear_scaleR_const f) ``` immler@61915 ` 188` ``` have "bounded_linear (\x. r x * norm f)" ``` immler@61915 ` 189` ``` by (metis bounded_linear_mult_const f) ``` immler@61915 ` 190` ``` from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"] ``` immler@61915 ` 191` ``` have "onorm r \ onorm (\x. r x * norm f) * inverse (norm f)" ``` wenzelm@61975 ` 192` ``` using \f \ 0\ ``` immler@61915 ` 193` ``` by (simp add: inverse_eq_divide) ``` immler@61915 ` 194` ``` also have "onorm (\x. r x * norm f) \ onorm (\x. r x *\<^sub>R f)" ``` immler@61915 ` 195` ``` by (rule onorm_bound) ``` immler@61915 ` 196` ``` (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm]) ``` immler@61915 ` 197` ``` finally show "onorm r * norm f \ onorm (\x. r x *\<^sub>R f)" ``` wenzelm@61975 ` 198` ``` using \f \ 0\ ``` immler@61915 ` 199` ``` by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) ``` immler@61915 ` 200` ``` qed ``` immler@61915 ` 201` ```qed (simp add: onorm_zero) ``` immler@61915 ` 202` wenzelm@53253 ` 203` ```lemma onorm_neg: ``` huffman@36581 ` 204` ``` shows "onorm (\x. - f x) = onorm f" ``` huffman@56223 ` 205` ``` unfolding onorm_def by simp ``` huffman@36581 ` 206` huffman@36581 ` 207` ```lemma onorm_triangle: ``` huffman@56223 ` 208` ``` assumes f: "bounded_linear f" ``` huffman@56223 ` 209` ``` assumes g: "bounded_linear g" ``` wenzelm@53253 ` 210` ``` shows "onorm (\x. f x + g x) \ onorm f + onorm g" ``` huffman@56223 ` 211` ```proof (rule onorm_bound) ``` huffman@56223 ` 212` ``` show "0 \ onorm f + onorm g" ``` huffman@56223 ` 213` ``` by (intro add_nonneg_nonneg onorm_pos_le f g) ``` huffman@56223 ` 214` ```next ``` huffman@56223 ` 215` ``` fix x ``` huffman@56223 ` 216` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@56223 ` 217` ``` by (rule norm_triangle_ineq) ``` huffman@56223 ` 218` ``` also have "norm (f x) + norm (g x) \ onorm f * norm x + onorm g * norm x" ``` huffman@56223 ` 219` ``` by (intro add_mono onorm f g) ``` huffman@56223 ` 220` ``` finally show "norm (f x + g x) \ (onorm f + onorm g) * norm x" ``` huffman@56223 ` 221` ``` by (simp only: distrib_right) ``` huffman@56223 ` 222` ```qed ``` huffman@36581 ` 223` wenzelm@53253 ` 224` ```lemma onorm_triangle_le: ``` huffman@56223 ` 225` ``` assumes "bounded_linear f" ``` huffman@56223 ` 226` ``` assumes "bounded_linear g" ``` huffman@56223 ` 227` ``` assumes "onorm f + onorm g \ e" ``` wenzelm@53688 ` 228` ``` shows "onorm (\x. f x + g x) \ e" ``` huffman@56223 ` 229` ``` using assms by (rule onorm_triangle [THEN order_trans]) ``` huffman@36581 ` 230` wenzelm@53253 ` 231` ```lemma onorm_triangle_lt: ``` huffman@56223 ` 232` ``` assumes "bounded_linear f" ``` huffman@56223 ` 233` ``` assumes "bounded_linear g" ``` huffman@56223 ` 234` ``` assumes "onorm f + onorm g < e" ``` wenzelm@53688 ` 235` ``` shows "onorm (\x. f x + g x) < e" ``` huffman@56223 ` 236` ``` using assms by (rule onorm_triangle [THEN order_le_less_trans]) ``` huffman@36581 ` 237` huffman@36581 ` 238` ```end ```