Module mathcomp.analysis.forms

From mathcomp
Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
From mathcomp
Require Import matrix mxalgebra vector falgebra ssrnum algC algnum.
From mathcomp
Require Import fieldext.
From mathcomp Require Import vector.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.

Reserved Notation "'[ u , v ]"
  (at level 2, format "'[hv' ''[' u , '/ '  v ] ']'").
Reserved Notation "'[ u , v ]_ M"
         (at level 2, format "'[hv' ''[' u , '/ '  v ]_ M ']'").
Reserved Notation "'[ u ]_ M" (at level 2, format "''[' u ]_ M").
Reserved Notation "'[ u ]" (at level 2, format "''[' u ]").
Reserved Notation "u '``_' i"
    (at level 3, i at level 2, left associativity, format "u '``_' i").
Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").

Notation "u '``_' i" := (u (GRing.zero (Zp_zmodType O)) i) : ring_scope.
Notation "''e_' i" := (delta_mx 0 i)
 (format "''e_' i", at level 3) : ring_scope.

Local Notation "M ^ phi" := (map_mx phi M).
Local Notation "M ^t phi" := (map_mx phi (M ^T)) (phi at level 30, at level 30).

Structure revop X Y Z ( f : Y -> X -> Z) := RevOp {
   fun_of_revop :> X -> Y -> Z;
  _ : forall x, f x =1 fun_of_revop^~ x
}.

Lemma eq_map_mx_id ( R : ringType) m n ( M : 'M[R]_(m,n)) ( f : R -> R) :
  f =1 id -> M ^ f = M.

Module Bilinear .

Section ClassDef .

Variables ( R : ringType) ( U U' : lmodType R) ( V : zmodType) ( s s' : R -> V -> V).
Implicit Type phUU'V : phant (U -> U' -> V).

