Theory Fundamental_Subspaces

header{*Fundamental Subspaces*}

theory Fundamental_Subspaces
imports 
    "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
    Miscellaneous
begin

(*  
    Title:      Fundamental_Subspaces.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{*The fundamental subspaces of a matrix*}

subsubsection{*Definitions*}

definition left_null_space :: "'a::{semiring_1}^'n^'m => ('a^'m) set"
  where "left_null_space A = {x. x v* A = 0}"

definition null_space :: "'a::{semiring_1}^'n^'m => ('a^'n) set"
  where "null_space A = {x. A *v x = 0}"
  
definition row_space :: "'a::{field}^'n^'m=>('a^'n) set"
  where "row_space A = vec.span (rows A)"

definition col_space :: "'a::{field}^'n^'m=>('a^'m) set"
  where "col_space A = vec.span (columns A)"

subsubsection{*Relationships among them*}

lemma left_null_space_eq_null_space_transpose: "left_null_space A = null_space (transpose A)"
  unfolding null_space_def left_null_space_def transpose_vector ..

lemma null_space_eq_left_null_space_transpose: "null_space A = left_null_space (transpose A)" 
  using left_null_space_eq_null_space_transpose[of "transpose A"]
  unfolding transpose_transpose ..

lemma row_space_eq_col_space_transpose:
  fixes A::"'a::{field}^'columns^'rows"
  shows "row_space A = col_space (transpose A)"
  unfolding col_space_def row_space_def columns_transpose[of A] ..

lemma col_space_eq_row_space_transpose:
  fixes A::"'a::{field}^'n^'m"
  shows "col_space A = row_space (transpose A)"
  unfolding col_space_def row_space_def unfolding rows_transpose[of A] ..

  
subsection{*Proving that they are subspaces*}

lemma subspace_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (null_space A)"
proof (unfold vec.subspace_def null_space_def, auto)
  show "A *v 0 = 0" by (metis add_diff_cancel eq_iff_diff_eq_0 matrix_vector_right_distrib) 
  fix x y
  assume Ax: "A *v x = 0" and Ay: "A *v y = 0"
  have "A *v (x + y) = (A *v x) + (A *v y)" unfolding matrix_vector_right_distrib ..
  also have "... = 0" unfolding Ax Ay by simp
  finally show "A *v (x + y) = 0" .
  fix c 
  have "A *v (c *s x) = c *s (A *v x)"
    unfolding scalar_matrix_vector_assoc matrix_scalar_vector_ac by auto
  also have "... = 0" unfolding Ax by simp
  finally show "A *v (c *s x) = 0" .
  qed

lemma subspace_left_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (left_null_space A)"
  unfolding left_null_space_eq_null_space_transpose using subspace_null_space .

lemma subspace_row_space:
  shows "vec.subspace (row_space A)" by (metis row_space_def vec.subspace_span)

lemma subspace_col_space:
  shows "vec.subspace (col_space A)" by (metis col_space_def vec.subspace_span)
  
subsection{*More useful properties and equivalences*}

(* In the previous version of the development, we had the following lemma proved over a real matrix.
  Now we want to generalize it, but if we follow the proof presented in the previous formalization,
  we have to impose the restriction semiring_char_0:*)

(*
lemma col_space_eq:
  fixes A::"'a::{field, semiring_char_0}^'m^'n"
  shows "col_space A = {y. ∃x. A *v x = y}"
proof (unfold col_space_def vector_space.span_explicit[OF vector_space_scale], rule)
  show "{y. ∃x. A *v x = y} ⊆ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *s v) = y}"
  proof (rule)
    fix y assume y: "y ∈ {y. ∃x. A *v x = y}"
    obtain x where x:"A *v x = y" using y by blast
    obtain f where setsum: "A *v x = setsum (λy. f y *s y)  (columns A)" using matrix_vmult_column_sum by auto  
    show "y ∈ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *s v) = y}"
      by (rule, rule exI[of _ "columns A"], auto, rule finite_columns, rule exI[of _ "f"], metis x setsum)      
  qed
next
  show "{y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *s v) = y} ⊆ {y. ∃x. A *v x = y}"
  proof (rule, auto)
    fix S and u::"('a, 'n) vec => 'a"
    assume finite_S: "finite S" and S_in_cols: "S ⊆ columns A"
    let ?f="λx. if x ∈ S then u x else 0"
    let ?x ="(χ i. if column i A ∈ S then (inverse (of_nat (card {a. column i A=column a A}))) * u (column i A) else 0)" 
    show "∃x. A *v x = (∑v∈S. (u v) *s v)"
    proof (unfold matrix_mult_vsum, rule exI[of _ "?x"], simp)
      let ?g="λy. {i. y=column i A}"
      have inj: "inj_on ?g (columns A)" unfolding inj_on_def unfolding columns_def by auto
      have union_univ: "\<Union>(?g`(columns A)) = UNIV" unfolding columns_def by auto               
      have "setsum (λi.(if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) UNIV 
        = setsum (λi.(if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) (\<Union>(?g`(columns A)))"
        unfolding union_univ ..
      also have "... = setsum (setsum (λi.(if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A)) (?g`(columns A))" 
        by (rule setsum_Union_disjoint, auto)
      also have "... = setsum ((setsum (λi.(if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A)) o ?g) 
        (columns A)" by (rule setsum_reindex, simp add: inj)
      also have "... = setsum (λy. ?f y  *s y) (columns A)"
      proof (rule setsum_cong2, auto)
        fix x
        assume x_in_cols: "x ∈ columns A" and x_notin_S: "x ∉ S"
        show "(∑i | x = column i A. (if column i A ∈ S then (inverse (of_nat (card {a. column i A = column a A}))) * u (column i A) else 0) *s column i A) = 0"
          apply (rule setsum_0') using x_notin_S by auto
      next
        fix x
        assume x_in_cols: "x ∈ columns A" and x_in_S: "x ∈ S"      
        have "setsum (λi. (if column i A ∈ S then (inverse (of_nat (card {a. column i A = column a A}))) * u (column i A) else 0) *s column i A) {i. x = column i A} = 
          setsum (λi. (inverse (of_nat (card {a. column i A = column a A}))) * u (column i A) *s column i A) {i. x = column i A}" apply (rule setsum_cong2) using x_in_S by simp
        also have "... = setsum (λi. (inverse (of_nat (card {a. x = column a A}))) * u x *s x) {i. x = column i A}" by auto
        also have "... = of_nat (card {i. x = column i A}) * (inverse (of_nat (card {a. x = column a A})) * u x *s x)" unfolding setsum_constant ..
        also have "... =  of_nat (card {i. x = column i A}) * (inverse (of_nat (card {a. x = column a A})) *s (u x *s x))" 
          unfolding vector_smult_assoc [of "inverse (of_nat (card {a. x = column a A}))" " u x" x , symmetric] ..        
        also have "... = of_nat (card {i. x = column i A}) *s (inverse (of_nat (card {a. x = column a A})) *s (u x *s x))"     
        proof auto
            have "!!v x⇩1 x⇩4. of_nat (card (v::'m set)) * x⇩1 *s (x⇩4::('a, 'n) vec) = (∑Q∈v. x⇩1 *s x⇩4)"
             by (metis Generalizations.setsum_constant_scaleR vector_space_Kn.scale_scale)
            hence "of_nat (card {R. x = column R A}) * (inverse (of_nat (card {R. x = column R A})) * u x) *s x = (∑Q∈{R. x = column R A}. inverse (of_nat (card {R. x = column R A})) * u x *s x)"
              by arith
            thus "of_nat (card {i. x = column i A}) * (inverse (of_nat (card {a. x = column a A})) * u x *s x) = of_nat (card {i. x = column i A}) * (inverse (of_nat (card {a. x = column a A})) * u x) *s x"
              using `(∑i::'m::finite | x = column i A. inverse (of_nat (card {a::'m::finite. (x::('a::{field,semiring_char_0}, 'n::finite) vec) = column a (A::(('a::{field,semiring_char_0}, 'm::finite) vec, 'n::finite) vec)})) * (u::('a::{field,semiring_char_0}, 'n::finite) vec => 'a::{field,semiring_char_0}) x *s x) = of_nat (card {i::'m::finite. x = column i A}) * (inverse (of_nat (card {a::'m::finite. x = column a A})) * u x *s x)` by simp
          qed        
        also have "... =  (of_nat (card {i. x = column i A}) * inverse (of_nat (card {a. x = column a A}))) *s (u x *s x)" unfolding vector_smult_assoc by auto
        also have "... = 1 *s (u x *s x)" apply (auto, rule right_inverse)  using x_in_cols unfolding columns_def by auto
        also have "... = u x *s x" by auto
        finally show " (∑i | x = column i A. (if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = u x *s x" .
      qed
      also have "... = setsum (λy. ?f y  *s y) (S ∪ ((columns A) - S))" apply (rule setsum_cong) using S_in_cols by auto
      also have "... = setsum (λy. ?f y  *s y) S + setsum  (λy. ?f y *s y) ((columns A) - S)" apply (rule setsum_Un_disjoint) using S_in_cols finite_S finite_columns by auto
      also have "... = setsum (λy. ?f y  *s y) S" by simp
      finally show "(∑i∈UNIV. (if column i A ∈ S then inverse (of_nat (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = (∑v∈S. u v *s v)" by auto
    qed 
  qed
qed*)

(*So we have had to change completely the proof:*)
lemma col_space_eq:
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = {y. ∃x. A *v x = y}"
  proof (unfold col_space_def vec.span_finite[OF finite_columns], auto)
  fix x
  show "∃u. (∑v∈columns A. u v *s v) = A *v x"  using matrix_vmult_column_sum[of A x] by auto
  next
  fix u::"('a, 'n) vec => 'a"
  let ?g="λy. {i. y=column i A}"
  let ?x="(χ i. if i=(LEAST a. a ∈ ?g (column i A)) then u (column i A) else 0)"
  show "∃x. A *v x = (∑v∈columns A. u v *s v)"
  proof (unfold matrix_mult_vsum, rule exI[of _ "?x"], auto)
      have inj: "inj_on ?g (columns A)" unfolding inj_on_def unfolding columns_def by auto
      have union_univ: "\<Union>(?g`(columns A)) = UNIV" unfolding columns_def by auto               
      have "setsum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) UNIV 
        = setsum (λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) (\<Union>(?g`(columns A)))"
        unfolding union_univ ..
    also have "... = setsum (setsum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)) (?g`(columns A))" 
        by (rule setsum_Union_disjoint, auto)
      also have "... = setsum ((setsum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)) o ?g) 
        (columns A)" by (rule setsum_reindex, simp add: inj)
      also have "... = setsum (λy. u y *s y) (columns A)"
       proof (rule setsum_cong2, auto)
        fix x
        assume x_in_cols: "x ∈ columns A"
        obtain b where b: "x=column b A" using x_in_cols unfolding columns_def by blast
        let ?f="(λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)" 
        have setsum_rw: "setsum ?f ({i. x = column i A} - {LEAST a. x = column a A}) = 0"
          by (rule setsum_0', auto)
        have "setsum ?f {i. x = column i A} = ?f (LEAST a. x = column a A) + setsum ?f ({i. x = column i A} - {LEAST a. x = column a A})" 
          apply (rule setsum_diff1', auto, rule LeastI_ex) 
          using x_in_cols unfolding columns_def by auto
        also have "... = ?f (LEAST a. x = column a A)" unfolding setsum_rw by simp
        also have "... = u x *s x"
        proof (auto, rule LeastI2)
          show "x = column b A" using b .
          fix xa
          assume x: "x = column xa A"
          show "u (column xa A) *s column xa A = u x *s x" unfolding x ..
          next
          assume "(LEAST a. x = column a A) ≠ (LEAST a. column (LEAST c. x = column c A) A = column a A)"
          moreover have "(LEAST a. x = column a A) = (LEAST a. column (LEAST c. x = column c A) A = column a A)"
            by (rule Least_equality[symmetric], rule LeastI2, simp_all add: b, rule Least_le, metis (lifting, full_types) LeastI)
          ultimately show "u x = 0" by contradiction
          qed
       finally show " (∑i | x = column i A. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = u x *s x" .
       qed
  finally show "(∑i∈UNIV. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = (∑y∈columns A. u y *s y)" .
qed
qed
 

corollary col_space_eq':
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = range (λx. A *v x)"
  unfolding col_space_eq by auto

lemma row_space_eq:
  fixes A::"'a::{field}^'m^'n::{finite, wellorder}"
  shows "row_space A = {w. ∃y. (transpose A) *v y = w}"
  unfolding row_space_eq_col_space_transpose col_space_eq ..

lemma null_space_eq_ker:
  fixes f::"('a::field^'n) => ('a^'m)"
  assumes lf: "linear op *s op *s f"
  shows "null_space (matrix f) = {x. f x = 0}" 
  unfolding null_space_def using matrix_works [OF lf] by auto

lemma col_space_eq_range:
  fixes f::"('a::field^'n::{finite, wellorder}) => ('a^'m)"
  assumes lf: "linear op *s op *s f"
  shows "col_space (matrix f) = range f"
  unfolding col_space_eq unfolding matrix_works[OF lf] by blast

lemma null_space_is_preserved:
fixes A::"'a::{field}^'cols^'rows"
assumes P: "invertible P"
shows "null_space (P**A) = null_space A"
unfolding null_space_def 
using P matrix_inv_left matrix_left_invertible_ker matrix_vector_mul_assoc matrix_vector_zero
by metis

lemma row_space_is_preserved:
fixes A::"'a::{field}^'cols^'rows::{finite, wellorder}" 
  and P::"'a::{field}^'rows::{finite, wellorder}^'rows::{finite, wellorder}"
assumes P: "invertible P"
shows "row_space (P**A) = row_space A"
proof (auto)
fix w
assume w: "w ∈ row_space (P**A)"
from this obtain y where w_By: "w=(transpose (P**A)) *v y" unfolding row_space_eq[of "P ** A" ] by fast
have "w = (transpose (P**A)) *v y" using w_By .
also have "... = ((transpose A) ** (transpose P)) *v y" unfolding matrix_transpose_mul ..
also have "... = (transpose A) *v ((transpose P) *v y)" unfolding matrix_vector_mul_assoc ..
finally show "w ∈ row_space A" unfolding row_space_eq by blast
next
fix w
assume w: "w ∈ row_space A"
from this obtain y where w_Ay: "w=(transpose A) *v y" unfolding row_space_eq by fast
have "w = (transpose A) *v y" using w_Ay .
also have "... = (transpose ((matrix_inv P) ** (P**A))) *v y" by (metis P matrix_inv_left matrix_mul_assoc matrix_mul_lid)
also have "... = (transpose (P**A) ** (transpose (matrix_inv P))) *v y" unfolding matrix_transpose_mul ..
also have "... = transpose (P**A) *v (transpose (matrix_inv P) *v y)" unfolding matrix_vector_mul_assoc ..
finally show "w ∈ row_space (P**A)"  unfolding row_space_eq by blast
qed
end