Theory Rank_Nullity_Theorem.Miscellaneous
section‹Miscellaneous›
theory Miscellaneous
imports
"HOL-Analysis.Determinants"
Mod_Type
"HOL-Library.Function_Algebras"
begin
context Vector_Spaces.linear begin
sublocale vector_space_pair by unfold_locales
end
hide_const (open) Real_Vector_Spaces.linear
abbreviation "linear ≡ Vector_Spaces.linear"
text‹In this file, we present some basic definitions and lemmas about linear algebra and matrices.›
subsection‹Definitions of number of rows and columns of a matrix›
definition nrows :: "'a^'columns^'rows => nat"
where "nrows A = CARD('rows)"
definition ncols :: "'a^'columns^'rows => nat"
where "ncols A = CARD('columns)"
definition matrix_scalar_mult :: "'a::ab_semigroup_mult => 'a ^'n^'m => 'a ^'n^'m"
(infixl ‹*k› 70)
where "k *k A ≡ (χ i j. k * A $ i $ j)"
subsection‹Basic properties about matrices›
lemma nrows_not_0[simp]:
shows "0 ≠ nrows A" unfolding nrows_def by simp
lemma ncols_not_0[simp]:
shows "0 ≠ ncols A" unfolding ncols_def by simp
lemma nrows_transpose: "nrows (transpose A) = ncols A"
unfolding nrows_def ncols_def ..
lemma ncols_transpose: "ncols (transpose A) = nrows A"
unfolding nrows_def ncols_def ..
lemma finite_rows: "finite (rows A)"
using finite_Atleast_Atmost_nat[of "λi. row i A"] unfolding rows_def .
lemma finite_columns: "finite (columns A)"
using finite_Atleast_Atmost_nat[of "λi. column i A"] unfolding columns_def .
lemma transpose_vector: "x v* A = transpose A *v (x::'a::comm_semiring_1^'m)"
by simp
lemma transpose_zero[simp]: "(transpose A = 0) = (A = 0)"
unfolding transpose_def zero_vec_def vec_eq_iff by auto
subsection‹Theorems obtained from the AFP›
text‹The following theorems and definitions have been obtained from the AFP
@{url "http://isa-afp.org/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html"}.
I have removed some restrictions over the type classes.›
lemma vector_scalar_matrix_ac:
fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
shows "x v* (k *k A) = k *s (x v* A)"
using scalar_vector_matrix_assoc
unfolding vector_matrix_mult_def matrix_scalar_mult_def vec_eq_iff
by (simp add: sum_distrib_left vector_space_over_itself.scale_scale)
(simp add: mult.commute)
lemma transpose_scalar: "transpose (k *k A) = k *k transpose A"
unfolding transpose_def
by (vector, simp add: matrix_scalar_mult_def)
lemma scalar_matrix_vector_assoc:
fixes A :: "'a::{field}^'m^'n"
shows "k *s (A *v v) = k *k A *v v"
by (metis transpose_scalar vector_scalar_matrix_ac vector_transpose_matrix)
lemma matrix_scalar_vector_ac:
fixes A :: "'a::{field}^'m^'n"
shows "A *v (k *s v) = k *k A *v v"
by (simp add: Miscellaneous.scalar_matrix_vector_assoc vec.scale)
definition
is_basis :: "('a::{field}^'n) set => bool" where
"is_basis S ≡ vec.independent S ∧ vec.span S = UNIV"
lemma card_finite:
assumes "card S = CARD('n::finite)"
shows "finite S"
proof -
from ‹card S = CARD('n)› have "card S ≠ 0" by simp
with card_eq_0_iff [of S] show "finite S" by simp
qed
lemma independent_is_basis:
fixes B :: "('a::{field}^'n) set"
shows "vec.independent B ∧ card B = CARD('n) ⟷ is_basis B"
proof
assume "vec.independent B ∧ card B = CARD('n)"
hence "vec.independent B" and "card B = CARD('n)" by simp+
from card_finite [of B, where 'n = 'n] and ‹card B = CARD('n)›
have "finite B" by simp
from ‹card B = CARD('n)›
have "card B = vec.dim (UNIV :: (('a^'n) set))" unfolding vec_dim_card .
with vec.card_eq_dim [of B UNIV] and ‹finite B› and ‹vec.independent B›
have "vec.span B = UNIV" by auto
with ‹vec.independent B› show "is_basis B" unfolding is_basis_def ..
next
assume "is_basis B"
hence "vec.independent B" unfolding is_basis_def ..
moreover have "card B = CARD('n)"
proof -
have "B ⊆ UNIV" by simp
moreover
{ from ‹is_basis B› have "UNIV ⊆ vec.span B" and "vec.independent B"
unfolding is_basis_def
by simp+ }
ultimately have "card B = vec.dim (UNIV::((real^'n) set))"
using vec.basis_card_eq_dim [of B UNIV]
unfolding vec_dim_card
by simp
then show "card B = CARD('n)"
by (metis vec_dim_card)
qed
ultimately show "vec.independent B ∧ card B = CARD('n)" ..
qed
lemma basis_finite:
fixes B :: "('a::{field}^'n) set"
assumes "is_basis B"
shows "finite B"
proof -
from independent_is_basis [of B] and ‹is_basis B› have "card B = CARD('n)"
by simp
with card_finite [of B, where 'n = 'n] show "finite B" by simp
qed
text‹Here ends the statements obtained from AFP:
@{url "http://isa-afp.org/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html"}
which have been generalized.›
subsection‹Basic properties involving span, linearity and dimensions›
context finite_dimensional_vector_space
begin
text‹This theorem is the reciprocal theorem of @{thm "indep_card_eq_dim_span"}›
lemma card_eq_dim_span_indep:
assumes "dim (span A) = card A" and "finite A"
shows "independent A"
by (metis assms card_le_dim_spanning dim_subset equalityE span_superset)
lemma dim_zero_eq:
assumes dim_A: "dim A = 0"
shows "A = {} ∨ A = {0}"
using dim_A local.card_ge_dim_independent local.independent_empty by force
lemma dim_zero_eq':
assumes A: "A = {} ∨ A = {0}"
shows "dim A = 0"
using assms local.dim_span local.indep_card_eq_dim_span local.independent_empty by fastforce
lemma dim_zero_subspace_eq:
assumes subs_A: "subspace A"
shows "(dim A = 0) = (A = {0})"
by (metis dim_zero_eq dim_zero_eq' subspace_0[OF subs_A] empty_iff)
lemma span_0_imp_set_empty_or_0:
assumes "span A = {0}"
shows "A = {} ∨ A = {0}" by (metis assms span_superset subset_singletonD)
end
context Vector_Spaces.linear
begin
lemma linear_injective_ker_0:
shows "inj f = ({x. f x = 0} = {0})"
using inj_iff_eq_0 by auto
end
lemma snd_if_conv:
shows "snd (if P then (A,B) else (C,D))=(if P then B else D)" by simp
subsection‹Basic properties about matrix multiplication›
lemma row_matrix_matrix_mult:
fixes A::"'a::{comm_ring_1}^'n^'m"
shows "(P $ i) v* A = (P ** A) $ i"
unfolding vec_eq_iff
unfolding vector_matrix_mult_def unfolding matrix_matrix_mult_def
by (auto intro!: sum.cong)
corollary row_matrix_matrix_mult':
fixes A::"'a::{comm_ring_1}^'n^'m"
shows "(row i P) v* A = row i (P ** A)"
using row_matrix_matrix_mult unfolding row_def vec_nth_inverse .
lemma column_matrix_matrix_mult:
shows "column i (P**A) = P *v (column i A)"
unfolding column_def matrix_vector_mult_def matrix_matrix_mult_def by fastforce
lemma matrix_matrix_mult_inner_mult:
shows "(A ** B) $ i $ j = row i A ∙ column j B"
unfolding inner_vec_def matrix_matrix_mult_def row_def column_def by auto
lemma matrix_vmult_column_sum:
fixes A::"'a::{field}^'n^'m"
shows "∃f. A *v x = sum (λy. f y *s y) (columns A)"
proof (rule exI[of _ "λy. sum (λi. x $ i) {i. y = column i A}"])
let ?f="λy. sum (λi. x $ i) {i. y = column i A}"
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: "⋃ (?g`(columns (A))) = UNIV" unfolding columns_def by auto
have "A *v x = (∑i∈UNIV. x $ i *s column i A)" unfolding matrix_mult_sum ..
also have "... = sum (λi. x $ i *s column i A) (⋃(?g`(columns A)))" unfolding union_univ ..
also have "... = sum (sum ((λi. x $ i *s column i A))) (?g`(columns A))"
by (rule sum.Union_disjoint[unfolded o_def], auto)
also have "... = sum ((sum ((λi. x $ i *s column i A))) ∘ ?g) (columns A)"
by (rule sum.reindex, simp add: inj)
also have "... = sum (λy. ?f y *s y) (columns A)"
proof (rule sum.cong, unfold o_def)
fix xa
have "sum (λi. x $ i *s column i A) {i. xa = column i A}
= sum (λi. x $ i *s xa) {i. xa = column i A}" by simp
also have "... = sum (λi. x $ i) {i. xa = column i A} *s xa"
using vec.scale_sum_left[of "(λi. x $ i)" "{i. xa = column i A}" xa] ..
finally show "(∑i | xa = column i A. x $ i *s column i A) = (∑i | xa = column i A. x $ i) *s xa" .
qed rule
finally show "A *v x = (∑y∈columns A. (∑i | y = column i A. x $ i) *s y)" .
qed
subsection‹Properties about invertibility›
lemma matrix_inv:
assumes "invertible M"
shows matrix_inv_left: "matrix_inv M ** M = mat 1"
and matrix_inv_right: "M ** matrix_inv M = mat 1"
using ‹invertible M› and someI_ex [of "λ N. M ** N = mat 1 ∧ N ** M = mat 1"]
unfolding invertible_def and matrix_inv_def
by simp_all
text‹In the library, @{thm "matrix_inv_def"} allows the use of non squary matrices.
The following lemma can be also proved fixing @{term "A::'a::{semiring_1}^'n^'m"}›
lemma matrix_inv_unique:
fixes A::"'a::{semiring_1}^'n^'n"
assumes AB: "A ** B = mat 1" and BA: "B ** A = mat 1"
shows "matrix_inv A = B"
by (metis AB BA invertible_def matrix_inv_right matrix_mul_assoc matrix_mul_lid)
lemma matrix_vector_mult_zero_eq:
assumes P: "invertible P"
shows "((P**A)*v x = 0) = (A *v x = 0)"
proof (rule iffI)
assume "P ** A *v x = 0"
hence "matrix_inv P *v (P ** A *v x) = matrix_inv P *v 0" by simp
hence "matrix_inv P *v (P ** A *v x) = 0" by (metis matrix_vector_mult_0_right)
hence "(matrix_inv P ** P ** A) *v x = 0" by (metis matrix_vector_mul_assoc)
thus "A *v x = 0" by (metis assms matrix_inv_left matrix_mul_lid)
next
assume "A *v x = 0"
thus "P ** A *v x = 0" by (metis matrix_vector_mul_assoc matrix_vector_mult_0_right)
qed
lemma independent_image_matrix_vector_mult:
fixes P::"'a::{field}^'n^'m"
assumes ind_B: "vec.independent B" and inv_P: "invertible P"
shows "vec.independent (((*v) P)` B)"
proof (rule vec.independent_injective_image)
show "vec.independent B" using ind_B .
show "inj_on ((*v) P) (vec.span B)"
using inj_matrix_vector_mult[OF inv_P] unfolding inj_on_def by simp
qed
lemma independent_preimage_matrix_vector_mult:
fixes P::"'a::{field}^'n^'n"
assumes ind_B: "vec.independent (((*v) P)` B)" and inv_P: "invertible P"
shows "vec.independent B"
proof -
have "vec.independent (((*v) (matrix_inv P))` (((*v) P)` B))"
proof (rule independent_image_matrix_vector_mult)
show "vec.independent ((*v) P ` B)" using ind_B .
show "invertible (matrix_inv P)"
by (metis matrix_inv_left matrix_inv_right inv_P invertible_def)
qed
moreover have "((*v) (matrix_inv P))` (((*v) P)` B) = B"
proof (auto)
fix x assume x: "x ∈ B" show "matrix_inv P *v (P *v x) ∈ B"
by (metis (full_types) x inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
thus "x ∈ (*v) (matrix_inv P) ` (*v) P ` B"
unfolding image_def
by (auto, metis inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
qed
ultimately show ?thesis by simp
qed
subsection‹Properties about the dimension of vectors›
lemma dimension_vector[code_unfold]: "vec.dimension TYPE('a::{field}) TYPE('rows::{mod_type})=CARD('rows)"
proof -
let ?f="λx. axis (from_nat x) 1::'a^'rows::{mod_type}"
have "vec.dimension TYPE('a::{field}) TYPE('rows::{mod_type}) = card (cart_basis::('a^'rows::{mod_type}) set)"
unfolding vec.dimension_def ..
also have "... = card{..<CARD('rows)}" unfolding cart_basis_def
proof (rule bij_betw_same_card[symmetric, of ?f], unfold bij_betw_def, unfold inj_on_def axis_eq_axis, auto)
fix x y assume x: "x < CARD('rows)" and y: "y < CARD('rows)" and eq: "from_nat x = (from_nat y::'rows)"
show "x = y" using from_nat_eq_imp_eq[OF eq x y] .
next
fix i show "axis i 1 ∈ (λx. axis (from_nat x::'rows) 1) ` {..<CARD('rows)}" unfolding image_def
by (auto, metis lessThan_iff to_nat_from_nat to_nat_less_card)
qed
also have "... = CARD('rows)" by (metis card_lessThan)
finally show ?thesis .
qed
subsection‹Instantiations and interpretations›
text‹Functions between two real vector spaces form a real vector›
instantiation "fun" :: (real_vector, real_vector) real_vector
begin
definition "scaleR_fun a f = (λi. a *⇩R f i )"
instance
by (intro_classes, auto simp add: fun_eq_iff scaleR_fun_def scaleR_left.add scaleR_right.add)
end
instantiation vec :: (type, finite) equal
begin
definition equal_vec :: "('a, 'b::finite) vec => ('a, 'b::finite) vec => bool"
where "equal_vec x y = (∀i. x$i = y$i)"
instance
proof (intro_classes)
fix x y::"('a, 'b::finite) vec"
show "equal_class.equal x y = (x = y)" unfolding equal_vec_def using vec_eq_iff by auto
qed
end