Library Algebra.Finite_dim.matrix
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Basic support for matrices on a ring.
Finite tables on a ring are called matrices.
Results needing a commutative Ring are only stated for the ring of real
numbers R_Ring.
Let K : Ring.
Let A : 'K^{m,n} and B : 'K^{n,p}.
Let A : 'K^{m,n}, u : 'K^m and v : 'K^n.
This module may be used through the import of
Algebra.Finite_dim.Finite_dim_MS, Algebra.Finite_dim.Finite_dim,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Definitions and notation
- mx_mult A B is the (m,p)-table where item (i,j) is the dot product of i-th row of A and j-th column of B;
- notation A ** B is for mx_mult A B.
- vecmat u A is the (unique) row of row1T u ** A;
- matvec A v is the (unique) column of A ** col1T v;
- mx_one is the identity matrix;
- notation II is for mx_one.
- Mx_R n is an alias for 'R^[n];
- mx_Ring is the type Mx_R n endowed with the Ring structure, ie the ring of square matrices on R. Of course, it is distinct from the fct_Ring 'R_Ring^[n] in which the multiplication is component-wise; hence the necessity for the type alias.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets.
From Algebra Require Import Hierarchy_compl Monoid Ring ModuleSpace.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section Matrix_Def.
Context {K : Ring}.
Definition mx_mult {m n p} (A : 'K^{m,n}) (B : 'K^{n,p}) : 'K^{m,p} :=
fun i j ⇒ row A i ⋅ col B j.
Definition vecmat {m n} (u : 'K^m) (A : 'K^{m,n}) : 'K^n :=
row (mx_mult (row1T u) A) ord0.
Definition matvec {m n} (A : 'K^{m,n}) (u : 'K^n) : 'K^m :=
col (mx_mult A (col1T u)) ord0.
Definition mx_one {n} : 'K^[n] := kron K.
End Matrix_Def.
Notation "A ** B" := (mx_mult A B) (at level 50) : Ring_scope.
Notation II := mx_one.
Section Matrix_Facts.
Context {K : Ring}.
Lemma mx_mult_correct :
∀ {m n p} (A : 'K^{m,n}) (B : 'K^{n,p}),
A ** B = fun i j ⇒ sum (fun k ⇒ A i k × B k j).
Proof. easy. Qed.
Lemma mx_mult_eq :
∀ {m n p} (A : 'K^{m,n}) (B : 'K^{n,p}) i j,
(A ** B) i j = lin_comb (A i) (flipT B j).
Proof. easy. Qed.
Lemma mx_mult_concatTr_l :
∀ {m1 m2 n p} (A1 : 'K^{m1,n}) (A2 : 'K^{m2,n}) (B : 'K^{n,p}),
concatTr A1 A2 ** B = concatTr (A1 ** B) (A2 ** B).
Proof.
intros m1 m2 n p A1 A2 B; apply extT; intros i j.
unfold mx_mult, dot_product, row, col; destruct (lt_dec i m1) as [Hi | Hi].
rewrite 2!(concatTr_correct_u _ _ Hi); easy.
rewrite 2!(concatTr_correct_d _ _ Hi); easy.
Qed.
Lemma mx_mult_concatTc_r :
∀ {m n p1 p2} (A : 'K^{m,n}) (B1 : 'K^{n,p1}) (B2 : 'K^{n,p2}),
A ** concatTc B1 B2 = concatTc (A ** B1) (A ** B2).
Proof.
intros m n p1 p2 A B1 B2; apply extT; intros i j.
unfold mx_mult, dot_product, row, col; destruct (lt_dec j p1) as [Hj | Hj].
rewrite (concatTc_correct_l _ _ _ Hj); f_equal; apply extF; intro.
apply (concatTc_correct_l _ _ _ Hj).
rewrite (concatTc_correct_r _ _ _ Hj); f_equal; apply extF; intro.
apply (concatTc_correct_r _ _ _ Hj).
Qed.
Lemma mx_mult_concatTrc :
∀ {m1 m2 n p1 p2} (A1 : 'K^{m1,n}) (A2 : 'K^{m2,n})
(B1 : 'K^{n,p1}) (B2 : 'K^{n,p2}),
concatTr A1 A2 ** concatTc B1 B2 =
concatT (A1 ** B1) (A1 ** B2) (A2 ** B1) (A2 ** B2).
Proof. intros; rewrite mx_mult_concatTr_l 2!mx_mult_concatTc_r; easy. Qed.
Lemma mx_mult_concatTcr :
∀ {m n1 n2 p} (A1 : 'K^{m,n1}) (A2 : 'K^{m,n2})
(B1 : 'K^{n1,p}) (B2 : 'K^{n2,p}),
concatTc A1 A2 ** concatTr B1 B2 = (A1 ** B1) + (A2 ** B2).
Proof.
intros; apply extT; move=>>;
rewrite mx_mult_eq lc_splitF_r -concatTc_flipT.
unfold concatTc; rewrite firstF_concatF lastF_concatF; easy.
Qed.
Lemma mx_mult_concatTr_r :
∀ {m n1 n2 p} (A : 'K^{m,n1 + n2}) (B1 : 'K^{n1,p}) (B2 : 'K^{n2,p}),
A ** concatTr B1 B2 = (leftT A ** B1) + (rightT A ** B2).
Proof.
intros; rewrite {1}(concatTc_splitTc A); apply mx_mult_concatTcr.
Qed.
Lemma mx_mult_concatTc_l :
∀ {m n1 n2 p} (A1 : 'K^{m,n1}) (A2 : 'K^{m,n2}) (B : 'K^{n1 + n2,p}),
concatTc A1 A2 ** B = (A1 ** upT B) + (A2 ** downT B).
Proof.
intros; rewrite {1}(concatTr_splitTr B); apply mx_mult_concatTcr.
Qed.
Lemma mx_mult_assoc :
∀ {m n p q} (A : 'K^{m,n}) (B : 'K^{n,p}) (C : 'K^{p,q}),
A ** (B ** C) = (A ** B) ** C.
Proof. intros; apply extT; move=>>; apply lc2_l_alt; easy. Qed.
Lemma mx_mult_one_r : ∀ {m n} (A : 'K^{m,n}), A ** II = A.
Proof.
intros m n A; apply extT; intros i j; unfold mx_mult, row.
rewrite -{2}(lc_kron_r (A i)) fct_lc_r_eq; easy.
Qed.
Lemma mx_mult_one_l : ∀ {m n} (A : 'K^{m,n}), II ** A = A.
Proof.
intros; apply extT; move=>>; unfold mx_mult, dot_product, row.
rewrite lc_kron_l_in_r; easy.
Qed.
Lemma mx_mult_distr_r :
∀ {m n p} (A B : 'K^{m,n}) (C : 'K^{n,p}),
(A + B) ** C = (A ** C) + (B ** C).
Proof. intros; apply extT; move=>>; apply dot_product_plus_l. Qed.
Lemma mx_one_sym : ∀ {n}, flipT (@II K n) = II.
Proof. intros; apply extT; intros i j; apply kron_sym. Qed.
End Matrix_Facts.
Section Matrix_R_Facts.
Lemma mx_mult_flipT :
∀ {m n p} (A : 'R^{n,m}) (B : 'R^{p,n}),
flipT A ** flipT B = flipT (B ** A).
Proof. intros; apply extT; move=>>; apply dot_product_comm. Qed.
Lemma mx_mult_distr_l :
∀ {m n p} (A : 'R^{m,n}) (B C : 'R^{n,p}),
A ** (B + C) = (A ** B) + (A ** C).
Proof. intros; apply extT; move=>>; apply dot_product_plus_r. Qed.
Definition mx_Ring_mixin {n} :=
Ring.Mixin _ _ (@II _ n)
mx_mult_assoc mx_mult_one_r mx_mult_one_l mx_mult_distr_r mx_mult_distr_l.
Definition Mx_R n := 'R^[n].
Canonical Structure mx_Ring {n} :=
Ring.Pack (Mx_R n) (Ring.Class _ _ mx_Ring_mixin) (Mx_R n).
End Matrix_R_Facts.