diff -r 60110f6d0b4e -r d51e5e41fafe src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 10:27:57 2019 +0100 +++ b/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 11:48:06 2019 +0100 @@ -462,4 +462,209 @@ lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1" unfolding vector_space_over_itself.dimension_def by simp + +lemma%unimportant dim_subset_UNIV_cart_gen: + fixes S :: "('a::field^'n) set" + shows "vec.dim S \ CARD('n)" + by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) + +lemma%unimportant dim_subset_UNIV_cart: + fixes S :: "(real^'n) set" + shows "dim S \ CARD('n)" + using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) + +text\Two sometimes fruitful ways of looking at matrix-vector multiplication.\ + +lemma%important matrix_mult_dot: "A *v x = (\ i. inner (A$i) x)" + by (simp add: matrix_vector_mult_def inner_vec_def) + +lemma%unimportant adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" + apply (rule adjoint_unique) + apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def + sum_distrib_right sum_distrib_left) + apply (subst sum.swap) + apply (simp add: ac_simps) + done + +lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" + shows "matrix(adjoint f) = transpose(matrix f)" +proof%unimportant - + have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))" + by (simp add: lf) + also have "\ = transpose(matrix f)" + unfolding adjoint_matrix matrix_of_matrix_vector_mul + apply rule + done + finally show ?thesis . +qed + + +subsection%important\ Rank of a matrix\ + +text\Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\ + +lemma%unimportant matrix_vector_mult_in_columnspace_gen: + fixes A :: "'a::field^'n^'m" + shows "(A *v x) \ vec.span(columns A)" + apply (simp add: matrix_vector_column columns_def transpose_def column_def) + apply (intro vec.span_sum vec.span_scale) + apply (force intro: vec.span_base) + done + +lemma%unimportant matrix_vector_mult_in_columnspace: + fixes A :: "real^'n^'m" + shows "(A *v x) \ span(columns A)" + using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) + +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" + by (simp add: subspace_def orthogonal_clauses) + +lemma%important orthogonal_nullspace_rowspace: + fixes A :: "real^'n^'m" + assumes 0: "A *v x = 0" and y: "y \ span(rows A)" + shows "orthogonal x y" + using y +proof%unimportant (induction rule: span_induct) + case base + then show ?case + by (simp add: subspace_orthogonal_to_vector) +next + case (step v) + then obtain i where "v = row i A" + by (auto simp: rows_def) + with 0 show ?case + unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def + by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) +qed + +lemma%unimportant nullspace_inter_rowspace: + fixes A :: "real^'n^'m" + shows "A *v x = 0 \ x \ span(rows A) \ x = 0" + using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right + by blast + +lemma%unimportant matrix_vector_mul_injective_on_rowspace: + fixes A :: "real^'n^'m" + shows "\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" + using nullspace_inter_rowspace [of A "x-y"] + by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) + +definition%important rank :: "'a::field^'n^'m=>nat" + where row_rank_def_gen: "rank A \ vec.dim(rows A)" + +lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" + by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) + +lemma%important dim_rows_le_dim_columns: + fixes A :: "real^'n^'m" + shows "dim(rows A) \ dim(columns A)" +proof%unimportant - + have "dim (span (rows A)) \ dim (span (columns A))" + proof - + obtain B where "independent B" "span(rows A) \ span B" + and B: "B \ span(rows A)""card B = dim (span(rows A))" + using basis_exists [of "span(rows A)"] by metis + with span_subspace have eq: "span B = span(rows A)" + by auto + then have inj: "inj_on ((*v) A) (span B)" + by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) + then have ind: "independent ((*v) A ` B)" + by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \independent B\]) + have "dim (span (rows A)) \ card ((*v) A ` B)" + unfolding B(2)[symmetric] + using inj + by (auto simp: card_image inj_on_subset span_superset) + also have "\ \ dim (span (columns A))" + using _ ind + by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) + finally show ?thesis . + qed + then show ?thesis + by (simp add: dim_span) +qed + +lemma%unimportant column_rank_def: + fixes A :: "real^'n^'m" + shows "rank A = dim(columns A)" + unfolding row_rank_def + by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) + +lemma%unimportant rank_transpose: + fixes A :: "real^'n^'m" + shows "rank(transpose A) = rank A" + by (metis column_rank_def row_rank_def rows_transpose) + +lemma%unimportant matrix_vector_mult_basis: + fixes A :: "real^'n^'m" + shows "A *v (axis k 1) = column k A" + by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) + +lemma%unimportant columns_image_basis: + fixes A :: "real^'n^'m" + shows "columns A = (*v) A ` (range (\i. axis i 1))" + by (force simp: columns_def matrix_vector_mult_basis [symmetric]) + +lemma%important rank_dim_range: + fixes A :: "real^'n^'m" + shows "rank A = dim(range (\x. A *v x))" + unfolding column_rank_def +proof%unimportant (rule span_eq_dim) + have "span (columns A) \ span (range ((*v) A))" (is "?l \ ?r") + by (simp add: columns_image_basis image_subsetI span_mono) + then show "?l = ?r" + by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace + span_eq span_span) +qed + +lemma%unimportant rank_bound: + fixes A :: "real^'n^'m" + shows "rank A \ min CARD('m) (CARD('n))" + by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff + column_rank_def row_rank_def) + +lemma%unimportant full_rank_injective: + fixes A :: "real^'n^'m" + shows "rank A = CARD('n) \ inj ((*v) A)" + by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def + dim_eq_full [symmetric] card_cart_basis vec.dimension_def) + +lemma%unimportant full_rank_surjective: + fixes A :: "real^'n^'m" + shows "rank A = CARD('m) \ surj ((*v) A)" + by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] + matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) + +lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" + by (simp add: full_rank_injective inj_on_def) + +lemma%unimportant less_rank_noninjective: + fixes A :: "real^'n^'m" + shows "rank A < CARD('n) \ \ inj ((*v) A)" +using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) + +lemma%unimportant matrix_nonfull_linear_equations_eq: + fixes A :: "real^'n^'m" + shows "(\x. (x \ 0) \ A *v x = 0) \ rank A \ CARD('n)" + by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) + +lemma%unimportant rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" + for A :: "real^'n^'m" + by (auto simp: rank_dim_range matrix_eq) + +lemma%important rank_mul_le_right: + fixes A :: "real^'n^'m" and B :: "real^'p^'n" + shows "rank(A ** B) \ rank B" +proof%unimportant - + have "rank(A ** B) \ dim ((*v) A ` range ((*v) B))" + by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) + also have "\ \ rank B" + by (simp add: rank_dim_range dim_image_le) + finally show ?thesis . +qed + +lemma%unimportant rank_mul_le_left: + fixes A :: "real^'n^'m" and B :: "real^'p^'n" + shows "rank(A ** B) \ rank A" + by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) + end \ No newline at end of file