Theory Jordan_Normal_Form.DL_Rank_Submatrix

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)

section ‹Rank and Submatrices›

theory DL_Rank_Submatrix
imports DL_Rank DL_Submatrix Matrix
begin

lemma row_submatrix_UNIV:
assumes "i < card {i. i < dim_row A ∧ i ∈ I}"
shows "row (submatrix A I UNIV) i = row A (pick I i)"
proof (rule eq_vecI)
  show dim_eq:"dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))"
    unfolding carrier_vecD[OF row_carrier] dim_submatrix by auto
  fix j assume "j < dim_vec (row A (pick I i))"
  then have "j < dim_col (submatrix A I UNIV)" "j < dim_col A" "j < card {j. j < dim_col A ∧ j ∈ UNIV}" using dim_eq by auto
  show "row (submatrix A I UNIV) i $ j = row A (pick I i) $ j"
    unfolding row_def index_vec[OF ‹j < dim_col (submatrix A I UNIV)›] index_vec[OF ‹j < dim_col A›]
    using submatrix_index[OF assms ‹j < card {j. j < dim_col A ∧ j ∈ UNIV}›] using pick_UNIV by auto
qed

lemma distinct_cols_submatrix_UNIV:
assumes "distinct (cols (submatrix A I UNIV))"
shows "distinct (cols A)"
using assms proof (rule contrapos_pp)
  assume "¬ distinct (cols A)"
  then obtain i j where "i < dim_col A" "j < dim_col A" "(cols A)!i = (cols A)!j" "i≠j"
    using distinct_conv_nth cols_length by metis
  have "i < dim_col (submatrix A I UNIV)" "j < dim_col (submatrix A I UNIV)"
    unfolding dim_submatrix using ‹i < dim_col A› ‹j < dim_col A›by simp_all
  then have "i < length (cols (submatrix A I UNIV))" "j < length (cols (submatrix A I UNIV))"
    unfolding cols_length by simp_all
  have "(cols (submatrix A I UNIV))!i = (cols (submatrix A I UNIV))!j"
  proof (rule eq_vecI)
    show "dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)"
      by (simp add: ‹i < dim_col (submatrix A I UNIV)› ‹j < dim_col (submatrix A I UNIV)›)
    fix k assume "k < dim_vec (cols (submatrix A I UNIV) ! j)"
    then have "k < dim_row (submatrix A I UNIV)"
      using ‹j < length (cols (submatrix A I UNIV))›  by auto
    then have  "k < card {j. j < dim_row A ∧ j ∈ I}"  using dim_submatrix(1) by metis
    have i_transfer:"cols (submatrix A I UNIV) ! i $ k = (cols A) ! i $ (pick I k)"
      unfolding cols_nth[OF ‹i < dim_col (submatrix A I UNIV)›] col_def index_vec[OF ‹k < dim_row (submatrix A I UNIV)›]
      unfolding submatrix_index[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}› ‹i < dim_col (submatrix A I UNIV)›[unfolded dim_submatrix]]
      unfolding pick_UNIV cols_nth[OF ‹i < dim_col A›] col_def index_vec[OF pick_le[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}›]]
      by metis
    have j_transfer:"cols (submatrix A I UNIV) ! j $ k = (cols A) ! j $ (pick I k)"
      unfolding cols_nth[OF ‹j < dim_col (submatrix A I UNIV)›] col_def index_vec[OF ‹k < dim_row (submatrix A I UNIV)›]
      unfolding submatrix_index[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}› ‹j < dim_col (submatrix A I UNIV)›[unfolded dim_submatrix]]
      unfolding pick_UNIV cols_nth[OF ‹j < dim_col A›] col_def index_vec[OF pick_le[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}›]]
      by metis
    show "cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k"
      using ‹cols A ! i = cols A ! j› i_transfer j_transfer by auto
  qed
  then show "¬ distinct (cols (submatrix A I UNIV))" unfolding distinct_conv_nth
    using ‹i < length (cols (submatrix A I UNIV))› ‹j < length (cols (submatrix A I UNIV))› ‹i ≠ j› by blast
qed

lemma cols_submatrix_subset: "set (cols (submatrix A UNIV J)) ⊆ set (cols A)"
proof
  fix c assume "c ∈ set (cols (submatrix A UNIV J))"
  then obtain j where "j < length (cols (submatrix A UNIV J))" "cols (submatrix A UNIV J) ! j = c"
    by (meson in_set_conv_nth)
  then have "j < dim_col (submatrix A UNIV J)" by simp
  then have "j < card {j. j < dim_col A ∧ j ∈ J}" by (simp add: dim_submatrix(2))
  have "cols (submatrix A UNIV J) ! j = cols A ! (pick J j)"
    unfolding cols_nth[OF ‹j < dim_col (submatrix A UNIV J)›] cols_nth[OF pick_le[OF ‹j < card {j. j < dim_col A ∧ j ∈ J}›]]
  proof (rule eq_vecI)
    show "dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))" unfolding dim_col dim_submatrix by auto
    fix i assume "i < dim_vec (col A (pick J j))"
    then have "i < dim_row A" by simp
    then have "i < dim_row (submatrix A UNIV J)" using ‹dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))› by auto
    show "col (submatrix A UNIV J) j $ i = col A (pick J j) $ i"
      unfolding col_def index_vec[OF ‹i < dim_row (submatrix A UNIV J)›] index_vec[OF ‹i < dim_row A›]
      using submatrix_index by (metis (no_types, lifting) ‹dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))›
      ‹i < dim_vec (col A (pick J j))› ‹j < dim_col (submatrix A UNIV J)› dim_col dim_submatrix(1) dim_submatrix(2) pick_UNIV)
  qed
  then show "c ∈ set (cols A)"
    using ‹cols (submatrix A UNIV J) ! j = c›
    using pick_le[OF ‹j < card {j. j < dim_col A ∧ j ∈ J}›] by (metis cols_length nth_mem)
