# Theory Missing_VS_Connect

```section ‹Missing Lemmas on Vector Spaces›

text ‹We provide some results on vector spaces which should be merged into other AFP entries.›
theory Missing_VS_Connect
imports
Jordan_Normal_Form.VS_Connect
Missing_Matrix
Polynomial_Factorization.Missing_List
begin

context vec_space
begin
lemma span_diff: assumes A: "A ⊆ carrier_vec n"
and a: "a ∈ span A" and b: "b ∈ span A"
shows "a - b ∈ span A"
proof -
from A a have an: "a ∈ carrier_vec n" by auto
from A b have bn: "b ∈ carrier_vec n" by auto
have "a + (-1 ⋅⇩v b) ∈ span A"
by (rule span_add1[OF A a], insert b A, auto)
also have "a + (-1 ⋅⇩v b) = a - b" using an bn by auto
finally show ?thesis by auto
qed

lemma finsum_scalar_prod_sum':
assumes f: "f ∈ U → carrier_vec n"
and w: "w ∈ carrier_vec n"
shows "w ∙ finsum V f U = sum (λu. w ∙ f u) U"
by (subst comm_scalar_prod[OF w], (insert f, auto)[1],
subst finsum_scalar_prod_sum[OF f w],
insert f, intro sum.cong[OF refl] comm_scalar_prod[OF _ w], auto)

lemma lincomb_scalar_prod_left: assumes "W ⊆ carrier_vec n" "v ∈ carrier_vec n"
shows "lincomb a W ∙ v = (∑w∈W. a w * (w ∙ v))"
unfolding lincomb_def
by (subst finsum_scalar_prod_sum, insert assms, auto intro!: sum.cong)

lemma lincomb_scalar_prod_right: assumes "W ⊆ carrier_vec n" "v ∈ carrier_vec n"
shows "v ∙ lincomb a W = (∑w∈W. a w * (v ∙ w))"
unfolding lincomb_def
by (subst finsum_scalar_prod_sum', insert assms, auto intro!: sum.cong)

lemma lin_indpt_empty[simp]: "lin_indpt {}"
using lin_dep_def by auto

lemma span_carrier_lin_indpt_card_n:
assumes "W ⊆ carrier_vec n" "card W = n" "lin_indpt W"
shows "span W = carrier_vec n"
using assms basis_def dim_is_n dim_li_is_basis fin_dim_li_fin by simp

lemma ortho_span: assumes W: "W ⊆ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ X ⟹ w ∙ x = 0"
and w: "w ∈ span W" and x: "x ∈ X"
shows "w ∙ x = 0"
proof -
from w W obtain c V where "finite V" and VW: "V ⊆ W" and w: "w = lincomb c V"
by (meson in_spanE)
show ?thesis unfolding w
by (subst lincomb_scalar_prod_left, insert W VW X x ortho, auto intro!: sum.neutral)
qed

lemma ortho_span': assumes W: "W ⊆ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ X ⟹ x ∙ w = 0"
and w: "w ∈ span W" and x: "x ∈ X"
shows "x ∙ w = 0"
proof -
from w W obtain c V where "finite V" and VW: "V ⊆ W" and w: "w = lincomb c V"
by (meson in_spanE)
show ?thesis unfolding w
by (subst lincomb_scalar_prod_right, insert W VW X x ortho, auto intro!: sum.neutral)
qed

lemma ortho_span_span: assumes W: "W ⊆ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ X ⟹ w ∙ x = 0"
and w: "w ∈ span W" and x: "x ∈ span X"
shows "w ∙ x = 0"
by (rule ortho_span[OF W _ ortho_span'[OF X W _ _] w x], insert W X ortho, auto)

lemma lincomb_in_span[intro]:
assumes X: "X⊆ carrier_vec n"
shows "lincomb a X ∈ span X"
proof(cases "finite X")
case False hence "lincomb a X = 0⇩v n" using X
thus ?thesis using X by force
qed (insert X, auto)

lemma generating_card_n_basis: assumes X: "X ⊆ carrier_vec n"
and span: "carrier_vec n ⊆ span X"
and card: "card X = n"
shows "basis X"
proof -
have fin: "finite X"
proof (cases "n = 0")
case False
with card show "finite X" by (meson card.infinite)
next
case True
with X have "X ⊆ carrier_vec 0" by auto
also have "… = {0⇩v 0}" by auto
finally have "X ⊆ {0⇩v 0}" .
from finite_subset[OF this] show "finite X" by auto
qed
from X have "span X ⊆ carrier_vec n" by auto
with span have span: "span X = carrier_vec n" by auto
from dim_is_n card have card: "card X ≤ dim" by auto
from dim_gen_is_basis[OF fin X span card] show "basis X" .
qed

lemma lincomb_list_append:
assumes Ws: "set Ws ⊆ carrier_vec n"
shows "set Vs ⊆ carrier_vec n ⟹ lincomb_list f (Vs @ Ws) =
lincomb_list f Vs + lincomb_list (λ i. f (i + length Vs)) Ws"
proof (induction Vs arbitrary: f)
case Nil show ?case by(simp add: lincomb_list_carrier[OF Ws])
next
case (Cons x Vs)
have "lincomb_list f (x # (Vs @ Ws)) = f 0 ⋅⇩v x + lincomb_list (f ∘ Suc) (Vs @ Ws)"
by (rule lincomb_list_Cons)
also have "lincomb_list (f ∘ Suc) (Vs @ Ws) =
lincomb_list (f ∘ Suc) Vs + lincomb_list (λ i. (f ∘ Suc) (i + length Vs)) Ws"
using Cons by auto
also have "(λ i. (f ∘ Suc) (i + length Vs)) = (λ i. f (i + length (x # Vs)))" by simp
also have "f 0 ⋅⇩v x + ((lincomb_list (f ∘ Suc) Vs) + lincomb_list … Ws) =
(f 0 ⋅⇩v x + (lincomb_list (f ∘ Suc) Vs)) + lincomb_list … Ws"
using assoc_add_vec Cons.prems Ws lincomb_list_carrier by auto
finally show ?case using lincomb_list_Cons by auto
qed

lemma lincomb_list_snoc[simp]:
shows "set Vs ⊆ carrier_vec n ⟹ x ∈ carrier_vec n ⟹
lincomb_list f (Vs @ [x]) = lincomb_list f Vs + f (length Vs) ⋅⇩v x"
using lincomb_list_append by auto

lemma lincomb_list_smult:
"set Vs ⊆ carrier_vec n ⟹ lincomb_list (λ i. a * c i) Vs = a ⋅⇩v lincomb_list c Vs"
proof (induction Vs rule: rev_induct)
case (snoc x Vs)
have x: "x ∈ carrier_vec n" and Vs: "set Vs ⊆ carrier_vec n" using snoc.prems by auto
have "lincomb_list (λ i. a * c i) (Vs @ [x]) =
lincomb_list (λ i. a * c i) Vs + (a * c (length Vs)) ⋅⇩v x"
using x Vs by auto
also have "lincomb_list (λ i. a * c i) Vs = a ⋅⇩v lincomb_list c Vs"
by(rule snoc.IH[OF Vs])
also have "(a * c (length Vs)) ⋅⇩v x = a ⋅⇩v (c (length Vs) ⋅⇩v x)"
using smult_smult_assoc x by auto
also have "a ⋅⇩v lincomb_list c Vs + … = a ⋅⇩v (lincomb_list c Vs + c (length Vs) ⋅⇩v x)"
using smult_add_distrib_vec[of _ n _ a] lincomb_list_carrier[OF Vs] x by simp
also have "lincomb_list c Vs + c (length Vs) ⋅⇩v x = lincomb_list c (Vs @ [x])"
using Vs x by auto
finally show ?case by auto
qed simp

lemma lincomb_list_index:
assumes i: "i < n"
shows "set Xs ⊆ carrier_vec n ⟹
lincomb_list c Xs \$ i = sum (λ j. c j * (Xs ! j) \$ i) {0..<length Xs}"
proof (induction Xs rule: rev_induct)
case (snoc x Xs)
hence x: "x ∈ carrier_vec n" and Xs: "set Xs ⊆ carrier_vec n" by auto
hence "lincomb_list c (Xs @ [x]) = lincomb_list c Xs + c (length Xs) ⋅⇩v x" by auto
also have "… \$ i = lincomb_list c Xs \$ i + (c (length Xs) ⋅⇩v x) \$ i"
using i index_add_vec(1) x by simp
also have "(c (length Xs) ⋅⇩v x) \$ i = c (length Xs) * x \$ i" using i x by simp
also have "x \$ i= (Xs @ [x]) ! (length Xs) \$ i" by simp
also have "lincomb_list c Xs \$ i = (∑j = 0..<length Xs. c j * Xs ! j \$ i)"
by (rule snoc.IH[OF Xs])
also have "… =  (∑j = 0..<length Xs. c j * (Xs @ [x]) ! j \$ i)"
by (rule R.finsum_restrict, force, rule restrict_ext, auto simp: append_Cons_nth_left)
finally show ?case
using sum.atLeast0_lessThan_Suc[of "λ j. c j * (Xs @ [x]) ! j \$ i" "length Xs"]
by fastforce