FinMatrix.Matrix.VectorSpace
Require Import LinearSpace.
Require Import Matrix.
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable Variable tA Aadd Azero Aopp Amul Aone Ainv Ale Alt Altb Aleb a2r.
Open Scope A_scope.
Open Scope vec_scope.
Open Scope VectorSpace_scope.
Section lcomb.
Context `{HVectorSpace : VectorSpace}.
Add Field field_inst : (make_field_theory F).
Notation "0" := Azero : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation "a - b" := ((a + - b)%A) : A_scope.
Notation vzero := (vzero 0%A).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation vscal := (@vscal _ Amul _).
Infix "s*" := vscal : vec_scope.
Notation vdot := (@vdot _ Aadd Azero Amul).
Infix "+" := Vadd : VectorSpace_scope.
Notation "0" := Vzero : VectorSpace_scope.
Notation "- v" := (Vopp v) : VectorSpace_scope.
Notation Vsub u v := (u + -v).
Infix "-" := Vsub : VectorSpace_scope.
Infix "s*" := Vscal : VectorSpace_scope.
Notation vsum := (@vsum _ Vadd 0 _).
Context `{HVectorSpace : VectorSpace}.
Add Field field_inst : (make_field_theory F).
Notation "0" := Azero : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation "a - b" := ((a + - b)%A) : A_scope.
Notation vzero := (vzero 0%A).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation vscal := (@vscal _ Amul _).
Infix "s*" := vscal : vec_scope.
Notation vdot := (@vdot _ Aadd Azero Amul).
Infix "+" := Vadd : VectorSpace_scope.
Notation "0" := Vzero : VectorSpace_scope.
Notation "- v" := (Vopp v) : VectorSpace_scope.
Notation Vsub u v := (u + -v).
Infix "-" := Vsub : VectorSpace_scope.
Infix "s*" := Vscal : VectorSpace_scope.
Notation vsum := (@vsum _ Vadd 0 _).
Linear combination of v1,v2, ..., vn by coefficients c1,c2, ..., cn
0 * v1 + 0 * v2 + ... + 0 * vn = 0
Lemma lcomb_coef_0 : forall {n} (vs : @vec V n), lcomb vzero vs = 0.
Proof.
intros. unfold lcomb. apply vsum_eq0. intros. rewrite vnth_vmap2.
rewrite vnth_vzero. rewrite vs_vscal_0_l. auto.
Qed.
Proof.
intros. unfold lcomb. apply vsum_eq0. intros. rewrite vnth_vmap2.
rewrite vnth_vzero. rewrite vs_vscal_0_l. auto.
Qed.
c1 * 0 + c2 * 0 + ... + cn * 0 = 0
Lemma lcomb_vec_0 : forall {n} (cs : @vec tA n), lcomb cs (@Vector.vzero _ Vzero _) = 0.
Proof.
intros. unfold lcomb. apply vsum_eq0. intros. rewrite vnth_vmap2.
rewrite vnth_vzero. rewrite vs_vscal_0_r. auto.
Qed.
Proof.
intros. unfold lcomb. apply vsum_eq0. intros. rewrite vnth_vmap2.
rewrite vnth_vzero. rewrite vs_vscal_0_r. auto.
Qed.
(c1 + c2) * v = c1 * v + c2 * v
Lemma lcomb_coef_add : forall {n} (vs : @vec V n) c1 c2,
lcomb (c1 + c2)%V vs = lcomb c1 vs + lcomb c2 vs.
Proof.
intros. unfold lcomb. rewrite vsum_add. apply vsum_eq; intros.
rewrite !vnth_vmap2. rewrite vnth_vadd. rewrite vs_vscal_aadd. auto.
Qed.
lcomb (c1 + c2)%V vs = lcomb c1 vs + lcomb c2 vs.
Proof.
intros. unfold lcomb. rewrite vsum_add. apply vsum_eq; intros.
rewrite !vnth_vmap2. rewrite vnth_vadd. rewrite vs_vscal_aadd. auto.
Qed.
(- c) * v = - (c * v)
Lemma lcomb_coef_opp : forall {n} (vs : @vec V n) c,
lcomb (- c)%V vs = - (lcomb c vs).
Proof.
intros. unfold lcomb. rewrite vsum_opp. apply vsum_eq; intros.
rewrite !vnth_vmap2. rewrite vnth_vopp. rewrite vs_vscal_opp. auto.
Qed.
lcomb (- c)%V vs = - (lcomb c vs).
Proof.
intros. unfold lcomb. rewrite vsum_opp. apply vsum_eq; intros.
rewrite !vnth_vmap2. rewrite vnth_vopp. rewrite vs_vscal_opp. auto.
Qed.
(c1 - c2) * v = c1 * v - c2 * v
Lemma lcomb_coef_sub : forall {n} (vs : @vec V n) c1 c2,
lcomb (c1 - c2)%V vs = lcomb c1 vs - lcomb c2 vs.
Proof.
intros. rewrite lcomb_coef_add. rewrite lcomb_coef_opp. auto.
Qed.
lcomb (c1 - c2)%V vs = lcomb c1 vs - lcomb c2 vs.
Proof.
intros. rewrite lcomb_coef_add. rewrite lcomb_coef_opp. auto.
Qed.
(a .* c) .* v = a .* (c .* v)
Lemma lcomb_coef_scal : forall {n} (vs : @vec V n) a c,
lcomb (a s* c)%V vs = a s* (lcomb c vs).
Proof.
intros. unfold lcomb. rewrite vsum_scal_l_ext.
- apply vsum_eq; intros. rewrite !vnth_vmap2. rewrite vnth_vscal.
apply vs_vscal_assoc.
- intros. apply vs_vscal_0_r.
- intros. apply vs_vscal_vadd.
Qed.
lcomb (a s* c)%V vs = a s* (lcomb c vs).
Proof.
intros. unfold lcomb. rewrite vsum_scal_l_ext.
- apply vsum_eq; intros. rewrite !vnth_vmap2. rewrite vnth_vscal.
apply vs_vscal_assoc.
- intros. apply vs_vscal_0_r.
- intros. apply vs_vscal_vadd.
Qed.
(veye i) * v = v
Lemma lcomb_coef_veye : forall {n} (vs : @vec V n) i,
lcomb (veye Azero Aone i) vs = vs.[i].
Proof.
intros. unfold lcomb. apply vsum_unique with (i:=i).
- rewrite vnth_vmap2. rewrite vnth_veye_eq. apply vs_vscal_1_l.
- intros. rewrite vnth_vmap2. rewrite vnth_veye_neq; auto. apply vs_vscal_0_l.
Qed.
lcomb (veye Azero Aone i) vs = vs.[i].
Proof.
intros. unfold lcomb. apply vsum_unique with (i:=i).
- rewrite vnth_vmap2. rewrite vnth_veye_eq. apply vs_vscal_1_l.
- intros. rewrite vnth_vmap2. rewrite vnth_veye_neq; auto. apply vs_vscal_0_l.
Qed.
(insert c i ci) * vs = c * (remove vs i) + ci * (vs.i)
Lemma lcomb_coef_vinsert :
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)) (ci : tA),
lcomb (vinsert c i ci) vs =
Vadd (lcomb c (vremove vs i)) (Vscal ci vs.[i]).
Proof.
intros. unfold lcomb.
rewrite (vmap2_vinsert_l (Azero:=Azero)(Bzero:=Vzero)(Czero:=Vzero)).
rewrite vsum_vinsert. auto.
Qed.
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)) (ci : tA),
lcomb (vinsert c i ci) vs =
Vadd (lcomb c (vremove vs i)) (Vscal ci vs.[i]).
Proof.
intros. unfold lcomb.
rewrite (vmap2_vinsert_l (Azero:=Azero)(Bzero:=Vzero)(Czero:=Vzero)).
rewrite vsum_vinsert. auto.
Qed.
(insert c i 0) * vs = c * (remove vs i)
Lemma lcomb_coef_vinsert_0 :
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)),
lcomb (vinsert c i Azero) vs = lcomb c (vremove vs i).
Proof.
intros. rewrite lcomb_coef_vinsert. rewrite vs_vscal_0_l at 1.
rewrite vs_vadd_0_r. auto.
Qed.
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)),
lcomb (vinsert c i Azero) vs = lcomb c (vremove vs i).
Proof.
intros. rewrite lcomb_coef_vinsert. rewrite vs_vscal_0_l at 1.
rewrite vs_vadd_0_r. auto.
Qed.
(insert c i 0) * vs = (insert c i (-1)) * vs + vs.i
Lemma lcomb_coef_vinsert_neg1 :
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)),
lcomb (vinsert c i Azero) vs =
Vadd (lcomb (vinsert c i (Aopp Aone)) vs) (vs i).
Proof.
intros. rewrite !lcomb_coef_vinsert. rewrite associative. f_equal.
replace (vs i) with (Aone s* vs i) at 3 by apply vs_vscal_1_l.
rewrite <- vs_vscal_aadd. f_equal. field.
Qed.
forall {n} (c : @vec tA n) (vs : @vec V (S n)) (i : fin (S n)),
lcomb (vinsert c i Azero) vs =
Vadd (lcomb (vinsert c i (Aopp Aone)) vs) (vs i).
Proof.
intros. rewrite !lcomb_coef_vinsert. rewrite associative. f_equal.
replace (vs i) with (Aone s* vs i) at 3 by apply vs_vscal_1_l.
rewrite <- vs_vscal_aadd. f_equal. field.
Qed.
(vset cs i a) * vs = cs * vs + (a - cs i)
Lemma lcomb_coef_vset :
forall {n} (cs : @vec tA n) (vs : @vec V n) (i : fin n) (a : tA),
lcomb (vset cs i a) vs = lcomb cs vs + (a - cs i)%A s* (vs i).
Proof.
intros. unfold lcomb.
replace ((a - cs i)%A s* vs i)
with (vsum (vset (@Vector.vzero _ Vzero n) i ((a - cs i)%A s* vs i))).
- rewrite vsum_add. f_equal.
apply veq_iff_vnth. intros j. rewrite !vnth_vmap2. destruct (i ??= j).
+ fin2nat. rewrite !vnth_vset_eq. rewrite <- vs_vscal_aadd. f_equal. ring.
+ fin2nat. rewrite !vnth_vset_neq; auto. rewrite vnth_vzero.
rewrite vs_vadd_0_r. auto.
- apply vsum_unique with (i:=i).
+ rewrite vnth_vset_eq. auto.
+ intros. rewrite vnth_vset_neq; auto.
Qed.
forall {n} (cs : @vec tA n) (vs : @vec V n) (i : fin n) (a : tA),
lcomb (vset cs i a) vs = lcomb cs vs + (a - cs i)%A s* (vs i).
Proof.
intros. unfold lcomb.
replace ((a - cs i)%A s* vs i)
with (vsum (vset (@Vector.vzero _ Vzero n) i ((a - cs i)%A s* vs i))).
- rewrite vsum_add. f_equal.
apply veq_iff_vnth. intros j. rewrite !vnth_vmap2. destruct (i ??= j).
+ fin2nat. rewrite !vnth_vset_eq. rewrite <- vs_vscal_aadd. f_equal. ring.
+ fin2nat. rewrite !vnth_vset_neq; auto. rewrite vnth_vzero.
rewrite vs_vadd_0_r. auto.
- apply vsum_unique with (i:=i).
+ rewrite vnth_vset_eq. auto.
+ intros. rewrite vnth_vset_neq; auto.
Qed.
cs * (vset vs i u) = cs * vs + (cs i)
Lemma lcomb_vec_vset :
forall {n} (cs : @vec tA n) (vs : @vec V n) (i : fin n) (u : V),
lcomb cs (vset vs i u) = lcomb cs vs + (cs i) s* (u - vs i).
Proof.
intros. unfold lcomb.
replace (cs i s* (u - vs i))
with (vsum (vset (@Vector.vzero _ Vzero n) i (cs i s* (u - vs i)))).
- rewrite vsum_add. f_equal. apply veq_iff_vnth. intros j.
rewrite !vnth_vmap2. destruct (i ??= j).
+ fin2nat. rewrite !vnth_vset_eq. rewrite <- vs_vscal_vadd. f_equal.
rewrite commutative. rewrite associative. rewrite inverseLeft.
rewrite vs_vadd_0_r; auto.
+ fin2nat. rewrite !vnth_vset_neq; auto. rewrite vnth_vzero.
rewrite vs_vadd_0_r; auto.
- apply vsum_unique with (i:=i).
+ rewrite vnth_vset_eq. auto.
+ intros. rewrite vnth_vset_neq; auto.
Qed.
forall {n} (cs : @vec tA n) (vs : @vec V n) (i : fin n) (u : V),
lcomb cs (vset vs i u) = lcomb cs vs + (cs i) s* (u - vs i).
Proof.
intros. unfold lcomb.
replace (cs i s* (u - vs i))
with (vsum (vset (@Vector.vzero _ Vzero n) i (cs i s* (u - vs i)))).
- rewrite vsum_add. f_equal. apply veq_iff_vnth. intros j.
rewrite !vnth_vmap2. destruct (i ??= j).
+ fin2nat. rewrite !vnth_vset_eq. rewrite <- vs_vscal_vadd. f_equal.
rewrite commutative. rewrite associative. rewrite inverseLeft.
rewrite vs_vadd_0_r; auto.
+ fin2nat. rewrite !vnth_vset_neq; auto. rewrite vnth_vzero.
rewrite vs_vadd_0_r; auto.
- apply vsum_unique with (i:=i).
+ rewrite vnth_vset_eq. auto.
+ intros. rewrite vnth_vset_neq; auto.
Qed.
lcomb (vremove cs i) (vremove vs i) = (lcomb cs vs) - (cs.i * vs.i)
Lemma lcomb_vremove_vremove : forall {n} (cs : @vec tA (S n)) (vs : @vec V (S n)) i,
lcomb (vremove cs i) (vremove vs i) = (lcomb cs vs) - (cs i s* vs i).
Proof.
intros. unfold lcomb. rewrite (@vmap2_vremove_vremove _ _ _ Azero Vzero Vzero).
rewrite vsum_vremove. auto.
Qed.
lcomb (vremove cs i) (vremove vs i) = (lcomb cs vs) - (cs i s* vs i).
Proof.
intros. unfold lcomb. rewrite (@vmap2_vremove_vremove _ _ _ Azero Vzero Vzero).
rewrite vsum_vremove. auto.
Qed.
lcomb (vconsH c cs) vs = c * (vhead vs) + (lcomb cs (vremoveH vs))
Lemma lcomb_coef_vconsH : forall {n} (cs : @vec tA n) (vs : @vec V (S n)) (c : tA),
lcomb (vconsH c cs) vs = c s* (vhead vs) + lcomb cs (vremoveH vs).
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
- rewrite vnth_vmap2. f_equal. rewrite vhead_eq. f_equal. fin.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsH_gt0. fin. Unshelve. fin.
Qed.
lcomb (vconsH c cs) vs = c s* (vhead vs) + lcomb cs (vremoveH vs).
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
- rewrite vnth_vmap2. f_equal. rewrite vhead_eq. f_equal. fin.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsH_gt0. fin. Unshelve. fin.
Qed.
lcomb (vconsT cs c) vs = (lcomb cs (vremoveT vs)) + c * (vtail vs)
Lemma lcomb_coef_vconsT : forall {n} (cs : @vec tA n) (vs : @vec V (S n)) (c : tA),
lcomb (vconsT cs c) vs = lcomb cs (vremoveT vs) + c s* (vtail vs).
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. f_equal.
rewrite vnth_vconsT_n; auto. rewrite fin2nat_nat2finS; auto.
Unshelve. fin.
Qed.
lcomb (vconsT cs c) vs = lcomb cs (vremoveT vs) + c s* (vtail vs).
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. f_equal.
rewrite vnth_vconsT_n; auto. rewrite fin2nat_nat2finS; auto.
Unshelve. fin.
Qed.
lcomb cs (vconsT vs u) = (lcomb (vremoveT cs) vs) + (vtail cs) * u
Lemma lcomb_vec_vconsT : forall {n} (cs : @vec tA (S n)) (vs : @vec V n) (u : V),
lcomb cs (vconsT vs u) = lcomb (vremoveT cs) vs + (vtail cs) s* u.
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. f_equal.
rewrite vnth_vconsT_n; auto. fin. Unshelve. fin.
Qed.
lcomb cs (vconsT vs u) = lcomb (vremoveT cs) vs + (vtail cs) s* u.
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. f_equal.
rewrite vnth_vconsT_n; auto. fin. Unshelve. fin.
Qed.
lcomb cs (vconsH u vs) = (vhead cs) * u + (lcomb (vremoveH cs) vs)
Lemma lcomb_vec_vconsH : forall {n} (cs : @vec tA (S n)) (vs : @vec V n) (u : V),
lcomb cs (vconsH u vs) = (vhead cs) s* u + lcomb (vremoveH cs) vs.
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
- rewrite vnth_vmap2. f_equal. rewrite vhead_eq. fin.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsH_gt0. fin. Unshelve. fin.
Qed.
lcomb cs (vconsH u vs) = (vhead cs) s* u + lcomb (vremoveH cs) vs.
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
- rewrite vnth_vmap2. f_equal. rewrite vhead_eq. fin.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. f_equal.
erewrite vnth_vconsH_gt0. fin. Unshelve. fin.
Qed.
lcomb (vconsT cs c) (vconsT vs v) = (lcomb cs vs) + c * v
Lemma lcomb_vconsT_vconsT : forall {n} (cs : @vec tA n) (vs : @vec V n) c v,
lcomb (vconsT cs c) (vconsT vs v) = lcomb cs vs + c s* v.
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. erewrite !vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. erewrite !vnth_vconsT_n; auto.
all: rewrite fin2nat_nat2finS; auto.
Unshelve. fin. fin.
Qed.
lcomb (vconsT cs c) (vconsT vs v) = lcomb cs vs + c s* v.
Proof.
intros. unfold lcomb. rewrite vsumS_tail. f_equal.
- apply vsum_eq; intros i. rewrite !vnth_vmap2. erewrite !vnth_vconsT_lt. fin.
- rewrite vnth_vmap2. erewrite !vnth_vconsT_n; auto.
all: rewrite fin2nat_nat2finS; auto.
Unshelve. fin. fin.
Qed.
lcomb (vconsH c cs) (vconsH v vs) = c * v + (lcomb cs vs)
Lemma lcomb_vconsH_vconsH : forall {n} (cs : @vec tA n) (vs : @vec V n) c v,
lcomb (vconsH c cs) (vconsH v vs) = c s* v + lcomb cs vs.
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
apply vsum_eq; intros i. rewrite !vnth_vmap2. erewrite !vnth_vconsH_gt0. fin.
Unshelve. fin. fin.
Qed.
lcomb (vconsH c cs) (vconsH v vs) = c s* v + lcomb cs vs.
Proof.
intros. unfold lcomb. rewrite vsumS_head. f_equal.
apply vsum_eq; intros i. rewrite !vnth_vmap2. erewrite !vnth_vconsH_gt0. fin.
Unshelve. fin. fin.
Qed.
lcomb (vapp cs ds) (vapp us vs) = (lcomb cs us) + (lcomb ds vs)
Lemma lcomb_vapp_vapp : forall {n m} (cs : @vec tA n) (ds : @vec tA m)
(us : @vec V n) (vs : @vec V m),
lcomb (vapp cs ds) (vapp us vs) = (lcomb cs us) + (lcomb ds vs).
Proof.
intros. unfold lcomb. rewrite vmap2_vapp_vapp.
remember (vmap2 Vscal cs us) as u.
remember (vmap2 Vscal ds vs) as v.
apply vsum_vapp.
Qed.
(us : @vec V n) (vs : @vec V m),
lcomb (vapp cs ds) (vapp us vs) = (lcomb cs us) + (lcomb ds vs).
Proof.
intros. unfold lcomb. rewrite vmap2_vapp_vapp.
remember (vmap2 Vscal cs us) as u.
remember (vmap2 Vscal ds vs) as v.
apply vsum_vapp.
Qed.
lcomb (lcomb u D) v = lcomb u (lcomb D v)
Lemma lcomb_assoc : forall {r c} (u : @vec tA c) (D : @vec (@vec tA r) c) (v : @vec V r),
lcomb (fun j => vdot u (fun i => D i j)) v = lcomb u (fun i : fin c => lcomb (D i) v).
Proof.
intros. unfold lcomb, vdot, vmap2.
pose proof (vsum_vsum c r (fun i j => Vscal (Amul (u i) (D i j)) (v j))).
match goal with
| H: ?a1 = ?a2 |- ?b1 = ?b2 => replace b1 with a2; [replace b2 with a1|]; auto
end.
- f_equal. extensionality i. rewrite vsum_scal_l_ext; intros; auto.
f_equal. extensionality j. rewrite vs_vscal_assoc. auto.
apply vs_vscal_0_r. apply vs_vscal_vadd.
- f_equal. extensionality i. rewrite vsum_scal_r_ext; intros; auto.
apply vs_vscal_0_l. apply vs_vscal_aadd.
Qed.
lcomb (fun j => vdot u (fun i => D i j)) v = lcomb u (fun i : fin c => lcomb (D i) v).
Proof.
intros. unfold lcomb, vdot, vmap2.
pose proof (vsum_vsum c r (fun i j => Vscal (Amul (u i) (D i j)) (v j))).
match goal with
| H: ?a1 = ?a2 |- ?b1 = ?b2 => replace b1 with a2; [replace b2 with a1|]; auto
end.
- f_equal. extensionality i. rewrite vsum_scal_l_ext; intros; auto.
f_equal. extensionality j. rewrite vs_vscal_assoc. auto.
apply vs_vscal_0_r. apply vs_vscal_vadd.
- f_equal. extensionality i. rewrite vsum_scal_r_ext; intros; auto.
apply vs_vscal_0_l. apply vs_vscal_aadd.
Qed.
(∃ ds, vs = fun i => lcomb ds.i vs) -> (∀ i, ∃ cs, lcomb cs vs = vs.i)
Lemma lcomb_any_ex_imply_all_ex : forall {r s} (us : @vec V r) (vs : @vec V s),
(exists ds : @vec (@vec tA r) s, vs = fun i => lcomb (ds i) us) ->
(forall i : fin s, exists cs : @vec tA r, lcomb cs us = vs i).
Proof. intros. destruct H as [d H]. rewrite H. exists (d i); auto. Qed.
(exists ds : @vec (@vec tA r) s, vs = fun i => lcomb (ds i) us) ->
(forall i : fin s, exists cs : @vec tA r, lcomb cs us = vs i).
Proof. intros. destruct H as [d H]. rewrite H. exists (d i); auto. Qed.
(∀ i, ∃ cs, lcomb cs us = vs.i) -> (∃ ds, vs = fun i => lcomb ds.i us)
Lemma lcomb_all_ex_imply_any_ex : forall {r s} (us : @vec V r) (vs : @vec V s),
(forall i : fin s, exists cs : @vec tA r, lcomb cs us = vs i) ->
(exists ds : @vec (@vec tA r) s, vs = fun i => lcomb (ds i) us).
Proof.
intros. generalize dependent s. induction s; intros.
- exists (@mkvec0 _ (@Vector.vzero _ Azero r)). apply v0eq.
- rewrite <- (vconsH_vhead_vremoveH vs).
assert (exists cs : vec r, vhead vs = lcomb cs us).
{ specialize (H fin0). destruct H as [cs H]. exists cs. rewrite H. auto. }
assert (forall i : fin s, exists cs : vec r, lcomb cs us = vremoveH vs i).
{ intros. specialize (H (fSuccRangeS i)). destruct H as [cs H].
exists cs. rewrite H. auto. }
destruct H0 as [c0 H0].
specialize (IHs (vremoveH vs) H1). destruct IHs as [c1 IHs].
rewrite H0,IHs. unfold vconsH.
exists (fun i : fin (S s) =>
match (fin2nat i ??= 0)%nat with
| left _ => c0
| right n => c1 (fPredRangeP i (neq_0_lt_stt (fin2nat i) n))
end).
apply veq_iff_vnth. intros. destruct (_??=_)%nat; auto.
Qed.
End lcomb.
(forall i : fin s, exists cs : @vec tA r, lcomb cs us = vs i) ->
(exists ds : @vec (@vec tA r) s, vs = fun i => lcomb (ds i) us).
Proof.
intros. generalize dependent s. induction s; intros.
- exists (@mkvec0 _ (@Vector.vzero _ Azero r)). apply v0eq.
- rewrite <- (vconsH_vhead_vremoveH vs).
assert (exists cs : vec r, vhead vs = lcomb cs us).
{ specialize (H fin0). destruct H as [cs H]. exists cs. rewrite H. auto. }
assert (forall i : fin s, exists cs : vec r, lcomb cs us = vremoveH vs i).
{ intros. specialize (H (fSuccRangeS i)). destruct H as [cs H].
exists cs. rewrite H. auto. }
destruct H0 as [c0 H0].
specialize (IHs (vremoveH vs) H1). destruct IHs as [c1 IHs].
rewrite H0,IHs. unfold vconsH.
exists (fun i : fin (S s) =>
match (fin2nat i ??= 0)%nat with
| left _ => c0
| right n => c1 (fPredRangeP i (neq_0_lt_stt (fin2nat i) n))
end).
apply veq_iff_vnth. intros. destruct (_??=_)%nat; auto.
Qed.
End lcomb.
Section leqs.
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Record leqs {n s : nat} := {
leqs_a : @vec (@vec tA n) s;
leqs_b : @vec V s
}.
Definition leqsAnswer {n s} (e : @leqs n s) (x : @vec V n) : Prop :=
vmap (fun ai => lcomb ai x) (leqs_a e) = (leqs_b e).
End leqs.
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Record leqs {n s : nat} := {
leqs_a : @vec (@vec tA n) s;
leqs_b : @vec V s
}.
Definition leqsAnswer {n s} (e : @leqs n s) (x : @vec V n) : Prop :=
vmap (fun ai => lcomb ai x) (leqs_a e) = (leqs_b e).
End leqs.
Section lrep.
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Definition lrep {n} (vs : @vec V n) (u : V) : Prop :=
exists (cs : @vec tA n), lcomb cs vs = u.
Definition nolrep {n} (vs : @vec V n) (u : V) := (~ (lrep vs u)).
Lemma lrep_in : forall {n} (vs : @vec V n), vforall vs (lrep vs).
Proof. intros. hnf. intros. hnf. exists (veye Azero Aone i). apply lcomb_coef_veye. Qed.
End lrep.
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Definition lrep {n} (vs : @vec V n) (u : V) : Prop :=
exists (cs : @vec tA n), lcomb cs vs = u.
Definition nolrep {n} (vs : @vec V n) (u : V) := (~ (lrep vs u)).
Lemma lrep_in : forall {n} (vs : @vec V n), vforall vs (lrep vs).
Proof. intros. hnf. intros. hnf. exists (veye Azero Aone i). apply lcomb_coef_veye. Qed.
End lrep.
Section lreps.
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Definition lreps {r s} (vs : @vec V s) (us : @vec V r) : Prop :=
vforall us (lrep vs).
Definition nolreps {r s} (vs : @vec V r) (us : @vec V s) := (~ (lreps vs us)).
Context `{HVectorSpace : VectorSpace}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Definition lreps {r s} (vs : @vec V s) (us : @vec V r) : Prop :=
vforall us (lrep vs).
Definition nolreps {r s} (vs : @vec V r) (us : @vec V s) := (~ (lreps vs us)).
lreps is reflexive
Lemma lreps_refl : forall {r} (vs : @vec V r), lreps vs vs.
Proof.
intros. unfold lreps, vforall, lrep. intros.
exists (veye Azero Aone i). rewrite lcomb_coef_veye. auto.
Qed.
Proof.
intros. unfold lreps, vforall, lrep. intros.
exists (veye Azero Aone i). rewrite lcomb_coef_veye. auto.
Qed.
If `us` could represent `vs` and `vs` could represent `u`, then `us` could
represent `u`
Lemma lreps_lrep : forall {r s} (us : @vec V r) (vs : @vec V s) (u : V),
lreps us vs -> lrep vs u -> lrep us u.
Proof.
intros. unfold lreps, vforall in H. unfold lrep in *.
destruct H0 as [c H0]. rewrite <- H0.
apply (lcomb_all_ex_imply_any_ex (Azero:=Azero)) in H.
destruct H as [d H]. rewrite H.
exists (fun i => vsum Aadd Azero (vmap2 Amul c (fun j => d j i))).
rewrite <- lcomb_assoc. f_equal.
Qed.
lreps us vs -> lrep vs u -> lrep us u.
Proof.
intros. unfold lreps, vforall in H. unfold lrep in *.
destruct H0 as [c H0]. rewrite <- H0.
apply (lcomb_all_ex_imply_any_ex (Azero:=Azero)) in H.
destruct H as [d H]. rewrite H.
exists (fun i => vsum Aadd Azero (vmap2 Amul c (fun j => d j i))).
rewrite <- lcomb_assoc. f_equal.
Qed.
lreps is transitive
Lemma lreps_trans :
forall {r s t} (us : @vec V r) (vs : @vec V s) (ws : @vec V t),
lreps us vs -> lreps vs ws -> lreps us ws.
Proof.
intros. unfold lreps, vforall. intros. apply lreps_lrep with (vs:=vs); auto.
Qed.
End lreps.
forall {r s t} (us : @vec V r) (vs : @vec V s) (ws : @vec V t),
lreps us vs -> lreps vs ws -> lreps us ws.
Proof.
intros. unfold lreps, vforall. intros. apply lreps_lrep with (vs:=vs); auto.
Qed.
End lreps.
Section vsequiv.
Context `{HVectorSpace : VectorSpace}.
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Context `{HVectorSpace : VectorSpace}.
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Two vector systems `us` and `vs` are equivalent
Definition vsequiv {r s} (us : @vec V r) (vs : @vec V s) : Prop :=
lreps us vs /\ lreps vs us.
Infix "\~" := vsequiv (at level 70).
Lemma vsequiv_refl : forall {n} (vs : @vec V n), vs \~ vs.
Proof. intros. hnf. split; apply lreps_refl. Qed.
Lemma vsequiv_sym : forall {r s} (us : @vec V r) (vs : @vec V s), us \~ vs -> vs \~ us.
Proof. intros. hnf in *. destruct H; auto. Qed.
Lemma vsequiv_trans : forall {r s t} (us : @vec V r) (vs : @vec V s) (ws : @vec V t),
us \~ vs -> vs \~ ws -> us \~ ws.
Proof.
intros. hnf in *. destruct H,H0. split.
apply lreps_trans with vs; auto.
apply lreps_trans with vs; auto.
Qed.
End vsequiv.
lreps us vs /\ lreps vs us.
Infix "\~" := vsequiv (at level 70).
Lemma vsequiv_refl : forall {n} (vs : @vec V n), vs \~ vs.
Proof. intros. hnf. split; apply lreps_refl. Qed.
Lemma vsequiv_sym : forall {r s} (us : @vec V r) (vs : @vec V s), us \~ vs -> vs \~ us.
Proof. intros. hnf in *. destruct H; auto. Qed.
Lemma vsequiv_trans : forall {r s t} (us : @vec V r) (vs : @vec V s) (ws : @vec V t),
us \~ vs -> vs \~ ws -> us \~ ws.
Proof.
intros. hnf in *. destruct H,H0. split.
apply lreps_trans with vs; auto.
apply lreps_trans with vs; auto.
Qed.
End vsequiv.
Section lspan.
Context `{HVectorSpace : VectorSpace}.
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Instance lspan_Struct {n} (vs : @vec V n) : SubSpaceStruct (lrep vs).
Proof.
unfold lrep. constructor.
- exists (vzero Azero). apply lcomb_coef_0.
- intros. pose proof u.prf; pose proof v.prf; simpl in *.
destruct H as [c H], H0 as [c0 H0]. rewrite <- H, <- H0.
exists (@vadd _ Aadd _ c c0). apply lcomb_coef_add.
- intros. pose proof v.prf; simpl in *.
destruct H as [c H]. rewrite <- H.
exists (@vscal _ Amul _ a c).
apply lcomb_coef_scal.
Qed.
Context `{HVectorSpace : VectorSpace}.
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Instance lspan_Struct {n} (vs : @vec V n) : SubSpaceStruct (lrep vs).
Proof.
unfold lrep. constructor.
- exists (vzero Azero). apply lcomb_coef_0.
- intros. pose proof u.prf; pose proof v.prf; simpl in *.
destruct H as [c H], H0 as [c0 H0]. rewrite <- H, <- H0.
exists (@vadd _ Aadd _ c c0). apply lcomb_coef_add.
- intros. pose proof v.prf; simpl in *.
destruct H as [c H]. rewrite <- H.
exists (@vscal _ Amul _ a c).
apply lcomb_coef_scal.
Qed.
由向量组 vs 张成的子空间,记作 <vs> 或 <v1,v2,...,vn>
#[export] Instance lspan {n} (vs : @vec V n) : VectorSpace Hadd Hzero Hopp Hscal :=
makeSubSpace (lspan_Struct vs).
End lspan.
makeSubSpace (lspan_Struct vs).
End lspan.
Section ldep.
Context `{HVectorSpace : VectorSpace}.
Context {AeqDec : Dec (@eq tA)}.
Context {VeqDec : Dec (@eq V)}.
Notation "- a" := (Aopp a) : A_scope.
Infix "*" := Amul : A_scope.
Notation "1" := Aone : A_scope.
Notation "/ a" := (Ainv a) : A_scope.
Notation Adiv a b := (a * / b).
Infix "/" := Adiv : A_scope.
Infix "+" := Vadd : VectorSpace_scope.
Notation "0" := Vzero : VectorSpace_scope.
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Notation nolrep := (@nolrep _ _ Vadd Vzero Vscal).
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Notation nolreps := (@nolreps _ _ _ Vadd Vzero Vscal).
Context `{HVectorSpace : VectorSpace}.
Context {AeqDec : Dec (@eq tA)}.
Context {VeqDec : Dec (@eq V)}.
Notation "- a" := (Aopp a) : A_scope.
Infix "*" := Amul : A_scope.
Notation "1" := Aone : A_scope.
Notation "/ a" := (Ainv a) : A_scope.
Notation Adiv a b := (a * / b).
Infix "/" := Adiv : A_scope.
Infix "+" := Vadd : VectorSpace_scope.
Notation "0" := Vzero : VectorSpace_scope.
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Notation nolrep := (@nolrep _ _ Vadd Vzero Vscal).
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Notation nolreps := (@nolreps _ _ _ Vadd Vzero Vscal).
Vectors {v1, v2, ..., vn} are linearly dependent
Definition ldep {n} (vs : @vec V n) : Prop :=
exists (cs : @vec tA n), cs <> vzero /\ lcomb cs vs = 0.
Definition lindep {n} (vs : @vec V n) : Prop := ~(ldep vs).
Lemma ldep_or_lindep : forall {n} (vs : @vec V n), ldep vs \/ lindep vs.
Proof. intros. unfold lindep. apply classic. Qed.
Lemma lindep_iff_coef0 : forall {n} (vs : @vec V n),
lindep vs <-> (forall cs, lcomb cs vs = 0 -> cs = vzero).
Proof.
intros. unfold lindep, ldep. split; intros.
- apply not_ex_all_not with (n:=cs) in H. apply not_and_or in H.
destruct H; try easy. apply NNPP in H. auto.
- intro. destruct H0 as [c [H0 H0']]. specialize (H c H0'). easy.
Qed.
exists (cs : @vec tA n), cs <> vzero /\ lcomb cs vs = 0.
Definition lindep {n} (vs : @vec V n) : Prop := ~(ldep vs).
Lemma ldep_or_lindep : forall {n} (vs : @vec V n), ldep vs \/ lindep vs.
Proof. intros. unfold lindep. apply classic. Qed.
Lemma lindep_iff_coef0 : forall {n} (vs : @vec V n),
lindep vs <-> (forall cs, lcomb cs vs = 0 -> cs = vzero).
Proof.
intros. unfold lindep, ldep. split; intros.
- apply not_ex_all_not with (n:=cs) in H. apply not_and_or in H.
destruct H; try easy. apply NNPP in H. auto.
- intro. destruct H0 as [c [H0 H0']]. specialize (H c H0'). easy.
Qed.
使用线性无关的向量组vs作出的两种线性组合时,必然是相同的系数
Lemma lindep_imply_coef_same : forall {n} (vs : @vec V n) c1 c2,
lindep vs -> lcomb c1 vs = lcomb c2 vs -> c1 = c2.
Proof.
intros. rewrite lindep_iff_coef0 in H. specialize (H (c1 - c2)).
apply vsub_eq0_iff_eq. apply H. rewrite lcomb_coef_sub. rewrite H0.
apply vs_vadd_vopp_r.
Qed.
lindep vs -> lcomb c1 vs = lcomb c2 vs -> c1 = c2.
Proof.
intros. rewrite lindep_iff_coef0 in H. specialize (H (c1 - c2)).
apply vsub_eq0_iff_eq. apply H. rewrite lcomb_coef_sub. rewrite H0.
apply vs_vadd_vopp_r.
Qed.
若向量组vs线性无关,且向量u可由vs线性表出,则表出方式唯一
Lemma lindep_imply_coef_uniq : forall {n} (vs : @vec V n) u,
lindep vs -> lrep vs u -> exists ! cs, u = lcomb cs vs.
Proof.
intros. unfold lrep in H0. destruct H0 as [cs H0]. exists cs. hnf. split; auto.
intros. rewrite <- H0 in H1. apply lindep_imply_coef_same in H1; auto.
Qed.
lindep vs -> lrep vs u -> exists ! cs, u = lcomb cs vs.
Proof.
intros. unfold lrep in H0. destruct H0 as [cs H0]. exists cs. hnf. split; auto.
intros. rewrite <- H0 in H1. apply lindep_imply_coef_same in H1; auto.
Qed.
包含零向量的向量组,必定线性相关
Lemma ldep_if_contain_0 : forall {n} (vs : @vec V n), (exists i, vs i = Vzero) -> ldep vs.
Proof.
intros. destruct H as [i H]. hnf. exists (veye Azero Aone i). split.
- apply veye_neq0. apply field_1_neq_0.
- rewrite lcomb_coef_veye. auto.
Qed.
Proof.
intros. destruct H as [i H]. hnf. exists (veye Azero Aone i). split.
- apply veye_neq0. apply field_1_neq_0.
- rewrite lcomb_coef_veye. auto.
Qed.
线性无关的向量组,必不含零向量
Lemma lindep_then_all_not0 : forall {n} (vs : @vec V n),
lindep vs -> forall i, vs i <> Vzero.
Proof.
intros n vs H. apply not_ex_all_not. intro. apply ldep_if_contain_0 in H0; auto.
Qed.
lindep vs -> forall i, vs i <> Vzero.
Proof.
intros n vs H. apply not_ex_all_not. intro. apply ldep_if_contain_0 in H0; auto.
Qed.
单个向量线性相关,iff,该向量为零
Lemma ldep_vec1_iff_eq0 : forall (vs : @vec V 1), ldep vs <-> vs = (fun i => Vzero).
Proof.
intros. split; intros.
- unfold ldep in H. destruct H as [c [H H']].
v2e c. apply v1neq_iff in H. cbv in H. cbv in H'.
rewrite vs_vadd_0_r in H'.
eapply vs_vscal_eq0_imply_k0_or_v0 in H'. destruct H'; try easy.
apply v1eq_iff. erewrite nat2finS_eq; auto. apply H0.
- apply ldep_if_contain_0. exists (nat2finS 0). rewrite H. auto.
Qed.
Proof.
intros. split; intros.
- unfold ldep in H. destruct H as [c [H H']].
v2e c. apply v1neq_iff in H. cbv in H. cbv in H'.
rewrite vs_vadd_0_r in H'.
eapply vs_vscal_eq0_imply_k0_or_v0 in H'. destruct H'; try easy.
apply v1eq_iff. erewrite nat2finS_eq; auto. apply H0.
- apply ldep_if_contain_0. exists (nat2finS 0). rewrite H. auto.
Qed.
单个向量线性无关,iff,该向量不为零
Lemma lindep_vec1_iff_neq0 : forall (vs : @vec V 1), lindep vs <-> vs <> (fun i => Vzero).
Proof. intros. unfold lindep. rewrite ldep_vec1_iff_eq0. easy. Qed.
Proof. intros. unfold lindep. rewrite ldep_vec1_iff_eq0. easy. Qed.
两个原则:
1. 如果向量组的一个部分组线性相关,那么整个向量组也线性相关
2. 如果向量组线性无关,那么它的任何一个部分组也线性无关
表现出来是如下的几组引理
vs线性相关,则{u,vs}线性相关
Lemma ldep_imply_vconsH_ldep : forall {n} (vs : @vec V n) (u : V),
ldep vs -> ldep (vconsH u vs).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vconsH Azero cs). split.
- apply vconsH_neq0_iff. auto.
- rewrite lcomb_vconsH_vconsH. rewrite H0. rewrite vs_vadd_0_r.
apply vs_vscal_0_l.
Qed.
ldep vs -> ldep (vconsH u vs).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vconsH Azero cs). split.
- apply vconsH_neq0_iff. auto.
- rewrite lcomb_vconsH_vconsH. rewrite H0. rewrite vs_vadd_0_r.
apply vs_vscal_0_l.
Qed.
vs线性相关,则{vs,u}线性相关
Lemma ldep_imply_vconsT_ldep : forall {n} (vs : @vec V n) (u : V),
ldep vs -> ldep (vconsT vs u).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vconsT cs Azero). split.
- apply vconsT_neq0_iff. auto.
- rewrite lcomb_vconsT_vconsT. rewrite H0. rewrite vs_vadd_0_l.
apply vs_vscal_0_l.
Qed.
ldep vs -> ldep (vconsT vs u).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vconsT cs Azero). split.
- apply vconsT_neq0_iff. auto.
- rewrite lcomb_vconsT_vconsT. rewrite H0. rewrite vs_vadd_0_l.
apply vs_vscal_0_l.
Qed.
{u,vs}线性无关,则vs线性无关
Lemma vconsH_lindep_imply_lindep : forall {n} (vs : @vec V n) (u : V),
lindep (vconsH u vs) -> lindep vs.
Proof.
intros. hnf in *. intros. destruct H. apply ldep_imply_vconsH_ldep; auto.
Qed.
lindep (vconsH u vs) -> lindep vs.
Proof.
intros. hnf in *. intros. destruct H. apply ldep_imply_vconsH_ldep; auto.
Qed.
{vs,u}线性无关,则vs线性无关
Lemma vconsT_lindep_imply_lindep : forall {n} (vs : @vec V n) (u : V),
lindep (vconsT vs u) -> lindep vs.
Proof.
intros. hnf in *. intros. destruct H. apply ldep_imply_vconsT_ldep; auto.
Qed.
lindep (vconsT vs u) -> lindep vs.
Proof.
intros. hnf in *. intros. destruct H. apply ldep_imply_vconsT_ldep; auto.
Qed.
vremoveH vs 线性相关,则 vs 线性相关
Lemma vremoveH_ldep_imply_ldep : forall {n} (vs : @vec V (S n)),
ldep (vremoveH vs) -> ldep vs.
Proof.
intros. rewrite <- vconsH_vhead_vremoveH. apply ldep_imply_vconsH_ldep; auto.
Qed.
ldep (vremoveH vs) -> ldep vs.
Proof.
intros. rewrite <- vconsH_vhead_vremoveH. apply ldep_imply_vconsH_ldep; auto.
Qed.
vremoveT vs 线性相关,则 vs 线性相关
Lemma vremoveT_ldep_imply_ldep : forall {n} (vs : @vec V (S n)),
ldep (vremoveT vs) -> ldep vs.
Proof.
intros. rewrite <- (vconsT_vremoveT_vtail vs).
apply ldep_imply_vconsT_ldep. auto.
Qed.
ldep (vremoveT vs) -> ldep vs.
Proof.
intros. rewrite <- (vconsT_vremoveT_vtail vs).
apply ldep_imply_vconsT_ldep. auto.
Qed.
vs 线性无关,则 vremoveH vs 线性无关
Lemma lindep_imply_vremoveH_lindep : forall {n} (vs : @vec V (S n)),
lindep vs -> lindep (vremoveH vs).
Proof.
intros. unfold lindep in *. intro. destruct H.
apply vremoveH_ldep_imply_ldep; auto.
Qed.
lindep vs -> lindep (vremoveH vs).
Proof.
intros. unfold lindep in *. intro. destruct H.
apply vremoveH_ldep_imply_ldep; auto.
Qed.
vs 线性无关,则 vremoveT vs 线性无关
Lemma lindpe_imply_vremoveT_lindep : forall {n} (vs : @vec V (S n)),
lindep vs -> lindep (vremoveT vs).
Proof.
intros. unfold lindep in *. intro. destruct H.
apply vremoveT_ldep_imply_ldep; auto.
Qed.
lindep vs -> lindep (vremoveT vs).
Proof.
intros. unfold lindep in *. intro. destruct H.
apply vremoveT_ldep_imply_ldep; auto.
Qed.
us线性相关,则{us,vs}线性相关
Lemma ldep_imply_vapp_ldep_L : forall {n m} (us : @vec V n) (vs : @vec V m),
ldep us -> ldep (vapp us vs).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vapp cs (@Vector.vzero _ Azero m)). split.
- rewrite vapp_eq0_iff. apply or_not_and. auto.
- rewrite lcomb_vapp_vapp. rewrite H0. rewrite lcomb_coef_0.
apply vs_vadd_0_r.
Qed.
ldep us -> ldep (vapp us vs).
Proof.
intros. hnf in *. destruct H as [cs [H H0]].
exists (vapp cs (@Vector.vzero _ Azero m)). split.
- rewrite vapp_eq0_iff. apply or_not_and. auto.
- rewrite lcomb_vapp_vapp. rewrite H0. rewrite lcomb_coef_0.
apply vs_vadd_0_r.
Qed.
vs线性相关,则{us,vs}线性相关
Lemma ldep_imply_vapp_ldep_R : forall {n m} (us : @vec V n) (vs : @vec V m),
ldep vs -> ldep (vapp us vs).
Proof.
intros. hnf in *. destruct H as [ds [H H0]].
exists (vapp (@Vector.vzero _ Azero n) ds). split.
- rewrite vapp_eq0_iff. apply or_not_and. auto.
- rewrite lcomb_vapp_vapp. rewrite H0. rewrite lcomb_coef_0.
apply vs_vadd_0_r.
Qed.
ldep vs -> ldep (vapp us vs).
Proof.
intros. hnf in *. destruct H as [ds [H H0]].
exists (vapp (@Vector.vzero _ Azero n) ds). split.
- rewrite vapp_eq0_iff. apply or_not_and. auto.
- rewrite lcomb_vapp_vapp. rewrite H0. rewrite lcomb_coef_0.
apply vs_vadd_0_r.
Qed.
{us,vs}线性无关,则us线性无关
Lemma vapp_lindep_imply_lindep_L : forall {n m} (us : @vec V n) (vs : @vec V m),
lindep (vapp us vs) -> lindep us.
Proof.
unfold lindep. intros. intro. destruct H. apply ldep_imply_vapp_ldep_L; auto.
Qed.
lindep (vapp us vs) -> lindep us.
Proof.
unfold lindep. intros. intro. destruct H. apply ldep_imply_vapp_ldep_L; auto.
Qed.
{us,vs}线性无关,则vs线性无关
Lemma vapp_lindep_imply_lindep_R : forall {n m} (us : @vec V n) (vs : @vec V m),
lindep (vapp us vs) -> lindep vs.
Proof.
unfold lindep. intros. intro. destruct H. apply ldep_imply_vapp_ldep_R; auto.
Qed.
lindep (vapp us vs) -> lindep vs.
Proof.
unfold lindep. intros. intro. destruct H. apply ldep_imply_vapp_ldep_R; auto.
Qed.
vs(n)线性相关,则vs(n+m)线性相关
Lemma vheadN_ldep_imply_ldep : forall {n m} (vs : @vec V (n + m)),
ldep (vheadN vs) -> ldep vs.
Proof.
intros. rewrite <- vapp_vheadN_vtailN. apply ldep_imply_vapp_ldep_L; auto.
Qed.
ldep (vheadN vs) -> ldep vs.
Proof.
intros. rewrite <- vapp_vheadN_vtailN. apply ldep_imply_vapp_ldep_L; auto.
Qed.
vs(m)线性相关,则vs(n+m)线性相关
Lemma vtailN_ldep_imply_ldep : forall {n m} (vs : @vec V (n + m)),
ldep (vtailN vs) -> ldep vs.
Proof.
intros. rewrite <- vapp_vheadN_vtailN. apply ldep_imply_vapp_ldep_R; auto.
Qed.
ldep (vtailN vs) -> ldep vs.
Proof.
intros. rewrite <- vapp_vheadN_vtailN. apply ldep_imply_vapp_ldep_R; auto.
Qed.
vs(n+m)线性无关,则vs(n)线性无关
Lemma lindep_imply_vheadN_lindep : forall {n m} (vs : @vec V (n + m)),
lindep vs -> lindep (vheadN vs).
Proof.
unfold lindep. intros. intro. destruct H. apply vheadN_ldep_imply_ldep; auto.
Qed.
lindep vs -> lindep (vheadN vs).
Proof.
unfold lindep. intros. intro. destruct H. apply vheadN_ldep_imply_ldep; auto.
Qed.
vs(n+m)线性无关,则vs(m)线性无关
Lemma lindep_imply_vtailN_lindep : forall {n m} (vs : @vec V (n + m)),
lindep vs -> lindep (vtailN vs).
Proof.
unfold lindep. intros. intro. destruct H. apply vtailN_ldep_imply_ldep; auto.
Qed.
lindep vs -> lindep (vtailN vs).
Proof.
unfold lindep. intros. intro. destruct H. apply vtailN_ldep_imply_ldep; auto.
Qed.
线性相关 <-> 其中至少有一个向量可以由其余向量线性表示
Lemma ldep_iff_exist_lrep : forall {n} (vs : @vec V (S n)),
ldep vs <-> exists i, lrep (vremove vs i) (vs i).
Proof.
intros. unfold ldep,lrep. split; intros.
- destruct H as [c [H H1]]. apply vneq_iff_exist_vnth_neq in H.
destruct H as [i H]. exists i.
exists (vmap (fun x => Aopp x / (c i)) (vremove c i)).
rewrite (@vmap_vremove _ _ Azero Azero). rewrite lcomb_vremove_vremove.
rewrite vnth_vmap. rewrite !vs_vscal_opp at 1. rewrite group_opp_opp.
rewrite field_mulInvR; auto. rewrite vs_vscal_1_l at 1.
replace (vmap (fun x => - x / c i)%A c) with (vscal (Amul:=Amul) (- (/ c i))%A c).
+ rewrite lcomb_coef_scal. rewrite H1. rewrite vs_vscal_0_r at 1.
apply vs_vadd_0_l.
+ apply veq_iff_vnth; intros j. rewrite vnth_vscal, vnth_vmap.
rewrite !ring_mul_opp_l at 1. f_equal. apply commutative.
- destruct H as [i [c H]].
exists (vinsert c i (Aopp Aone)). split.
+ apply vinsert_neq0_iff. right. apply field_neg1_neq_0.
+ pose proof (lcomb_coef_vinsert_0 c vs i).
pose proof (lcomb_coef_vinsert_neg1 c vs i).
rewrite H0 in H1. rewrite H in H1.
symmetry in H1. apply vs_add_eqR_imply0 in H1. auto.
Qed.
ldep vs <-> exists i, lrep (vremove vs i) (vs i).
Proof.
intros. unfold ldep,lrep. split; intros.
- destruct H as [c [H H1]]. apply vneq_iff_exist_vnth_neq in H.
destruct H as [i H]. exists i.
exists (vmap (fun x => Aopp x / (c i)) (vremove c i)).
rewrite (@vmap_vremove _ _ Azero Azero). rewrite lcomb_vremove_vremove.
rewrite vnth_vmap. rewrite !vs_vscal_opp at 1. rewrite group_opp_opp.
rewrite field_mulInvR; auto. rewrite vs_vscal_1_l at 1.
replace (vmap (fun x => - x / c i)%A c) with (vscal (Amul:=Amul) (- (/ c i))%A c).
+ rewrite lcomb_coef_scal. rewrite H1. rewrite vs_vscal_0_r at 1.
apply vs_vadd_0_l.
+ apply veq_iff_vnth; intros j. rewrite vnth_vscal, vnth_vmap.
rewrite !ring_mul_opp_l at 1. f_equal. apply commutative.
- destruct H as [i [c H]].
exists (vinsert c i (Aopp Aone)). split.
+ apply vinsert_neq0_iff. right. apply field_neg1_neq_0.
+ pose proof (lcomb_coef_vinsert_0 c vs i).
pose proof (lcomb_coef_vinsert_neg1 c vs i).
rewrite H0 in H1. rewrite H in H1.
symmetry in H1. apply vs_add_eqR_imply0 in H1. auto.
Qed.
线性无关 <-> 其中每一个向量都不能由其余向量线性表示
Lemma lindep_iff_none_lrep : forall {n} (vs : @vec V (S n)),
lindep vs <-> forall i, ~ (lrep (vremove vs i) (vs i)).
Proof.
intros. unfold lindep. rewrite ldep_iff_exist_lrep. split; intro.
apply not_ex_all_not; auto. apply all_not_not_ex; auto.
Qed.
lindep vs <-> forall i, ~ (lrep (vremove vs i) (vs i)).
Proof.
intros. unfold lindep. rewrite ldep_iff_exist_lrep. split; intro.
apply not_ex_all_not; auto. apply all_not_not_ex; auto.
Qed.
向量u可以由vs线性表示,则{vs,u}线性相关
Lemma lrep_imply_vconsT_ldep : forall {n} (vs : @vec V n) (u : V),
lrep vs u -> ldep (vconsT vs u).
Proof.
intros. unfold lrep,ldep in *. destruct H as [cs H].
exists (vconsT cs (-(1))%A). split.
- rewrite vconsT_eq0_iff. apply or_not_and. right. apply field_neg1_neq_0.
- rewrite lcomb_vconsT_vconsT. rewrite H.
rewrite vs_vscal_opp1. apply vs_vadd_vopp_r.
Qed.
lrep vs u -> ldep (vconsT vs u).
Proof.
intros. unfold lrep,ldep in *. destruct H as [cs H].
exists (vconsT cs (-(1))%A). split.
- rewrite vconsT_eq0_iff. apply or_not_and. right. apply field_neg1_neq_0.
- rewrite lcomb_vconsT_vconsT. rewrite H.
rewrite vs_vscal_opp1. apply vs_vadd_vopp_r.
Qed.
向量u可以由vs线性表示,则{u,vs}线性相关
Lemma lrep_imply_vconsH_ldep : forall {n} (vs : @vec V n) (u : V),
lrep vs u -> ldep (vconsH u vs).
Proof.
intros. unfold lrep,ldep in *. destruct H as [cs H].
exists (vconsH (-(1))%A cs). split.
- rewrite vconsH_eq0_iff. apply or_not_and. left. apply field_neg1_neq_0.
- rewrite lcomb_vconsH_vconsH. rewrite H.
rewrite vs_vscal_opp1 at 1. apply vs_vadd_vopp_l.
Qed.
lrep vs u -> ldep (vconsH u vs).
Proof.
intros. unfold lrep,ldep in *. destruct H as [cs H].
exists (vconsH (-(1))%A cs). split.
- rewrite vconsH_eq0_iff. apply or_not_and. left. apply field_neg1_neq_0.
- rewrite lcomb_vconsH_vconsH. rewrite H.
rewrite vs_vscal_opp1 at 1. apply vs_vadd_vopp_l.
Qed.
设向量组vs线性无关,向量组{vs,u}线性相关,则向量u可由vs线性表示
Theorem ldep_vconsT_lindep_imply_lrep : forall {n} (vs : @vec V n) (u : V),
lindep vs -> ldep (vconsT vs u) -> lrep vs u.
Proof.
intros. unfold lindep, ldep in *. destruct H0 as [cs [H0 H1]].
destruct (Aeqdec (vtail cs) Azero) as [H2|H2].
-
assert (exists cs, cs <> vzero /\ lcomb cs vs = 0); try tauto.
exists (vremoveT cs). split.
+ apply vremoveT_neq0_if; auto.
+ rewrite lcomb_vec_vconsT in H1. rewrite H2 in H1.
rewrite vs_vscal_0_l in H1 at 1. rewrite vs_vadd_0_r in H1. auto.
-
hnf. exists (vscal (Amul:=Amul) (- / vtail cs)%A (vremoveT cs)).
rewrite lcomb_coef_scal. rewrite lcomb_vec_vconsT in H1.
remember (lcomb (vremoveT cs) vs) as v1. rewrite vs_vscal_opp.
apply group_opp_uniq_r in H1. rewrite <- H1. rewrite vs_vscal_vopp.
rewrite group_opp_opp. rewrite <- vs_vscal_assoc.
rewrite field_mulInvL; auto. apply vs_vscal_1_l.
Qed.
lindep vs -> ldep (vconsT vs u) -> lrep vs u.
Proof.
intros. unfold lindep, ldep in *. destruct H0 as [cs [H0 H1]].
destruct (Aeqdec (vtail cs) Azero) as [H2|H2].
-
assert (exists cs, cs <> vzero /\ lcomb cs vs = 0); try tauto.
exists (vremoveT cs). split.
+ apply vremoveT_neq0_if; auto.
+ rewrite lcomb_vec_vconsT in H1. rewrite H2 in H1.
rewrite vs_vscal_0_l in H1 at 1. rewrite vs_vadd_0_r in H1. auto.
-
hnf. exists (vscal (Amul:=Amul) (- / vtail cs)%A (vremoveT cs)).
rewrite lcomb_coef_scal. rewrite lcomb_vec_vconsT in H1.
remember (lcomb (vremoveT cs) vs) as v1. rewrite vs_vscal_opp.
apply group_opp_uniq_r in H1. rewrite <- H1. rewrite vs_vscal_vopp.
rewrite group_opp_opp. rewrite <- vs_vscal_assoc.
rewrite field_mulInvL; auto. apply vs_vscal_1_l.
Qed.
设向量组vs线性无关,向量组{u,vs}线性相关,则向量u可由vs线性表示
Theorem ldep_vconsH_lindep_imply_lrep : forall {n} (vs : @vec V n) (u : V),
lindep vs -> ldep (vconsH u vs) -> lrep vs u.
Proof.
intros. unfold lindep, ldep in *. destruct H0 as [cs [H0 H1]].
destruct (Aeqdec (vhead cs) Azero) as [H2|H2].
-
assert (exists cs, cs <> vzero /\ lcomb cs vs = 0); try tauto.
exists (vremoveH cs). split.
+ apply vremoveH_neq0_if; auto.
+ rewrite lcomb_vec_vconsH in H1. rewrite H2 in H1.
rewrite vs_vscal_0_l in H1 at 1. rewrite vs_vadd_0_l in H1. auto.
-
hnf. exists (vscal (Amul:=Amul) (- / vhead cs)%A (vremoveH cs)).
rewrite lcomb_coef_scal. rewrite lcomb_vec_vconsH in H1.
remember (lcomb (vremoveH cs) vs) as v1. rewrite vs_vscal_opp.
rewrite <- vs_vscal_vopp. apply group_opp_uniq_r in H1. rewrite H1.
rewrite <- vs_vscal_assoc. rewrite field_mulInvL; auto. apply vs_vscal_1_l.
Qed.
lindep vs -> ldep (vconsH u vs) -> lrep vs u.
Proof.
intros. unfold lindep, ldep in *. destruct H0 as [cs [H0 H1]].
destruct (Aeqdec (vhead cs) Azero) as [H2|H2].
-
assert (exists cs, cs <> vzero /\ lcomb cs vs = 0); try tauto.
exists (vremoveH cs). split.
+ apply vremoveH_neq0_if; auto.
+ rewrite lcomb_vec_vconsH in H1. rewrite H2 in H1.
rewrite vs_vscal_0_l in H1 at 1. rewrite vs_vadd_0_l in H1. auto.
-
hnf. exists (vscal (Amul:=Amul) (- / vhead cs)%A (vremoveH cs)).
rewrite lcomb_coef_scal. rewrite lcomb_vec_vconsH in H1.
remember (lcomb (vremoveH cs) vs) as v1. rewrite vs_vscal_opp.
rewrite <- vs_vscal_vopp. apply group_opp_uniq_r in H1. rewrite H1.
rewrite <- vs_vscal_assoc. rewrite field_mulInvL; auto. apply vs_vscal_1_l.
Qed.
设向量组vs线性无关,则:向量u可由vs线性表示,当且仅当,向量组{vs,u}线性相关
Corollary lrep_iff_vconsT_ldep : forall {n} (vs : @vec V n) (u : V),
lindep vs -> (lrep vs u <-> ldep (vconsT vs u)).
Proof.
intros. split; intros.
- apply lrep_imply_vconsT_ldep; auto.
- apply ldep_vconsT_lindep_imply_lrep; auto.
Qed.
lindep vs -> (lrep vs u <-> ldep (vconsT vs u)).
Proof.
intros. split; intros.
- apply lrep_imply_vconsT_ldep; auto.
- apply ldep_vconsT_lindep_imply_lrep; auto.
Qed.
设向量组vs线性无关,则:向量u可由vs线性表示,当且仅当,向量组{u,vs}线性相关
Corollary lrep_iff_vconsH_ldep : forall {n} (vs : @vec V n) (u : V),
lindep vs -> (lrep vs u <-> ldep (vconsH u vs)).
Proof.
intros. split; intros.
- apply lrep_imply_vconsH_ldep; auto.
- apply ldep_vconsH_lindep_imply_lrep; auto.
Qed.
lindep vs -> (lrep vs u <-> ldep (vconsH u vs)).
Proof.
intros. split; intros.
- apply lrep_imply_vconsH_ldep; auto.
- apply ldep_vconsH_lindep_imply_lrep; auto.
Qed.
向量{u,vs}线性相关,当且仅当,向量组{vs,u}线性相关
Corollary vconsH_ldep_iff_vconsT_ldep : forall {n} (vs : @vec V n) (u : V),
ldep (vconsH u vs) <-> ldep (vconsT vs u).
Proof.
intros. destruct (ldep_or_lindep vs).
- split; intros.
+ apply ldep_imply_vconsT_ldep; auto.
+ apply ldep_imply_vconsH_ldep; auto.
- split; intros.
+ apply lrep_iff_vconsH_ldep in H0; auto. apply lrep_iff_vconsT_ldep; auto.
+ apply lrep_iff_vconsT_ldep in H0; auto. apply lrep_iff_vconsH_ldep; auto.
Qed.
ldep (vconsH u vs) <-> ldep (vconsT vs u).
Proof.
intros. destruct (ldep_or_lindep vs).
- split; intros.
+ apply ldep_imply_vconsT_ldep; auto.
+ apply ldep_imply_vconsH_ldep; auto.
- split; intros.
+ apply lrep_iff_vconsH_ldep in H0; auto. apply lrep_iff_vconsT_ldep; auto.
+ apply lrep_iff_vconsT_ldep in H0; auto. apply lrep_iff_vconsH_ldep; auto.
Qed.
设向量组vs线性无关,则:向量u不能由vs线性表示,当且仅当,向量组{vs,u}线性无关
Corollary nolrep_iff_vconsT_lindep : forall {n} (vs : @vec V n) (u : V),
lindep vs -> (nolrep vs u <-> lindep (vconsT vs u)).
Proof.
intros. unfold nolrep, lindep. apply not_iff_compat.
apply lrep_iff_vconsT_ldep; auto.
Qed.
lindep vs -> (nolrep vs u <-> lindep (vconsT vs u)).
Proof.
intros. unfold nolrep, lindep. apply not_iff_compat.
apply lrep_iff_vconsT_ldep; auto.
Qed.
p90, 例7,替换定理:
设向量组v1,...,vn线性无关,u=c1v1+...+cnvn。若ci<>0,则用u替换vi后得到的
向量组v1,...,v(i-1),u,v(i+1),...,vn也线性相关
Lemma lindep_subst : forall {n} (vs : @vec V n) (cs : @vec tA n) (i : fin n),
lindep vs -> cs i <> Azero -> lindep (vset vs i (lcomb cs vs)).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H. destruct H1 as [ds [H1 H2]].
exists (vadd (vset ds i Azero) (vscal (Amul:=Amul) (ds i) cs)). split.
- apply vneq_iff_exist_vnth_neq in H1. destruct H1 as [j H1].
apply vneq_iff_exist_vnth_neq.
destruct (i ??= j).
+
fin2nat. rewrite <- e in *.
exists i. rewrite vnth_vadd. rewrite vnth_vset_eq. rewrite identityLeft.
rewrite vnth_vscal. rewrite vnth_vzero in *.
apply field_mul_neq0_iff; auto.
+
fin2nat. destruct (Aeqdec (ds i) Azero).
*
exists j. rewrite e. rewrite vscal_0_l. rewrite vadd_0_r.
rewrite vnth_vset_neq; auto.
*
exists i. rewrite vnth_vadd. rewrite vnth_vset_eq. rewrite vnth_vscal.
rewrite identityLeft. apply field_mul_neq0_iff; auto.
- rewrite <- H2 at 2.
rewrite lcomb_coef_add. rewrite lcomb_coef_scal. rewrite lcomb_coef_vset.
rewrite lcomb_vec_vset. rewrite vs_vscal_vadd.
rewrite associative. f_equal. rewrite commutative. f_equal.
rewrite vs_vscal_aadd. rewrite vs_vscal_vopp at 1. rewrite vs_vscal_opp at 1.
rewrite vs_vscal_0_l at 1. apply vs_vadd_0_l.
Qed.
Lemma lreps_more_imply_ldep : forall {r s} (vs : @vec V r) (us : @vec V s),
lreps us vs -> r > s -> ldep vs.
Proof.
intros. unfold lreps,vforall in *. induction r. lia.
destruct (r ??= s)%nat.
2:{
assert (r > s). lia.
pose proof (IHr (vremoveH vs)).
assert (forall i, lrep us (vremoveH vs i)).
{ intro. specialize (H (fSuccRangeS i)). auto. }
specialize (H2 H3 H1).
apply vremoveH_ldep_imply_ldep; auto. }
- subst. clear IHr H0.
destruct (ldep_or_lindep vs); auto. exfalso.
Abort.
End ldep.
lindep vs -> cs i <> Azero -> lindep (vset vs i (lcomb cs vs)).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H. destruct H1 as [ds [H1 H2]].
exists (vadd (vset ds i Azero) (vscal (Amul:=Amul) (ds i) cs)). split.
- apply vneq_iff_exist_vnth_neq in H1. destruct H1 as [j H1].
apply vneq_iff_exist_vnth_neq.
destruct (i ??= j).
+
fin2nat. rewrite <- e in *.
exists i. rewrite vnth_vadd. rewrite vnth_vset_eq. rewrite identityLeft.
rewrite vnth_vscal. rewrite vnth_vzero in *.
apply field_mul_neq0_iff; auto.
+
fin2nat. destruct (Aeqdec (ds i) Azero).
*
exists j. rewrite e. rewrite vscal_0_l. rewrite vadd_0_r.
rewrite vnth_vset_neq; auto.
*
exists i. rewrite vnth_vadd. rewrite vnth_vset_eq. rewrite vnth_vscal.
rewrite identityLeft. apply field_mul_neq0_iff; auto.
- rewrite <- H2 at 2.
rewrite lcomb_coef_add. rewrite lcomb_coef_scal. rewrite lcomb_coef_vset.
rewrite lcomb_vec_vset. rewrite vs_vscal_vadd.
rewrite associative. f_equal. rewrite commutative. f_equal.
rewrite vs_vscal_aadd. rewrite vs_vscal_vopp at 1. rewrite vs_vscal_opp at 1.
rewrite vs_vscal_0_l at 1. apply vs_vadd_0_l.
Qed.
Lemma lreps_more_imply_ldep : forall {r s} (vs : @vec V r) (us : @vec V s),
lreps us vs -> r > s -> ldep vs.
Proof.
intros. unfold lreps,vforall in *. induction r. lia.
destruct (r ??= s)%nat.
2:{
assert (r > s). lia.
pose proof (IHr (vremoveH vs)).
assert (forall i, lrep us (vremoveH vs i)).
{ intro. specialize (H (fSuccRangeS i)). auto. }
specialize (H2 H3 H1).
apply vremoveH_ldep_imply_ldep; auto. }
- subst. clear IHr H0.
destruct (ldep_or_lindep vs); auto. exfalso.
Abort.
End ldep.
Section lmis.
Context `{HVectorSpace : VectorSpace}.
Context {AeqDec : Dec (@eq tA)}.
Context {VeqDec : Dec (@eq V)}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Notation ldep := (@ldep _ Azero _ Vadd Vzero Vscal).
Notation lindep := (@lindep _ Azero _ Vadd Vzero Vscal).
Notation vsequiv := (@vsequiv _ _ Vadd Vzero Vscal).
Context `{HVectorSpace : VectorSpace}.
Context {AeqDec : Dec (@eq tA)}.
Context {VeqDec : Dec (@eq V)}.
Notation lcomb := (@lcomb _ _ Vadd Vzero Vscal).
Notation lrep := (@lrep _ _ Vadd Vzero Vscal).
Notation lreps := (@lreps _ _ Vadd Vzero Vscal).
Notation ldep := (@ldep _ Azero _ Vadd Vzero Vscal).
Notation lindep := (@lindep _ Azero _ Vadd Vzero Vscal).
Notation vsequiv := (@vsequiv _ _ Vadd Vzero Vscal).
向量组 ms 是向量组 vs 的极大线性无关组
Definition lmis {n s} (vs : @vec V n) (ms : @vec V s) : Prop :=
vmems ms vs /\
lindep ms /\
(vforall vs (fun v => ~(vmem ms v) -> ldep (vconsT ms v))) .
vmems ms vs /\
lindep ms /\
(vforall vs (fun v => ~(vmem ms v) -> ldep (vconsT ms v))) .
向量组与其极大线性无关组等价
Lemma lmis_vsequiv_self : forall {n s} (vs : @vec V n) (ms : @vec V s),
lmis vs ms -> vsequiv vs ms.
Proof.
intros. unfold lmis, vsequiv in *. destruct H as [H [H1 H2]].
unfold vmems,vmem,vexist,vforall,lreps,vforall in *. split.
- intros. pose proof (lrep_in vs). unfold vforall in H0.
specialize (H i). destruct H as [j H]. rewrite <- H. auto.
- intros. specialize (H2 i). pose proof (vmem_dec ms (vs i)).
destruct H0 as [H0|H0].
+ destruct H0 as [j H0]. rewrite <- H0. apply lrep_in.
+ epose proof (lrep_iff_vconsT_ldep (vs i) H1). apply H3; auto.
Qed.
lmis vs ms -> vsequiv vs ms.
Proof.
intros. unfold lmis, vsequiv in *. destruct H as [H [H1 H2]].
unfold vmems,vmem,vexist,vforall,lreps,vforall in *. split.
- intros. pose proof (lrep_in vs). unfold vforall in H0.
specialize (H i). destruct H as [j H]. rewrite <- H. auto.
- intros. specialize (H2 i). pose proof (vmem_dec ms (vs i)).
destruct H0 as [H0|H0].
+ destruct H0 as [j H0]. rewrite <- H0. apply lrep_in.
+ epose proof (lrep_iff_vconsT_ldep (vs i) H1). apply H3; auto.
Qed.
向量组的任意两个极大线性无关组等价
Corollary lmis_vsequiv_any :
forall {n s t} (vs : @vec V n) (ms1 : @vec V s) (ms2 : @vec V t),
lmis vs ms1 -> lmis vs ms2 -> vsequiv ms1 ms2.
Proof.
intros. apply lmis_vsequiv_self in H, H0.
apply vsequiv_trans with vs; auto. apply vsequiv_sym; auto.
Qed.
forall {n s t} (vs : @vec V n) (ms1 : @vec V s) (ms2 : @vec V t),
lmis vs ms1 -> lmis vs ms2 -> vsequiv ms1 ms2.
Proof.
intros. apply lmis_vsequiv_self in H, H0.
apply vsequiv_trans with vs; auto. apply vsequiv_sym; auto.
Qed.
向量u可由向量组vs线性表出当且仅当u可由vs的一个极大线性线性无关组线性表出
Corollary lrep_iff_lrepByLmis :
forall {n s} (vs : @vec V n) (ms : @vec V s) (u : V),
lmis vs ms -> (lrep vs u <-> lrep ms u).
Proof.
intros. apply lmis_vsequiv_self in H. unfold vsequiv in H. destruct H.
split; intros. apply (lreps_lrep H0 H1). apply (lreps_lrep H H1).
Qed.
End lmis.
forall {n s} (vs : @vec V n) (ms : @vec V s) (u : V),
lmis vs ms -> (lrep vs u <-> lrep ms u).
Proof.
intros. apply lmis_vsequiv_self in H. unfold vsequiv in H. destruct H.
split; intros. apply (lreps_lrep H0 H1). apply (lreps_lrep H H1).
Qed.
End lmis.
Section vectorSpace.
Context `{HField : Field tA Aadd Azero Aopp Amul Aone Ainv}.
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Notation vopp := (@vopp _ Aopp).
Notation vscal := (@vscal _ Amul).
#[export] Instance vectorSpace {n : nat} :
VectorSpace (V:=vec n) vadd vzero vopp vscal.
Proof.
constructor; try apply vadd_AGroup; intros.
apply vscal_1_l. rewrite vscal_assoc; auto.
apply vscal_add. apply vscal_vadd.
Qed.
End vectorSpace.
Arguments vectorSpace {tA Aadd Azero Aopp Amul Aone Ainv} HField {n}.
Section props.
Context `{HField : Field tA Aadd Azero Aopp Amul Aone Ainv}.
Notation vectorSpace := (vectorSpace HField).
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation vscal := (@vscal _ Amul).
Notation vsum := (@vsum _ Aadd Azero).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Notation lcomb := (@lcomb _ _ vadd vzero vscal).
Notation lrep := (@lrep _ _ vadd vzero vscal).
Notation ldep := (@ldep _ Azero _ vadd vzero vscal).
Notation lindep := (@lindep _ Azero _ vadd vzero vscal).
Context `{HField : Field tA Aadd Azero Aopp Amul Aone Ainv}.
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Notation vopp := (@vopp _ Aopp).
Notation vscal := (@vscal _ Amul).
#[export] Instance vectorSpace {n : nat} :
VectorSpace (V:=vec n) vadd vzero vopp vscal.
Proof.
constructor; try apply vadd_AGroup; intros.
apply vscal_1_l. rewrite vscal_assoc; auto.
apply vscal_add. apply vscal_vadd.
Qed.
End vectorSpace.
Arguments vectorSpace {tA Aadd Azero Aopp Amul Aone Ainv} HField {n}.
Section props.
Context `{HField : Field tA Aadd Azero Aopp Amul Aone Ainv}.
Notation vectorSpace := (vectorSpace HField).
Notation vzero := (vzero Azero).
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vopp := (@vopp _ Aopp).
Notation "- v" := (vopp v) : vec_scope.
Notation vsub a b := (a + - b).
Notation "a - b" := ((a + (-b))%V) : vec_scope.
Notation vscal := (@vscal _ Amul).
Notation vsum := (@vsum _ Aadd Azero).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Notation lcomb := (@lcomb _ _ vadd vzero vscal).
Notation lrep := (@lrep _ _ vadd vzero vscal).
Notation ldep := (@ldep _ Azero _ vadd vzero vscal).
Notation lindep := (@lindep _ Azero _ vadd vzero vscal).
(lcomb cs vs).i = ∑(vmap2 Amul cs (vcol vs i))
Lemma vnth_lcomb : forall {n r} (cs : @vec tA r) (vs : mat tA r n) (i : fin n),
(lcomb cs vs) i = vsum (vmap2 Amul cs (mcol vs i)).
Proof. intros. unfold lcomb. rewrite vnth_vsum. auto. Qed.
(lcomb cs vs) i = vsum (vmap2 Amul cs (mcol vs i)).
Proof. intros. unfold lcomb. rewrite vnth_vsum. auto. Qed.
lcomb over vectors from `vmap2 vapp us vs`
Lemma lcomb_vec_vmap2_vapp :
forall (m n r : nat) (cs : @vec tA r)
(us : @mat tA r m) (vs : @mat tA r n) (i : fin (m + n)),
lcomb cs (vmap2 vapp us vs) i = vapp (lcomb cs us) (lcomb cs vs) i.
Proof.
intros. rewrite vnth_lcomb. destruct (fin2nat i ??< m).
- rewrite vnth_vapp_l with (H:=l). unfold lcomb.
rewrite vnth_vsum. apply vsum_eq; intros j.
rewrite !vnth_vmap2. rewrite !vnth_vscal. f_equal. rewrite !vnth_mcol.
rewrite vnth_vmap2. rewrite vnth_vapp_l with (H:=l); auto.
- assert (m <= fin2nat i). lia. rewrite vnth_vapp_r with (H:=H). unfold lcomb.
rewrite vnth_vsum. apply vsum_eq; intros j.
rewrite !vnth_vmap2. rewrite !vnth_vscal. f_equal. rewrite !vnth_mcol.
rewrite vnth_vmap2. rewrite vnth_vapp_r with (H:=H). auto.
Qed.
forall (m n r : nat) (cs : @vec tA r)
(us : @mat tA r m) (vs : @mat tA r n) (i : fin (m + n)),
lcomb cs (vmap2 vapp us vs) i = vapp (lcomb cs us) (lcomb cs vs) i.
Proof.
intros. rewrite vnth_lcomb. destruct (fin2nat i ??< m).
- rewrite vnth_vapp_l with (H:=l). unfold lcomb.
rewrite vnth_vsum. apply vsum_eq; intros j.
rewrite !vnth_vmap2. rewrite !vnth_vscal. f_equal. rewrite !vnth_mcol.
rewrite vnth_vmap2. rewrite vnth_vapp_l with (H:=l); auto.
- assert (m <= fin2nat i). lia. rewrite vnth_vapp_r with (H:=H). unfold lcomb.
rewrite vnth_vsum. apply vsum_eq; intros j.
rewrite !vnth_vmap2. rewrite !vnth_vscal. f_equal. rewrite !vnth_mcol.
rewrite vnth_vmap2. rewrite vnth_vapp_r with (H:=H). auto.
Qed.
F^n的下述子集U是一个子空间 U = {(a1,...,ak,0,...,0) | ai ∈ F, 1 <= k < n }
Section topKWithZero_SubSpace.
Context {n k : nat}.
Context {Hk : 1 <= k < n}.
Instance topKWithZero_SubSpaceStruct
: SubSpaceStruct
(fun v => forall (i:fin n),
if (fin2nat i ??> k)%nat then v i = Azero else True).
Proof.
constructor; intros.
- destruct (_??<_); auto.
- destruct (_??<_); auto. rewrite vnth_vadd.
pose proof (u.prf). pose proof (v.prf). simpl in *.
specialize (H i). specialize (H0 i).
destruct (_??<_) in H,H0; try lia. rewrite H,H0. apply identityLeft.
- destruct (_??<_); auto. rewrite vnth_vscal.
pose proof (v.prf). simpl in *. specialize (H i).
destruct (_??<_) in H; try lia. rewrite H. apply ring_mul_0_r.
Qed.
#[export] Instance topKWithZero_SubSpace : VectorSpace Hadd Hzero Hopp Hscal :=
makeSubSpace topKWithZero_SubSpaceStruct.
End topKWithZero_SubSpace.
Context {n k : nat}.
Context {Hk : 1 <= k < n}.
Instance topKWithZero_SubSpaceStruct
: SubSpaceStruct
(fun v => forall (i:fin n),
if (fin2nat i ??> k)%nat then v i = Azero else True).
Proof.
constructor; intros.
- destruct (_??<_); auto.
- destruct (_??<_); auto. rewrite vnth_vadd.
pose proof (u.prf). pose proof (v.prf). simpl in *.
specialize (H i). specialize (H0 i).
destruct (_??<_) in H,H0; try lia. rewrite H,H0. apply identityLeft.
- destruct (_??<_); auto. rewrite vnth_vscal.
pose proof (v.prf). simpl in *. specialize (H i).
destruct (_??<_) in H; try lia. rewrite H. apply ring_mul_0_r.
Qed.
#[export] Instance topKWithZero_SubSpace : VectorSpace Hadd Hzero Hopp Hscal :=
makeSubSpace topKWithZero_SubSpaceStruct.
End topKWithZero_SubSpace.
F^n的下述子集U是一个子空间 U = {(a1,0,a3,0,...0,an) | ai ∈ F, i=1,3,...,n}
Section oddWithZero_SubSpace.
Context {n : nat}.
Instance oddWithZero_SubSpaceStruct
: SubSpaceStruct
(fun v => forall (i : fin n),
if ((fin2nat i mod 2) ??= 0)%nat then v i = Azero else True).
Proof.
constructor; intros.
- destruct (_??=_)%nat; auto.
- destruct (_??=_)%nat; auto. rewrite vnth_vadd.
pose proof (u.prf). pose proof (v.prf). hnf in H,H0.
specialize (H i). specialize (H0 i).
destruct (_??=_)%nat in H,H0; try lia. rewrite H,H0. apply identityLeft.
- destruct (_??=_)%nat; auto. rewrite vnth_vscal.
pose proof (v.prf). hnf in H. specialize (H i).
destruct (_??=_)%nat in H; try lia. rewrite H. apply ring_mul_0_r.
Qed.
#[export] Instance oddWithZero_SubSpace : VectorSpace Hadd Hzero Hopp Hscal :=
makeSubSpace oddWithZero_SubSpaceStruct.
End oddWithZero_SubSpace.
Context {n : nat}.
Instance oddWithZero_SubSpaceStruct
: SubSpaceStruct
(fun v => forall (i : fin n),
if ((fin2nat i mod 2) ??= 0)%nat then v i = Azero else True).
Proof.
constructor; intros.
- destruct (_??=_)%nat; auto.
- destruct (_??=_)%nat; auto. rewrite vnth_vadd.
pose proof (u.prf). pose proof (v.prf). hnf in H,H0.
specialize (H i). specialize (H0 i).
destruct (_??=_)%nat in H,H0; try lia. rewrite H,H0. apply identityLeft.
- destruct (_??=_)%nat; auto. rewrite vnth_vscal.
pose proof (v.prf). hnf in H. specialize (H i).
destruct (_??=_)%nat in H; try lia. rewrite H. apply ring_mul_0_r.
Qed.
#[export] Instance oddWithZero_SubSpace : VectorSpace Hadd Hzero Hopp Hscal :=
makeSubSpace oddWithZero_SubSpaceStruct.
End oddWithZero_SubSpace.
添加或去掉向量的一些分量构成的延伸组与缩短组的一对性质:
1. 如果向量组线性无关,那么把每个向量在相同位置添上m个分量得到的延伸组也线性无关
2. 如果向量组线性相关,那么把每个向量在相同位置去掉m个分量得到的缩短组也线性相关
如何表示“延伸组和缩短组”?
1. 如何表示“延伸的向量”,“缩短的向量”?
(1) 在头部加入/去掉数个元素,在尾部加入/去掉数个元素,在任意位置加入/去掉数个元素
(2) 在任意位置的操作包含了头部或尾部。
3. 如何表示“延伸组”,“缩短组”?
(1) 关键是要对向量组在相同的位置进行操作。
(2) 还可以换一种思路,不进行具体的操作,但是可以判断两个向量是否具有“延伸组”或
“缩短组”的关系?
给定v1,...,vs,记其延伸组为 v1',...,vs',
则从 k1v1'+...ksvs'=0 可得到 k1v1+...+ksvs=0。
若v1,...,vs线性无关,则可知k1=...=ks=0,从而v1',...,vs'也线性无关。
若向量组线性无关,每个向量的相同位置添上m个分量后的延伸组线性无关。
在每个向量头部都加入数个元素后保持线性无关
Lemma lindep_extend_head :
forall {m n r} (us : @vec (@vec tA m) r) (vs : @vec (@vec tA n) r),
lindep vs -> lindep (vmap2 vapp us vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeAddL i)).
rewrite vnth_vzero in *. rewrite <- H0 at 2.
rewrite lcomb_vec_vmap2_vapp. erewrite vnth_vapp_r.
rewrite fin2AddRangeAddL'_fin2AddRangeAddL. auto.
Unshelve. rewrite fin2nat_fin2AddRangeAddL. lia.
Qed.
forall {m n r} (us : @vec (@vec tA m) r) (vs : @vec (@vec tA n) r),
lindep vs -> lindep (vmap2 vapp us vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeAddL i)).
rewrite vnth_vzero in *. rewrite <- H0 at 2.
rewrite lcomb_vec_vmap2_vapp. erewrite vnth_vapp_r.
rewrite fin2AddRangeAddL'_fin2AddRangeAddL. auto.
Unshelve. rewrite fin2nat_fin2AddRangeAddL. lia.
Qed.
在每个向量尾部都加入数个元素后保持线性无关
Lemma lindep_extend_tail :
forall {m n r} (us : @vec (@vec tA m) r) (vs : @vec (@vec tA n) r),
lindep us -> lindep (vmap2 vapp us vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeR i)).
rewrite vnth_vzero in *. rewrite <- H0 at 2.
rewrite lcomb_vec_vmap2_vapp. erewrite vnth_vapp_l.
rewrite fin2AddRangeR'_fin2AddRangeR. auto.
Unshelve. rewrite fin2nat_fin2AddRangeR. apply fin2nat_lt.
Qed.
forall {m n r} (us : @vec (@vec tA m) r) (vs : @vec (@vec tA n) r),
lindep us -> lindep (vmap2 vapp us vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeR i)).
rewrite vnth_vzero in *. rewrite <- H0 at 2.
rewrite lcomb_vec_vmap2_vapp. erewrite vnth_vapp_l.
rewrite fin2AddRangeR'_fin2AddRangeR. auto.
Unshelve. rewrite fin2nat_fin2AddRangeR. apply fin2nat_lt.
Qed.
对每个向量都插入1个元素后保持线性无关
Lemma lindep_extend_insert :
forall {n r} (vs : @vec (@vec tA n) r) (i : fin (S n)) (a : tA),
lindep vs -> lindep (vmap (fun v => vinsert v i a) vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; intros; auto.
rewrite veq_iff_vnth. intros j. rewrite veq_iff_vnth in H0.
destruct (fin2nat j ??< fin2nat i).
- specialize (H0 (fSuccRange j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. rewrite !vnth_vmap2. f_equal. unfold mcol.
rewrite !vnth_vmap. erewrite vnth_vinsert_lt. fin.
- specialize (H0 (fSuccRangeS j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. rewrite !vnth_vmap2. f_equal. unfold mcol.
rewrite !vnth_vmap. erewrite vnth_vinsert_gt; fin.
Unshelve. all: fin.
Qed.
End lindep_extend.
forall {n r} (vs : @vec (@vec tA n) r) (i : fin (S n)) (a : tA),
lindep vs -> lindep (vmap (fun v => vinsert v i a) vs).
Proof.
intros. unfold lindep, ldep in *. intro. destruct H.
destruct H0 as [cs [H H0]]. exists cs. split; intros; auto.
rewrite veq_iff_vnth. intros j. rewrite veq_iff_vnth in H0.
destruct (fin2nat j ??< fin2nat i).
- specialize (H0 (fSuccRange j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. rewrite !vnth_vmap2. f_equal. unfold mcol.
rewrite !vnth_vmap. erewrite vnth_vinsert_lt. fin.
- specialize (H0 (fSuccRangeS j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. rewrite !vnth_vmap2. f_equal. unfold mcol.
rewrite !vnth_vmap. erewrite vnth_vinsert_gt; fin.
Unshelve. all: fin.
Qed.
End lindep_extend.
若向量组线性相关,每个向量的相同位置去掉m个分量后的延伸组线性相关。
在每个向量头部都去掉数个元素后保持线性相关
Lemma ldep_shorten_head : forall {m n r} (vs : @vec (@vec tA (m + n)) r),
ldep vs -> ldep (vmap vtailN vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeAddL i)). rewrite vnth_vzero in *.
rewrite <- H0 at 2. rewrite !vnth_lcomb. apply vsum_eq; intros j.
rewrite !vnth_vmap2. f_equal.
Qed.
ldep vs -> ldep (vmap vtailN vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeAddL i)). rewrite vnth_vzero in *.
rewrite <- H0 at 2. rewrite !vnth_lcomb. apply vsum_eq; intros j.
rewrite !vnth_vmap2. f_equal.
Qed.
在每个向量尾部都去掉数个元素后保持线性相关
Lemma ldep_shorten_tail : forall {m n r} (vs : @vec (@vec tA (m + n)) r),
ldep vs -> ldep (vmap vheadN vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeR i)). rewrite vnth_vzero in *.
rewrite <- H0 at 2. rewrite !vnth_lcomb. apply vsum_eq; intros j.
rewrite !vnth_vmap2. f_equal.
Qed.
ldep vs -> ldep (vmap vheadN vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; auto.
rewrite veq_iff_vnth. rewrite veq_iff_vnth in H0. intros.
specialize (H0 (fin2AddRangeR i)). rewrite vnth_vzero in *.
rewrite <- H0 at 2. rewrite !vnth_lcomb. apply vsum_eq; intros j.
rewrite !vnth_vmap2. f_equal.
Qed.
对每个向量都删除1个元素后保持线性相关
Lemma ldep_shorten_delete :
forall {n r} (vs : @vec (@vec tA (S n)) r) (i : fin (S n)) (a : tA),
ldep vs -> ldep (vmap (fun v => vremove v i) vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; intros; auto.
rewrite veq_iff_vnth. intros j. rewrite veq_iff_vnth in H0.
destruct (fin2nat j ??< fin2nat i).
- specialize (H0 (fSuccRange j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. f_equal. apply veq_iff_vnth; intros s.
rewrite !vnth_mcol. rewrite !vnth_vmap.
rewrite (@vnth_vremove_lt _ Azero); auto. erewrite nth_v2f. fin.
apply fin2nat_imply_nat2fin. fin.
- specialize (H0 (fSuccRangeS j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. f_equal. apply veq_iff_vnth; intros s.
rewrite !vnth_mcol. rewrite !vnth_vmap.
rewrite (@vnth_vremove_ge _ Azero); auto; try lia.
+ erewrite nth_v2f. f_equal. apply fin2nat_imply_nat2fin.
rewrite fin2nat_fSuccRangeS. auto.
+ apply fin2nat_lt.
Unshelve. pose proof (fin2nat_lt j). lia.
pose proof (fin2nat_lt j). lia.
Qed.
End ldep_shorten.
forall {n r} (vs : @vec (@vec tA (S n)) r) (i : fin (S n)) (a : tA),
ldep vs -> ldep (vmap (fun v => vremove v i) vs).
Proof.
intros. unfold ldep in *. destruct H as [cs [H H0]]. exists cs. split; intros; auto.
rewrite veq_iff_vnth. intros j. rewrite veq_iff_vnth in H0.
destruct (fin2nat j ??< fin2nat i).
- specialize (H0 (fSuccRange j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. f_equal. apply veq_iff_vnth; intros s.
rewrite !vnth_mcol. rewrite !vnth_vmap.
rewrite (@vnth_vremove_lt _ Azero); auto. erewrite nth_v2f. fin.
apply fin2nat_imply_nat2fin. fin.
- specialize (H0 (fSuccRangeS j)).
rewrite vnth_vzero in *. rewrite <- H0 at 2. rewrite !vnth_lcomb.
apply vsum_eq; intros k. f_equal. apply veq_iff_vnth; intros s.
rewrite !vnth_mcol. rewrite !vnth_vmap.
rewrite (@vnth_vremove_ge _ Azero); auto; try lia.
+ erewrite nth_v2f. f_equal. apply fin2nat_imply_nat2fin.
rewrite fin2nat_fSuccRangeS. auto.
+ apply fin2nat_lt.
Unshelve. pose proof (fin2nat_lt j). lia.
pose proof (fin2nat_lt j). lia.
Qed.
End ldep_shorten.
F^n中的s个向量中的每一个都在这个向量组张成的线性空间中。
即,vi ∈ <v1,v2,...,vs>, 1<=i<=s, vi∈F^n
Lemma in_lspan : forall {n s} (vs : @vec (@vec tA n) s) i,
Hbelong (ss := lspan_Struct vs) (vs i).
Proof. intros. hnf. apply lrep_in. Qed.
Hbelong (ss := lspan_Struct vs) (vs i).
Proof. intros. hnf. apply lrep_in. Qed.
在F^n中,任意向量都能由n个线性无关的向量来线性表示
Lemma lindep_imply_lrep_any : forall {n} (vs : @vec (@vec tA n) n) (u : @vec tA n),
lindep vs -> lrep vs u.
Proof.
intros.
pose proof (in_lspan vs). unfold Hbelong in H0.
rewrite lindep_iff_coef0 in H.
unfold lindep,ldep in H. unfold lrep.
Admitted.
lindep vs -> lrep vs u.
Proof.
intros.
pose proof (in_lspan vs). unfold Hbelong in H0.
rewrite lindep_iff_coef0 in H.
unfold lindep,ldep in H. unfold lrep.
Admitted.
在F^n中,任意n+1个向量都线性相关
Lemma ldep_Sn : forall {n} (vs : @vec (@vec tA n) (S n)), ldep vs.
Proof.
intros.
rewrite <- vconsT_vremoveT_vtail.
assert ({ldep (vremoveT vs)} + {~ (ldep (vremoveT vs))}).
admit.
destruct H.
- apply ldep_imply_vconsT_ldep. auto.
-
Admitted.
Section veyes.
Context {n : nat}.
Notation veyes := (veyes 0 1).
Proof.
intros.
rewrite <- vconsT_vremoveT_vtail.
assert ({ldep (vremoveT vs)} + {~ (ldep (vremoveT vs))}).
admit.
destruct H.
- apply ldep_imply_vconsT_ldep. auto.
-
Admitted.
Section veyes.
Context {n : nat}.
Notation veyes := (veyes 0 1).
任意向量都能写成自然基的线性组合: v * eyes = v
Lemma lcomb_veyes : forall v : vec n, lcomb v (veyes n) = v.
Proof.
intros. unfold lcomb. apply veq_iff_vnth. intros.
rewrite vnth_vsum.
apply vsum_unique with (i:=i).
- rewrite vnth_vmap2. rewrite vnth_vscal. rewrite vnth_veyes_eq.
apply identityRight.
- intros. rewrite vnth_vmap2. rewrite vnth_vscal.
rewrite vnth_veyes_neq; auto. apply ring_mul_0_r.
Qed.
Proof.
intros. unfold lcomb. apply veq_iff_vnth. intros.
rewrite vnth_vsum.
apply vsum_unique with (i:=i).
- rewrite vnth_vmap2. rewrite vnth_vscal. rewrite vnth_veyes_eq.
apply identityRight.
- intros. rewrite vnth_vmap2. rewrite vnth_vscal.
rewrite vnth_veyes_neq; auto. apply ring_mul_0_r.
Qed.
自然基是线性无关的
Lemma lindep_veyes : lindep (veyes n).
Proof.
intros. unfold lindep, ldep. intro. destruct H as [v [H H0]]. destruct H.
rewrite lcomb_veyes in H0. auto.
Qed.
Proof.
intros. unfold lindep, ldep. intro. destruct H as [v [H H0]]. destruct H.
rewrite lcomb_veyes in H0. auto.
Qed.
任意向量 v 都可由自然基线性表示
Lemma lrep_veyes : forall (v : vec n), lrep (veyes n) v.
Proof. intros. unfold lrep. exists v. apply lcomb_veyes. Qed.
Proof. intros. unfold lrep. exists v. apply lcomb_veyes. Qed.
任意向量 v,用自然基线性表示的方式唯一