146 |
146 |
147 text{* Constant Vectors *} |
147 text{* Constant Vectors *} |
148 |
148 |
149 definition "vec x = (\<chi> i. x)" |
149 definition "vec x = (\<chi> i. x)" |
150 |
150 |
151 text{* Dot products. *} |
|
152 |
|
153 definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where |
|
154 "x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV" |
|
155 |
|
156 lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)" |
|
157 by (simp add: dot_def setsum_1) |
|
158 |
|
159 lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)" |
|
160 by (simp add: dot_def setsum_2) |
|
161 |
|
162 lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" |
|
163 by (simp add: dot_def setsum_3) |
|
164 |
|
165 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} |
151 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} |
166 |
152 |
167 method_setup vector = {* |
153 method_setup vector = {* |
168 let |
154 let |
169 val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, |
155 val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym, |
170 @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, |
156 @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, |
171 @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] |
157 @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] |
172 val ss2 = @{simpset} addsimps |
158 val ss2 = @{simpset} addsimps |
173 [@{thm vector_add_def}, @{thm vector_mult_def}, |
159 [@{thm vector_add_def}, @{thm vector_mult_def}, |
174 @{thm vector_minus_def}, @{thm vector_uminus_def}, |
160 @{thm vector_minus_def}, @{thm vector_uminus_def}, |
844 by (simp add: power2_norm_eq_inner) |
830 by (simp add: power2_norm_eq_inner) |
845 qed |
831 qed |
846 |
832 |
847 end |
833 end |
848 |
834 |
849 subsection{* Properties of the dot product. *} |
|
850 |
|
851 lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x" |
|
852 by (vector mult_commute) |
|
853 lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)" |
|
854 by (vector ring_simps) |
|
855 lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)" |
|
856 by (vector ring_simps) |
|
857 lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)" |
|
858 by (vector ring_simps) |
|
859 lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)" |
|
860 by (vector ring_simps) |
|
861 lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps) |
|
862 lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps) |
|
863 lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector |
|
864 lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector |
|
865 lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector |
|
866 lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector |
|
867 lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x" |
|
868 by (simp add: dot_def setsum_nonneg) |
|
869 |
|
870 lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)" |
835 lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)" |
871 using fS fp setsum_nonneg[OF fp] |
836 using fS fp setsum_nonneg[OF fp] |
872 proof (induct set: finite) |
837 proof (induct set: finite) |
873 case empty thus ?case by simp |
838 case empty thus ?case by simp |
874 next |
839 next |
877 from insert.hyps Fp setsum_nonneg[OF Fp] |
842 from insert.hyps Fp setsum_nonneg[OF Fp] |
878 have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis |
843 have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis |
879 from add_nonneg_eq_0_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) |
844 from add_nonneg_eq_0_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) |
880 show ?case by (simp add: h) |
845 show ?case by (simp add: h) |
881 qed |
846 qed |
882 |
|
883 lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" |
|
884 by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq) |
|
885 |
|
886 lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] |
|
887 by (auto simp add: le_less) |
|
888 |
847 |
889 subsection{* The collapse of the general concepts to dimension one. *} |
848 subsection{* The collapse of the general concepts to dimension one. *} |
890 |
849 |
891 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" |
850 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" |
892 by (simp add: Cart_eq forall_1) |
851 by (simp add: Cart_eq forall_1) |
1017 by (rule norm_zero) |
976 by (rule norm_zero) |
1018 |
977 |
1019 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" |
978 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" |
1020 by (simp add: norm_vector_def vector_component setL2_right_distrib |
979 by (simp add: norm_vector_def vector_component setL2_right_distrib |
1021 abs_mult cong: strong_setL2_cong) |
980 abs_mult cong: strong_setL2_cong) |
1022 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))" |
981 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))" |
1023 by (simp add: norm_vector_def dot_def setL2_def power2_eq_square) |
982 by (simp add: norm_vector_def setL2_def power2_eq_square) |
1024 lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)" |
|
1025 by (simp add: norm_vector_def setL2_def dot_def power2_eq_square) |
|
1026 lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x" |
|
1027 by (simp add: real_vector_norm_def) |
|
1028 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) |
983 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) |
1029 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" |
984 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" |
1030 by vector |
985 by vector |
1031 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" |
986 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" |
1032 by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) |
987 by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) |
1034 by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) |
989 by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) |
1035 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" |
990 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" |
1036 by (metis vector_mul_lcancel) |
991 by (metis vector_mul_lcancel) |
1037 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" |
992 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" |
1038 by (metis vector_mul_rcancel) |
993 by (metis vector_mul_rcancel) |
|
994 |
1039 lemma norm_cauchy_schwarz: |
995 lemma norm_cauchy_schwarz: |
1040 fixes x y :: "real ^ 'n" |
996 fixes x y :: "real ^ 'n" |
1041 shows "x \<bullet> y <= norm x * norm y" |
997 shows "inner x y <= norm x * norm y" |
1042 proof- |
998 using Cauchy_Schwarz_ineq2[of x y] by auto |
1043 {assume "norm x = 0" |
|
1044 hence ?thesis by (simp add: dot_lzero dot_rzero)} |
|
1045 moreover |
|
1046 {assume "norm y = 0" |
|
1047 hence ?thesis by (simp add: dot_lzero dot_rzero)} |
|
1048 moreover |
|
1049 {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0" |
|
1050 let ?z = "norm y *s x - norm x *s y" |
|
1051 from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps) |
|
1052 from dot_pos_le[of ?z] |
|
1053 have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2" |
|
1054 apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps) |
|
1055 by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym) |
|
1056 hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p |
|
1057 by (simp add: field_simps) |
|
1058 hence ?thesis using h by (simp add: power2_eq_square)} |
|
1059 ultimately show ?thesis by metis |
|
1060 qed |
|
1061 |
999 |
1062 lemma norm_cauchy_schwarz_abs: |
1000 lemma norm_cauchy_schwarz_abs: |
1063 fixes x y :: "real ^ 'n" |
1001 fixes x y :: "real ^ 'n" |
1064 shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y" |
1002 shows "\<bar>inner x y\<bar> \<le> norm x * norm y" |
1065 using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"] |
1003 using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"] |
1066 by (simp add: real_abs_def dot_rneg) |
1004 by (simp add: real_abs_def) |
1067 |
1005 |
1068 lemma norm_triangle_sub: |
1006 lemma norm_triangle_sub: |
1069 fixes x y :: "'a::real_normed_vector" |
1007 fixes x y :: "'a::real_normed_vector" |
1070 shows "norm x \<le> norm y + norm (x - y)" |
1008 shows "norm x \<le> norm y + norm (x - y)" |
1071 using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) |
1009 using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) |
1087 lemma real_abs_norm: "\<bar>norm x\<bar> = norm x" |
1025 lemma real_abs_norm: "\<bar>norm x\<bar> = norm x" |
1088 by (rule abs_norm_cancel) |
1026 by (rule abs_norm_cancel) |
1089 lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)" |
1027 lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)" |
1090 by (rule norm_triangle_ineq3) |
1028 by (rule norm_triangle_ineq3) |
1091 lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" |
1029 lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" |
1092 by (simp add: real_vector_norm_def) |
1030 by (simp add: norm_eq_sqrt_inner) |
1093 lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" |
1031 lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" |
1094 by (simp add: real_vector_norm_def) |
1032 by (simp add: norm_eq_sqrt_inner) |
1095 lemma norm_eq: "norm(x::real ^ 'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y" |
1033 lemma norm_eq: "norm(x::real ^ 'n) = norm (y::real ^ 'n) \<longleftrightarrow> x \<bullet> x = y \<bullet> y" |
1096 by (simp add: order_eq_iff norm_le) |
1034 apply(subst order_eq_iff) unfolding norm_le by auto |
1097 lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1" |
1035 lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1" |
1098 by (simp add: real_vector_norm_def) |
1036 unfolding norm_eq_sqrt_inner by auto |
1099 |
1037 |
1100 text{* Squaring equations and inequalities involving norms. *} |
1038 text{* Squaring equations and inequalities involving norms. *} |
1101 |
1039 |
1102 lemma dot_square_norm: "x \<bullet> x = norm(x)^2" |
1040 lemma dot_square_norm: "x \<bullet> x = norm(x)^2" |
1103 by (simp add: real_vector_norm_def) |
1041 by (simp add: norm_eq_sqrt_inner) |
1104 |
1042 |
1105 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" |
1043 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" |
1106 by (auto simp add: real_vector_norm_def) |
1044 by (auto simp add: norm_eq_sqrt_inner) |
1107 |
1045 |
1108 lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" |
1046 lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" |
1109 proof- |
1047 proof- |
1110 have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square) |
1048 have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square) |
1111 also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith |
1049 also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith |
1129 lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" |
1067 lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" |
1130 by (metis norm_le_square not_less) |
1068 by (metis norm_le_square not_less) |
1131 |
1069 |
1132 text{* Dot product in terms of the norm rather than conversely. *} |
1070 text{* Dot product in terms of the norm rather than conversely. *} |
1133 |
1071 |
|
1072 lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left |
|
1073 inner.scaleR_left inner.scaleR_right |
|
1074 |
1134 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" |
1075 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" |
1135 by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym) |
1076 unfolding power2_norm_eq_inner inner_simps inner_commute by auto |
1136 |
1077 |
1137 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" |
1078 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" |
1138 by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym) |
1079 unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:group_simps) |
1139 |
|
1140 |
1080 |
1141 text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} |
1081 text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} |
1142 |
1082 |
1143 lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") |
1083 lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") |
1144 proof |
1084 proof |
1145 assume "?lhs" then show ?rhs by simp |
1085 assume "?lhs" then show ?rhs by simp |
1146 next |
1086 next |
1147 assume ?rhs |
1087 assume ?rhs |
1148 then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y\<bullet> y = 0" by simp |
1088 then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp |
1149 hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" |
1089 hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute) |
1150 by (simp add: dot_rsub dot_lsub dot_sym) |
1090 then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps inner_simps inner_commute) |
1151 then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps dot_lsub dot_rsub) |
1091 then show "x = y" by (simp) |
1152 then show "x = y" by (simp add: dot_eq_0) |
1092 qed |
1153 qed |
|
1154 |
|
1155 |
1093 |
1156 subsection{* General linear decision procedure for normed spaces. *} |
1094 subsection{* General linear decision procedure for normed spaces. *} |
1157 |
1095 |
1158 lemma norm_cmul_rule_thm: |
1096 lemma norm_cmul_rule_thm: |
1159 fixes x :: "'a::real_normed_vector" |
1097 fixes x :: "'a::real_normed_vector" |
1479 finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" . |
1417 finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" . |
1480 qed |
1418 qed |
1481 finally show ?thesis . |
1419 finally show ?thesis . |
1482 qed |
1420 qed |
1483 |
1421 |
1484 lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S " |
1422 lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{real_inner}^'n) = setsum (\<lambda>x. f x \<bullet> y) S " |
1485 by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) |
1423 apply(induct rule: finite_induct) by(auto simp add: inner_simps) |
1486 |
1424 |
1487 lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S " |
1425 lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{real_inner}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S " |
1488 by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) |
1426 apply(induct rule: finite_induct) by(auto simp add: inner_simps) |
1489 |
1427 |
1490 subsection{* Basis vectors in coordinate directions. *} |
1428 subsection{* Basis vectors in coordinate directions. *} |
1491 |
|
1492 |
1429 |
1493 definition "basis k = (\<chi> i. if i = k then 1 else 0)" |
1430 definition "basis k = (\<chi> i. if i = k then 1 else 0)" |
1494 |
1431 |
1495 lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)" |
1432 lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)" |
1496 unfolding basis_def by simp |
1433 unfolding basis_def by simp |
1498 lemma delta_mult_idempotent: |
1435 lemma delta_mult_idempotent: |
1499 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) |
1436 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) |
1500 |
1437 |
1501 lemma norm_basis: |
1438 lemma norm_basis: |
1502 shows "norm (basis k :: real ^'n) = 1" |
1439 shows "norm (basis k :: real ^'n) = 1" |
1503 apply (simp add: basis_def real_vector_norm_def dot_def) |
1440 apply (simp add: basis_def norm_eq_sqrt_inner) unfolding inner_vector_def |
1504 apply (vector delta_mult_idempotent) |
1441 apply (vector delta_mult_idempotent) |
1505 using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] |
1442 using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto |
1506 apply auto |
|
1507 done |
|
1508 |
1443 |
1509 lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1" |
1444 lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1" |
1510 by (rule norm_basis) |
1445 by (rule norm_basis) |
1511 |
1446 |
1512 lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c" |
1447 lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c" |
1555 |
1490 |
1556 lemma basis_nonzero: |
1491 lemma basis_nonzero: |
1557 shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)" |
1492 shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)" |
1558 by (simp add: basis_eq_0) |
1493 by (simp add: basis_eq_0) |
1559 |
1494 |
1560 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)" |
1495 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::real^'n)" |
1561 apply (auto simp add: Cart_eq dot_basis) |
1496 apply (auto simp add: Cart_eq dot_basis) |
1562 apply (erule_tac x="basis i" in allE) |
1497 apply (erule_tac x="basis i" in allE) |
1563 apply (simp add: dot_basis) |
1498 apply (simp add: dot_basis) |
1564 apply (subgoal_tac "y = z") |
1499 apply (subgoal_tac "y = z") |
1565 apply simp |
1500 apply simp |
1566 apply (simp add: Cart_eq) |
1501 apply (simp add: Cart_eq) |
1567 done |
1502 done |
1568 |
1503 |
1569 lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)" |
1504 lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::real^'n)" |
1570 apply (auto simp add: Cart_eq dot_basis) |
1505 apply (auto simp add: Cart_eq dot_basis) |
1571 apply (erule_tac x="basis i" in allE) |
1506 apply (erule_tac x="basis i" in allE) |
1572 apply (simp add: dot_basis) |
1507 apply (simp add: dot_basis) |
1573 apply (subgoal_tac "x = y") |
1508 apply (subgoal_tac "x = y") |
1574 apply simp |
1509 apply simp |
1578 subsection{* Orthogonality. *} |
1513 subsection{* Orthogonality. *} |
1579 |
1514 |
1580 definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" |
1515 definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" |
1581 |
1516 |
1582 lemma orthogonal_basis: |
1517 lemma orthogonal_basis: |
1583 shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x$i = (0::'a::ring_1)" |
1518 shows "orthogonal (basis i) x \<longleftrightarrow> x$i = (0::real)" |
1584 by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) |
1519 by (auto simp add: orthogonal_def inner_vector_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) |
1585 |
1520 |
1586 lemma orthogonal_basis_basis: |
1521 lemma orthogonal_basis_basis: |
1587 shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j" |
1522 shows "orthogonal (basis i :: real^'n) (basis j) \<longleftrightarrow> i \<noteq> j" |
1588 unfolding orthogonal_basis[of i] basis_component[of j] by simp |
1523 unfolding orthogonal_basis[of i] basis_component[of j] by simp |
1589 |
1524 |
1590 (* FIXME : Maybe some of these require less than comm_ring, but not all*) |
1525 (* FIXME : Maybe some of these require less than comm_ring, but not all*) |
1591 lemma orthogonal_clauses: |
1526 lemma orthogonal_clauses: |
1592 "orthogonal a (0::'a::comm_ring ^'n)" |
1527 "orthogonal a (0::real ^'n)" |
1593 "orthogonal a x ==> orthogonal a (c *s x)" |
1528 "orthogonal a x ==> orthogonal a (c *\<^sub>R x)" |
1594 "orthogonal a x ==> orthogonal a (-x)" |
1529 "orthogonal a x ==> orthogonal a (-x)" |
1595 "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)" |
1530 "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)" |
1596 "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x - y)" |
1531 "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x - y)" |
1597 "orthogonal 0 a" |
1532 "orthogonal 0 a" |
1598 "orthogonal x a ==> orthogonal (c *s x) a" |
1533 "orthogonal x a ==> orthogonal (c *\<^sub>R x) a" |
1599 "orthogonal x a ==> orthogonal (-x) a" |
1534 "orthogonal x a ==> orthogonal (-x) a" |
1600 "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x + y) a" |
1535 "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x + y) a" |
1601 "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x - y) a" |
1536 "orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x - y) a" |
1602 unfolding orthogonal_def dot_rneg dot_rmult dot_radd dot_rsub |
1537 unfolding orthogonal_def inner_simps by auto |
1603 dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub |
1538 |
1604 by simp_all |
1539 lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x" |
1605 |
1540 by (simp add: orthogonal_def inner_commute) |
1606 lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x" |
|
1607 by (simp add: orthogonal_def dot_sym) |
|
1608 |
1541 |
1609 subsection{* Explicit vector construction from lists. *} |
1542 subsection{* Explicit vector construction from lists. *} |
1610 |
1543 |
1611 primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}" |
1544 primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}" |
1612 where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n" |
1545 where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n" |
1992 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)" |
1925 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)" |
1993 |
1926 |
1994 lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis |
1927 lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis |
1995 |
1928 |
1996 lemma adjoint_works_lemma: |
1929 lemma adjoint_works_lemma: |
1997 fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m" |
1930 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
1998 assumes lf: "linear f" |
1931 assumes lf: "linear f" |
1999 shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y" |
1932 shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y" |
2000 proof- |
1933 proof- |
2001 let ?N = "UNIV :: 'n set" |
1934 let ?N = "UNIV :: 'n set" |
2002 let ?M = "UNIV :: 'm set" |
1935 let ?M = "UNIV :: 'm set" |
2003 have fN: "finite ?N" by simp |
1936 have fN: "finite ?N" by simp |
2004 have fM: "finite ?M" by simp |
1937 have fM: "finite ?M" by simp |
2005 {fix y:: "'a ^ 'm" |
1938 {fix y:: "real ^ 'm" |
2006 let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: 'a ^ 'n" |
1939 let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: real ^ 'n" |
2007 {fix x |
1940 {fix x |
2008 have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *s basis i) ?N) \<bullet> y" |
1941 have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *s basis i) ?N) \<bullet> y" |
2009 by (simp only: basis_expansion) |
1942 by (simp only: basis_expansion) |
2010 also have "\<dots> = (setsum (\<lambda>i. (x$i) *s f (basis i)) ?N) \<bullet> y" |
1943 also have "\<dots> = (setsum (\<lambda>i. (x$i) *s f (basis i)) ?N) \<bullet> y" |
2011 unfolding linear_setsum[OF lf fN] |
1944 unfolding linear_setsum[OF lf fN] |
2012 by (simp add: linear_cmul[OF lf]) |
1945 by (simp add: linear_cmul[OF lf]) |
2013 finally have "f x \<bullet> y = x \<bullet> ?w" |
1946 finally have "f x \<bullet> y = x \<bullet> ?w" |
2014 apply (simp only: ) |
1947 apply (simp only: ) |
2015 apply (simp add: dot_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps) |
1948 apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps) |
2016 done} |
1949 done} |
2017 } |
1950 } |
2018 then show ?thesis unfolding adjoint_def |
1951 then show ?thesis unfolding adjoint_def |
2019 some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"] |
1952 some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"] |
2020 using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "] |
1953 using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "] |
2021 by metis |
1954 by metis |
2022 qed |
1955 qed |
2023 |
1956 |
2024 lemma adjoint_works: |
1957 lemma adjoint_works: |
2025 fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m" |
1958 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
2026 assumes lf: "linear f" |
1959 assumes lf: "linear f" |
2027 shows "x \<bullet> adjoint f y = f x \<bullet> y" |
1960 shows "x \<bullet> adjoint f y = f x \<bullet> y" |
2028 using adjoint_works_lemma[OF lf] by metis |
1961 using adjoint_works_lemma[OF lf] by metis |
2029 |
1962 |
2030 |
|
2031 lemma adjoint_linear: |
1963 lemma adjoint_linear: |
2032 fixes f :: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m" |
1964 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
2033 assumes lf: "linear f" |
1965 assumes lf: "linear f" |
2034 shows "linear (adjoint f)" |
1966 shows "linear (adjoint f)" |
2035 by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf]) |
1967 unfolding linear_def vector_eq_ldot[symmetric] apply safe |
|
1968 unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto |
2036 |
1969 |
2037 lemma adjoint_clauses: |
1970 lemma adjoint_clauses: |
2038 fixes f:: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m" |
1971 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
2039 assumes lf: "linear f" |
1972 assumes lf: "linear f" |
2040 shows "x \<bullet> adjoint f y = f x \<bullet> y" |
1973 shows "x \<bullet> adjoint f y = f x \<bullet> y" |
2041 and "adjoint f y \<bullet> x = y \<bullet> f x" |
1974 and "adjoint f y \<bullet> x = y \<bullet> f x" |
2042 by (simp_all add: adjoint_works[OF lf] dot_sym ) |
1975 by (simp_all add: adjoint_works[OF lf] inner_commute) |
2043 |
1976 |
2044 lemma adjoint_adjoint: |
1977 lemma adjoint_adjoint: |
2045 fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m" |
1978 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
2046 assumes lf: "linear f" |
1979 assumes lf: "linear f" |
2047 shows "adjoint (adjoint f) = f" |
1980 shows "adjoint (adjoint f) = f" |
2048 apply (rule ext) |
1981 apply (rule ext) |
2049 by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf]) |
1982 by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf]) |
2050 |
1983 |
2051 lemma adjoint_unique: |
1984 lemma adjoint_unique: |
2052 fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m" |
1985 fixes f:: "real ^'n \<Rightarrow> real ^'m" |
2053 assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y" |
1986 assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y" |
2054 shows "f' = adjoint f" |
1987 shows "f' = adjoint f" |
2055 apply (rule ext) |
1988 apply (rule ext) |
2056 using u |
1989 using u |
2057 by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf]) |
1990 by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf]) |
2124 apply (erule_tac x="basis ia" in allE) |
2057 apply (erule_tac x="basis ia" in allE) |
2125 apply (erule_tac x="i" in allE) |
2058 apply (erule_tac x="i" in allE) |
2126 by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) |
2059 by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) |
2127 |
2060 |
2128 lemma matrix_vector_mul_component: |
2061 lemma matrix_vector_mul_component: |
2129 shows "((A::'a::semiring_1^_^_) *v x)$k = (A$k) \<bullet> x" |
2062 shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x" |
2130 by (simp add: matrix_vector_mult_def dot_def) |
2063 by (simp add: matrix_vector_mult_def inner_vector_def) |
2131 |
2064 |
2132 lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \<bullet> y = x \<bullet> (A *v y)" |
2065 lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)" |
2133 apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) |
2066 apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) |
2134 apply (subst setsum_commute) |
2067 apply (subst setsum_commute) |
2135 by simp |
2068 by simp |
2136 |
2069 |
2137 lemma transpose_mat: "transpose (mat n) = mat n" |
2070 lemma transpose_mat: "transpose (mat n) = mat n" |
2138 by (vector transpose_def mat_def) |
2071 by (vector transpose_def mat_def) |
2217 by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) |
2150 by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) |
2218 |
2151 |
2219 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" |
2152 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" |
2220 by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute) |
2153 by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute) |
2221 |
2154 |
2222 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
2155 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
2223 apply (rule adjoint_unique[symmetric]) |
2156 apply (rule adjoint_unique[symmetric]) |
2224 apply (rule matrix_vector_mul_linear) |
2157 apply (rule matrix_vector_mul_linear) |
2225 apply (simp add: transpose_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) |
2158 apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) |
2226 apply (subst setsum_commute) |
2159 apply (subst setsum_commute) |
2227 apply (auto simp add: mult_ac) |
2160 apply (auto simp add: mult_ac) |
2228 done |
2161 done |
2229 |
2162 |
2230 lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^'m)" |
2163 lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)" |
2231 shows "matrix(adjoint f) = transpose(matrix f)" |
2164 shows "matrix(adjoint f) = transpose(matrix f)" |
2232 apply (subst matrix_vector_mul[OF lf]) |
2165 apply (subst matrix_vector_mul[OF lf]) |
2233 unfolding adjoint_matrix matrix_of_matrix_vector_mul .. |
2166 unfolding adjoint_matrix matrix_of_matrix_vector_mul .. |
2234 |
2167 |
2235 subsection{* Interlude: Some properties of real sets *} |
2168 subsection{* Interlude: Some properties of real sets *} |
2647 lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))" |
2580 lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))" |
2648 proof- |
2581 proof- |
2649 have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" |
2582 have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" |
2650 by (simp add: pastecart_fst_snd) |
2583 by (simp add: pastecart_fst_snd) |
2651 have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)" |
2584 have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)" |
2652 by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg) |
2585 by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg) |
2653 then show ?thesis |
2586 then show ?thesis |
2654 unfolding th0 |
2587 unfolding th0 |
2655 unfolding real_vector_norm_def real_sqrt_le_iff id_def |
2588 unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def |
2656 by (simp add: dot_def) |
2589 by (simp add: inner_vector_def) |
2657 qed |
2590 qed |
2658 |
2591 |
2659 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y" |
2592 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y" |
2660 unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart) |
2593 unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart) |
2661 |
2594 |
2662 lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))" |
2595 lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))" |
2663 proof- |
2596 proof- |
2664 have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" |
2597 have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" |
2665 by (simp add: pastecart_fst_snd) |
2598 by (simp add: pastecart_fst_snd) |
2666 have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)" |
2599 have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)" |
2667 by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg) |
2600 by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg) |
2668 then show ?thesis |
2601 then show ?thesis |
2669 unfolding th0 |
2602 unfolding th0 |
2670 unfolding real_vector_norm_def real_sqrt_le_iff id_def |
2603 unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def |
2671 by (simp add: dot_def) |
2604 by (simp add: inner_vector_def) |
2672 qed |
2605 qed |
2673 |
2606 |
2674 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y" |
2607 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y" |
2675 unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart) |
2608 unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart) |
2676 |
2609 |
2677 lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2" |
2610 lemma dot_pastecart: "(pastecart (x1::real^'n) (x2::real^'m)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2" |
2678 by (simp add: dot_def setsum_UNIV_sum pastecart_def) |
2611 by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def) |
2679 |
2612 |
2680 text {* TODO: move to NthRoot *} |
2613 text {* TODO: move to NthRoot *} |
2681 lemma sqrt_add_le_add_sqrt: |
2614 lemma sqrt_add_le_add_sqrt: |
2682 assumes x: "0 \<le> x" and y: "0 \<le> y" |
2615 assumes x: "0 \<le> x" and y: "0 \<le> y" |
2683 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
2616 shows "sqrt (x + y) \<le> sqrt x + sqrt y" |
3865 (* Picking an orthogonal replacement for a spanning set. *) |
3798 (* Picking an orthogonal replacement for a spanning set. *) |
3866 (* ------------------------------------------------------------------------- *) |
3799 (* ------------------------------------------------------------------------- *) |
3867 (* FIXME : Move to some general theory ?*) |
3800 (* FIXME : Move to some general theory ?*) |
3868 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)" |
3801 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)" |
3869 |
3802 |
3870 lemma vector_sub_project_orthogonal: "(b::'a::linordered_field^'n) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0" |
3803 lemma vector_sub_project_orthogonal: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0" |
3871 apply (cases "b = 0", simp) |
3804 unfolding inner_simps smult_conv_scaleR by auto |
3872 apply (simp add: dot_rsub dot_rmult) |
|
3873 unfolding times_divide_eq_right[symmetric] |
|
3874 by (simp add: field_simps dot_eq_0) |
|
3875 |
3805 |
3876 lemma basis_orthogonal: |
3806 lemma basis_orthogonal: |
3877 fixes B :: "(real ^'n) set" |
3807 fixes B :: "(real ^'n) set" |
3878 assumes fB: "finite B" |
3808 assumes fB: "finite B" |
3879 shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C" |
3809 shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C" |
3884 case (2 a B) |
3814 case (2 a B) |
3885 note fB = `finite B` and aB = `a \<notin> B` |
3815 note fB = `finite B` and aB = `a \<notin> B` |
3886 from `\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C` |
3816 from `\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C` |
3887 obtain C where C: "finite C" "card C \<le> card B" |
3817 obtain C where C: "finite C" "card C \<le> card B" |
3888 "span C = span B" "pairwise orthogonal C" by blast |
3818 "span C = span B" "pairwise orthogonal C" by blast |
3889 let ?a = "a - setsum (\<lambda>x. (x\<bullet>a / (x\<bullet>x)) *s x) C" |
3819 let ?a = "a - setsum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *s x) C" |
3890 let ?C = "insert ?a C" |
3820 let ?C = "insert ?a C" |
3891 from C(1) have fC: "finite ?C" by simp |
3821 from C(1) have fC: "finite ?C" by simp |
3892 from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)" by (simp add: card_insert_if) |
3822 from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)" by (simp add: card_insert_if) |
3893 {fix x k |
3823 {fix x k |
3894 have th0: "\<And>(a::'b::comm_ring) b c. a - (b - c) = c + (a - b)" by (simp add: ring_simps) |
3824 have th0: "\<And>(a::'b::comm_ring) b c. a - (b - c) = c + (a - b)" by (simp add: ring_simps) |
3910 {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C" |
3840 {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C" |
3911 from ya have Cy: "C = insert y (C - {y})" by blast |
3841 from ya have Cy: "C = insert y (C - {y})" by blast |
3912 have fth: "finite (C - {y})" using C by simp |
3842 have fth: "finite (C - {y})" using C by simp |
3913 have "orthogonal x y" |
3843 have "orthogonal x y" |
3914 using xa ya |
3844 using xa ya |
3915 unfolding orthogonal_def xa dot_lsub dot_rsub diff_eq_0_iff_eq |
3845 unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq |
3916 apply simp |
3846 apply simp |
3917 apply (subst Cy) |
3847 apply (subst Cy) |
3918 using C(1) fth |
3848 using C(1) fth |
3919 apply (simp only: setsum_clauses) |
3849 apply (simp only: setsum_clauses) unfolding smult_conv_scaleR |
3920 thm dot_ladd |
3850 apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of y a] dot_lsum[OF fth]) |
3921 apply (auto simp add: dot_ladd dot_radd dot_lmult dot_rmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth]) |
|
3922 apply (rule setsum_0') |
3851 apply (rule setsum_0') |
3923 apply clarsimp |
3852 apply clarsimp |
3924 apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) |
3853 apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) |
3925 by auto} |
3854 by auto} |
3926 moreover |
3855 moreover |
3927 {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a" |
3856 {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a" |
3928 from xa have Cx: "C = insert x (C - {x})" by blast |
3857 from xa have Cx: "C = insert x (C - {x})" by blast |
3929 have fth: "finite (C - {x})" using C by simp |
3858 have fth: "finite (C - {x})" using C by simp |
3930 have "orthogonal x y" |
3859 have "orthogonal x y" |
3931 using xa ya |
3860 using xa ya |
3932 unfolding orthogonal_def ya dot_rsub dot_lsub diff_eq_0_iff_eq |
3861 unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq |
3933 apply simp |
3862 apply simp |
3934 apply (subst Cx) |
3863 apply (subst Cx) |
3935 using C(1) fth |
3864 using C(1) fth |
3936 apply (simp only: setsum_clauses) |
3865 apply (simp only: setsum_clauses) unfolding smult_conv_scaleR |
3937 apply (subst dot_sym[of x]) |
3866 apply (subst inner_commute[of x]) |
3938 apply (auto simp add: dot_radd dot_rmult dot_eq_0 dot_sym[of x a] dot_rsum[OF fth]) |
3867 apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of x a] dot_rsum[OF fth]) |
3939 apply (rule setsum_0') |
3868 apply (rule setsum_0') |
3940 apply clarsimp |
3869 apply clarsimp |
3941 apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) |
3870 apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) |
3942 by auto} |
3871 by auto} |
3943 moreover |
3872 moreover |
3986 B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B" |
3915 B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B" |
3987 by blast |
3916 by blast |
3988 from B have fB: "finite B" "card B = dim S" using independent_bound by auto |
3917 from B have fB: "finite B" "card B = dim S" using independent_bound by auto |
3989 from span_mono[OF B(2)] span_mono[OF B(3)] |
3918 from span_mono[OF B(2)] span_mono[OF B(3)] |
3990 have sSB: "span S = span B" by (simp add: span_span) |
3919 have sSB: "span S = span B" by (simp add: span_span) |
3991 let ?a = "a - setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B" |
3920 let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B" |
3992 have "setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B \<in> span S" |
3921 have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B \<in> span S" |
3993 unfolding sSB |
3922 unfolding sSB |
3994 apply (rule span_setsum[OF fB(1)]) |
3923 apply (rule span_setsum[OF fB(1)]) |
3995 apply clarsimp |
3924 apply clarsimp |
3996 apply (rule span_mul) |
3925 apply (rule span_mul) |
3997 by (rule span_superset) |
3926 by (rule span_superset) |
3998 with a have a0:"?a \<noteq> 0" by auto |
3927 with a have a0:"?a \<noteq> 0" by auto |
3999 have "\<forall>x\<in>span B. ?a \<bullet> x = 0" |
3928 have "\<forall>x\<in>span B. ?a \<bullet> x = 0" |
4000 proof(rule span_induct') |
3929 proof(rule span_induct') |
4001 show "subspace (\<lambda>x. ?a \<bullet> x = 0)" |
3930 show "subspace (\<lambda>x. ?a \<bullet> x = 0)" by (auto simp add: subspace_def mem_def inner_simps smult_conv_scaleR) |
4002 by (auto simp add: subspace_def mem_def dot_radd dot_rmult) |
3931 |
4003 next |
3932 next |
4004 {fix x assume x: "x \<in> B" |
3933 {fix x assume x: "x \<in> B" |
4005 from x have B': "B = insert x (B - {x})" by blast |
3934 from x have B': "B = insert x (B - {x})" by blast |
4006 have fth: "finite (B - {x})" using fB by simp |
3935 have fth: "finite (B - {x})" using fB by simp |
4007 have "?a \<bullet> x = 0" |
3936 have "?a \<bullet> x = 0" |
4008 apply (subst B') using fB fth |
3937 apply (subst B') using fB fth |
4009 unfolding setsum_clauses(2)[OF fth] |
3938 unfolding setsum_clauses(2)[OF fth] |
4010 apply simp |
3939 apply simp unfolding inner_simps smult_conv_scaleR |
4011 apply (clarsimp simp add: dot_lsub dot_ladd dot_lmult dot_lsum dot_eq_0) |
3940 apply (clarsimp simp add: inner_simps inner_eq_zero_iff smult_conv_scaleR dot_lsum) |
4012 apply (rule setsum_0', rule ballI) |
3941 apply (rule setsum_0', rule ballI) |
4013 unfolding dot_sym |
3942 unfolding inner_commute |
4014 by (auto simp add: x field_simps dot_eq_0 intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} |
3943 by (auto simp add: x field_simps inner_eq_zero_iff intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])} |
4015 then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast |
3944 then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast |
4016 qed |
3945 qed |
4017 with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) |
3946 with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) |
4018 qed |
3947 qed |
4019 |
3948 |
4778 |
4707 |
4779 lemma dot_rowvector_columnvector: |
4708 lemma dot_rowvector_columnvector: |
4780 "columnvector (A *v v) = A ** columnvector v" |
4709 "columnvector (A *v v) = A ** columnvector v" |
4781 by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) |
4710 by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) |
4782 |
4711 |
4783 lemma dot_matrix_product: "(x::'a::semiring_1^'n) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" |
4712 lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" |
4784 by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def) |
4713 by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vector_def) |
4785 |
4714 |
4786 lemma dot_matrix_vector_mul: |
4715 lemma dot_matrix_vector_mul: |
4787 fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" |
4716 fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" |
4788 shows "(A *v x) \<bullet> (B *v y) = |
4717 shows "(A *v x) \<bullet> (B *v y) = |
4789 (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" |
4718 (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" |
4935 have "real ?d \<ge> 0" by simp |
4864 have "real ?d \<ge> 0" by simp |
4936 hence d2: "(sqrt (real ?d))^2 = real ?d" |
4865 hence d2: "(sqrt (real ?d))^2 = real ?d" |
4937 by (auto intro: real_sqrt_pow2) |
4866 by (auto intro: real_sqrt_pow2) |
4938 have th: "sqrt (real ?d) * infnorm x \<ge> 0" |
4867 have th: "sqrt (real ?d) * infnorm x \<ge> 0" |
4939 by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le) |
4868 by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le) |
4940 have th1: "x\<bullet>x \<le> (sqrt (real ?d) * infnorm x)^2" |
4869 have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2" |
4941 unfolding power_mult_distrib d2 |
4870 unfolding power_mult_distrib d2 |
|
4871 unfolding real_of_nat_def inner_vector_def |
|
4872 apply (subst power2_abs[symmetric]) |
|
4873 apply (rule setsum_bounded) |
|
4874 apply(auto simp add: power2_eq_square[symmetric]) |
4942 apply (subst power2_abs[symmetric]) |
4875 apply (subst power2_abs[symmetric]) |
4943 unfolding real_of_nat_def dot_def power2_eq_square[symmetric] |
|
4944 apply (subst power2_abs[symmetric]) |
|
4945 apply (rule setsum_bounded) |
|
4946 apply (rule power_mono) |
4876 apply (rule power_mono) |
4947 unfolding abs_of_nonneg[OF infnorm_pos_le] |
|
4948 unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] |
4877 unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma] |
4949 unfolding infnorm_set_image bex_simps |
4878 unfolding infnorm_set_image bex_simps apply(rule_tac x=i in exI) by auto |
4950 apply blast |
4879 from real_le_lsqrt[OF inner_ge_zero th th1] |
4951 by (rule abs_ge_zero) |
4880 show ?thesis unfolding norm_eq_sqrt_inner id_def . |
4952 from real_le_lsqrt[OF dot_pos_le th th1] |
|
4953 show ?thesis unfolding real_vector_norm_def id_def . |
|
4954 qed |
4881 qed |
4955 |
4882 |
4956 (* Equality in Cauchy-Schwarz and triangle inequalities. *) |
4883 (* Equality in Cauchy-Schwarz and triangle inequalities. *) |
4957 |
4884 |
4958 lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs") |
4885 lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs") |
4962 moreover |
4889 moreover |
4963 {assume h: "y = 0" |
4890 {assume h: "y = 0" |
4964 hence ?thesis by simp} |
4891 hence ?thesis by simp} |
4965 moreover |
4892 moreover |
4966 {assume x: "x \<noteq> 0" and y: "y \<noteq> 0" |
4893 {assume x: "x \<noteq> 0" and y: "y \<noteq> 0" |
4967 from dot_eq_0[of "norm y *s x - norm x *s y"] |
4894 from inner_eq_zero_iff[of "norm y *s x - norm x *s y"] |
4968 have "?rhs \<longleftrightarrow> (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) - norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)" |
4895 have "?rhs \<longleftrightarrow> (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) - norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)" |
4969 using x y |
4896 using x y |
4970 unfolding dot_rsub dot_lsub dot_lmult dot_rmult |
4897 unfolding inner_simps smult_conv_scaleR |
4971 unfolding norm_pow_2[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: dot_sym) |
4898 unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute) |
4972 apply (simp add: ring_simps) |
4899 apply (simp add: ring_simps) by metis |
4973 apply metis |
|
4974 done |
|
4975 also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y |
4900 also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y |
4976 by (simp add: ring_simps dot_sym) |
4901 by (simp add: ring_simps inner_commute) |
4977 also have "\<dots> \<longleftrightarrow> ?lhs" using x y |
4902 also have "\<dots> \<longleftrightarrow> ?lhs" using x y |
4978 apply simp |
4903 apply simp |
4979 by metis |
4904 by metis |
4980 finally have ?thesis by blast} |
4905 finally have ?thesis by blast} |
4981 ultimately show ?thesis by blast |
4906 ultimately show ?thesis by blast |