wenzelm@41959: (* Title: HOL/Multivariate_Analysis/Operator_Norm.thy huffman@36581: Author: Amine Chaieb, University of Cambridge huffman@36581: *) huffman@36581: huffman@36581: header {* Operator Norm *} huffman@36581: huffman@36581: theory Operator_Norm huffman@44133: imports Linear_Algebra huffman@36581: begin huffman@36581: huffman@36581: definition "onorm f = Sup {norm (f x)| x. norm x = 1}" huffman@36581: huffman@36581: lemma norm_bound_generalize: wenzelm@53253: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" huffman@36581: assumes lf: "linear f" wenzelm@53253: shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" wenzelm@53253: (is "?lhs \ ?rhs") wenzelm@53253: proof wenzelm@53253: assume H: ?rhs wenzelm@53253: { wenzelm@53253: fix x :: "'a" wenzelm@53253: assume x: "norm x = 1" wenzelm@53253: from H[rule_format, of x] x have "norm (f x) \ b" by simp wenzelm@53253: } wenzelm@53253: then show ?lhs by blast wenzelm@53253: next wenzelm@53253: assume H: ?lhs wenzelm@53253: have bp: "b \ 0" wenzelm@53253: apply - wenzelm@53253: apply (rule order_trans [OF norm_ge_zero]) wenzelm@53253: apply (rule H[rule_format, of "SOME x::'a. x \ Basis"]) wenzelm@53253: apply (auto intro: SOME_Basis norm_Basis) wenzelm@53253: done wenzelm@53253: { wenzelm@53253: fix x :: "'a" wenzelm@53253: { wenzelm@53253: assume "x = 0" wenzelm@53253: then have "norm (f x) \ b * norm x" wenzelm@53253: by (simp add: linear_0[OF lf] bp) wenzelm@53253: } wenzelm@53253: moreover wenzelm@53253: { wenzelm@53253: assume x0: "x \ 0" wenzelm@53253: then have n0: "norm x \ 0" by (metis norm_eq_zero) wenzelm@53253: let ?c = "1/ norm x" wenzelm@53253: have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0) wenzelm@53253: with H have "norm (f (?c *\<^sub>R x)) \ b" by blast wenzelm@53253: then have "?c * norm (f x) \ b" wenzelm@53253: by (simp add: linear_cmul[OF lf]) wenzelm@53253: then have "norm (f x) \ b * norm x" wenzelm@53253: using n0 norm_ge_zero[of x] by (auto simp add: field_simps) wenzelm@53253: } wenzelm@53253: ultimately have "norm (f x) \ b * norm x" by blast wenzelm@53253: } wenzelm@53253: then show ?rhs by blast wenzelm@53253: qed huffman@36581: huffman@36581: lemma onorm: hoelzl@37489: fixes f:: "'a::euclidean_space \ 'b::euclidean_space" huffman@36581: assumes lf: "linear f" wenzelm@53253: shows "norm (f x) \ onorm f * norm x" wenzelm@53253: and "\x. norm (f x) \ b * norm x \ onorm f \ b" wenzelm@53253: proof - wenzelm@53253: let ?S = "{norm (f x) |x. norm x = 1}" wenzelm@53253: have "norm (f (SOME i. i \ Basis)) \ ?S" wenzelm@53253: by (auto intro!: exI[of _ "SOME i. i \ Basis"] norm_Basis SOME_Basis) wenzelm@53253: then have Se: "?S \ {}" by auto wenzelm@53253: from linear_bounded[OF lf] have b: "\ b. ?S *<= b" wenzelm@53253: unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) wenzelm@53253: from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] wenzelm@53253: show "norm (f x) <= onorm f * norm x" wenzelm@53253: apply - wenzelm@53253: apply (rule spec[where x = x]) wenzelm@53253: unfolding norm_bound_generalize[OF lf, symmetric] wenzelm@53253: apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) wenzelm@53253: done wenzelm@53253: show "\x. norm (f x) <= b * norm x \ onorm f <= b" wenzelm@53253: using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] wenzelm@53253: unfolding norm_bound_generalize[OF lf, symmetric] wenzelm@53253: by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) huffman@36581: qed huffman@36581: wenzelm@53253: lemma onorm_pos_le: wenzelm@53253: assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" wenzelm@53253: shows "0 \ onorm f" wenzelm@53253: using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \ Basis"]] hoelzl@50526: by (simp add: SOME_Basis) huffman@36581: wenzelm@53253: lemma onorm_eq_0: wenzelm@53253: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" huffman@36581: shows "onorm f = 0 \ (\x. f x = 0)" huffman@36581: using onorm[OF lf] huffman@36581: apply (auto simp add: onorm_pos_le) huffman@36581: apply atomize huffman@36581: apply (erule allE[where x="0::real"]) huffman@36581: using onorm_pos_le[OF lf] huffman@36581: apply arith huffman@36581: done huffman@36581: hoelzl@37489: lemma onorm_const: "onorm(\x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y" wenzelm@53253: proof - hoelzl@37489: let ?f = "\x::'a. (y::'b)" huffman@36581: have th: "{norm (?f x)| x. norm x = 1} = {norm y}" hoelzl@50526: by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \ Basis"]) huffman@36581: show ?thesis huffman@36581: unfolding onorm_def th wenzelm@53253: apply (rule cSup_unique) wenzelm@53253: apply (simp_all add: setle_def) wenzelm@53253: done huffman@36581: qed huffman@36581: wenzelm@53253: lemma onorm_pos_lt: wenzelm@53253: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" huffman@36581: shows "0 < onorm f \ ~(\x. f x = 0)" huffman@36581: unfolding onorm_eq_0[OF lf, symmetric] huffman@36581: using onorm_pos_le[OF lf] by arith huffman@36581: huffman@36581: lemma onorm_compose: hoelzl@37489: assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" wenzelm@53253: and lg: "linear (g::'k::euclidean_space \ 'n::euclidean_space)" wenzelm@53253: shows "onorm (f o g) \ onorm f * onorm g" wenzelm@53253: apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) wenzelm@53253: unfolding o_def wenzelm@53253: apply (subst mult_assoc) wenzelm@53253: apply (rule order_trans) wenzelm@53253: apply (rule onorm(1)[OF lf]) wenzelm@53253: apply (rule mult_left_mono) wenzelm@53253: apply (rule onorm(1)[OF lg]) wenzelm@53253: apply (rule onorm_pos_le[OF lf]) wenzelm@53253: done huffman@36581: wenzelm@53253: lemma onorm_neg_lemma: wenzelm@53253: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" huffman@36581: shows "onorm (\x. - f x) \ onorm f" huffman@36581: using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] huffman@36581: unfolding norm_minus_cancel by metis huffman@36581: wenzelm@53253: lemma onorm_neg: wenzelm@53253: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" huffman@36581: shows "onorm (\x. - f x) = onorm f" huffman@36581: using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] huffman@36581: by simp huffman@36581: huffman@36581: lemma onorm_triangle: wenzelm@53253: assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" wenzelm@53253: and lg: "linear g" wenzelm@53253: shows "onorm (\x. f x + g x) \ onorm f + onorm g" huffman@36581: apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) huffman@36581: apply (rule order_trans) huffman@36581: apply (rule norm_triangle_ineq) huffman@36581: apply (simp add: distrib) huffman@36581: apply (rule add_mono) huffman@36581: apply (rule onorm(1)[OF lf]) huffman@36581: apply (rule onorm(1)[OF lg]) huffman@36581: done huffman@36581: wenzelm@53253: lemma onorm_triangle_le: wenzelm@53253: "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ wenzelm@53253: linear g \ onorm f + onorm g \ e \ onorm (\x. f x + g x) \ e" huffman@36581: apply (rule order_trans) huffman@36581: apply (rule onorm_triangle) huffman@36581: apply assumption+ huffman@36581: done huffman@36581: wenzelm@53253: lemma onorm_triangle_lt: wenzelm@53253: "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ linear g \ wenzelm@53253: onorm f + onorm g < e \ onorm(\x. f x + g x) < e" huffman@36581: apply (rule order_le_less_trans) huffman@36581: apply (rule onorm_triangle) wenzelm@53253: apply assumption+ wenzelm@53253: done huffman@36581: huffman@36581: end