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 by (simp add: lincomb_def) 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 qed (simp add: i) end end