author nipkow Sun, 22 Feb 2009 09:52:49 +0100 changeset 30048 6cf1fe60ac73 parent 30046 49f603f92c47 (diff) parent 30047 46c88406e6c0 (current diff) child 30051 a416ed407f82 child 30052 410fefc247aa
merged
```--- a/src/HOL/Library/Euclidean_Space.thy	Sun Feb 22 09:52:28 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Sun Feb 22 09:52:49 2009 +0100
@@ -8,6 +8,7 @@
theory Euclidean_Space
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+  Inner_Product
uses ("normarith.ML")
begin

@@ -547,6 +548,38 @@

end

+subsection {* Inner products *}
+
+instantiation "^" :: (real_inner, type) real_inner
+begin
+
+definition vector_inner_def:
+  "inner x y = setsum (\<lambda>i. inner (x\$i) (y\$i)) {1 .. dimindex(UNIV::'b set)}"
+
+instance proof
+  fix r :: real and x y z :: "'a ^ 'b"
+  show "inner x y = inner y x"
+    unfolding vector_inner_def
+  show "inner (x + y) z = inner x z + inner y z"
+    unfolding vector_inner_def
+    by (vector inner_left_distrib)
+  show "inner (scaleR r x) y = r * inner x y"
+    unfolding vector_inner_def
+    by (vector inner_scaleR_left)
+  show "0 \<le> inner x x"
+    unfolding vector_inner_def
+  show "inner x x = 0 \<longleftrightarrow> x = 0"
+    unfolding vector_inner_def
+    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
+  show "norm x = sqrt (inner x x)"
+    unfolding vector_inner_def vector_norm_def setL2_def
+qed
+
+end
+
subsection{* Properties of the dot product.  *}

lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x" ```
```--- a/src/HOL/Library/Inner_Product.thy	Sun Feb 22 09:52:28 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Sun Feb 22 09:52:49 2009 +0100
@@ -65,7 +65,7 @@
lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"

-lemma Cauchy_Schwartz_ineq:
+lemma Cauchy_Schwarz_ineq:
"(inner x y)\<twosuperior> \<le> inner x x * inner y y"
proof (cases)
assume "y = 0"
@@ -86,11 +86,11 @@
qed

-lemma Cauchy_Schwartz_ineq2:
+lemma Cauchy_Schwarz_ineq2:
"\<bar>inner x y\<bar> \<le> norm x * norm y"
proof (rule power2_le_imp_le)
have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
-    using Cauchy_Schwartz_ineq .
+    using Cauchy_Schwarz_ineq .
thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
show "0 \<le> norm x * norm y"
@@ -108,7 +108,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_Schwartz_ineq2])
+        by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
unfolding power2_sum power2_norm_eq_inner