fix spelling
authorhuffman
Sat Feb 21 16:51:42 2009 -0800 (2009-02-21)
changeset 3004649f603f92c47
parent 30045 b8ddd7667eed
child 30048 6cf1fe60ac73
fix spelling
src/HOL/Library/Inner_Product.thy
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Sat Feb 21 15:39:59 2009 -0800
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Sat Feb 21 16:51:42 2009 -0800
     1.3 @@ -65,7 +65,7 @@
     1.4  lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
     1.5    by (simp add: norm_eq_sqrt_inner)
     1.6  
     1.7 -lemma Cauchy_Schwartz_ineq:
     1.8 +lemma Cauchy_Schwarz_ineq:
     1.9    "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
    1.10  proof (cases)
    1.11    assume "y = 0"
    1.12 @@ -86,11 +86,11 @@
    1.13      by (simp add: pos_divide_le_eq y)
    1.14  qed
    1.15  
    1.16 -lemma Cauchy_Schwartz_ineq2:
    1.17 +lemma Cauchy_Schwarz_ineq2:
    1.18    "\<bar>inner x y\<bar> \<le> norm x * norm y"
    1.19  proof (rule power2_le_imp_le)
    1.20    have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
    1.21 -    using Cauchy_Schwartz_ineq .
    1.22 +    using Cauchy_Schwarz_ineq .
    1.23    thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
    1.24      by (simp add: power_mult_distrib power2_norm_eq_inner)
    1.25    show "0 \<le> norm x * norm y"
    1.26 @@ -108,7 +108,7 @@
    1.27    show "norm (x + y) \<le> norm x + norm y"
    1.28      proof (rule power2_le_imp_le)
    1.29        have "inner x y \<le> norm x * norm y"
    1.30 -        by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2])
    1.31 +        by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
    1.32        thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
    1.33          unfolding power2_sum power2_norm_eq_inner
    1.34          by (simp add: inner_distrib inner_commute)
    1.35 @@ -140,7 +140,7 @@
    1.36    show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
    1.37    proof
    1.38      show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
    1.39 -      by (simp add: Cauchy_Schwartz_ineq2)
    1.40 +      by (simp add: Cauchy_Schwarz_ineq2)
    1.41    qed
    1.42  qed
    1.43