# HG changeset patch # User huffman # Date 1173904828 -3600 # Node ID 15d9ed9b505127356e96c1a3f507f78ec60fdc50 # Parent 7da872d34ace8d0893847c6e7d61df48818a1598 move bounded (bi)linear operator locales from Lim.thy to RealVector.thy diff -r 7da872d34ace -r 15d9ed9b5051 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Wed Mar 14 01:35:02 2007 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Wed Mar 14 21:40:28 2007 +0100 @@ -292,25 +292,7 @@ finally show "norm (g x - 0) \ norm (f x - 0)" . qed -subsubsection {* Bounded Linear Operators *} - -locale bounded_linear = additive + - constrains f :: "'a::real_normed_vector \ 'b::real_normed_vector" - assumes scaleR: "f (scaleR r x) = scaleR r (f x)" - assumes bounded: "\K. \x. norm (f x) \ norm x * K" - -lemma (in bounded_linear) pos_bounded: - "\K>0. \x. norm (f x) \ norm x * K" -apply (cut_tac bounded, erule exE) -apply (rule_tac x="max 1 K" in exI, safe) -apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) -apply (drule spec, erule order_trans) -apply (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) -done - -lemma (in bounded_linear) pos_boundedE: - obtains K where "0 < K" and "\x. norm (f x) \ norm x * K" - using pos_bounded by fast +text {* Bounded Linear Operators *} lemma (in bounded_linear) cont: "f -- a --> f a" proof (rule LIM_I) @@ -337,53 +319,7 @@ "g -- a --> 0 \ (\x. f (g x)) -- a --> 0" by (drule LIM, simp only: zero) -subsubsection {* Bounded Bilinear Operators *} - -locale bounded_bilinear = - fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] - \ 'c::real_normed_vector" - (infixl "**" 70) - assumes add_left: "prod (a + a') b = prod a b + prod a' b" - assumes add_right: "prod a (b + b') = prod a b + prod a b'" - assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" - assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" - assumes bounded: "\K. \a b. norm (prod a b) \ norm a * norm b * K" - -lemma (in bounded_bilinear) pos_bounded: - "\K>0. \a b. norm (a ** b) \ norm a * norm b * K" -apply (cut_tac bounded, erule exE) -apply (rule_tac x="max 1 K" in exI, safe) -apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) -apply (drule spec, drule spec, erule order_trans) -apply (rule mult_left_mono [OF le_maxI2]) -apply (intro mult_nonneg_nonneg norm_ge_zero) -done - -lemma (in bounded_bilinear) additive_right: "additive (\b. prod a b)" -by (rule additive.intro, rule add_right) - -lemma (in bounded_bilinear) additive_left: "additive (\a. prod a b)" -by (rule additive.intro, rule add_left) - -lemma (in bounded_bilinear) zero_left: "prod 0 b = 0" -by (rule additive.zero [OF additive_left]) - -lemma (in bounded_bilinear) zero_right: "prod a 0 = 0" -by (rule additive.zero [OF additive_right]) - -lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b" -by (rule additive.minus [OF additive_left]) - -lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b" -by (rule additive.minus [OF additive_right]) - -lemma (in bounded_bilinear) diff_left: - "prod (a - a') b = prod a b - prod a' b" -by (rule additive.diff [OF additive_left]) - -lemma (in bounded_bilinear) diff_right: - "prod a (b - b') = prod a b - prod a b'" -by (rule additive.diff [OF additive_right]) +text {* Bounded Bilinear Operators *} lemma (in bounded_bilinear) LIM_prod_zero: assumes f: "f -- a --> 0" @@ -419,26 +355,6 @@ qed qed -lemma (in bounded_bilinear) bounded_linear_left: - "bounded_linear (\a. a ** b)" -apply (unfold_locales) -apply (rule add_left) -apply (rule scaleR_left) -apply (cut_tac bounded, safe) -apply (rule_tac x="norm b * K" in exI) -apply (simp add: mult_ac) -done - -lemma (in bounded_bilinear) bounded_linear_right: - "bounded_linear (\b. a ** b)" -apply (unfold_locales) -apply (rule add_right) -apply (rule scaleR_right) -apply (cut_tac bounded, safe) -apply (rule_tac x="norm a * K" in exI) -apply (simp add: mult_ac) -done - lemma (in bounded_bilinear) LIM_left_zero: "f -- a --> 0 \ (\x. f x ** c) -- a --> 0" by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) @@ -447,10 +363,6 @@ "f -- a --> 0 \ (\x. c ** f x) -- a --> 0" by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) -lemma (in bounded_bilinear) prod_diff_prod: - "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" -by (simp add: diff_left diff_right) - lemma (in bounded_bilinear) LIM: "\f -- a --> L; g -- a --> M\ \ (\x. f x ** g x) -- a --> L ** M" apply (drule LIM_zero) @@ -464,28 +376,6 @@ apply (erule LIM_right_zero) done -interpretation bounded_bilinear_mult: - bounded_bilinear ["op * :: 'a \ 'a \ 'a::real_normed_algebra"] -apply (rule bounded_bilinear.intro) -apply (rule left_distrib) -apply (rule right_distrib) -apply (rule mult_scaleR_left) -apply (rule mult_scaleR_right) -apply (rule_tac x="1" in exI) -apply (simp add: norm_mult_ineq) -done - -interpretation bounded_bilinear_scaleR: - bounded_bilinear ["scaleR"] -apply (rule bounded_bilinear.intro) -apply (rule scaleR_left_distrib) -apply (rule scaleR_right_distrib) -apply (simp add: real_scaleR_def) -apply (rule scaleR_left_commute) -apply (rule_tac x="1" in exI) -apply (simp add: norm_scaleR) -done - lemmas LIM_mult = bounded_bilinear_mult.LIM lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero diff -r 7da872d34ace -r 15d9ed9b5051 src/HOL/Real/RealVector.thy --- a/src/HOL/Real/RealVector.thy Wed Mar 14 01:35:02 2007 +0100 +++ b/src/HOL/Real/RealVector.thy Wed Mar 14 21:40:28 2007 +0100 @@ -524,4 +524,144 @@ shows "norm (x ^ n) = norm x ^ n" by (induct n) (simp_all add: power_Suc norm_mult) + +subsection {* Bounded Linear and Bilinear Operators *} + +locale bounded_linear = additive + + constrains f :: "'a::real_normed_vector \ 'b::real_normed_vector" + assumes scaleR: "f (scaleR r x) = scaleR r (f x)" + assumes bounded: "\K. \x. norm (f x) \ norm x * K" + +lemma (in bounded_linear) pos_bounded: + "\K>0. \x. norm (f x) \ norm x * K" +proof - + obtain K where K: "\x. norm (f x) \ norm x * K" + using bounded by fast + show ?thesis + proof (intro exI impI conjI allI) + show "0 < max 1 K" + by (rule order_less_le_trans [OF zero_less_one le_maxI1]) + next + fix x + have "norm (f x) \ norm x * K" using K . + also have "\ \ norm x * max 1 K" + by (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) + finally show "norm (f x) \ norm x * max 1 K" . + qed +qed + +lemma (in bounded_linear) nonneg_bounded: + "\K\0. \x. norm (f x) \ norm x * K" +proof - + from pos_bounded + show ?thesis by (auto intro: order_less_imp_le) +qed + +locale bounded_bilinear = + fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] + \ 'c::real_normed_vector" + (infixl "**" 70) + assumes add_left: "prod (a + a') b = prod a b + prod a' b" + assumes add_right: "prod a (b + b') = prod a b + prod a b'" + assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" + assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" + assumes bounded: "\K. \a b. norm (prod a b) \ norm a * norm b * K" + +lemma (in bounded_bilinear) pos_bounded: + "\K>0. \a b. norm (a ** b) \ norm a * norm b * K" +apply (cut_tac bounded, erule exE) +apply (rule_tac x="max 1 K" in exI, safe) +apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) +apply (drule spec, drule spec, erule order_trans) +apply (rule mult_left_mono [OF le_maxI2]) +apply (intro mult_nonneg_nonneg norm_ge_zero) +done + +lemma (in bounded_bilinear) nonneg_bounded: + "\K\0. \a b. norm (a ** b) \ norm a * norm b * K" +proof - + from pos_bounded + show ?thesis by (auto intro: order_less_imp_le) +qed + +lemma (in bounded_bilinear) additive_right: "additive (\b. prod a b)" +by (rule additive.intro, rule add_right) + +lemma (in bounded_bilinear) additive_left: "additive (\a. prod a b)" +by (rule additive.intro, rule add_left) + +lemma (in bounded_bilinear) zero_left: "prod 0 b = 0" +by (rule additive.zero [OF additive_left]) + +lemma (in bounded_bilinear) zero_right: "prod a 0 = 0" +by (rule additive.zero [OF additive_right]) + +lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b" +by (rule additive.minus [OF additive_left]) + +lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b" +by (rule additive.minus [OF additive_right]) + +lemma (in bounded_bilinear) diff_left: + "prod (a - a') b = prod a b - prod a' b" +by (rule additive.diff [OF additive_left]) + +lemma (in bounded_bilinear) diff_right: + "prod a (b - b') = prod a b - prod a b'" +by (rule additive.diff [OF additive_right]) + +lemma (in bounded_bilinear) bounded_linear_left: + "bounded_linear (\a. a ** b)" +apply (unfold_locales) +apply (rule add_left) +apply (rule scaleR_left) +apply (cut_tac bounded, safe) +apply (rule_tac x="norm b * K" in exI) +apply (simp add: mult_ac) +done + +lemma (in bounded_bilinear) bounded_linear_right: + "bounded_linear (\b. a ** b)" +apply (unfold_locales) +apply (rule add_right) +apply (rule scaleR_right) +apply (cut_tac bounded, safe) +apply (rule_tac x="norm a * K" in exI) +apply (simp add: mult_ac) +done + +lemma (in bounded_bilinear) prod_diff_prod: + "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" +by (simp add: diff_left diff_right) + +interpretation bounded_bilinear_mult: + bounded_bilinear ["op * :: 'a \ 'a \ 'a::real_normed_algebra"] +apply (rule bounded_bilinear.intro) +apply (rule left_distrib) +apply (rule right_distrib) +apply (rule mult_scaleR_left) +apply (rule mult_scaleR_right) +apply (rule_tac x="1" in exI) +apply (simp add: norm_mult_ineq) +done + +interpretation bounded_linear_mult_left: + bounded_linear ["(\x::'a::real_normed_algebra. x * y)"] +by (rule bounded_bilinear_mult.bounded_linear_left) + +interpretation bounded_linear_mult_right: + bounded_linear ["(\y::'a::real_normed_algebra. x * y)"] +by (rule bounded_bilinear_mult.bounded_linear_right) + +interpretation bounded_bilinear_scaleR: + bounded_bilinear ["scaleR"] +apply (rule bounded_bilinear.intro) +apply (rule scaleR_left_distrib) +apply (rule scaleR_right_distrib) +apply (simp add: real_scaleR_def) +apply (rule scaleR_left_commute) +apply (rule_tac x="1" in exI) +apply (simp add: norm_scaleR) +done + end