diff options
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 81 |
1 files changed, 61 insertions, 20 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 9a0034d..686da21 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -490,6 +490,17 @@ rewrite -{4}[B]mulmx_ebase -!mulmxA mulKmx //. by rewrite (mulmxA (pid_mx _)) pid_mx_id // !mulmxA -{}defA mulmxKV. Qed. +Lemma mulmxVp m n (A : 'M[F]_(m, n)) : row_free A -> A *m pinvmx A = 1%:M. +Proof. +move=> fA; rewrite -[X in X *m _]mulmx_ebase !mulmxA mulmxK ?row_ebase_unit//. +rewrite -[X in X *m _]mulmxA mul_pid_mx !minnn (minn_idPr _) ?rank_leq_col//. +by rewrite (eqP fA) pid_mx_1 mulmx1 mulmxV ?col_ebase_unit. +Qed. + +Lemma mulmxKp p m n (B : 'M[F]_(m, n)) : row_free B -> + cancel ((@mulmx _ p _ _)^~ B) (mulmx^~ (pinvmx B)). +Proof. by move=> ? A; rewrite -mulmxA mulmxVp ?mulmx1. Qed. + Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists D, A = D *m B) (A <= B)%MS. Proof. @@ -715,6 +726,21 @@ Proof. by rewrite /ltmx sub1mx submx1. Qed. Lemma lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false. Proof. by rewrite /ltmx submx1 andbF. Qed. +Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx -> pinvmx A = invmx A. +Proof. +move=> A_unit; apply: (@row_free_inj _ _ _ A); rewrite ?row_free_unit//. +by rewrite -[pinvmx _]mul1mx mulmxKpV ?sub1mx ?row_full_unit// mulVmx. +Qed. + +Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A -> pinvmx A *m A = 1%:M. +Proof. by move=> fA; rewrite -[pinvmx _]mul1mx mulmxKpV// sub1mx. Qed. + +Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A -> row_free (pinvmx A). +Proof. by move=> /mulVpmx pAA1; apply/row_freeP; exists A. Qed. + +Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A -> row_full (pinvmx A). +Proof. by move=> /mulmxVp ApA1; apply/row_fullP; exists A. Qed. + Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :=: B)%MS (A == B)%MS. Proof. @@ -805,6 +831,9 @@ exists (col_ebase A *m pid_mx (\rank A)). by rewrite mulmxA -(mulmxA _ _ (pid_mx _)) pid_mx_id // mulmx_ebase. Qed. +Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0. +Proof. by apply/eqmx0P; rewrite !eq_row_base !sub0mx. Qed. + Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M). Proof. by rewrite /qidmx eqxx pid_mx_1. Qed. @@ -1093,22 +1122,30 @@ Lemma eqmx_sums P n (A B : I -> 'M[F]_n) : (\sum_(i | P i) A i :=: \sum_(i | P i) B i)%MS. Proof. by move=> eqAB; apply/eqmxP; rewrite !sumsmxS // => i; move/eqAB->. Qed. -Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : - reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) - (A <= \sum_(i | P i) B_ i)%MS. +Lemma sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I -> 'M_(n, p)) : + reflect (exists u_ : I -> 'M_(m, n), A = \sum_(i | P i) u_ i *m B_ i) + (A <= \sum_(i | P i) <<B_ i>>)%MS. Proof. apply: (iffP idP) => [| [u_ ->]]; last first. - by apply: summx_sub_sums => i _; apply: submxMl. + by apply: summx_sub_sums => i _; rewrite genmxE; apply: submxMl. have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. -rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi /sub_addsmxP[u ->]. +rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi. +rewrite (adds_eqmx (genmxE _) (eqmx_refl _)) => /sub_addsmxP[u ->]. have [u_ ->] := IHi _ (submxMl u.2 _). -exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi) /= eqxx; congr (_ + _). +exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi)/= eqxx; congr (_ + _). by apply: eq_bigr => j /andP[_ /negPf->]. Qed. +Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : + reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) + (A <= \sum_(i | P i) B_ i)%MS. +Proof. +by rewrite -(eqmx_sums (fun _ _ => genmxE _)); apply/sub_sums_genmxP. +Qed. + Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) : ((\sum_(i | P i) A i)%MS *m B :=: \sum_(i | P i) <<A i *m B>>)%MS. Proof. @@ -1174,11 +1211,22 @@ apply: (iffP submxP) => [[D ->]|]; first by rewrite -mulmxA mulmx_ker mulmx0. by move/mulmxKV_ker; exists (B *m col_ebase A). Qed. +Lemma sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) : + (B <= kermx A)%MS = (B *m A == 0). +Proof. exact/sub_kermxP/eqP. Qed. + +Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS. +Proof. by apply/eqmxP; rewrite submx1/= sub_kermx mulmx0. Qed. + +Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : + row_free B -> (A *m B == 0) = (A == 0). +Proof. by rewrite -sub_kermx -kermx_eq0 => /eqP->; rewrite submx0. Qed. + Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : A *m B = 0 -> \rank A + \rank B <= n. Proof. move=> AB0; rewrite -{3}(subnK (rank_leq_row B)) leq_add2r. -by rewrite -mxrank_ker mxrankS //; apply/sub_kermxP. +by rewrite -mxrank_ker mxrankS // sub_kermx AB0. Qed. Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : @@ -1192,7 +1240,7 @@ set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker. rewrite -(mxrankMfree _ (row_base_free (A *m B))). have: (row_base (A *m B) <= row_base B)%MS by rewrite !eq_row_base submxMl. case/submxP=> D defD; rewrite defD mulmxA mxrankMfree ?mxrankS //. -by apply/sub_kermxP; rewrite -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. +by rewrite sub_kermx -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. Qed. Lemma mxrank_mul_min m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : @@ -1218,7 +1266,7 @@ apply/idP/andP=> [sAI | [/submxP[B' ->{A}] /submxP[C' eqBC']]]. rewrite -{1}[K]hsubmxK mul_row_col; move/(canRL (addrK _))->. by rewrite add0r -mulNmx submxMl. have: (row_mx B' (- C') <= kermx (col_mx B C))%MS. - by apply/sub_kermxP; rewrite mul_row_col eqBC' mulNmx subrr. + by rewrite sub_kermx mul_row_col eqBC' mulNmx subrr. case/submxP=> D; rewrite -[kermx _]hsubmxK mul_mx_row. by case/eq_row_mx=> -> _; rewrite -mulmxA submxMl. Qed. @@ -1450,11 +1498,9 @@ apply/eqP; set K := kermx B; set C := (A :&: K)%MS. rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B. rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l. rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup. - rewrite sub_capmx -(eq_row_base A) submxMl. - by apply/sub_kermxP; rewrite -mulmxA mulmx_ker. + by rewrite sub_capmx -(eq_row_base A) submxMl sub_kermx -mulmxA mulmx_ker/=. have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl. -rewrite defC submxMr //; apply/sub_kermxP. -by rewrite mulmxA -defC; apply/sub_kermxP; rewrite capmxSr. +by rewrite defC submxMr // sub_kermx mulmxA -defC -sub_kermx capmxSr. Qed. Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) : @@ -1936,10 +1982,7 @@ Definition eigenvalue : pred F := fun a => eigenspace a != 0. Lemma eigenspaceP a m (W : 'M_(m, n)) : reflect (W *m g = a *: W) (W <= eigenspace a)%MS. -Proof. -rewrite (sameP (sub_kermxP _ _) eqP). -by rewrite mulmxBr subr_eq0 mul_mx_scalar; apply: eqP. -Qed. +Proof. by rewrite sub_kermx mulmxBr subr_eq0 mul_mx_scalar; apply/eqP. Qed. Lemma eigenvalueP a : reflect (exists2 v : 'rV_n, v *m g = a *: v & v != 0) (eigenvalue a). @@ -2155,9 +2198,7 @@ rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first. rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0. rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0. by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r. -rewrite -sum_nat_const; apply: eq_bigr; rewrite /= -[n.+1]/(1 + n)%N => v nzv. -case: (pickP (fun i => v i 0 != 0)) => [k nza | v0]; last first. - by case/eqP: nzv; apply/colP=> i; move/eqP: (v0 i); rewrite mxE. +rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza]. have xrkK: involutive (@xrow F _ _ 0 k). by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1. rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N. |