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