184 by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) |
184 by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) |
185 |
185 |
186 lemma%unimportant matrix_mult_transpose_dot_row: |
186 lemma%unimportant matrix_mult_transpose_dot_row: |
187 shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))" |
187 shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))" |
188 by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) |
188 by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) |
189 |
|
190 text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close> |
|
191 |
|
192 lemma%important matrix_mult_dot: "A *v x = (\<chi> i. inner (A$i) x)" |
|
193 by (simp add: matrix_vector_mult_def inner_vec_def) |
|
194 |
|
195 lemma%unimportant adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
|
196 apply (rule adjoint_unique) |
|
197 apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def |
|
198 sum_distrib_right sum_distrib_left) |
|
199 apply (subst sum.swap) |
|
200 apply (simp add: ac_simps) |
|
201 done |
|
202 |
|
203 lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)" |
|
204 shows "matrix(adjoint f) = transpose(matrix f)" |
|
205 proof%unimportant - |
|
206 have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))" |
|
207 by (simp add: lf) |
|
208 also have "\<dots> = transpose(matrix f)" |
|
209 unfolding adjoint_matrix matrix_of_matrix_vector_mul |
|
210 apply rule |
|
211 done |
|
212 finally show ?thesis . |
|
213 qed |
|
214 |
189 |
215 lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" |
190 lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" |
216 using matrix_vector_mul_linear[of A] |
191 using matrix_vector_mul_linear[of A] |
217 by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq) |
192 by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq) |
218 |
193 |
905 lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>" |
846 lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>" |
906 by (simp add: norm_vector_1) |
847 by (simp add: norm_vector_1) |
907 |
848 |
908 lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>" |
849 lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>" |
909 by (auto simp add: norm_real dist_norm) |
850 by (auto simp add: norm_real dist_norm) |
910 |
|
911 subsection%important\<open> Rank of a matrix\<close> |
|
912 |
|
913 text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close> |
|
914 |
|
915 lemma%unimportant matrix_vector_mult_in_columnspace_gen: |
|
916 fixes A :: "'a::field^'n^'m" |
|
917 shows "(A *v x) \<in> vec.span(columns A)" |
|
918 apply (simp add: matrix_vector_column columns_def transpose_def column_def) |
|
919 apply (intro vec.span_sum vec.span_scale) |
|
920 apply (force intro: vec.span_base) |
|
921 done |
|
922 |
|
923 lemma%unimportant matrix_vector_mult_in_columnspace: |
|
924 fixes A :: "real^'n^'m" |
|
925 shows "(A *v x) \<in> span(columns A)" |
|
926 using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) |
|
927 |
|
928 lemma%important orthogonal_nullspace_rowspace: |
|
929 fixes A :: "real^'n^'m" |
|
930 assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)" |
|
931 shows "orthogonal x y" |
|
932 using y |
|
933 proof%unimportant (induction rule: span_induct) |
|
934 case base |
|
935 then show ?case |
|
936 by (simp add: subspace_orthogonal_to_vector) |
|
937 next |
|
938 case (step v) |
|
939 then obtain i where "v = row i A" |
|
940 by (auto simp: rows_def) |
|
941 with 0 show ?case |
|
942 unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def |
|
943 by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) |
|
944 qed |
|
945 |
|
946 lemma%unimportant nullspace_inter_rowspace: |
|
947 fixes A :: "real^'n^'m" |
|
948 shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0" |
|
949 using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right |
|
950 by blast |
|
951 |
|
952 lemma%unimportant matrix_vector_mul_injective_on_rowspace: |
|
953 fixes A :: "real^'n^'m" |
|
954 shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y" |
|
955 using nullspace_inter_rowspace [of A "x-y"] |
|
956 by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) |
|
957 |
|
958 definition%important rank :: "'a::field^'n^'m=>nat" |
|
959 where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)" |
|
960 |
|
961 lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" |
|
962 by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) |
|
963 |
|
964 lemma%important dim_rows_le_dim_columns: |
|
965 fixes A :: "real^'n^'m" |
|
966 shows "dim(rows A) \<le> dim(columns A)" |
|
967 proof%unimportant - |
|
968 have "dim (span (rows A)) \<le> dim (span (columns A))" |
|
969 proof - |
|
970 obtain B where "independent B" "span(rows A) \<subseteq> span B" |
|
971 and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))" |
|
972 using basis_exists [of "span(rows A)"] by metis |
|
973 with span_subspace have eq: "span B = span(rows A)" |
|
974 by auto |
|
975 then have inj: "inj_on ((*v) A) (span B)" |
|
976 by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) |
|
977 then have ind: "independent ((*v) A ` B)" |
|
978 by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>]) |
|
979 have "dim (span (rows A)) \<le> card ((*v) A ` B)" |
|
980 unfolding B(2)[symmetric] |
|
981 using inj |
|
982 by (auto simp: card_image inj_on_subset span_superset) |
|
983 also have "\<dots> \<le> dim (span (columns A))" |
|
984 using _ ind |
|
985 by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) |
|
986 finally show ?thesis . |
|
987 qed |
|
988 then show ?thesis |
|
989 by (simp add: dim_span) |
|
990 qed |
|
991 |
|
992 lemma%unimportant column_rank_def: |
|
993 fixes A :: "real^'n^'m" |
|
994 shows "rank A = dim(columns A)" |
|
995 unfolding row_rank_def |
|
996 by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) |
|
997 |
|
998 lemma%unimportant rank_transpose: |
|
999 fixes A :: "real^'n^'m" |
|
1000 shows "rank(transpose A) = rank A" |
|
1001 by (metis column_rank_def row_rank_def rows_transpose) |
|
1002 |
|
1003 lemma%unimportant matrix_vector_mult_basis: |
|
1004 fixes A :: "real^'n^'m" |
|
1005 shows "A *v (axis k 1) = column k A" |
|
1006 by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) |
|
1007 |
|
1008 lemma%unimportant columns_image_basis: |
|
1009 fixes A :: "real^'n^'m" |
|
1010 shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))" |
|
1011 by (force simp: columns_def matrix_vector_mult_basis [symmetric]) |
|
1012 |
|
1013 lemma%important rank_dim_range: |
|
1014 fixes A :: "real^'n^'m" |
|
1015 shows "rank A = dim(range (\<lambda>x. A *v x))" |
|
1016 unfolding column_rank_def |
|
1017 proof%unimportant (rule span_eq_dim) |
|
1018 have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r") |
|
1019 by (simp add: columns_image_basis image_subsetI span_mono) |
|
1020 then show "?l = ?r" |
|
1021 by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace |
|
1022 span_eq span_span) |
|
1023 qed |
|
1024 |
|
1025 lemma%unimportant rank_bound: |
|
1026 fixes A :: "real^'n^'m" |
|
1027 shows "rank A \<le> min CARD('m) (CARD('n))" |
|
1028 by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff |
|
1029 column_rank_def row_rank_def) |
|
1030 |
|
1031 lemma%unimportant full_rank_injective: |
|
1032 fixes A :: "real^'n^'m" |
|
1033 shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)" |
|
1034 by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def |
|
1035 dim_eq_full [symmetric] card_cart_basis vec.dimension_def) |
|
1036 |
|
1037 lemma%unimportant full_rank_surjective: |
|
1038 fixes A :: "real^'n^'m" |
|
1039 shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)" |
|
1040 by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] |
|
1041 matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) |
|
1042 |
|
1043 lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" |
|
1044 by (simp add: full_rank_injective inj_on_def) |
|
1045 |
|
1046 lemma%unimportant less_rank_noninjective: |
|
1047 fixes A :: "real^'n^'m" |
|
1048 shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)" |
|
1049 using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) |
|
1050 |
|
1051 lemma%unimportant matrix_nonfull_linear_equations_eq: |
|
1052 fixes A :: "real^'n^'m" |
|
1053 shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)" |
|
1054 by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) |
|
1055 |
|
1056 lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" |
|
1057 for A :: "real^'n^'m" |
|
1058 by (auto simp: rank_dim_range matrix_eq) |
|
1059 |
|
1060 lemma%important rank_mul_le_right: |
|
1061 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
1062 shows "rank(A ** B) \<le> rank B" |
|
1063 proof%unimportant - |
|
1064 have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))" |
|
1065 by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) |
|
1066 also have "\<dots> \<le> rank B" |
|
1067 by (simp add: rank_dim_range dim_image_le) |
|
1068 finally show ?thesis . |
|
1069 qed |
|
1070 |
|
1071 lemma%unimportant rank_mul_le_left: |
|
1072 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
1073 shows "rank(A ** B) \<le> rank A" |
|
1074 by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) |
|
1075 |
851 |
1076 subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close> |
852 subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close> |
1077 |
853 |
1078 lemma vector_one_nth [simp]: |
854 lemma vector_one_nth [simp]: |
1079 fixes x :: "'a^1" shows "vec (x $ 1) = x" |
855 fixes x :: "'a^1" shows "vec (x $ 1) = x" |