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.

Brief description

Basic support for matrices on a ring.

Description

Finite tables on a ring are called matrices.
Results needing a commutative Ring are only stated for the ring of real numbers R_Ring.

Definitions and notation

Let K : Ring. Let A : 'K^{m,n} and B : 'K^{n,p}.
  • 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.
Let A : 'K^{m,n}, u : 'K^m and v : 'K^n.
  • 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

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.

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 jrow 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 jsum (fun kA 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.