Library mxorder

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
Require Import bigop ssralg zmodp matrix ssrnum complex.
Require Import big_minmax.

Here we define a partial order over matrices. A <m: B == forall i and j, A i j < B i j. A <=m: B == forall i and j, A i j <= B i j. Mabs A == the matrix where each coefficient is the absolute value (or module) of the corresponding coefficient of the atrix A.

Set Implicit Arguments.
Import Prenex Implicits.

Local Open Scope ring_scope.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Section matRDef.

Variable R : numDomainType.
Variable p q: nat.

Definitions for absolute value of a matrix and componentwise order

Definition Mabs (A: 'M [R ]_(p , q )) := map_mx normr A.

Definition Mle (A B: 'M [R ]_(p , q )) := forall i j, A i j <= B i j.

Definition Mlt (A B: 'M [R ]_(p , q )) := forall i j, A i j < B i j.

Definition one_M: matrix R p q := \matrix_(i, j) 1.

End matRDef.

Implicit Arguments one_M[p q].

Infix "<m:" := Mlt (at level 70): ring_scope.
Infix "<=m:" := Mle (at level 70): ring_scope.

Section matRProp.

Variable R : numDomainType.
Variable n p q: nat.

Open Scope ring_scope.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Lemma Mle_trans (A B C : 'M [R ]_(p , q )) : A <=m : B -> B <=m : C -> A <=m : C.

Lemma Mle_refl (A : 'M [R ]_(p , q )) : A <=m : A.

Lemma Mlt_trans (A B C : 'M [R ]_(p , q )) : A <m : B -> B <m : C -> A <m : C.

Lemma Mlt_le_trans (A B C : 'M [R ]_(p , q )) : A <m : B -> B <=m : C -> A <m : C.

Lemma MltW (A B : 'M [R ]_(p , q )) : A <m : B -> A <=m : B.

Lemma Mabs_eq0 (A : 'M [R ]_(p , q )) : ((Mabs A ) == 0) = (A == 0).

Lemma Mabs_ge0 (A : 'M [R ]_(p , q )) : 0 <=m : Mabs A.

Lemma Mabs_triang (A B : 'M [R ]_(p ,q )) : (Mabs (A + B)) <=m : (Mabs A + Mabs B ).

Lemma Mle_add:
forall (a b c d: 'M [R ]_(p ,q )), Mle a b -> Mle c d -> Mle (a + c) (b + d).

Lemma MabsM (M : 'M [R ]_(n , p )) (N :'M_(p , q )) :
  Mabs (M *m N) <=m : (Mabs M ) *m (Mabs N ).

Lemma Mabs_scalemx a (M : 'M [R ]_(n , p )) : Mabs (a *: M) = `|a | *: Mabs M.

Lemma eq_Mabs_id (M : 'M [R ]_(n , p )) : 0 <=m : M -> Mabs M = M.

Lemma subr_Mge0 (A B : 'M [R ]_(p ,q )) : B <=m : A <-> 0 <=m : (A - B ).

Lemma subr_Mgt (A B C : 'M [R ]_(p ,q )) : B + A <m : C <-> A <m : C - B.

Lemma mulmx_gt0 (A: 'M [R ]_(p ,q )) (x : 'cV_q) : 0 <m : A ->
   0 <=m : x -> x != 0 -> 0 <m : A *m x.

Lemma Mlt_scaler (A B : 'M [R ]_(p ,q )) a : 0 < a -> A <m : B -> a *: A <m : a *: B.

Lemma ltr_sum (I : eqType) (r : seq I) (P : pred I) (F G : I -> R) (i : I) :
(forall i, P i -> F i < G i) -> i \in r -> P i ->
\sum_(i <- r | P i ) F i < \sum_(i <- r | P i ) G i.

Lemma Mlt_pmul2r (A B : 'M [R ]_(n , p .+1 )) (C :'M_(p .+1 , q )) :
  0 <m : C -> A <m : B -> A *m C <m : B *m C.

Lemma Mlt_pmul2l (C : 'M [R ]_(n , p .+1 )) (A B :'M_(p .+1 , q )) :
  0 <m : C -> A <m : B -> C *m A <m : C *m B.

Lemma Mle_wpmul2l (C : 'M [R ]_(n , p )) (A B :'M_(p , q )) :
  0 <=m : C -> A <=m : B -> C *m A <=m : C *m B.

Lemma Mle_wpmul2r (C : 'M [R ]_(p , n )) (A B :'M_(q , p )) :
  0 <=m : C -> A <=m : B -> A *m C <=m : B *m C.

End matRProp.

Section matRProp2.
Variable R : rcfType.
Variable p q n : nat.

Lemma Mle_wpmul :
forall (a b: 'M [R ]_(q ,n )) (u v: 'M_(p , q )),
  u <=m : v -> a <=m : b -> Mle 0 a -> Mle 0 u -> u *m a <=m : v *m b.

Local Notation "A ^%:C" := (map_mx (real_complex_def (Phant R)) A) (at level 2).

Lemma Mabs_real_complex (A : 'M [R ]_(p ,q )) : Mabs A ^%:C = (Mabs A )^%:C.

Lemma mxreal_gt0 m (A : 'M [R ]_(m ,n )) : 0 <m : A <-> 0 <m : A ^%:C.

Lemma mxreal_ge0 m (A : 'M [R ]_(m ,n )) : 0 <=m : A <-> 0 <=m : A ^%:C.

End matRProp2.

Section theory.

Variable R : numFieldType.

Lemma Mle_eps m (u v : 'cV [R ]_m .+1) :
    let F i := ((u i 0) / 2%:R )/ (v i 0) in
    let eps := min_fT F in
    0 <m : u -> 0 <m : v -> eps *: v <m : u.

End theory.

This page has been generated by coqdoc