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