--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 31 07:51:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 31 08:11:47 2011 -0700
@@ -7,7 +7,7 @@
theory Euclidean_Space
imports
- Complex_Main
+ L2_Norm
"~~/src/HOL/Library/Inner_Product"
"~~/src/HOL/Library/Product_Vector"
begin
@@ -216,10 +216,20 @@
simp add: inner_setsum_left inner_setsum_right
dot_basis if_distrib setsum_cases mult_commute)
+lemma euclidean_dist_l2:
+ fixes x y :: "'a::euclidean_space"
+ shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}"
+ unfolding dist_norm norm_eq_sqrt_inner setL2_def
+ by (simp add: euclidean_inner power2_eq_square)
+
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
unfolding euclidean_component_def
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
+lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
+ unfolding euclidean_dist_l2 [where 'a='a]
+ by (cases "i < DIM('a)", rule member_le_setL2, auto)
+
subsection {* Subclass relationships *}
instance euclidean_space \<subseteq> perfect_space