--- a/src/HOL/Library/Inner_Product.thy Thu Sep 26 23:27:09 2013 +0200
+++ b/src/HOL/Library/Inner_Product.thy Thu Sep 26 16:33:32 2013 -0700
@@ -114,6 +114,9 @@
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
qed
+lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
+ using Cauchy_Schwarz_ineq2 [of x y] by auto
+
subclass real_normed_vector
proof
fix a :: real and x y :: 'a
@@ -122,7 +125,7 @@
show "norm (x + y) \<le> norm x + norm y"
proof (rule power2_le_imp_le)
have "inner x y \<le> norm x * norm y"
- by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
+ by (rule norm_cauchy_schwarz)
thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
unfolding power2_sum power2_norm_eq_inner
by (simp add: inner_add inner_commute)
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 26 23:27:09 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 26 16:33:32 2013 -0700
@@ -69,10 +69,6 @@
lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
by simp (* TODO: delete *)
-lemma norm_cauchy_schwarz: "x \<bullet> y \<le> norm x * norm y"
- (* TODO: move to Inner_Product.thy *)
- using Cauchy_Schwarz_ineq2[of x y] by auto
-
lemma norm_triangle_sub:
fixes x y :: "'a::real_normed_vector"
shows "norm x \<le> norm y + norm (x - y)"