460 by unfold_locales (auto simp: vector_space_over_itself.span_singleton) |
460 by unfold_locales (auto simp: vector_space_over_itself.span_singleton) |
461 |
461 |
462 lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1" |
462 lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1" |
463 unfolding vector_space_over_itself.dimension_def by simp |
463 unfolding vector_space_over_itself.dimension_def by simp |
464 |
464 |
|
465 |
|
466 lemma%unimportant dim_subset_UNIV_cart_gen: |
|
467 fixes S :: "('a::field^'n) set" |
|
468 shows "vec.dim S \<le> CARD('n)" |
|
469 by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) |
|
470 |
|
471 lemma%unimportant dim_subset_UNIV_cart: |
|
472 fixes S :: "(real^'n) set" |
|
473 shows "dim S \<le> CARD('n)" |
|
474 using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) |
|
475 |
|
476 text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close> |
|
477 |
|
478 lemma%important matrix_mult_dot: "A *v x = (\<chi> i. inner (A$i) x)" |
|
479 by (simp add: matrix_vector_mult_def inner_vec_def) |
|
480 |
|
481 lemma%unimportant adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
|
482 apply (rule adjoint_unique) |
|
483 apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def |
|
484 sum_distrib_right sum_distrib_left) |
|
485 apply (subst sum.swap) |
|
486 apply (simp add: ac_simps) |
|
487 done |
|
488 |
|
489 lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)" |
|
490 shows "matrix(adjoint f) = transpose(matrix f)" |
|
491 proof%unimportant - |
|
492 have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))" |
|
493 by (simp add: lf) |
|
494 also have "\<dots> = transpose(matrix f)" |
|
495 unfolding adjoint_matrix matrix_of_matrix_vector_mul |
|
496 apply rule |
|
497 done |
|
498 finally show ?thesis . |
|
499 qed |
|
500 |
|
501 |
|
502 subsection%important\<open> Rank of a matrix\<close> |
|
503 |
|
504 text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close> |
|
505 |
|
506 lemma%unimportant matrix_vector_mult_in_columnspace_gen: |
|
507 fixes A :: "'a::field^'n^'m" |
|
508 shows "(A *v x) \<in> vec.span(columns A)" |
|
509 apply (simp add: matrix_vector_column columns_def transpose_def column_def) |
|
510 apply (intro vec.span_sum vec.span_scale) |
|
511 apply (force intro: vec.span_base) |
|
512 done |
|
513 |
|
514 lemma%unimportant matrix_vector_mult_in_columnspace: |
|
515 fixes A :: "real^'n^'m" |
|
516 shows "(A *v x) \<in> span(columns A)" |
|
517 using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) |
|
518 |
|
519 lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" |
|
520 by (simp add: subspace_def orthogonal_clauses) |
|
521 |
|
522 lemma%important orthogonal_nullspace_rowspace: |
|
523 fixes A :: "real^'n^'m" |
|
524 assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)" |
|
525 shows "orthogonal x y" |
|
526 using y |
|
527 proof%unimportant (induction rule: span_induct) |
|
528 case base |
|
529 then show ?case |
|
530 by (simp add: subspace_orthogonal_to_vector) |
|
531 next |
|
532 case (step v) |
|
533 then obtain i where "v = row i A" |
|
534 by (auto simp: rows_def) |
|
535 with 0 show ?case |
|
536 unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def |
|
537 by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) |
|
538 qed |
|
539 |
|
540 lemma%unimportant nullspace_inter_rowspace: |
|
541 fixes A :: "real^'n^'m" |
|
542 shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0" |
|
543 using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right |
|
544 by blast |
|
545 |
|
546 lemma%unimportant matrix_vector_mul_injective_on_rowspace: |
|
547 fixes A :: "real^'n^'m" |
|
548 shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y" |
|
549 using nullspace_inter_rowspace [of A "x-y"] |
|
550 by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) |
|
551 |
|
552 definition%important rank :: "'a::field^'n^'m=>nat" |
|
553 where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)" |
|
554 |
|
555 lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" |
|
556 by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) |
|
557 |
|
558 lemma%important dim_rows_le_dim_columns: |
|
559 fixes A :: "real^'n^'m" |
|
560 shows "dim(rows A) \<le> dim(columns A)" |
|
561 proof%unimportant - |
|
562 have "dim (span (rows A)) \<le> dim (span (columns A))" |
|
563 proof - |
|
564 obtain B where "independent B" "span(rows A) \<subseteq> span B" |
|
565 and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))" |
|
566 using basis_exists [of "span(rows A)"] by metis |
|
567 with span_subspace have eq: "span B = span(rows A)" |
|
568 by auto |
|
569 then have inj: "inj_on ((*v) A) (span B)" |
|
570 by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) |
|
571 then have ind: "independent ((*v) A ` B)" |
|
572 by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>]) |
|
573 have "dim (span (rows A)) \<le> card ((*v) A ` B)" |
|
574 unfolding B(2)[symmetric] |
|
575 using inj |
|
576 by (auto simp: card_image inj_on_subset span_superset) |
|
577 also have "\<dots> \<le> dim (span (columns A))" |
|
578 using _ ind |
|
579 by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) |
|
580 finally show ?thesis . |
|
581 qed |
|
582 then show ?thesis |
|
583 by (simp add: dim_span) |
|
584 qed |
|
585 |
|
586 lemma%unimportant column_rank_def: |
|
587 fixes A :: "real^'n^'m" |
|
588 shows "rank A = dim(columns A)" |
|
589 unfolding row_rank_def |
|
590 by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) |
|
591 |
|
592 lemma%unimportant rank_transpose: |
|
593 fixes A :: "real^'n^'m" |
|
594 shows "rank(transpose A) = rank A" |
|
595 by (metis column_rank_def row_rank_def rows_transpose) |
|
596 |
|
597 lemma%unimportant matrix_vector_mult_basis: |
|
598 fixes A :: "real^'n^'m" |
|
599 shows "A *v (axis k 1) = column k A" |
|
600 by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) |
|
601 |
|
602 lemma%unimportant columns_image_basis: |
|
603 fixes A :: "real^'n^'m" |
|
604 shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))" |
|
605 by (force simp: columns_def matrix_vector_mult_basis [symmetric]) |
|
606 |
|
607 lemma%important rank_dim_range: |
|
608 fixes A :: "real^'n^'m" |
|
609 shows "rank A = dim(range (\<lambda>x. A *v x))" |
|
610 unfolding column_rank_def |
|
611 proof%unimportant (rule span_eq_dim) |
|
612 have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r") |
|
613 by (simp add: columns_image_basis image_subsetI span_mono) |
|
614 then show "?l = ?r" |
|
615 by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace |
|
616 span_eq span_span) |
|
617 qed |
|
618 |
|
619 lemma%unimportant rank_bound: |
|
620 fixes A :: "real^'n^'m" |
|
621 shows "rank A \<le> min CARD('m) (CARD('n))" |
|
622 by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff |
|
623 column_rank_def row_rank_def) |
|
624 |
|
625 lemma%unimportant full_rank_injective: |
|
626 fixes A :: "real^'n^'m" |
|
627 shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)" |
|
628 by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def |
|
629 dim_eq_full [symmetric] card_cart_basis vec.dimension_def) |
|
630 |
|
631 lemma%unimportant full_rank_surjective: |
|
632 fixes A :: "real^'n^'m" |
|
633 shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)" |
|
634 by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] |
|
635 matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) |
|
636 |
|
637 lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" |
|
638 by (simp add: full_rank_injective inj_on_def) |
|
639 |
|
640 lemma%unimportant less_rank_noninjective: |
|
641 fixes A :: "real^'n^'m" |
|
642 shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)" |
|
643 using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) |
|
644 |
|
645 lemma%unimportant matrix_nonfull_linear_equations_eq: |
|
646 fixes A :: "real^'n^'m" |
|
647 shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)" |
|
648 by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) |
|
649 |
|
650 lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" |
|
651 for A :: "real^'n^'m" |
|
652 by (auto simp: rank_dim_range matrix_eq) |
|
653 |
|
654 lemma%important rank_mul_le_right: |
|
655 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
656 shows "rank(A ** B) \<le> rank B" |
|
657 proof%unimportant - |
|
658 have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))" |
|
659 by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) |
|
660 also have "\<dots> \<le> rank B" |
|
661 by (simp add: rank_dim_range dim_image_le) |
|
662 finally show ?thesis . |
|
663 qed |
|
664 |
|
665 lemma%unimportant rank_mul_le_left: |
|
666 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
667 shows "rank(A ** B) \<le> rank A" |
|
668 by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) |
|
669 |
465 end |
670 end |