src/HOL/Multivariate_Analysis/Operator_Norm.thy
 author wenzelm Wed Sep 18 00:11:15 2013 +0200 (2013-09-18) changeset 53688 63892cfef47f parent 53253 220f306f5c4e child 54263 c4159fe6fa46 permissions -rw-r--r--
tuned proofs;
 wenzelm@41959 ` 1` ```(* Title: HOL/Multivariate_Analysis/Operator_Norm.thy ``` huffman@36581 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` huffman@36581 ` 3` ```*) ``` huffman@36581 ` 4` huffman@36581 ` 5` ```header {* Operator Norm *} ``` huffman@36581 ` 6` huffman@36581 ` 7` ```theory Operator_Norm ``` huffman@44133 ` 8` ```imports Linear_Algebra ``` huffman@36581 ` 9` ```begin ``` huffman@36581 ` 10` huffman@36581 ` 11` ```definition "onorm f = Sup {norm (f x)| x. norm x = 1}" ``` huffman@36581 ` 12` huffman@36581 ` 13` ```lemma norm_bound_generalize: ``` wenzelm@53253 ` 14` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` huffman@36581 ` 15` ``` assumes lf: "linear f" ``` wenzelm@53253 ` 16` ``` shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" ``` wenzelm@53253 ` 17` ``` (is "?lhs \ ?rhs") ``` wenzelm@53253 ` 18` ```proof ``` wenzelm@53253 ` 19` ``` assume H: ?rhs ``` wenzelm@53253 ` 20` ``` { ``` wenzelm@53253 ` 21` ``` fix x :: "'a" ``` wenzelm@53253 ` 22` ``` assume x: "norm x = 1" ``` wenzelm@53688 ` 23` ``` from H[rule_format, of x] x have "norm (f x) \ b" ``` wenzelm@53688 ` 24` ``` by simp ``` wenzelm@53253 ` 25` ``` } ``` wenzelm@53253 ` 26` ``` then show ?lhs by blast ``` wenzelm@53253 ` 27` ```next ``` wenzelm@53253 ` 28` ``` assume H: ?lhs ``` wenzelm@53253 ` 29` ``` have bp: "b \ 0" ``` wenzelm@53253 ` 30` ``` apply - ``` wenzelm@53253 ` 31` ``` apply (rule order_trans [OF norm_ge_zero]) ``` wenzelm@53253 ` 32` ``` apply (rule H[rule_format, of "SOME x::'a. x \ Basis"]) ``` wenzelm@53253 ` 33` ``` apply (auto intro: SOME_Basis norm_Basis) ``` wenzelm@53253 ` 34` ``` done ``` wenzelm@53253 ` 35` ``` { ``` wenzelm@53253 ` 36` ``` fix x :: "'a" ``` wenzelm@53253 ` 37` ``` { ``` wenzelm@53253 ` 38` ``` assume "x = 0" ``` wenzelm@53253 ` 39` ``` then have "norm (f x) \ b * norm x" ``` wenzelm@53253 ` 40` ``` by (simp add: linear_0[OF lf] bp) ``` wenzelm@53253 ` 41` ``` } ``` wenzelm@53253 ` 42` ``` moreover ``` wenzelm@53253 ` 43` ``` { ``` wenzelm@53253 ` 44` ``` assume x0: "x \ 0" ``` wenzelm@53688 ` 45` ``` then have n0: "norm x \ 0" ``` wenzelm@53688 ` 46` ``` by (metis norm_eq_zero) ``` wenzelm@53253 ` 47` ``` let ?c = "1/ norm x" ``` wenzelm@53688 ` 48` ``` have "norm (?c *\<^sub>R x) = 1" ``` wenzelm@53688 ` 49` ``` using x0 by (simp add: n0) ``` wenzelm@53688 ` 50` ``` with H have "norm (f (?c *\<^sub>R x)) \ b" ``` wenzelm@53688 ` 51` ``` by blast ``` wenzelm@53253 ` 52` ``` then have "?c * norm (f x) \ b" ``` wenzelm@53253 ` 53` ``` by (simp add: linear_cmul[OF lf]) ``` wenzelm@53253 ` 54` ``` then have "norm (f x) \ b * norm x" ``` wenzelm@53688 ` 55` ``` using n0 norm_ge_zero[of x] ``` wenzelm@53688 ` 56` ``` by (auto simp add: field_simps) ``` wenzelm@53253 ` 57` ``` } ``` wenzelm@53688 ` 58` ``` ultimately have "norm (f x) \ b * norm x" ``` wenzelm@53688 ` 59` ``` by blast ``` wenzelm@53253 ` 60` ``` } ``` wenzelm@53253 ` 61` ``` then show ?rhs by blast ``` wenzelm@53253 ` 62` ```qed ``` huffman@36581 ` 63` huffman@36581 ` 64` ```lemma onorm: ``` hoelzl@37489 ` 65` ``` fixes f:: "'a::euclidean_space \ 'b::euclidean_space" ``` huffman@36581 ` 66` ``` assumes lf: "linear f" ``` wenzelm@53253 ` 67` ``` shows "norm (f x) \ onorm f * norm x" ``` wenzelm@53253 ` 68` ``` and "\x. norm (f x) \ b * norm x \ onorm f \ b" ``` wenzelm@53253 ` 69` ```proof - ``` wenzelm@53253 ` 70` ``` let ?S = "{norm (f x) |x. norm x = 1}" ``` wenzelm@53253 ` 71` ``` have "norm (f (SOME i. i \ Basis)) \ ?S" ``` wenzelm@53253 ` 72` ``` by (auto intro!: exI[of _ "SOME i. i \ Basis"] norm_Basis SOME_Basis) ``` wenzelm@53688 ` 73` ``` then have Se: "?S \ {}" ``` wenzelm@53688 ` 74` ``` by auto ``` wenzelm@53253 ` 75` ``` from linear_bounded[OF lf] have b: "\ b. ?S *<= b" ``` wenzelm@53688 ` 76` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` wenzelm@53688 ` 77` ``` by (auto simp add: setle_def) ``` wenzelm@53253 ` 78` ``` from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] ``` wenzelm@53688 ` 79` ``` show "norm (f x) \ onorm f * norm x" ``` wenzelm@53253 ` 80` ``` apply - ``` wenzelm@53253 ` 81` ``` apply (rule spec[where x = x]) ``` wenzelm@53253 ` 82` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` wenzelm@53253 ` 83` ``` apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) ``` wenzelm@53253 ` 84` ``` done ``` wenzelm@53688 ` 85` ``` show "\x. norm (f x) \ b * norm x \ onorm f \ b" ``` wenzelm@53253 ` 86` ``` using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] ``` wenzelm@53253 ` 87` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` wenzelm@53253 ` 88` ``` by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) ``` huffman@36581 ` 89` ```qed ``` huffman@36581 ` 90` wenzelm@53253 ` 91` ```lemma onorm_pos_le: ``` wenzelm@53688 ` 92` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` wenzelm@53688 ` 93` ``` assumes lf: "linear f" ``` wenzelm@53253 ` 94` ``` shows "0 \ onorm f" ``` wenzelm@53253 ` 95` ``` using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \ Basis"]] ``` hoelzl@50526 ` 96` ``` by (simp add: SOME_Basis) ``` huffman@36581 ` 97` wenzelm@53253 ` 98` ```lemma onorm_eq_0: ``` wenzelm@53688 ` 99` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` wenzelm@53688 ` 100` ``` assumes lf: "linear f" ``` huffman@36581 ` 101` ``` shows "onorm f = 0 \ (\x. f x = 0)" ``` huffman@36581 ` 102` ``` using onorm[OF lf] ``` huffman@36581 ` 103` ``` apply (auto simp add: onorm_pos_le) ``` huffman@36581 ` 104` ``` apply atomize ``` huffman@36581 ` 105` ``` apply (erule allE[where x="0::real"]) ``` huffman@36581 ` 106` ``` using onorm_pos_le[OF lf] ``` huffman@36581 ` 107` ``` apply arith ``` huffman@36581 ` 108` ``` done ``` huffman@36581 ` 109` wenzelm@53688 ` 110` ```lemma onorm_const: ``` wenzelm@53688 ` 111` ``` "onorm (\x::'a::euclidean_space. y::'b::euclidean_space) = norm y" ``` wenzelm@53253 ` 112` ```proof - ``` wenzelm@53688 ` 113` ``` let ?f = "\x::'a. y::'b" ``` huffman@36581 ` 114` ``` have th: "{norm (?f x)| x. norm x = 1} = {norm y}" ``` hoelzl@50526 ` 115` ``` by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \ Basis"]) ``` huffman@36581 ` 116` ``` show ?thesis ``` huffman@36581 ` 117` ``` unfolding onorm_def th ``` wenzelm@53253 ` 118` ``` apply (rule cSup_unique) ``` wenzelm@53253 ` 119` ``` apply (simp_all add: setle_def) ``` wenzelm@53253 ` 120` ``` done ``` huffman@36581 ` 121` ```qed ``` huffman@36581 ` 122` wenzelm@53253 ` 123` ```lemma onorm_pos_lt: ``` wenzelm@53688 ` 124` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` wenzelm@53688 ` 125` ``` assumes lf: "linear f" ``` wenzelm@53688 ` 126` ``` shows "0 < onorm f \ \ (\x. f x = 0)" ``` huffman@36581 ` 127` ``` unfolding onorm_eq_0[OF lf, symmetric] ``` huffman@36581 ` 128` ``` using onorm_pos_le[OF lf] by arith ``` huffman@36581 ` 129` huffman@36581 ` 130` ```lemma onorm_compose: ``` wenzelm@53688 ` 131` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` wenzelm@53688 ` 132` ``` and g :: "'k::euclidean_space \ 'n::euclidean_space" ``` wenzelm@53688 ` 133` ``` assumes lf: "linear f" ``` wenzelm@53688 ` 134` ``` and lg: "linear g" ``` wenzelm@53688 ` 135` ``` shows "onorm (f \ g) \ onorm f * onorm g" ``` wenzelm@53253 ` 136` ``` apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) ``` wenzelm@53253 ` 137` ``` unfolding o_def ``` wenzelm@53253 ` 138` ``` apply (subst mult_assoc) ``` wenzelm@53253 ` 139` ``` apply (rule order_trans) ``` wenzelm@53253 ` 140` ``` apply (rule onorm(1)[OF lf]) ``` wenzelm@53253 ` 141` ``` apply (rule mult_left_mono) ``` wenzelm@53253 ` 142` ``` apply (rule onorm(1)[OF lg]) ``` wenzelm@53253 ` 143` ``` apply (rule onorm_pos_le[OF lf]) ``` wenzelm@53253 ` 144` ``` done ``` huffman@36581 ` 145` wenzelm@53253 ` 146` ```lemma onorm_neg_lemma: ``` wenzelm@53688 ` 147` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` wenzelm@53688 ` 148` ``` assumes lf: "linear f" ``` huffman@36581 ` 149` ``` shows "onorm (\x. - f x) \ onorm f" ``` huffman@36581 ` 150` ``` using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] ``` huffman@36581 ` 151` ``` unfolding norm_minus_cancel by metis ``` huffman@36581 ` 152` wenzelm@53253 ` 153` ```lemma onorm_neg: ``` wenzelm@53688 ` 154` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` wenzelm@53688 ` 155` ``` assumes lf: "linear f" ``` huffman@36581 ` 156` ``` shows "onorm (\x. - f x) = onorm f" ``` huffman@36581 ` 157` ``` using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] ``` huffman@36581 ` 158` ``` by simp ``` huffman@36581 ` 159` huffman@36581 ` 160` ```lemma onorm_triangle: ``` wenzelm@53688 ` 161` ``` fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" ``` wenzelm@53688 ` 162` ``` assumes lf: "linear f" ``` wenzelm@53253 ` 163` ``` and lg: "linear g" ``` wenzelm@53253 ` 164` ``` shows "onorm (\x. f x + g x) \ onorm f + onorm g" ``` huffman@36581 ` 165` ``` apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) ``` huffman@36581 ` 166` ``` apply (rule order_trans) ``` huffman@36581 ` 167` ``` apply (rule norm_triangle_ineq) ``` huffman@36581 ` 168` ``` apply (simp add: distrib) ``` huffman@36581 ` 169` ``` apply (rule add_mono) ``` huffman@36581 ` 170` ``` apply (rule onorm(1)[OF lf]) ``` huffman@36581 ` 171` ``` apply (rule onorm(1)[OF lg]) ``` huffman@36581 ` 172` ``` done ``` huffman@36581 ` 173` wenzelm@53253 ` 174` ```lemma onorm_triangle_le: ``` wenzelm@53688 ` 175` ``` fixes f :: "'n::euclidean_space \ 'm::euclidean_space" ``` wenzelm@53688 ` 176` ``` assumes "linear f" ``` wenzelm@53688 ` 177` ``` and "linear g" ``` wenzelm@53688 ` 178` ``` and "onorm f + onorm g \ e" ``` wenzelm@53688 ` 179` ``` shows "onorm (\x. f x + g x) \ e" ``` huffman@36581 ` 180` ``` apply (rule order_trans) ``` huffman@36581 ` 181` ``` apply (rule onorm_triangle) ``` wenzelm@53688 ` 182` ``` apply (rule assms)+ ``` huffman@36581 ` 183` ``` done ``` huffman@36581 ` 184` wenzelm@53253 ` 185` ```lemma onorm_triangle_lt: ``` wenzelm@53688 ` 186` ``` fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" ``` wenzelm@53688 ` 187` ``` assumes "linear f" ``` wenzelm@53688 ` 188` ``` and "linear g" ``` wenzelm@53688 ` 189` ``` and "onorm f + onorm g < e" ``` wenzelm@53688 ` 190` ``` shows "onorm (\x. f x + g x) < e" ``` huffman@36581 ` 191` ``` apply (rule order_le_less_trans) ``` huffman@36581 ` 192` ``` apply (rule onorm_triangle) ``` wenzelm@53688 ` 193` ``` apply (rule assms)+ ``` wenzelm@53253 ` 194` ``` done ``` huffman@36581 ` 195` huffman@36581 ` 196` ```end ```