header{*Fundamental Subspaces*}
theory Fundamental_Subspaces
imports
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
Miscellaneous
begin
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::{real_vector}^'n^'m=>('a^'n) set"
where "row_space A = span (rows A)"
definition col_space :: "'a::{real_vector}^'n^'m=>('a^'m) set"
where "col_space A = 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::{real_vector, semiring_1}^'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::{real_vector,semiring_1}^'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::{semiring_1, real_algebra}^'n^'m"
shows "subspace (null_space A)"
proof (unfold 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 *⇩R x = c *⇩R (A *v x)" unfolding scalar_matrix_vector_assoc matrix_scalar_vector_ac ..
also have "... = 0" unfolding Ax by simp
finally show "A *v c *⇩R x = 0" .
qed
lemma subspace_left_null_space:
fixes A::"'a::{semiring_1, real_algebra}^'n^'m"
shows "subspace (left_null_space A)"
unfolding left_null_space_eq_null_space_transpose using subspace_null_space .
lemma subspace_row_space:
shows "subspace (row_space A)" by (metis row_space_def subspace_span)
lemma subspace_col_space:
shows "subspace (col_space A)" by (metis col_space_def subspace_span)
subsection{*More useful properties and equivalences*}
lemma col_space_eq:
fixes A::"real^'m^'n"
shows "col_space A = {y. ∃x. A *v x = y}"
proof (unfold col_space_def span_explicit, rule)
show "{y. ∃x. A *v x = y} ⊆ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *⇩R 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 *⇩R y) (columns A)" using matrix_vmult_column_sum by auto
show "y ∈ {y. ∃S u. finite S ∧ S ⊆ columns A ∧ (∑v∈S. u v *⇩R 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 *⇩R v) = y} ⊆ {y. ∃x. A *v x = y}"
proof (rule, auto)
fix S and u::"(real, 'n) vec => real"
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 (real (card {a. column i A=column a A}))) * u (column i A) else 0)"
show "∃x. A *v x = (∑v∈S. u v *⇩R 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 (real (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 (real (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 (real (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 (real (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 *⇩R 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 (real (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 (real (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 (real (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 (real (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 (real (card {a. x = column a A})) * u x *s x)" unfolding setsum_constant ..
also have "... = of_nat (card {i. x = column i A}) * (inverse (real (card {a. x = column a A})) *s (u x *s x))"
unfolding vector_smult_assoc [of "inverse (real (card {a. x = column a A}))" " u x" x , symmetric] ..
also have "... = real (card {i. x = column i A}) *⇩R (inverse (real (card {a. x = column a A})) *s (u x *s x))"
by (auto, metis real_of_nat_def setsum_constant setsum_constant_scaleR)
also have "... = real (card {i. x = column i A}) *s (inverse (real (card {a. x = column a A})) *s (u x *s x))" unfolding scalar_mult_eq_scaleR ..
also have "... = (real (card {i. x = column i A}) * inverse (real (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
also have "... = u x *⇩R x" unfolding scalar_mult_eq_scaleR ..
finally show " (∑i | x = column i A. (if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = u x *⇩R x" .
qed
also have "... = setsum (λy. ?f y *⇩R y) (S ∪ ((columns A) - S))" apply (rule setsum_cong) using S_in_cols by auto
also have "... = setsum (λy. ?f y *⇩R y) S + setsum (λy. ?f y *⇩R 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 *⇩R y) S" by simp
finally show "(∑i∈UNIV. (if column i A ∈ S then inverse (real (card {a. column i A = column a A})) * u (column i A) else 0) *s column i A) = (∑v∈S. u v *⇩R v)" by auto
qed
qed
qed
corollary col_space_eq':
fixes A::"real^'m^'n"
shows "col_space A = range (λx. A *v x)"
unfolding col_space_eq by auto
lemma row_space_eq:
fixes A::"real^'n^'m"
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::"(real^'n) => (real^'m)"
assumes lf: "linear 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::"(real^'a) => (real^'b)"
assumes lf: "linear 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::"real^'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::"real^'cols^'rows"
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 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