# HG changeset patch # User huffman # Date 1395287424 25200 # Node ID 7696903b9e61efd2b8630a77dd4e716e48fc0a0a # Parent 6599c627854544640bf07b88d6866c5b4fbe9fc6 generalize theory of operator norms to work with class real_normed_vector diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Mar 19 23:13:45 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Mar 19 20:50:24 2014 -0700 @@ -269,7 +269,7 @@ case goal1 then show ?case using differentiable_bound[OF assms(1) d0', of 0 x y] and `x \ s` - unfolding onorm_const + unfolding onorm_zero by auto qed then show ?thesis @@ -1128,11 +1128,10 @@ and "x \ s" "y \ s" shows "norm(f x - f y) \ B * norm(x - y)" apply (rule differentiable_bound [OF cvs]) - using assms - apply (auto simp: has_field_derivative_def Ball_def onorm_def) - apply (rule cSUP_least) - apply (auto simp: norm_mult) - apply (metis norm_one) + apply (rule ballI, erule df [unfolded has_field_derivative_def]) + apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn) + apply fact + apply fact done subsection{*Inverse function theorem for complex derivatives.*} @@ -1405,4 +1404,3 @@ qed end - diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 19 23:13:45 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 19 20:50:24 2014 -0700 @@ -766,7 +766,7 @@ text {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *} lemma mvt_general: - fixes f :: "real \ 'a::euclidean_space" + fixes f :: "real \ 'a::real_inner" assumes "a < b" and "continuous_on {a .. b} f" and "\x\{a<.. 'b::euclidean_space" + fixes f :: "'a::real_normed_vector \ 'b::real_inner" assumes "convex s" and "\x\s. (f has_derivative f' x) (at x within s)" and "\x\s. onorm (f' x) \ B" @@ -863,7 +863,7 @@ proof - case goal1 have "norm (f' x y) \ onorm (f' x) * norm y" - by (rule onorm(1)[OF derivative_is_linear[OF assms(2)[rule_format,OF goal1]]]) + by (rule onorm[OF derivative_linear[OF assms(2)[rule_format,OF goal1]]]) also have "\ \ B * norm y" apply (rule mult_right_mono) using assms(3)[rule_format,OF goal1] @@ -885,19 +885,6 @@ by (auto simp add: norm_minus_commute) qed -lemma differentiable_bound_real: - fixes f :: "real \ real" - assumes "convex s" - and "\x\s. (f has_derivative f' x) (at x within s)" - and "\x\s. onorm (f' x) \ B" - and x: "x \ s" - and y: "y \ s" - shows "norm (f x - f y) \ B * norm (x - y)" - using differentiable_bound[of s f f' B x y] - unfolding Ball_def image_iff o_def - using assms - by auto - text {* In particular. *} lemma has_derivative_zero_constant: @@ -913,8 +900,8 @@ proof - case goal1 then show ?case - using differentiable_bound_real[OF assms(1-2), of 0 x y] and `x \ s` - unfolding onorm_const + using differentiable_bound[OF assms(1-2), of 0 x y] and `x \ s` + unfolding onorm_zero by auto qed then show ?thesis @@ -1526,7 +1513,7 @@ apply auto done then have *: "0 < onorm g'" - unfolding onorm_pos_lt[OF assms(3)[unfolded linear_linear]] + unfolding onorm_pos_lt[OF assms(3)] by fastforce def k \ "1 / onorm g' / 2" have *: "k > 0" @@ -1590,14 +1577,13 @@ have "onorm (\v. v - g' (f' u v)) \ onorm g' * onorm (\w. f' a w - f' u w)" unfolding * apply (rule onorm_compose) - unfolding linear_conv_bounded_linear apply (rule assms(3) **)+ done also have "\ \ onorm g' * k" apply (rule mult_left_mono) using d1(2)[of u] - using onorm_neg[OF **(1)[unfolded linear_linear]] - using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] + using onorm_neg[where f="\x. f' u x - f' a x"] + using d and u and onorm_pos_le[OF assms(3)] apply (auto simp add: algebra_simps) done also have "\ \ 1 / 2" @@ -1652,10 +1638,7 @@ } then show "onorm (\h. f' m x h - f' n x h) \ 2 * e" apply - - apply (rule onorm(2)) - apply (rule linear_compose_sub) - unfolding linear_conv_bounded_linear - using assms(2)[rule_format,OF `x \ s`, THEN derivative_linear] + apply (rule onorm_le) apply auto done qed diff -r 6599c6278545 -r 7696903b9e61 src/HOL/Multivariate_Analysis/Operator_Norm.thy --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Mar 19 23:13:45 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Mar 19 20:50:24 2014 -0700 @@ -1,5 +1,6 @@ (* Title: HOL/Multivariate_Analysis/Operator_Norm.thy Author: Amine Chaieb, University of Cambridge + Author: Brian Huffman *) header {* Operator Norm *} @@ -8,176 +9,176 @@ imports Linear_Algebra begin -definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))" +text {* This formulation yields zero if @{text 'a} is the trivial vector space. *} + +definition onorm :: "('a::real_normed_vector \ 'b::real_normed_vector) \ real" + where "onorm f = (SUP x. norm (f x) / norm x)" + +lemma onorm_bound: + assumes "0 \ b" and "\x. norm (f x) \ b * norm x" + shows "onorm f \ b" + unfolding onorm_def +proof (rule cSUP_least) + fix x + show "norm (f x) / norm x \ b" + using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq) +qed simp + +text {* In non-trivial vector spaces, the first assumption is redundant. *} -lemma norm_bound_generalize: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" - shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" - (is "?lhs \ ?rhs") -proof - assume H: ?rhs - { - fix x :: "'a" - assume x: "norm x = 1" - from H[rule_format, of x] x have "norm (f x) \ b" - by simp - } - then show ?lhs by blast -next - assume H: ?lhs - have bp: "b \ 0" - apply - - apply (rule order_trans [OF norm_ge_zero]) - apply (rule H[rule_format, of "SOME x::'a. x \ Basis"]) - apply (auto intro: SOME_Basis norm_Basis) - done - { - fix x :: "'a" - { - assume "x = 0" - then have "norm (f x) \ b * norm x" - by (simp add: linear_0[OF lf] bp) - } - moreover - { - assume x0: "x \ 0" - then have n0: "norm x \ 0" - by (metis norm_eq_zero) - let ?c = "1/ norm x" - have "norm (?c *\<^sub>R x) = 1" - using x0 by (simp add: n0) - with H have "norm (f (?c *\<^sub>R x)) \ b" - by blast - then have "?c * norm (f x) \ b" - by (simp add: linear_cmul[OF lf]) - then have "norm (f x) \ b * norm x" - using n0 norm_ge_zero[of x] - by (auto simp add: field_simps) - } - ultimately have "norm (f x) \ b * norm x" - by blast - } - then show ?rhs by blast +lemma onorm_le: + fixes f :: "'a::{real_normed_vector, perfect_space} \ 'b::real_normed_vector" + assumes "\x. norm (f x) \ b * norm x" + shows "onorm f \ b" +proof (rule onorm_bound [OF _ assms]) + have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV) + then obtain a :: 'a where "a \ 0" by fast + have "0 \ b * norm a" + by (rule order_trans [OF norm_ge_zero assms]) + with `a \ 0` show "0 \ b" + by (simp add: zero_le_mult_iff) +qed + +lemma le_onorm: + assumes "bounded_linear f" + shows "norm (f x) / norm x \ onorm f" +proof - + interpret f: bounded_linear f by fact + obtain b where "0 \ b" and "\x. norm (f x) \ norm x * b" + using f.nonneg_bounded by auto + then have "\x. norm (f x) / norm x \ b" + by (clarify, case_tac "x = 0", + simp_all add: f.zero pos_divide_le_eq mult_commute) + then have "bdd_above (range (\x. norm (f x) / norm x))" + unfolding bdd_above_def by fast + with UNIV_I show ?thesis + unfolding onorm_def by (rule cSUP_upper) qed lemma onorm: - fixes f:: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" + assumes "bounded_linear f" shows "norm (f x) \ onorm f * norm x" - and "\x. norm (f x) \ b * norm x \ onorm f \ b" proof - - let ?S = "(\x. norm (f x))`{x. norm x = 1}" - have "norm (f (SOME i. i \ Basis)) \ ?S" - by (auto intro!: exI[of _ "SOME i. i \ Basis"] norm_Basis SOME_Basis) - then have Se: "?S \ {}" - by auto - from linear_bounded[OF lf] have b: "bdd_above ?S" - unfolding norm_bound_generalize[OF lf, symmetric] by auto - then show "norm (f x) \ onorm f * norm x" - apply - - apply (rule spec[where x = x]) - unfolding norm_bound_generalize[OF lf, symmetric] - apply (auto simp: onorm_def intro!: cSUP_upper) - done - show "\x. norm (f x) \ b * norm x \ onorm f \ b" - unfolding norm_bound_generalize[OF lf, symmetric] - using Se by (auto simp: onorm_def intro!: cSUP_least b) + interpret f: bounded_linear f by fact + show ?thesis + proof (cases) + assume "x = 0" + then show ?thesis by (simp add: f.zero) + next + assume "x \ 0" + have "norm (f x) / norm x \ onorm f" + by (rule le_onorm [OF assms]) + then show "norm (f x) \ onorm f * norm x" + by (simp add: pos_divide_le_eq `x \ 0`) + qed qed lemma onorm_pos_le: - fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - assumes lf: "linear f" + assumes f: "bounded_linear f" shows "0 \ onorm f" - using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \ Basis"]] - by (simp add: SOME_Basis) + using le_onorm [OF f, where x=0] by simp + +lemma onorm_zero: "onorm (\x. 0) = 0" +proof (rule order_antisym) + show "onorm (\x. 0) \ 0" + by (simp add: onorm_bound) + show "0 \ onorm (\x. 0)" + using bounded_linear_zero by (rule onorm_pos_le) +qed lemma onorm_eq_0: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" + assumes f: "bounded_linear f" shows "onorm f = 0 \ (\x. f x = 0)" - using onorm[OF lf] - apply (auto simp add: onorm_pos_le) - apply atomize - apply (erule allE[where x="0::real"]) - using onorm_pos_le[OF lf] - apply arith - done - -lemma onorm_const: "onorm (\x::'a::euclidean_space. y::'b::euclidean_space) = norm y" - using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis) + using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero) lemma onorm_pos_lt: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" + assumes f: "bounded_linear f" shows "0 < onorm f \ \ (\x. f x = 0)" - unfolding onorm_eq_0[OF lf, symmetric] - using onorm_pos_le[OF lf] by arith + by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f]) lemma onorm_compose: - fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - and g :: "'k::euclidean_space \ 'n::euclidean_space" - assumes lf: "linear f" - and lg: "linear g" + assumes f: "bounded_linear f" + assumes g: "bounded_linear g" shows "onorm (f \ g) \ onorm f * onorm g" - apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) - unfolding o_def - apply (subst mult_assoc) - apply (rule order_trans) - apply (rule onorm(1)[OF lf]) - apply (rule mult_left_mono) - apply (rule onorm(1)[OF lg]) - apply (rule onorm_pos_le[OF lf]) - done +proof (rule onorm_bound) + show "0 \ onorm f * onorm g" + by (intro mult_nonneg_nonneg onorm_pos_le f g) +next + fix x + have "norm (f (g x)) \ onorm f * norm (g x)" + by (rule onorm [OF f]) + also have "onorm f * norm (g x) \ onorm f * (onorm g * norm x)" + by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]]) + finally show "norm ((f \ g) x) \ onorm f * onorm g * norm x" + by (simp add: mult_assoc) +qed -lemma onorm_neg_lemma: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" - shows "onorm (\x. - f x) \ onorm f" - using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] - unfolding norm_minus_cancel by metis +lemma onorm_scaleR_lemma: + assumes f: "bounded_linear f" + shows "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f" +proof (rule onorm_bound) + show "0 \ \r\ * onorm f" + by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f) +next + fix x + have "\r\ * norm (f x) \ \r\ * (onorm f * norm x)" + by (intro mult_left_mono onorm abs_ge_zero f) + then show "norm (r *\<^sub>R f x) \ \r\ * onorm f * norm x" + by (simp only: norm_scaleR mult_assoc) +qed + +lemma onorm_scaleR: + assumes f: "bounded_linear f" + shows "onorm (\x. r *\<^sub>R f x) = \r\ * onorm f" +proof (cases "r = 0") + assume "r \ 0" + show ?thesis + proof (rule order_antisym) + show "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f" + using f by (rule onorm_scaleR_lemma) + next + have "bounded_linear (\x. r *\<^sub>R f x)" + using bounded_linear_scaleR_right f by (rule bounded_linear_compose) + then have "onorm (\x. inverse r *\<^sub>R r *\<^sub>R f x) \ \inverse r\ * onorm (\x. r *\<^sub>R f x)" + by (rule onorm_scaleR_lemma) + with `r \ 0` show "\r\ * onorm f \ onorm (\x. r *\<^sub>R f x)" + by (simp add: inverse_eq_divide pos_le_divide_eq mult_commute) + qed +qed (simp add: onorm_zero) lemma onorm_neg: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes lf: "linear f" shows "onorm (\x. - f x) = onorm f" - using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] - by simp + unfolding onorm_def by simp lemma onorm_triangle: - fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" - assumes lf: "linear f" - and lg: "linear g" + assumes f: "bounded_linear f" + assumes g: "bounded_linear g" shows "onorm (\x. f x + g x) \ onorm f + onorm g" - apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) - apply (rule order_trans) - apply (rule norm_triangle_ineq) - apply (simp add: distrib) - apply (rule add_mono) - apply (rule onorm(1)[OF lf]) - apply (rule onorm(1)[OF lg]) - done +proof (rule onorm_bound) + show "0 \ onorm f + onorm g" + by (intro add_nonneg_nonneg onorm_pos_le f g) +next + fix x + have "norm (f x + g x) \ norm (f x) + norm (g x)" + by (rule norm_triangle_ineq) + also have "norm (f x) + norm (g x) \ onorm f * norm x + onorm g * norm x" + by (intro add_mono onorm f g) + finally show "norm (f x + g x) \ (onorm f + onorm g) * norm x" + by (simp only: distrib_right) +qed lemma onorm_triangle_le: - fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - assumes "linear f" - and "linear g" - and "onorm f + onorm g \ e" + assumes "bounded_linear f" + assumes "bounded_linear g" + assumes "onorm f + onorm g \ e" shows "onorm (\x. f x + g x) \ e" - apply (rule order_trans) - apply (rule onorm_triangle) - apply (rule assms)+ - done + using assms by (rule onorm_triangle [THEN order_trans]) lemma onorm_triangle_lt: - fixes f g :: "'n::euclidean_space \ 'm::euclidean_space" - assumes "linear f" - and "linear g" - and "onorm f + onorm g < e" + assumes "bounded_linear f" + assumes "bounded_linear g" + assumes "onorm f + onorm g < e" shows "onorm (\x. f x + g x) < e" - apply (rule order_le_less_trans) - apply (rule onorm_triangle) - apply (rule assms)+ - done + using assms by (rule onorm_triangle [THEN order_le_less_trans]) end