src/HOL/Multivariate_Analysis/Operator_Norm.thy
 author huffman Wed Apr 28 15:05:45 2010 -0700 (2010-04-28) changeset 36581 bbea7f52e8e1 child 36593 fb69c8cd27bd permissions -rw-r--r--
move operator norm stuff to new theory file
 huffman@36581 ` 1` ```(* Title: Library/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@36581 ` 8` ```imports Euclidean_Space ``` 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: ``` huffman@36581 ` 14` ``` fixes f:: "real ^'n \ real^'m" ``` huffman@36581 ` 15` ``` assumes lf: "linear f" ``` huffman@36581 ` 16` ``` shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") ``` huffman@36581 ` 17` ```proof- ``` huffman@36581 ` 18` ``` {assume H: ?rhs ``` huffman@36581 ` 19` ``` {fix x :: "real^'n" assume x: "norm x = 1" ``` huffman@36581 ` 20` ``` from H[rule_format, of x] x have "norm (f x) \ b" by simp} ``` huffman@36581 ` 21` ``` then have ?lhs by blast } ``` huffman@36581 ` 22` huffman@36581 ` 23` ``` moreover ``` huffman@36581 ` 24` ``` {assume H: ?lhs ``` huffman@36581 ` 25` ``` from H[rule_format, of "basis arbitrary"] ``` huffman@36581 ` 26` ``` have bp: "b \ 0" using norm_ge_zero[of "f (basis arbitrary)"] ``` huffman@36581 ` 27` ``` by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero]) ``` huffman@36581 ` 28` ``` {fix x :: "real ^'n" ``` huffman@36581 ` 29` ``` {assume "x = 0" ``` huffman@36581 ` 30` ``` then have "norm (f x) \ b * norm x" by (simp add: linear_0[OF lf] bp)} ``` huffman@36581 ` 31` ``` moreover ``` huffman@36581 ` 32` ``` {assume x0: "x \ 0" ``` huffman@36581 ` 33` ``` hence n0: "norm x \ 0" by (metis norm_eq_zero) ``` huffman@36581 ` 34` ``` let ?c = "1/ norm x" ``` huffman@36581 ` 35` ``` have "norm (?c*s x) = 1" using x0 by (simp add: n0) ``` huffman@36581 ` 36` ``` with H have "norm (f(?c*s x)) \ b" by blast ``` huffman@36581 ` 37` ``` hence "?c * norm (f x) \ b" ``` huffman@36581 ` 38` ``` by (simp add: linear_cmul[OF lf]) ``` huffman@36581 ` 39` ``` hence "norm (f x) \ b * norm x" ``` huffman@36581 ` 40` ``` using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} ``` huffman@36581 ` 41` ``` ultimately have "norm (f x) \ b * norm x" by blast} ``` huffman@36581 ` 42` ``` then have ?rhs by blast} ``` huffman@36581 ` 43` ``` ultimately show ?thesis by blast ``` huffman@36581 ` 44` ```qed ``` huffman@36581 ` 45` huffman@36581 ` 46` ```lemma onorm: ``` huffman@36581 ` 47` ``` fixes f:: "real ^'n \ real ^'m" ``` huffman@36581 ` 48` ``` assumes lf: "linear f" ``` huffman@36581 ` 49` ``` shows "norm (f x) <= onorm f * norm x" ``` huffman@36581 ` 50` ``` and "\x. norm (f x) <= b * norm x \ onorm f <= b" ``` huffman@36581 ` 51` ```proof- ``` huffman@36581 ` 52` ``` { ``` huffman@36581 ` 53` ``` let ?S = "{norm (f x) |x. norm x = 1}" ``` huffman@36581 ` 54` ``` have Se: "?S \ {}" using norm_basis by auto ``` huffman@36581 ` 55` ``` from linear_bounded[OF lf] have b: "\ b. ?S *<= b" ``` huffman@36581 ` 56` ``` unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) ``` huffman@36581 ` 57` ``` {from Sup[OF Se b, unfolded onorm_def[symmetric]] ``` huffman@36581 ` 58` ``` show "norm (f x) <= onorm f * norm x" ``` huffman@36581 ` 59` ``` apply - ``` huffman@36581 ` 60` ``` apply (rule spec[where x = x]) ``` huffman@36581 ` 61` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` huffman@36581 ` 62` ``` by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} ``` huffman@36581 ` 63` ``` { ``` huffman@36581 ` 64` ``` show "\x. norm (f x) <= b * norm x \ onorm f <= b" ``` huffman@36581 ` 65` ``` using Sup[OF Se b, unfolded onorm_def[symmetric]] ``` huffman@36581 ` 66` ``` unfolding norm_bound_generalize[OF lf, symmetric] ``` huffman@36581 ` 67` ``` by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} ``` huffman@36581 ` 68` ``` } ``` huffman@36581 ` 69` ```qed ``` huffman@36581 ` 70` huffman@36581 ` 71` ```lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "0 <= onorm f" ``` huffman@36581 ` 72` ``` using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp ``` huffman@36581 ` 73` huffman@36581 ` 74` ```lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \ real ^'m)" ``` huffman@36581 ` 75` ``` shows "onorm f = 0 \ (\x. f x = 0)" ``` huffman@36581 ` 76` ``` using onorm[OF lf] ``` huffman@36581 ` 77` ``` apply (auto simp add: onorm_pos_le) ``` huffman@36581 ` 78` ``` apply atomize ``` huffman@36581 ` 79` ``` apply (erule allE[where x="0::real"]) ``` huffman@36581 ` 80` ``` using onorm_pos_le[OF lf] ``` huffman@36581 ` 81` ``` apply arith ``` huffman@36581 ` 82` ``` done ``` huffman@36581 ` 83` huffman@36581 ` 84` ```lemma onorm_const: "onorm(\x::real^'n. (y::real ^'m)) = norm y" ``` huffman@36581 ` 85` ```proof- ``` huffman@36581 ` 86` ``` let ?f = "\x::real^'n. (y::real ^ 'm)" ``` huffman@36581 ` 87` ``` have th: "{norm (?f x)| x. norm x = 1} = {norm y}" ``` huffman@36581 ` 88` ``` by(auto intro: vector_choose_size set_ext) ``` huffman@36581 ` 89` ``` show ?thesis ``` huffman@36581 ` 90` ``` unfolding onorm_def th ``` huffman@36581 ` 91` ``` apply (rule Sup_unique) by (simp_all add: setle_def) ``` huffman@36581 ` 92` ```qed ``` huffman@36581 ` 93` huffman@36581 ` 94` ```lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \ real ^'m)" ``` huffman@36581 ` 95` ``` shows "0 < onorm f \ ~(\x. f x = 0)" ``` huffman@36581 ` 96` ``` unfolding onorm_eq_0[OF lf, symmetric] ``` huffman@36581 ` 97` ``` using onorm_pos_le[OF lf] by arith ``` huffman@36581 ` 98` huffman@36581 ` 99` ```lemma onorm_compose: ``` huffman@36581 ` 100` ``` assumes lf: "linear (f::real ^'n \ real ^'m)" ``` huffman@36581 ` 101` ``` and lg: "linear (g::real^'k \ real^'n)" ``` huffman@36581 ` 102` ``` shows "onorm (f o g) <= onorm f * onorm g" ``` huffman@36581 ` 103` ``` apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) ``` huffman@36581 ` 104` ``` unfolding o_def ``` huffman@36581 ` 105` ``` apply (subst mult_assoc) ``` huffman@36581 ` 106` ``` apply (rule order_trans) ``` huffman@36581 ` 107` ``` apply (rule onorm(1)[OF lf]) ``` huffman@36581 ` 108` ``` apply (rule mult_mono1) ``` huffman@36581 ` 109` ``` apply (rule onorm(1)[OF lg]) ``` huffman@36581 ` 110` ``` apply (rule onorm_pos_le[OF lf]) ``` huffman@36581 ` 111` ``` done ``` huffman@36581 ` 112` huffman@36581 ` 113` ```lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \ real^'m)" ``` huffman@36581 ` 114` ``` shows "onorm (\x. - f x) \ onorm f" ``` huffman@36581 ` 115` ``` using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] ``` huffman@36581 ` 116` ``` unfolding norm_minus_cancel by metis ``` huffman@36581 ` 117` huffman@36581 ` 118` ```lemma onorm_neg: assumes lf: "linear (f::real ^'n \ real^'m)" ``` huffman@36581 ` 119` ``` shows "onorm (\x. - f x) = onorm f" ``` huffman@36581 ` 120` ``` using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] ``` huffman@36581 ` 121` ``` by simp ``` huffman@36581 ` 122` huffman@36581 ` 123` ```lemma onorm_triangle: ``` huffman@36581 ` 124` ``` assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" ``` huffman@36581 ` 125` ``` shows "onorm (\x. f x + g x) <= onorm f + onorm g" ``` huffman@36581 ` 126` ``` apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) ``` huffman@36581 ` 127` ``` apply (rule order_trans) ``` huffman@36581 ` 128` ``` apply (rule norm_triangle_ineq) ``` huffman@36581 ` 129` ``` apply (simp add: distrib) ``` huffman@36581 ` 130` ``` apply (rule add_mono) ``` huffman@36581 ` 131` ``` apply (rule onorm(1)[OF lf]) ``` huffman@36581 ` 132` ``` apply (rule onorm(1)[OF lg]) ``` huffman@36581 ` 133` ``` done ``` huffman@36581 ` 134` huffman@36581 ` 135` ```lemma onorm_triangle_le: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) <= e ``` huffman@36581 ` 136` ``` \ onorm(\x. f x + g x) <= e" ``` huffman@36581 ` 137` ``` apply (rule order_trans) ``` huffman@36581 ` 138` ``` apply (rule onorm_triangle) ``` huffman@36581 ` 139` ``` apply assumption+ ``` huffman@36581 ` 140` ``` done ``` huffman@36581 ` 141` huffman@36581 ` 142` ```lemma onorm_triangle_lt: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) < e ``` huffman@36581 ` 143` ``` ==> onorm(\x. f x + g x) < e" ``` huffman@36581 ` 144` ``` apply (rule order_le_less_trans) ``` huffman@36581 ` 145` ``` apply (rule onorm_triangle) ``` huffman@36581 ` 146` ``` by assumption+ ``` huffman@36581 ` 147` huffman@36581 ` 148` ```end ```