Theory DL_Rank_CP_Rank
section ‹CP-Rank and Matrix Rank›
theory DL_Rank_CP_Rank
imports Tensor_Rank Jordan_Normal_Form.DL_Rank Tensor_Matricization
Jordan_Normal_Form.DL_Submatrix Jordan_Normal_Form.Missing_VectorSpace
begin
abbreviation "mrank A == vec_space.rank (dim_row A) A"
no_notation "normal_rel" (infixl "⊲" 60)
lemma lookup_order1_prod:
assumes "⋀B. B∈set Bs ⟹ Tensor.order B = 1"
assumes "is ⊲ dims (prod_list Bs)"
shows "lookup (prod_list Bs) is = prod_list (map (λ(i,B). lookup B [i]) (zip is Bs))"
using assms proof (induction Bs arbitrary:"is")
case Nil
then show ?case unfolding "prod_list.Nil" unfolding zip.simps tensor_one_def
by (metis (no_types, lifting) dims_tensor_from_lookup length_greater_0_conv length_map prod_list.Nil
lookup_tensor_from_lookup tensor_one_def tensor_one_from_lookup)
next
case (Cons B Bs "is'")
then obtain i "is" where "is' = i # is"
by (metis append_is_Nil_conv dims_tensor_prod length_0_conv list.set_intros(1) prod_list.Cons valid_index.simps zero_neq_one)
have "Tensor.order B = 1" using Cons by auto
then have valid1:"[i] ⊲ dims B"
using ‹is' ⊲ dims (prod_list (B # Bs))›[unfolded prod_list.Cons dims_tensor_prod ‹is' = i # is›]
by (metis One_nat_def Suc_length_conv hd_append2 length_0_conv list.sel(1) list.simps(3) valid_index.Nil valid_index.simps)
have valid2:"is ⊲ dims (prod_list Bs)"
using ‹is' ⊲ dims (prod_list (B # Bs))›[unfolded prod_list.Cons dims_tensor_prod ‹is' = i # is›] ‹Tensor.order B = 1›
by (metis One_nat_def Suc_length_conv append_eq_Cons_conv length_0_conv list.sel(3) list.simps(3) self_append_conv2 valid_indexE)
show ?case unfolding ‹is' = i # is› List.zip_Cons_Cons List.list.map(2) prod_list.Cons
lookup_tensor_prod[OF valid1 valid2, simplified] by (simp add: Cons.IH Cons.prems(1) valid2)
qed
lemma matricize_cprank_max1:
fixes A::"'a::field tensor"
assumes "cprank_max1 A"
shows "mrank (matricize I A) ≤ 1"
proof -
obtain Bs a where "⋀B. B ∈ set Bs ⟹ Tensor.order B = 1" "a ⋅ prod_list Bs = A"
using cprank_max1_prod_listE assms by metis
define row_factor
where "row_factor ris = a * prod_list (map (λ(i,B). lookup B [i]) (zip ris (nths Bs I)))"
for ris
define col_factor
where "col_factor cis = prod_list (map (λ(i,B). lookup B [i]) (zip cis (nths Bs (-I))))"
for cis
have "⋀is. is ⊲ dims A ⟹ lookup A is = row_factor (nths is I) * col_factor (nths is (-I))"
proof -
fix "is" assume "is ⊲ dims A"
then have "lookup A is = a * (prod_list (map (λ(i,B). lookup B [i]) (zip is Bs)))"
using lookup_order1_prod[OF ‹⋀B. B ∈ set Bs ⟹ Tensor.order B = 1›] lookup_smult
using ‹a ⋅ prod_list Bs = A› dims_smult by fastforce
also have "... = a * (prod_list (map (λ(i,B). lookup B [i]) (nths (zip is Bs) I))) *
(prod_list (map (λ(i,B). lookup B [i]) (nths (zip is Bs) (-I))))"
using prod_list_complementary_nthss by auto
also have "... = row_factor (nths is I) * col_factor (nths is (-I))"
using nths_zip row_factor_def col_factor_def by metis
finally show "lookup A is = row_factor (nths is I) * col_factor (nths is (-I))" .
qed
define row_factor'
where "row_factor' r = row_factor (digit_encode (nths (Tensor.dims A) I) r)" for r
define col_factor'
where "col_factor' c = col_factor (digit_encode (nths (Tensor.dims A) (-I)) c)" for c
have "⋀r c. r<dim_row (matricize I A) ⟹ c<dim_col (matricize I A) ⟹ matricize I A $$ (r,c) = row_factor' r * col_factor' c"
proof -
fix r c assume "r<dim_row (matricize I A)" "c<dim_col (matricize I A)"
then have "matricize I A $$ (r,c) = Tensor.lookup A (weave I
(digit_encode (nths (Tensor.dims A) I) r)
(digit_encode (nths (Tensor.dims A) (-I)) c)
)" unfolding dims_matricize unfolding matricize_def by simp
also have "... = row_factor' r * col_factor' c"
using ‹⋀is. is ⊲ dims A ⟹ lookup A is = row_factor (nths is I) * col_factor (nths is (- I))›
valid_index_weave[OF
digit_encode_valid_index[OF ‹r < dim_row (matricize I A)›[unfolded dims_matricize]]
digit_encode_valid_index[OF ‹c < dim_col (matricize I A)›[unfolded dims_matricize]]]
valid_index_weave(2) valid_index_weave(3) row_factor'_def col_factor'_def by metis
finally show "matricize I A $$ (r,c) = row_factor' r * col_factor' c" .
qed
then show ?thesis using vec_space.rank_le_1_product_entries[of "matricize I A"] by blast
qed
lemma matrix_rank_le_cprank_max:
fixes A :: "('a::field) tensor"
assumes "cprank_max r A"
shows "mrank (matricize I A) ≤ r"
using assms
proof (induction rule:cprank_max.induct)
fix ds :: "nat list"
have "matricize I (tensor0 ds) = 0⇩m (dim_row (matricize I (tensor0 ds))) (dim_col (matricize I (tensor0 ds)))"
using matricize_0 by auto
then show "mrank (matricize I (tensor0 ds)) ≤ 0"
using eq_imp_le vec_space.rank_0I by metis
next
fix A B::"'a tensor" and j::nat
assume "dims A = dims B"
assume "cprank_max1 A"
assume "mrank (matricize I B) ≤ j"
have "mrank (matricize I A) ≤ 1" using ‹cprank_max1 A› matricize_cprank_max1 by auto
have "mrank (matricize I (A + B)) ≤ mrank (matricize I A) + mrank (matricize I B)"
using matricize_add vec_space.rank_subadditive dims_matricize
carrier_matI index_add_mat(2) ‹dims A = dims B› by metis
then show "mrank (matricize I (A + B)) ≤ Suc j"
using ‹mrank (matricize I A) ≤ 1› ‹mrank (matricize I B) ≤ j› by linarith
qed
lemma matrix_rank_le_cp_rank:
fixes A :: "('a::field) tensor"
shows "mrank (matricize I A) ≤ cprank A"
using matrix_rank_le_cprank_max using cprank_max_cprank by auto
end