Local Coercion GRing.Scale.op : GRing.Scale.law >-> Funclass.
Definition axiom ( f : U -> U' -> V) ( s_law : GRing.Scale.law s) ( eqs : s = s_law)
                                    ( s'_law : GRing.Scale.law s') ( eqs' : s' = s'_law) :=
  ((forall u', GRing.Linear.axiom (f^~ u') eqs)
  * (forall u, GRing.Linear.axiom (f u) eqs'))%type.

Record class_of ( f : U -> U' -> V) : Prop := Class {
   basel : forall u', GRing.Linear.class_of s (f^~ u');
   baser : forall u, GRing.Linear.class_of s' (f u)
}.

Lemma class_of_axiom f s_law s'_law Ds Ds' :
   @axiom f s_law Ds s'_law Ds' -> class_of f.

Structure map phUU'V := Pack {apply; _ : class_of apply}.
Local Coercion apply : map >-> Funclass.

Definition class ( phUU'V : _) ( cF : map phUU'V) :=
   let: Pack _ c as cF' := cF return class_of cF' in c.

Canonical additiver phU'V phUU'V ( u : U) cF := GRing.Additive.Pack phU'V
  (baser (@class phUU'V cF) u).
Canonical linearr phU'V phUU'V ( u : U) cF := GRing.Linear.Pack phU'V
  (baser (@class phUU'V cF) u).

Definition applyr_head t ( f : U -> U' -> V) u v := let: tt := t in f v u.
Notation applyr := (@applyr_head tt).

Canonical additivel phUV phUU'V ( u' : U') ( cF : map _) :=
  @GRing.Additive.Pack _ _ phUV (applyr cF u') (basel (@class phUU'V cF) u').
Canonical linearl phUV phUU'V ( u' : U') ( cF : map _) :=
  @GRing.Linear.Pack _ _ _ _ phUV (applyr cF u') (basel (@class phUU'V cF) u').

Definition pack ( phUV : phant (U -> V)) ( phU'V : phant (U' -> V))
           ( revf : U' -> U -> V) ( rf : revop revf) f ( g : U -> U' -> V) of (g = fun_of_revop rf) :=
  fun ( bFl : U' -> GRing.Linear.map s phUV) flc of (forall u', revf u' = bFl u') &
      (forall u', phant_id (GRing.Linear.class (bFl u')) (flc u')) =>
  fun ( bFr : U -> GRing.Linear.map s' phU'V) frc of (forall u, g u = bFr u) &
      (forall u, phant_id (GRing.Linear.class (bFr u)) (frc u)) =>
  @Pack (Phant _) f (Class flc frc).



End ClassDef.

Module Exports .
Delimit Scope linear_ring_scope with linR.
Notation bilinear_for s s' f := (axiom f (erefl s) (erefl s')).
Notation bilinear f := (bilinear_for *:%R *:%R f).
Notation biscalar f := (bilinear_for *%R *%R f).
Notation bilmorphism_for s s' f := (class_of s s' f).
Notation bilmorphism f := (bilmorphism_for *:%R *:%R f).
Coercion class_of_axiom : axiom >-> bilmorphism_for.
Coercion baser : bilmorphism_for >-> Funclass.
Coercion apply : map >-> Funclass.
Notation "{ 'bilinear' fUV | s & s' }" := (map s s' (Phant fUV))
  (at level 0, format "{ 'bilinear'  fUV  |  s  &  s' }") : ring_scope.
Notation "{ 'bilinear' fUV | s }" := (map s.1 s.2 (Phant fUV))
  (at level 0, format "{ 'bilinear'  fUV  |  s }") : ring_scope.
Notation "{ 'bilinear' fUV }" := {bilinear fUV | *:%R & *:%R}
  (at level 0, format "{ 'bilinear'  fUV }") : ring_scope.
Notation "{ 'biscalar' U }" := {bilinear U -> U -> _ | *%R & *%R}
  (at level 0, format "{ 'biscalar'  U }") : ring_scope.
Notation "[ 'bilinear' 'of' f 'as' g ]" :=
  (@pack _ _ _ _ _ _ _ _ _ _ f g erefl _ _
         (fun=> erefl) (fun=> idfun) _ _ (fun=> erefl) (fun=> idfun)).
Notation "[ 'bilinear' 'of' f ]" := [bilinear of f as f]
  (at level 0, format "[ 'bilinear'  'of'  f ]") : form_scope.
Coercion additiver : map >-> GRing.Additive.map.
Coercion linearr : map >-> GRing.Linear.map.
Canonical additiver.
Canonical linearr.
Canonical additivel.
Canonical linearl.
Notation applyr := (@applyr_head _ _ _ _ tt).
End Exports.

End Bilinear.
Include Bilinear.Exports.

Section BilinearTheory .

Variable R : ringType.

Section GenericProperties .

Variables ( U U' : lmodType R) ( V : zmodType) ( s : R -> V -> V) ( s' : R -> V -> V).
Variable f : {bilinear U -> U' -> V | s & s'}.

Lemma linear0r z : f z 0 = 0
Lemma linearNr z : {morph f z : x / - x}
Lemma linearDr z : {morph f z : x y / x + y}
Lemma linearBr z : {morph f z : x y / x - y}
Lemma linearMnr z n : {morph f z : x / x *+ n}
Lemma linearMNnr z n : {morph f z : x / x *- n}
Lemma linear_sumr z I r ( P : pred I) E :
  f z (\sum_( i <- r | P i) E i) = \sum_( i <- r | P i) f z (E i).

Lemma linearZr_LR z : scalable_for s' (f z)
Lemma linearPr z a : {morph f z : u v / a *: u + v >-> s' a u + v}.

Lemma applyrE x : applyr f x =1 f^~ x

Lemma linear0l z : f 0 z = 0
Lemma linearNl z : {morph f^~ z : x / - x}.
Lemma linearDl z : {morph f^~ z : x y / x + y}.
Lemma linearBl z : {morph f^~ z : x y / x - y}.
Lemma linearMnl z n : {morph f^~ z : x / x *+ n}.
Lemma linearMNnl z n : {morph f^~ z : x / x *- n}.
Lemma linear_suml z I r ( P : pred I) E :
  f (\sum_( i <- r | P i) E i) z = \sum_( i <- r | P i) f (E i) z.

Lemma linearZl_LR z : scalable_for s (f^~ z).
Lemma linearPl z a : {morph f^~ z : u v / a *: u + v >-> s a u + v}.

End GenericProperties.

Section BidirectionalLinearZ .

Variables ( U : lmodType R) ( V : zmodType) ( s : R -> V -> V).
Variables ( S : ringType) ( h : S -> V -> V) ( h_law : GRing.Scale.law h).


End BidirectionalLinearZ.

End BilinearTheory.

Canonical rev_mulmx ( R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
  (@mulmx R m n p) (fun _ _ => erefl).

Canonical mulmx_bilinear ( R : comRingType) m n p := [bilinear of @mulmx R m n p].





Section BilinearForms .

Variables ( R : fieldType) ( theta : {rmorphism R -> R}).
Variables ( n : nat) ( M : 'M[R]_n).
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).

Definition form u v := (u *m M *m (v ^t theta)) 0 0.

Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.

Lemma form0l u : '[0, u] = 0.

Lemma form0r u : '[u, 0] = 0.

Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w].

Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w].

Lemma formZr a u v : '[u, a *: v] = theta a * '[u, v].

Lemma formZl a u v : '[a *: u, v] = a * '[u, v].

Lemma formNl u v : '[- u, v] = - '[u, v].

Lemma formNr u v : '[u, - v] = - '[u, v].

Lemma formee i j : '['e_i, 'e_j] = M i j.

Lemma form0_eq0 : M = 0 -> forall u v, '[u, v] = 0.

End BilinearForms.

Section Sesquilinear .

Variable R : fieldType.
Variable n : nat.
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).

Section Def .
Variable eps_theta : (bool * {rmorphism R -> R}).

Definition sesqui :=
  [qualify M : 'M_n | M == ((-1) ^+ eps_theta.1) *: M ^t eps_theta.2].
Fact sesqui_key : pred_key sesqui
Canonical sesqui_keyed := KeyedQualifier sesqui_key.
End Def.

Local Notation "eps_theta .-sesqui" := (sesqui eps_theta).

Variables ( eps : bool) ( theta : {rmorphism R -> R}).
Variables ( M : 'M[R]_n).
Local Notation "''[' u , v ]" := (form theta M u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.

Lemma sesquiE : (M \is (eps,theta).-sesqui) = (M == (-1) ^+ eps *: M ^t theta).

Lemma sesquiP : reflect (M = (-1) ^+ eps *: M ^t theta)
                        (M \is (eps,theta).-sesqui).

Hypothesis ( thetaK : involutive theta).
Hypothesis ( M_sesqui : M \is (eps, theta).-sesqui).

Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta.

Lemma maptrmx_sesqui : M^t theta = (-1) ^+ eps *: M.

Lemma formC u v : '[u, v] = (-1) ^+ eps * theta '[v, u].

Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).

Definition ortho m ( B : 'M_(m,n)) := (kermx (M *m (B ^t theta))).
Local Notation "B ^_|_" := (ortho B) : ring_scope.
Local Notation "A _|_ B" := (A%MS <= B^_|_)%MS : ring_scope.

Lemma normalE u v : (u _|_ v) = ('[u, v] == 0).

Lemma form_eq0P {u v} : reflect ('[u, v] = 0) (u _|_ v).

Lemma normalP p q ( A : 'M_(p, n)) ( B :'M_(q, n)) :
  reflect (forall ( u v : 'rV_n), (u <= A)%MS -> (v <= B)%MS -> u _|_ v)
          (A _|_ B).

Lemma normalC p q ( A : 'M_(p, n)) ( B :'M_(q, n)) : (A _|_ B) = (B _|_ A).

Lemma normal_ortho_mx p ( A : 'M_(p, n)) : ((A^_|_) _|_ A).

Lemma normal_mx_ortho p ( A : 'M_(p, n)) : (A _|_ (A^_|_)).

Lemma rank_normal u : (\rank (u ^_|_) >= n.-1)%N.

Definition rad := 1%:M^_|_.

Lemma rad_ker : rad = kermx M.

Theorem formDd u v : u _|_ v -> '[u + v] = '[u] + '[v].

Lemma formZ a u : '[a *: u]= (a * theta a) * '[u].

Lemma formN u : '[- u] = '[u].

Lemma form_sign m u : '[(-1) ^+ m *: u] = '[u].

Lemma formD u v : let d := '[u, v] in
  '[u + v] = '[u] + '[v] + (d + (-1) ^+ eps * theta d).

Lemma formB u v : let d := '[u, v] in
  '[u - v] = '[u] + '[v] - (d + (-1) ^+ eps * theta d).

Lemma formBd u v : u _|_ v -> '[u - v] = '[u] + '[v].







End Sesquilinear.

Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope.

Notation symmetric_form := (false, [rmorphism of idfun]).-sesqui.
Notation skew := (true, [rmorphism of idfun]).-sesqui.
Notation hermitian := (false, @conjC _).-sesqui.