Module mathcomp.analysis.forms
From HB Require Import structures.From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
From mathcomp Require Import matrix mxalgebra vector falgebra ssrnum fieldext.
From mathcomp Require Import vector mathcomp_extra.
Bilinear forms
(undocumented)
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, 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 (0 : 'I_1) 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).
Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) :
f =1 id -> M ^ f = M.
Proof.
HB.mixin Record isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : R -> V -> V) (s' : R -> V -> V) (f : U -> U' -> V) := {
additivel_subproof : forall u', additive (f^~ u');
additiver_subproof : forall u, additive (f u);
linearl_subproof : forall u', scalable_for s (f^~ u');
linearr_subproof : forall u, scalable_for s' (f u);
}.
HB.structure Definition Bilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : R -> V -> V) (s' : R -> V -> V) :=
{f of isBilinear R U U' V s s' f}.
Definition bilinear_for (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) :=
((forall u', GRing.linear_for (s : R -> V -> V) (f^~ u'))
* (forall u, GRing.linear_for s' (f u)))%type.
HB.factory Record bilinear_isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) := {
bilinear_subproof : bilinear_for s s' f;
}.
HB.builders Context R U U' V s s' f of bilinear_isBilinear R U U' V s s' f.
HB.instance Definition _ := isBilinear.Build R U U' V s s' f
(fun u' => additive_linear (bilinear_subproof.1 u'))
(fun u => additive_linear (bilinear_subproof.2 u))
(fun u' => scalable_linear (bilinear_subproof.1 u'))
(fun u => scalable_linear (bilinear_subproof.2 u)).
HB.end.
Module BilinearExports.
Notation bilinear f := (bilinear_for *:%R *:%R f).
Notation biscalar f := (bilinear_for *%R *%R f).
Module Bilinear.
Definition map (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : R -> V -> V) (s' : R -> V -> V)
(phUU'V : phant (U -> U' -> V)) := Bilinear.type U U' s s'.
End Bilinear.
Notation "{ 'bilinear' fUV | s & s' }" := (Bilinear.map s s' (Phant fUV))
(at level 0, format "{ 'bilinear' fUV | s & s' }") : ring_scope.
Notation "{ 'bilinear' fUV | s }" := (Bilinear.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 ]" := (Bilinear.clone _ _ _ _ _ _ f g)
(at level 0, format "[ 'bilinear' 'of' f 'as' g ]") : form_scope.
Notation "[ 'bilinear' 'of' f ]" := (Bilinear.clone _ _ _ _ _ _ f _)
(at level 0, format "[ 'bilinear' 'of' f ]") : form_scope.
End BilinearExports.
Export BilinearExports.
Section applyr.
Variables (R : ringType) (U U' : lmodType R) (V : zmodType) (s s' : R -> V -> V).
Definition applyr_head t (f : U -> U' -> V) u v := let: tt := t in f v u.
End applyr.
Notation applyr := (applyr_head tt).
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'}.
Section GenericPropertiesr.
Variable z : U.
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isAdditive.Build _ _ (f z) (@additiver_subproof _ _ _ _ _ _ f z).
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isScalable.Build _ _ _ _ (f z) (@linearr_subproof _ _ _ _ _ _ f z).
Lemma linear0r : f z 0 = 0. Proof. by rewrite raddf0.Lemma linearNr : {morph f z : x / - x}. Proof. exact: raddfN.Lemma linearDr : {morph f z : x y / x + y}. Proof. exact: raddfD.Lemma linearBr : {morph f z : x y / x - y}. Proof. exact: raddfB.Lemma linearMnr n : {morph f z : x / x *+ n}. Proof. exact: raddfMn.Lemma linearMNnr n : {morph f z : x / x *- n}. Proof. exact: raddfMNn.Lemma linear_sumr I r (P : pred I) E :
f z (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f z (E i).
Proof.
Lemma linearZr_LR : scalable_for s' (f z)
Proof.
Lemma linearPr a : {morph f z : u v / a *: u + v >-> s' a u + v}.Proof.
End GenericPropertiesr.
Lemma applyrE x : applyr f x =1 f^~ x. Proof. by [].
Section GenericPropertiesl.
Variable z : U'.
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isAdditive.Build _ _ (applyr f z) (@additivel_subproof _ _ _ _ _ _ f z).
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isScalable.Build _ _ _ _ (applyr f z) (@linearl_subproof _ _ _ _ _ _ f z).
Lemma linear0l : f 0 z = 0. Proof. by rewrite -applyrE raddf0.Lemma linearNl : {morph f^~ z : x / - x}.
Proof.
Lemma linearDl : {morph f^~ z : x y / x + y}.Proof.
Lemma linearBl : {morph f^~ z : x y / x - y}.Proof.
Lemma linearMnl n : {morph f^~ z : x / x *+ n}.Proof.
Lemma linearMNnl n : {morph f^~ z : x / x *- n}.Proof.
Lemma linear_suml I r (P : pred I) E :f (\sum_(i <- r | P i) E i) z = \sum_(i <- r | P i) f (E i) z.
Proof.
Lemma linearZl_LR : scalable_for s (f^~ z).
Proof.
Lemma linearPl a : {morph f^~ z : u v / a *: u + v >-> s a u + v}.Proof.
End GenericPropertiesl.
End GenericProperties.
Section BidirectionalLinearZ.
Variables (U : lmodType R) (V : zmodType) (s : R -> V -> V).
Variables (S : ringType) (h : GRing.Scale.law S V).
End BidirectionalLinearZ.
End BilinearTheory.
Lemma mulmx_is_bilinear (R : comRingType) m n p :
bilinear_for
(GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)
(@mulmx R m n p).
Proof.
HB.instance Definition _ (R : comRingType) m n p :=
bilinear_isBilinear.Build R
[the lmodType R of 'M[R]_(m, n)] [the lmodType R of 'M[R]_(n, p)]
[the zmodType of 'M[R]_(m, p)] _ _ (@mulmx R m n p)
(mulmx_is_bilinear 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.
Proof.
Lemma form0r u : '[u, 0] = 0.
Proof.
Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w].
Proof.
Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w].
Proof.
Lemma formZr a u v : '[u, a *: v] = theta a * '[u, v].
Proof.
Lemma formZl a u v : '[a *: u, v] = a * '[u, v].
Proof.
Lemma formNl u v : '[- u, v] = - '[u, v].
Proof.
Lemma formNr u v : '[u, - v] = - '[u, v].
Proof.
Lemma formee i j : '['e_i, 'e_j] = M i j.
Proof.
Lemma form0_eq0 : M = 0 -> forall u v, '[u, v] = 0.
Proof.
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. Proof. by [].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).
Proof.
Lemma sesquiP : reflect (M = (-1) ^+ eps *: M ^t theta)
(M \is (eps,theta).-sesqui).
Proof.
Hypothesis (thetaK : involutive theta).
Hypothesis (M_sesqui : M \is (eps, theta).-sesqui).
Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta.
Proof.
Lemma maptrmx_sesqui : M^t theta = (-1) ^+ eps *: M.
Proof.
Lemma formC u v : '[u, v] = (-1) ^+ eps * theta '[v, u].
Proof.
Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).
Proof.
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).
Proof.
Lemma form_eq0P {u v} : reflect ('[u, v] = 0) (u _|_ v).
Proof.
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).
Proof.
Lemma normalC p q (A : 'M_(p, n)) (B :'M_(q, n)) : (A _|_ B) = (B _|_ A).
Proof.
Lemma normal_ortho_mx p (A : 'M_(p, n)) : ((A^_|_) _|_ A).
Proof.
Lemma normal_mx_ortho p (A : 'M_(p, n)) : (A _|_ (A^_|_)).
Proof.
Lemma rank_normal u : (\rank (u ^_|_) >= n.-1)%N.
Proof.
Definition rad := 1%:M^_|_.
Lemma rad_ker : rad = kermx M.
Proof.
Theorem formDd u v : u _|_ v -> '[u + v] = '[u] + '[v].
Proof.
Lemma formZ a u : '[a *: u]= (a * theta a) * '[u].
Proof.
Lemma formN u : '[- u] = '[u].
Proof.
Lemma form_sign m u : '[(-1) ^+ m *: u] = '[u].
Proof.
Lemma formD u v : let d := '[u, v] in
'[u + v] = '[u] + '[v] + (d + (-1) ^+ eps * theta d).
Proof.
Lemma formB u v : let d := '[u, v] in
'[u - v] = '[u] + '[v] - (d + (-1) ^+ eps * theta d).
Proof.
Lemma formBd u v : u _|_ v -> '[u - v] = '[u] + '[v].
Proof.
End Sesquilinear.
Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope.
Notation symmetric_form := (false, idfun).-sesqui.
Notation skew := (true, idfun).-sesqui.
Notation hermitian := (false, @Num.conj_op _).-sesqui.