Theory Bases_Of_Fundamental_Subspaces
section‹Bases of the four fundamental subspaces›
theory Bases_Of_Fundamental_Subspaces
imports
Gauss_Jordan_PA
begin
subsection‹Computation of the bases of the fundamental subspaces›
definition "basis_null_space A = {row i (P_Gauss_Jordan (transpose A)) | i. to_nat i ≥ rank A}"
definition "basis_row_space A = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) ≠ 0}"
definition "basis_col_space A = {row i (Gauss_Jordan (transpose A)) |i. row i (Gauss_Jordan (transpose A)) ≠ 0}"
definition "basis_left_null_space A = {row i (P_Gauss_Jordan A) | i. to_nat i ≥ rank A}"
subsection‹Relatioships amongst the bases›
lemma basis_null_space_eq_basis_left_null_space_transpose:
"basis_null_space A = basis_left_null_space (transpose A)"
unfolding basis_null_space_def
unfolding basis_left_null_space_def
unfolding rank_transpose[of A, symmetric] ..
lemma basis_null_space_transpose_eq_basis_left_null_space:
shows "basis_null_space (transpose A) = basis_left_null_space A"
by (metis transpose_transpose basis_null_space_eq_basis_left_null_space_transpose)
lemma basis_col_space_eq_basis_row_space_transpose:
"basis_col_space A = basis_row_space (transpose A)"
unfolding basis_col_space_def basis_row_space_def ..
subsection‹Code equations›
text‹Code equations to make more efficient the computations.›
lemma basis_null_space_code[code]: "basis_null_space A = (let GJ = Gauss_Jordan_PA (transpose A);
rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ) ≠ 0) + 1)
in {row i (fst GJ) | i. to_nat i ≥ rank_A})"
unfolding basis_null_space_def Let_def P_Gauss_Jordan_def
unfolding Gauss_Jordan_PA_eq
unfolding rank_transpose[symmetric, of A]
unfolding rank_Gauss_Jordan_code[of "transpose A"]
unfolding Let_def
unfolding transpose_zero ..
lemma basis_row_space_code[code]: "basis_row_space A = (let A' = Gauss_Jordan A in {row i A' |i. row i A' ≠ 0})"
unfolding basis_row_space_def Let_def ..
lemma basis_col_space_code[code]: "basis_col_space A = (let A' = Gauss_Jordan (transpose A) in {row i A' |i. row i A' ≠ 0})"
unfolding basis_col_space_def Let_def ..
lemma basis_left_null_space_code[code]: "basis_left_null_space A = (let GJ = Gauss_Jordan_PA A;
rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ) ≠ 0) + 1)
in {row i (fst GJ) | i. to_nat i ≥ rank_A})"
unfolding basis_left_null_space_def Let_def P_Gauss_Jordan_def
unfolding Gauss_Jordan_PA_eq
unfolding rank_Gauss_Jordan_code[of "A"]
unfolding Let_def
unfolding transpose_zero ..
subsection‹Demonstrations that they are bases›
text‹We prove that we have obtained a basis for each subspace›
lemma independent_basis_left_null_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "vec.independent (basis_left_null_space A)"
proof (unfold basis_left_null_space_def, rule vec.independent_mono)
show "vec.independent (rows (P_Gauss_Jordan A))"
by (metis P_Gauss_Jordan_def det_dependent_rows invertible_det_nz invertible_fst_Gauss_Jordan_PA)
show "{row i (P_Gauss_Jordan A) |i. rank A ≤ to_nat i} ⊆ (rows (P_Gauss_Jordan A))" unfolding rows_def by fast
qed
lemma card_basis_left_null_space_eq_dim:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "card (basis_left_null_space A) = vec.dim (left_null_space A)"
proof -
let ?f="λn. row (from_nat (n + (rank A))) (P_Gauss_Jordan A)"
have "card (basis_left_null_space A) = card {row i (P_Gauss_Jordan A) | i. to_nat i ≥ rank A}" unfolding basis_left_null_space_def ..
also have "... = card {..<(vec.dimension TYPE('a) TYPE('rows)) - rank A}"
proof (rule bij_betw_same_card[symmetric, of ?f], unfold bij_betw_def, rule conjI)
show "inj_on ?f {..<(vec.dimension TYPE('a) TYPE('rows)) - rank A}" unfolding inj_on_def
proof (auto, rule ccontr, unfold dimension_vector)
fix x y
assume x: "x <CARD('rows) - rank A"
and y: "y < CARD('rows) - rank A"
and eq: "row (from_nat (x + rank A)) (P_Gauss_Jordan A) = row (from_nat (y + rank A)) (P_Gauss_Jordan A)"
and x_not_y: "x ≠ y"
have "det (P_Gauss_Jordan A) = 0"
proof (rule det_identical_rows[OF _ eq])
have "(x + rank A) ≠ (y + rank A)" using x_not_y x y by simp
thus "(from_nat (x + rank A)::'rows) ≠ from_nat (y + rank A)" by (metis (mono_tags) from_nat_eq_imp_eq less_diff_conv x y)
qed
moreover have "invertible (P_Gauss_Jordan A)" by (metis P_Gauss_Jordan_def invertible_fst_Gauss_Jordan_PA)
ultimately show False unfolding invertible_det_nz by contradiction
qed
show "?f ` {..<(vec.dimension TYPE('a) TYPE('rows)) - rank A} = {row i (P_Gauss_Jordan A) |i. rank A ≤ to_nat i}"
proof (unfold image_def dimension_vector, auto, metis le_add2 less_diff_conv to_nat_from_nat_id)
fix i::'rows
assume rank_le_i: "rank A ≤ to_nat i"
show "∃x∈{..<CARD('rows) - rank A}. row i (P_Gauss_Jordan A) = row (from_nat (x + rank A)) (P_Gauss_Jordan A)"
proof (rule bexI[of _ "(to_nat i - rank A)"])
have "i = (from_nat (to_nat i - rank A + rank A))" by (metis rank_le_i from_nat_to_nat_id le_add_diff_inverse2)
thus "row i (P_Gauss_Jordan A) = row (from_nat (to_nat i - rank A + rank A)) (P_Gauss_Jordan A)" by presburger
show "to_nat i - rank A ∈ {..<CARD('rows) - rank A}" using rank_le_i by (metis diff_less_mono lessThan_def mem_Collect_eq to_nat_less_card)
qed
qed
qed
also have "... = (vec.dimension TYPE('a) TYPE('rows)) - rank A" unfolding card_lessThan ..
also have "... = vec.dim (null_space (transpose A))" unfolding dim_null_space rank_transpose ..
also have "... = vec.dim (left_null_space A)" unfolding left_null_space_eq_null_space_transpose ..
finally show ?thesis .
qed
lemma basis_left_null_space_in_left_null_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "basis_left_null_space A ⊆ left_null_space A"
proof (unfold basis_left_null_space_def left_null_space_def, auto)
fix i::'rows
assume rank_le_i: " rank A ≤ to_nat i"
have "row i (P_Gauss_Jordan A) v* A = ((P_Gauss_Jordan A) $ i) v* A" unfolding row_def vec_nth_inverse ..
also have "... = ((P_Gauss_Jordan A) ** A) $ i" unfolding row_matrix_matrix_mult by simp
also have "... = (Gauss_Jordan A) $ i" unfolding P_Gauss_Jordan_def Gauss_Jordan_PA_eq[symmetric] using fst_Gauss_Jordan_PA by metis
also have "... = 0" by (rule rank_less_row_i_imp_i_is_zero[OF rank_le_i])
finally show "row i (P_Gauss_Jordan A) v* A = 0" .
qed
lemma left_null_space_subset_span_basis:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "left_null_space A ⊆ vec.span (basis_left_null_space A)"
proof (rule vec.card_ge_dim_independent)
show "basis_left_null_space A ⊆ left_null_space A" by (rule basis_left_null_space_in_left_null_space)
show "vec.independent (basis_left_null_space A)" by (rule independent_basis_left_null_space)
show "vec.dim (left_null_space A) ≤ card (basis_left_null_space A)"
proof -
have "{x. x v* A = 0} = {x. (transpose A) *v x = 0}" by (metis transpose_vector)
thus ?thesis using card_basis_left_null_space_eq_dim by (metis order_refl)
qed
qed
corollary basis_left_null_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "vec.independent (basis_left_null_space A) ∧
left_null_space A = vec.span (basis_left_null_space A)"
by (metis basis_left_null_space_in_left_null_space independent_basis_left_null_space
left_null_space_subset_span_basis vec.span_subspace subspace_left_null_space)
corollary basis_null_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "vec.independent (basis_null_space A) ∧
null_space A = vec.span (basis_null_space A)"
unfolding basis_null_space_eq_basis_left_null_space_transpose
unfolding null_space_eq_left_null_space_transpose
by (rule basis_left_null_space)
lemma basis_row_space_subset_row_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "basis_row_space A ⊆ row_space A"
proof -
have "basis_row_space A = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) ≠ 0}" unfolding basis_row_space_def ..
also have "... ⊆ row_space (Gauss_Jordan A)"
proof (unfold row_space_def, clarify)
fix i assume "row i (Gauss_Jordan A) ≠ 0"
show "row i (Gauss_Jordan A) ∈ vec.span (rows (Gauss_Jordan A))"
using rows_def vec.span_base by auto
qed
also have "... = row_space A" unfolding Gauss_Jordan_PA_eq[symmetric] unfolding fst_Gauss_Jordan_PA[symmetric]
by (rule row_space_is_preserved[OF invertible_fst_Gauss_Jordan_PA])
finally show ?thesis .
qed
lemma row_space_subset_span_basis_row_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "row_space A ⊆ vec.span (basis_row_space A)"
proof (rule vec.card_ge_dim_independent)
show "basis_row_space A ⊆ row_space A" by (rule basis_row_space_subset_row_space)
show "vec.independent (basis_row_space A)" unfolding basis_row_space_def by (rule independent_not_zero_rows_rref[OF rref_Gauss_Jordan])
show "vec.dim (row_space A) ≤ card (basis_row_space A)"
unfolding basis_row_space_def
using rref_rank[OF rref_Gauss_Jordan, of A] unfolding row_rank_def[symmetric] rank_def[symmetric] rank_Gauss_Jordan[symmetric] by fastforce
qed
lemma basis_row_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "vec.independent (basis_row_space A)
∧ vec.span (basis_row_space A) = row_space A"
proof (rule conjI)
show "vec.independent (basis_row_space A)" unfolding basis_row_space_def using independent_not_zero_rows_rref[OF rref_Gauss_Jordan] .
show "vec.span (basis_row_space A) = row_space A"
proof (rule vec.span_subspace)
show "basis_row_space A ⊆ row_space A" by (rule basis_row_space_subset_row_space)
show "row_space A ⊆ vec.span (basis_row_space A)" by (rule row_space_subset_span_basis_row_space)
show "vec.subspace (row_space A)" by (rule subspace_row_space)
qed
qed
corollary basis_col_space:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "vec.independent (basis_col_space A)
∧ vec.span (basis_col_space A) = col_space A"
unfolding col_space_eq_row_space_transpose basis_col_space_eq_basis_row_space_transpose
by (rule basis_row_space)
end