# HG changeset patch
# User huffman
# Date 1380238412 25200
# Node ID eb93cca4589a8e3759ed0cf036e8f4a2debc2ce9
# Parent  f95765a28b1de3d80ce612be5ad751fff05524ff
moved lemma

diff -r f95765a28b1d -r eb93cca4589a src/HOL/Library/Inner_Product.thy
--- 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)
diff -r f95765a28b1d -r eb93cca4589a src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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)"