Theory Linear_Algebra2
section "Linear algebra"
theory Linear_Algebra2
imports Miscellany
begin
lemma exhaust_4:
fixes x :: 4
shows "x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4"
proof (induct x)
case (of_int z)
hence "0 ≤ z" and "z < 4" by simp_all
hence "z = 0 ∨ z = 1 ∨ z = 2 ∨ z = 3" by arith
thus ?case by auto
qed
lemma forall_4: "(∀ i::4. P i) ⟷ P 1 ∧ P 2 ∧ P 3 ∧ P 4"
by (metis exhaust_4)
lemma UNIV_4: "(UNIV::(4 set)) = {1, 2, 3, 4}"
using exhaust_4
by auto
lemma vector_4:
fixes w :: "'a::zero"
shows "(vector [w, x, y, z] :: 'a^4)$1 = w"
and "(vector [w, x, y, z] :: 'a^4)$2 = x"
and "(vector [w, x, y, z] :: 'a^4)$3 = y"
and "(vector [w, x, y, z] :: 'a^4)$4 = z"
unfolding vector_def
by simp_all
definition
is_basis :: "(real^'n) set ⇒ bool" where
"is_basis S ≡ independent S ∧ 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 :: "(real^'n) set"
shows "independent B ∧ card B = CARD('n) ⟷ is_basis B"
proof
assume L: "independent B ∧ card B = CARD('n)"
then have "card (Basis::(real^'n) set) = card B"
by simp
with L show "is_basis B"
by (metis (no_types) card_eq_dim dim_UNIV independent_bound is_basis_def subset_antisym top_greatest)
next
assume "is_basis B"
then show "independent B ∧ card B = CARD('n)"
by (metis DIM_cart DIM_real basis_card_eq_dim dim_UNIV is_basis_def mult.right_neutral top.extremum)
qed
lemma basis_finite:
fixes B :: "(real^'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
lemma basis_expand:
assumes "is_basis B"
shows "∃c. v = (∑w∈B. (c w) *⇩R w)"
proof -
from ‹is_basis B› have "v ∈ span B" unfolding is_basis_def by simp
from basis_finite [of B] and ‹is_basis B› have "finite B" by simp
with span_finite [of B] and ‹v ∈ span B›
show "∃c. v = (∑w∈B. (c w) *⇩R w)" by (simp add: scalar_equiv) auto
qed
lemma not_span_independent_insert:
fixes v :: "('a::real_vector)^'n"
assumes "independent S" and "v ∉ span S"
shows "independent (insert v S)"
by (simp add: assms independent_insert)
lemma orthogonal_sum:
fixes v :: "real^'n"
assumes "⋀w. w∈S ⟹ orthogonal v w"
shows "orthogonal v (∑w∈S. c w *s w)"
by (metis (no_types, lifting) assms orthogonal_clauses(1,2) orthogonal_rvsum scalar_equiv sum.infinite)
lemma orthogonal_self_eq_0:
fixes v :: "('a::real_inner)^'n"
assumes "orthogonal v v"
shows "v = 0"
using inner_eq_zero_iff [of v] and assms
unfolding orthogonal_def
by simp
lemma orthogonal_in_span_eq_0:
fixes v :: "real^'n"
assumes "v ∈ span S" and "⋀w. w∈S ⟹ orthogonal v w"
shows "v = 0"
using assms orthogonal_self orthogonal_to_span by blast
lemma orthogonal_independent:
fixes v :: "real^'n"
assumes "independent S" and "v ≠ 0" and "⋀w. w∈S ⟹ orthogonal v w"
shows "independent (insert v S)"
using assms not_span_independent_insert orthogonal_in_span_eq_0 by blast
lemma dot_scaleR_mult:
shows "(k *⇩R a) ∙ b = k * (a ∙ b)" and "a ∙ (k *⇩R b) = k * (a ∙ b)"
by auto
lemma dependent_explicit_finite:
fixes S :: "(('a::{real_vector,field})^'n) set"
assumes "finite S"
shows "dependent S ⟷ (∃ u. (∃ v∈S. u v ≠ 0) ∧ (∑ v∈S. u v *⇩R v) = 0)"
by (simp add: assms dependent_finite)
lemma dependent_explicit_2:
fixes v w :: "('a::{field,real_vector})^'n"
assumes "v ≠ w"
shows "dependent {v, w} ⟷ (∃ i j. (i ≠ 0 ∨ j ≠ 0) ∧ i *⇩R v + j *⇩R w = 0)"
proof
let ?S = "{v, w}"
have "finite ?S" by simp
{ assume "dependent ?S"
with dependent_explicit_finite [of ?S] and ‹finite ?S› and ‹v ≠ w›
show "∃ i j. (i ≠ 0 ∨ j ≠ 0) ∧ i *⇩R v + j *⇩R w = 0" by auto }
{ assume "∃ i j. (i ≠ 0 ∨ j ≠ 0) ∧ i *⇩R v + j *⇩R w = 0"
then obtain i and j where "i ≠ 0 ∨ j ≠ 0" and "i *⇩R v + j *⇩R w = 0" by auto
let ?u = "λ x. if x = v then i else j"
from ‹i ≠ 0 ∨ j ≠ 0› and ‹v ≠ w› have "∃ x∈?S. ?u x ≠ 0" by simp
from ‹i *⇩R v + j *⇩R w = 0› and ‹v ≠ w›
have "(∑ x∈?S. ?u x *⇩R x) = 0" by simp
with dependent_explicit_finite [of ?S]
and ‹finite ?S› and ‹∃ x∈?S. ?u x ≠ 0›
show "dependent ?S" by best }
qed
subsection "Matrices"
lemma zero_not_invertible:
"¬ (invertible (0::real^'n^'n))"
using invertible_times_eq_zero matrix_vector_mult_0 by blast
text ‹Based on matrix-vector-column in
HOL/Multivariate\_Analysis/Euclidean\_Space.thy in Isabelle 2009-1:›
lemma vector_matrix_row:
fixes x :: "('a::comm_semiring_1)^'m" and A :: "('a^'n^'m)"
shows "x v* A = (∑ i∈UNIV. (x$i) *s (A$i))"
unfolding vector_matrix_mult_def
by (simp add: vec_eq_iff mult.commute)
lemma matrix_inv:
assumes "invertible M"
shows "matrix_inv M ** M = mat 1"
and "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
lemma matrix_inv_invertible:
assumes "invertible M"
shows "invertible (matrix_inv M)"
using ‹invertible M› and matrix_inv
unfolding invertible_def [of "matrix_inv M"]
by auto
lemma invertible_times_non_zero:
fixes M :: "real^'n^'n"
assumes "invertible M" and "v ≠ 0"
shows "M *v v ≠ 0"
using ‹invertible M› and ‹v ≠ 0› and invertible_times_eq_zero [of M v]
by auto
lemma matrix_right_invertible_ker:
fixes M :: "real^('m::finite)^'n"
shows "(∃ M'. M ** M' = mat 1) ⟷ (∀ x. x v* M = 0 ⟶ x = 0)"
using left_invertible_transpose matrix_left_invertible_ker by force
lemma left_invertible_iff_invertible:
fixes M :: "real^'n^'n"
shows "(∃ N. N ** M = mat 1) ⟷ invertible M"
by (simp add: invertible_def matrix_left_right_inverse)
lemma right_invertible_iff_invertible:
fixes M :: "real^'n^'n"
shows "(∃ N. M ** N = mat 1) ⟷ invertible M"
by (simp add: invertible_def matrix_left_right_inverse)
definition symmatrix :: "'a^'n^'n ⇒ bool" where
"symmatrix M ≡ transpose M = M"
lemma symmatrix_preserve:
fixes M N :: "('a::comm_semiring_1)^'n^'n"
assumes "symmatrix M"
shows "symmatrix (N ** M ** transpose N)"
proof -
have "transpose (N ** M ** transpose N) = N ** (M ** transpose N)"
by (metis (no_types) transpose_transpose assms matrix_transpose_mul symmatrix_def)
then show ?thesis
by (simp add: matrix_mul_assoc symmatrix_def)
qed
lemma non_zero_mult_invertible_non_zero:
fixes M :: "real^'n^'n"
assumes "v ≠ 0" and "invertible M"
shows "v v* M ≠ 0"
using ‹v ≠ 0› and ‹invertible M› and times_invertible_eq_zero
by auto
end