equal
deleted
inserted
replaced
624 by (metis component_le_norm_cart le_less_trans) |
624 by (metis component_le_norm_cart le_less_trans) |
625 |
625 |
626 lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV" |
626 lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV" |
627 by (simp add: norm_vec_def L2_set_le_sum) |
627 by (simp add: norm_vec_def L2_set_le_sum) |
628 |
628 |
629 lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)" |
629 lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)" |
630 apply standard |
630 apply standard |
631 apply (rule vector_add_component) |
631 apply (rule vector_add_component) |
632 apply (rule vector_scaleR_component) |
632 apply (rule vector_scaleR_component) |
633 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
633 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
634 done |
634 done |