qed

lemma (in vec_space) lin_dep_submatrix_UNIV:
assumes "A ∈ carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols (submatrix A I UNIV))"
shows "LinearCombinations.module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n ∧ i ∈ I})) (set (cols (submatrix A I UNIV)))"
  (is "LinearCombinations.module.lin_dep class_ring ?M (set ?S')")
proof -
  obtain v where 2:"v ∈ carrier_vec nc" and 3:"v ≠ 0⇩v nc" and "A *⇩v v = 0⇩v n"
    using vec_space.lin_depE[OF assms(1) assms(2) distinct_cols_submatrix_UNIV[OF assms(3)]] by auto
  have 1: "submatrix A I UNIV ∈ carrier_mat (card {i. i < n ∧ i ∈ I}) nc"
    apply (rule carrier_matI) unfolding dim_submatrix using ‹A ∈ carrier_mat n nc› by auto
  have 4:"submatrix A I UNIV *⇩v v = 0⇩v (card {i. i < n ∧ i ∈ I})"
  proof (rule eq_vecI)
    show dim_eq:"dim_vec (submatrix A I UNIV *⇩v v) = dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))" using "1" by auto
    fix i assume "i < dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))"
    then have i_le:"i < card {i. i < n ∧ i ∈ I}" by auto
    have "(submatrix A I UNIV *⇩v v) $ i = row (submatrix A I UNIV) i ∙ v" using dim_eq i_le by auto
    also have "... = row A (pick I i) ∙ v" using row_submatrix_UNIV
      by (metis (no_types, lifting)  dim_eq dim_mult_mat_vec dim_submatrix(1) ‹i < dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))›)
    also have "... = 0"
      using ‹A *⇩v v = 0⇩v n› i_le[THEN pick_le] by (metis assms(1) index_mult_mat_vec carrier_matD(1) index_zero_vec(1))
    also have "... = 0⇩v (card {i. i < n ∧ i ∈ I}) $ i" by (simp add: i_le)
    finally show "(submatrix A I UNIV *⇩v v) $ i = 0⇩v (card {i. i < n ∧ i ∈ I}) $ i" by metis
  qed
  show ?thesis using vec_space.lin_depI[OF 1 2 3 4] using assms(3) by auto
qed

lemma (in vec_space) rank_gt_minor:
assumes "A ∈ carrier_mat n nc"
assumes "det (submatrix A I J) ≠ 0"
shows "card {j. j < nc ∧ j ∈ J} ≤ rank A"
proof -
  have square:"dim_row (submatrix A I J) = dim_col (submatrix A I J)"
   using det_def ‹det (submatrix A I J) ≠ 0› by metis
  then have full_rank:"vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)"
   using vec_space.low_rank_det_zero assms(2) carrier_matI by auto
  then have distinct:"distinct (cols (submatrix A I J))" 
    using vec_space.non_distinct_low_rank square less_irrefl carrier_matI by metis
  then have indpt:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))"
     using vec_space.full_rank_lin_indpt[OF _ full_rank distinct] square by fastforce

  have distinct2: "distinct (cols (submatrix (submatrix A UNIV J) I UNIV))" using submatrix_split distinct by metis
  have indpt2:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (card {i. i < n ∧ i ∈ I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))"
    using submatrix_split dim_submatrix(1) indpt by (metis (full_types) assms(1) carrier_matD(1))

  have "submatrix A UNIV J ∈ carrier_mat n (dim_col (submatrix A UNIV J))"
    apply (rule carrier_matI) unfolding dim_submatrix(1) using ‹A ∈ carrier_mat n nc› carrier_matD by simp_all
  have "lin_indpt (set (cols (submatrix A UNIV J)))"
    using indpt2 vec_space.lin_dep_submatrix_UNIV[OF ‹submatrix A UNIV J ∈ carrier_mat n (dim_col (submatrix A UNIV J))› _ distinct2] by blast
  have distinct3:"distinct (cols (submatrix A UNIV J))" by (metis distinct distinct_cols_submatrix_UNIV submatrix_split)
  show ?thesis using
    rank_ge_card_indpt[OF ‹A ∈ carrier_mat n nc› cols_submatrix_subset ‹lin_indpt (set (cols (submatrix A UNIV J)))›,
    unfolded distinct_card[OF distinct3, unfolded cols_length dim_submatrix], unfolded carrier_matD(2)[OF ‹A ∈ carrier_mat n nc›]]
    by blast
qed

end