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