Theory Rank

header{*Rank of a matrix*}

theory Rank
imports 
      Dim_Formula
begin

(*  
    Title:      Rank.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Maintainer: Jose Divasón <jose.divasonm at unirioja.es>
*)

subsection{*Row rank, column rank and rank*}

text{*Definitions of row rank, column rank and rank*}

definition row_rank :: "'a::{real_vector}^'n^'m=>nat"
  where "row_rank A = dim (row_space A)"

definition col_rank :: "'a::{real_vector}^'n^'m=>nat"
  where "col_rank A = dim (col_space A)"

definition rank :: "real^'n^'m=>nat"
  where "rank A = row_rank A"

subsection{*Properties*}

(*TODO: Maybe move the following two or three lemmas to another file?*)
lemma norm_mult_vec:
  fixes a::"(real,'b::finite) vec"
  shows "norm (x • x) = norm x * norm x"
  by (metis inner_real_def norm_cauchy_schwarz_eq norm_mult)

lemma norm_equivalence: 
  fixes A::"real^'n^'m"
  shows "((transpose A) *v (A *v x) = 0) <-> (A *v x = 0)" 
proof (auto)
  show "transpose A *v 0 = 0" unfolding matrix_vector_zero ..
next
  assume a: "transpose A *v (A *v x) = 0"
  have eq: "(x v* (transpose A)) = (A *v x)"
    by (metis Cartesian_Euclidean_Space.transpose_transpose transpose_vector)
  have eq_0: "0 = (x v* (transpose A)) * (A *v x)"
    by (metis a comm_semiring_1_class.normalizing_semiring_rules(7) dot_lmul_matrix inner_eq_zero_iff inner_zero_left mult_zero_left transpose_vector)
  hence "0 = norm ((x v* (transpose A)) * (A *v x))" by auto
  also have "... = norm ((A *v x)*(A *v x))" unfolding eq ..
  also have "... = norm ((A *v x)  • (A *v x))"
    by (metis eq_0 a dot_lmul_matrix eq inner_zero_right norm_zero)
  also have "... = norm (A *v x)^2" unfolding norm_mult_vec[of "(A *v x)"] power2_eq_square ..
  finally show "A *v x = 0"
    by (metis (lifting) field_power_not_zero norm_eq_0_imp)
qed


lemma combination_columns:
  fixes A::"real^'n^'m"
  assumes x: "x ∈ columns (transpose A ** A)"
  shows "∃f. (∑y∈columns(transpose A). f y *⇩R y) = x"
proof -
  obtain j where j: "x= column j (transpose A ** A)" using x unfolding columns_def by auto
  let ?g="(λy. {i. y=column i (transpose A)})"
  have inj: "inj_on ?g (columns (transpose A))" unfolding inj_on_def unfolding columns_def by auto
  have union_univ: "\<Union> (?g`(columns (transpose A))) = UNIV" unfolding columns_def by auto
  let ?f="(λy. card {a. y = column a (transpose A)} * A $ (SOME a. y = column a (transpose A)) $ j)"
  have "column j (transpose A ** A) =  (∑i∈UNIV. (A$i$j) *⇩R (column i (transpose A)))" 
    unfolding matrix_matrix_mult_def unfolding column_def by (vector, auto, rule setsum_cong2, auto)
  also have "...  = setsum  (λi. (A$i$j) *⇩R (column i (transpose A))) (\<Union>(?g`(columns (transpose A))))" unfolding union_univ ..
  also have "... = setsum (setsum (λi. (A$i$j) *⇩R (column i (transpose A)))) (?g`(columns (transpose A)))" by (rule setsum_Union_disjoint, auto)
  also have "... = setsum ((setsum (λi. (A$i$j) *⇩R (column i (transpose A)))) o ?g) (columns (transpose A))" apply (rule setsum_reindex) using inj by auto
  also have "... = setsum  (λy. ?f y  *⇩R y)  (columns (transpose A))"  
  proof (rule setsum_cong2, unfold o_def)
    fix x assume x: "x ∈ columns (transpose A)"
    obtain b where xb: "x = column b (transpose A)" using x unfolding columns_def by auto
    have "∀a c. a∈ {i. x = column i (transpose A)} ∧ c∈ {i. x = column i (transpose A)} --> A $ a $ j = A $ c $ j"
      by (unfold column_def transpose_def, auto, metis vec_lambda_inverse vec_nth)
    hence rw_b: "∀a. a∈ {i. x = column i (transpose A)} --> A $ a $ j = A $ b $ j" using xb by fast
    have Abj: "A $ b $ j = A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j"
      by (metis (lifting, mono_tags) xb mem_Collect_eq rw_b some_eq_ex)    
    have "(∑i | x = column i (Cartesian_Euclidean_Space.transpose A). A $ i $ j *⇩R column i (Cartesian_Euclidean_Space.transpose A))
      = setsum (λi. A $ i $ j *⇩R x) {i. x = column i (transpose A)}" by auto  
    also have "... =  (∑i∈{i. x = column i (transpose A)}. A $ b $ j *⇩R x)" using rw_b by auto    
    also have "... =  of_nat (card {i. x = column i (transpose A)}) * (A $ b $ j *⇩R x)" unfolding setsum_constant by auto    
    also have "... = (real (card {i. x = column i (transpose A)})) *⇩R (A $ b $ j *⇩R x)"
      by (metis (no_types) real_of_nat_def setsum_constant setsum_constant_scaleR) 
    also have "... = (real (card {a. x = column a (transpose A)}) * A $ b $ j) *⇩R x" by auto
    also have "... = (real (card {a. x = column a (transpose A)}) * A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j) *⇩R x"
      unfolding Abj ..      
    finally show "(∑i | x = column i (Cartesian_Euclidean_Space.transpose A). A $ i $ j *⇩R column i (Cartesian_Euclidean_Space.transpose A)) =
      (real (card {a. x = column a (Cartesian_Euclidean_Space.transpose A)}) * A $ (SOME a. x = column a (Cartesian_Euclidean_Space.transpose A)) $ j) *⇩R x" .    
  qed
  finally show ?thesis unfolding j by auto
