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
    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