Library mxstructure
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import ssralg fintype perm poly mxpoly finfun tuple.
Require Import matrix bigop zmodp polydiv.
Require Import ssrcomplements.
Require Import ssralg fintype perm poly mxpoly finfun tuple.
Require Import matrix bigop zmodp polydiv.
Require Import ssrcomplements.
This file contains three parts about different structures of matrices.
Lower and upper triangular matrices :
upper_triangular_mx M == The BOOLEAN predicate that hold if M is an upper traiangular matrix. lower_triangular_mx M == The same as upper_trianglar_mx but for lower triangular matrices. is_triangular_mx M == M is upper or lower triangular matrix.Block diagonal matrices :
diag_block_mx s F == A block diagonal matrix where the ith block is F (nth 0 s i) i. F n i is a square matrix of dimension n.+1, and s is the sequence of dimension of each block minus 1. It is defined by calling recursivly the function block_mx. (size_sum s).+1 == It is the type of the matrix diag_block_mx s F.Diagonal matrices :
diag_mx_seq m n s == A diagonal matrix of type 'M_(m,n) where the ith diagonal coefficient is the ith element of s.Set Implicit Arguments.
Triangular Matrices
Section Triangular.
Local Open Scope ring_scope.
Variable R : ringType.
Definition upper_part_mx m n (M : 'M[R]_(m,n)) :=
\matrix_(i, j) (M i j *+ (i <= j)).
Definition lower_part_mx m n (M : 'M[R]_(m,n)) :=
\matrix_(i, j) (M i j *+ (j <= i)).
Definition upper_triangular_mx m n (M : 'M[R]_(m,n)) := M == upper_part_mx M.
Lemma upper_triangular_mxP m n {M : 'M_(m,n)} :
reflect (forall (i : 'I_m) (j : 'I_n), j < i -> M i j = 0)
(upper_triangular_mx M).
Definition lower_triangular_mx m n (M : 'M[R]_(m,n)) := M == lower_part_mx M.
Definition is_triangular_mx m n (M : 'M[R]_(m,n)) :=
upper_triangular_mx M || lower_triangular_mx M.
Lemma upper_triangular_mx0 m n : upper_triangular_mx (0 : 'M[R]_(m,n)).
Lemma lower_triangular_mxP m n (M : 'M[R]_(m,n)) :
lower_triangular_mx M <-> upper_triangular_mx M^T.
End Triangular.
Section TriangularBlock.
Local Open Scope ring_scope.
Variable R : ringType.
Variables m1 m2 n1 n2 : nat.
Variables (Aul : 'M[R]_(m1, n1)) (Aur : 'M[R]_(m1, n2)).
Variables (Adl : 'M[R]_(m2, n1)) (Adr : 'M[R]_(m2, n2)).
Lemma upper_triangular_block_mxdl :
n1 <= m1 -> upper_triangular_mx (block_mx Aul Aur Adl Adr) -> Adl = 0.
Lemma upper_triangular_block_mxdr :
n1 <= m1 -> upper_triangular_mx (block_mx Aul Aur Adl Adr) ->
upper_triangular_mx Adr.
Lemma upper_triangular_block : m1 <= n1 -> upper_triangular_mx Aul ->
upper_triangular_mx Adr -> upper_triangular_mx (block_mx Aul 0 0 Adr).
End TriangularBlock.
Section SquareTriangular.
Local Open Scope ring_scope.
Variable R : comRingType.
Lemma det_triangular_mx : forall n (M : 'M[R]_n),
upper_triangular_mx M -> \det M = \prod_i M i i.
Lemma char_poly_mx_triangular_mx n (M : 'M[R]_n) :
upper_triangular_mx M -> upper_triangular_mx (char_poly_mx M).
Lemma row'_col'_triangular_mx n (M : 'M[R]_n) i:
upper_triangular_mx M -> upper_triangular_mx (row' i (col' i M)).
End SquareTriangular.
Section SquareTriangular2.
Local Open Scope ring_scope.
Variable R : comRingType.
Lemma char_poly_triangular_mx n (M : 'M[R]_n) :
upper_triangular_mx M -> char_poly M = \prod_i ('X - (M i i)%:P).
End SquareTriangular2.
Block Diagonal Matrices
Section diag_block_ringType.
Variable R : ringType.
Local Open Scope ring_scope.
Import GRing.Theory.
Fixpoint size_sum_rec k (s : seq nat) : nat :=
if s is x :: l then (k + (size_sum_rec x l).+1)%N else k.
Fixpoint diag_block_mx_rec k (s : seq nat)
(F : (forall n, nat -> 'M[R]_n.+1)) :=
if s is x :: l return 'M_((size_sum_rec k s).+1)
then block_mx (F k 0%N) 0 0 (diag_block_mx_rec x l (fun n i => F n i.+1))
else F k 0%N.
Definition size_sum s := if s is x :: l then size_sum_rec x l else 0%N.
Definition diag_block_mx s F :=
if s is x :: l return 'M_((size_sum s).+1)
then diag_block_mx_rec x l F else 0.
Lemma size_sum_big_cons : forall s x,
(size_sum (x :: s)).+1 = (\sum_(k <- x :: s) k.+1)%N.
Lemma size_sum_big s : s != [::] ->
(size_sum s).+1 = (\sum_(k <- s) k.+1)%N.
Lemma ext_block s (F1 F2 : forall n, nat -> 'M_n.+1) :
(forall i, i < size s ->
(F1 (nth 0%N s i) i) = (F2 (nth 0%N s i) i)) ->
diag_block_mx s F1 = diag_block_mx s F2.
Lemma upper_triangular_diag_block (s : seq nat)
(F : (forall n, nat -> 'M[R]_n.+1)) :
(forall j, upper_triangular_mx (F (nth 0%N s j) j)) ->
upper_triangular_mx (diag_block_mx s F).
Lemma scalar_diag_block_mx c s (F : forall n, nat -> 'M_n.+1) :
s != [::] -> (forall i, i < size s -> F (nth 0%N s i) i = c%:M ) ->
diag_block_mx s F = c%:M.
Lemma diag_block_mx0 s (F : forall n, nat -> 'M_n.+1) :
(forall i, i < size s -> F (nth 0%N s i) i = 0) <->
diag_block_mx s F = 0.
Lemma add_diag_block s F1 F2 :
diag_block_mx s F1 + diag_block_mx s F2 =
diag_block_mx s (fun n i => F1 n i + F2 n i).
Lemma mulmx_diag_block s F1 F2 :
diag_block_mx s F1 *m diag_block_mx s F2 =
diag_block_mx s (fun n i => F1 n i *m F2 n i).
Lemma exp_diag_block_S s F k :
(diag_block_mx s F)^+ k.+1 = diag_block_mx s (fun n i => (F n i)^+ k.+1).
Lemma exp_diag_block_cons s F k : s != [::] ->
(diag_block_mx s F)^+ k = diag_block_mx s (fun n i => (F n i)^+ k).
Lemma tr_diag_block_mx s F :
(diag_block_mx s F)^T = diag_block_mx s (fun n i => (F n i)^T).
End diag_block_ringType.
Section diag_block_ringType2.
Variable R : ringType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma char_diag_block_mx s (F : forall n, nat -> 'M[R]_n.+1) :
s != [::] -> char_poly_mx (diag_block_mx s F) =
diag_block_mx s (fun n i => char_poly_mx (F n i)).
End diag_block_ringType2.
Section diag_block_comRingType.
Variable R : comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma det_diag_block s (F : forall n, nat -> 'M[R]_n.+1) :
s != [::] ->
\det (diag_block_mx s F) =
\prod_(i < size s) \det (F (nth 0%N s i) i).
Lemma horner_mx_diag_block (p : {poly R}) s F :
s != [::] ->
horner_mx (diag_block_mx s F) p =
diag_block_mx s (fun n i => horner_mx (F n i) p).
End diag_block_comRingType.
Section diag_block_comUnitRingType.
Variable R : comUnitRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma unitmx_diag_block s (F : forall n, nat -> 'M[R]_n.+1) :
s != [::] ->
(forall i, i < size s -> (F (nth 0%N s i) i) \in unitmx) ->
(diag_block_mx s F) \in unitmx.
Lemma invmx_diag_block s (F : forall n, nat -> 'M[R]_n.+1) :
(diag_block_mx s F) \in unitmx ->
(diag_block_mx s F)^-1 = diag_block_mx s (fun n i => (F n i)^-1).
End diag_block_comUnitRingType.
Diagonal Matrices
Section diag_mx_seq.
Variable R : ringType.
Local Open Scope ring_scope.
Import GRing.Theory.
Definition diag_mx_seq m n (s : seq R) :=
\matrix_(i < m, j < n) (s`_i *+ (i == j :> nat)).
Lemma diag_mx_seq_nil m n : diag_mx_seq m n [::] = 0.
Lemma diag_mx_seq_cons m n x (s : seq R) :
diag_mx_seq (1 + m) (1 + n) (x :: s) =
block_mx x%:M 0 0 (diag_mx_seq m n s).
Lemma diag_mx_seq_cat m1 m2 n1 n2 (s1 s2 : seq R) :
size s1 = m1 -> size s1 = n1 ->
diag_mx_seq (m1 + m2) (n1 + n2) (s1 ++ s2) =
block_mx (diag_mx_seq m1 n1 s1) 0 0 (diag_mx_seq m2 n2 s2).
Lemma diag_mx_seq_block_mx m m' n n' s :
size s <= minn m n ->
diag_mx_seq (m + m') (n + n') s = block_mx (diag_mx_seq m n s) 0 0 0.
Lemma diag_mx_seq_block s :
let l := nseq (size s) 0%N in
let F := (fun n i => (@scalar_mx _ n.+1 s`_i)) in
diag_mx_seq (size_sum l).+1 (size_sum l).+1 s =
diag_block_mx l F.
Lemma diag_block_mx_seq s (F : forall n, nat -> 'M_n.+1) :
let n := size_sum s in
let l := mkseq (fun i => (F 0%N i) ord0 ord0) (size s) in
(forall i, nth 0%N s i = 0%N) ->
diag_block_mx s F =
diag_mx_seq n.+1 n.+1 l.
Lemma diag_mx_seq_deltal m n (i : 'I_m) (j : 'I_n) (s : seq R) :
delta_mx i j *m diag_mx_seq n n s = s`_j *: delta_mx i j.
Lemma diag_mx_seq_deltar m n (i : 'I_m) (j : 'I_n) (s : seq R) :
diag_mx_seq m m s *m delta_mx i j = s`_i *: delta_mx i j.
Lemma diag_mx_seq_takel m n (s : seq R) :
diag_mx_seq m n (take m s) = diag_mx_seq m n s.
Lemma diag_mx_seq_taker m n (s : seq R) :
diag_mx_seq m n (take n s) = diag_mx_seq m n s.
Lemma diag_mx_seq_take_min m n (s : seq R) :
diag_mx_seq m n (take (minn (minn m n) (size s)) s) = diag_mx_seq m n s.
Lemma tr_diag_mx_seq m n s : (diag_mx_seq m n s)^T = diag_mx_seq n m s.
Lemma mul_pid_mx_diag m n p r s :
r <= p ->
@pid_mx R m p r *m diag_mx_seq p n s = diag_mx_seq m n (take r s).
End diag_mx_seq.
Section diag_mx_seq2.
Variable R : ringType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma mul_diag_mx_pid m n p r s :
r <= p ->
diag_mx_seq m p s *m @pid_mx R p n r = diag_mx_seq m n (take r s).
Lemma mul_diag_mx_copid m n r s :
minn (minn m n) (size s) <= r ->
diag_mx_seq m n s *m @copid_mx R n r = 0.
End diag_mx_seq2.
Section diag_mx_seq_comRingType.
Variable R : comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma det_diag_mx_seq_truncated m (s : seq R) :
\det (diag_mx_seq m m s) = (\prod_(i <- take m s) i) *+ (m <= size s).
Lemma det_diag_mx_seq m (s : seq R) : size s = m ->
\det (diag_mx_seq m m s) = \prod_(i <- s) i.
End diag_mx_seq_comRingType.
Section diag_mx_idomain.
Variable R : idomainType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma mul_mx_diag_seq_min m r (s : seq R) (A : 'M_(m, r)) (B : 'M_(r, m)) :
all (predC1 0) s -> m <= size s ->
A *m B = diag_mx_seq _ _ s -> m <= r.
End diag_mx_idomain.
This page has been generated by coqdoc