qed


lemma rrk_crk:
  fixes A::"real^'n^'m"
  shows "col_rank A ≤ row_rank A"
proof -
  have null_space_eq: "null_space A = null_space (transpose A ** A)" using norm_equivalence unfolding matrix_vector_mul_assoc unfolding null_space_def by fastforce
  have col_rank_transpose: "col_rank A = col_rank (transpose A ** A)"
    using rank_nullity_theorem_matrices[of A] rank_nullity_theorem_matrices[of "(transpose A ** A)"]
    unfolding col_space_eq[symmetric]
    unfolding null_space_eq by (metis col_rank_def nat_add_left_cancel)  
  have "col_rank (transpose A ** A) ≤ col_rank (transpose A)"   
  proof (unfold col_rank_def, rule subset_le_dim, unfold col_space_def, unfold span_span, clarify)
    fix x assume x_in: "x ∈ span (columns (transpose A ** A))"
    show "x ∈ span (columns (transpose A))" 
    proof (rule span_induct)
      show "x ∈ span (columns (transpose A ** A))" using x_in .
      show "subspace (span (columns (transpose A)))" using subspace_span .    
      fix y assume y: "y ∈ columns (transpose A ** A)"
      show "y ∈ span (columns (transpose A))"
      proof (unfold span_explicit, simp, rule exI[of _ "columns (transpose A)"], auto intro: combination_columns[OF y])
        show "finite (columns (transpose A))" unfolding columns_def using finite_Atleast_Atmost_nat by auto
      qed
    qed 
  qed  
  thus ?thesis    
    unfolding col_rank_transpose[symmetric]
    unfolding col_rank_def col_space_def columns_transpose row_rank_def row_space_def .
qed

corollary row_rank_eq_col_rank:
  fixes A::"real^'n^'m"
  shows "row_rank A = col_rank A" 
  using rrk_crk[of A] using rrk_crk[of "transpose A"] 
  unfolding col_rank_def row_rank_def row_space_def col_space_def
  unfolding rows_transpose columns_transpose by simp

theorem rank_col_rank:
  shows "rank A = col_rank A" unfolding rank_def row_rank_eq_col_rank ..

theorem rank_eq_dim_image:
  "rank A = dim (range (λx. A *v (x::real^'n)))"
  unfolding rank_col_rank col_rank_def col_space_eq' ..

theorem rank_eq_dim_col_space:
  "rank A = dim (col_space A)" using rank_col_rank unfolding col_rank_def .

lemma rank_transpose: "rank (transpose A) = rank A"
  by (metis rank_def rank_eq_dim_col_space row_rank_def row_space_eq_col_space_transpose)

lemma rank_le_nrows: "rank A ≤ nrows A"
  unfolding rank_eq_dim_col_space nrows_def using dim_subset_UNIV[of "col_space A"]
  unfolding DIM_cart DIM_real by simp

lemma rank_le_ncols: "rank A ≤ ncols A"
  unfolding rank_def row_rank_def ncols_def using dim_subset_UNIV[of "row_space A"]
  unfolding DIM_cart DIM_real by simp

end