# HG changeset patch # User huffman # Date 1235263902 28800 # Node ID 49f603f92c4726af753d07b808b3dafec916f010 # Parent b8ddd7667eede528abffabd44fc7c18ea720171c fix spelling diff -r b8ddd7667eed -r 49f603f92c47 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Sat Feb 21 15:39:59 2009 -0800 +++ b/src/HOL/Library/Inner_Product.thy Sat Feb 21 16:51:42 2009 -0800 @@ -65,7 +65,7 @@ lemma power2_norm_eq_inner: "(norm x)\ = inner x x" by (simp add: norm_eq_sqrt_inner) -lemma Cauchy_Schwartz_ineq: +lemma Cauchy_Schwarz_ineq: "(inner x y)\ \ inner x x * inner y y" proof (cases) assume "y = 0" @@ -86,11 +86,11 @@ by (simp add: pos_divide_le_eq y) qed -lemma Cauchy_Schwartz_ineq2: +lemma Cauchy_Schwarz_ineq2: "\inner x y\ \ norm x * norm y" proof (rule power2_le_imp_le) have "(inner x y)\ \ inner x x * inner y y" - using Cauchy_Schwartz_ineq . + using Cauchy_Schwarz_ineq . thus "\inner x y\\ \ (norm x * norm y)\" by (simp add: power_mult_distrib power2_norm_eq_inner) show "0 \ norm x * norm y" @@ -108,7 +108,7 @@ show "norm (x + y) \ norm x + norm y" proof (rule power2_le_imp_le) have "inner x y \ norm x * norm y" - by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2]) + by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2]) thus "(norm (x + y))\ \ (norm x + norm y)\" unfolding power2_sum power2_norm_eq_inner by (simp add: inner_distrib inner_commute) @@ -140,7 +140,7 @@ show "\K. \x y::'a. norm (inner x y) \ norm x * norm y * K" proof show "\x y::'a. norm (inner x y) \ norm x * norm y * 1" - by (simp add: Cauchy_Schwartz_ineq2) + by (simp add: Cauchy_Schwarz_ineq2) qed qed