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 algC algnum.
From mathcomp
Require Import fieldext.
From mathcomp Require Import vector.
# 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, 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 [the zmodType of '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).
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.
Proof.
by move=> /eq_map_mx->; rewrite map_mx_id. Qed.
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.
Lemma linearNr : {morph f z : x / - x}
Proof.
Lemma linearDr : {morph f z : x y / x + y}
Proof.
Lemma linearBr : {morph f z : x y / x - y}
Proof.
Lemma linearMnr n : {morph f z : x / x *+ n}
Proof.
Lemma linearMNnr n : {morph f z : x / x *- n}
Proof.
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 []. Qed.
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. Qed.
Lemma linearNl : {morph f^~ z : x / - x}.
Proof.
by move=> ?; rewrite -applyrE raddfN. Qed.
Lemma linearDl : {morph f^~ z : x y / x + y}.
Proof.
by move=> ??; rewrite -applyrE raddfD. Qed.
Lemma linearBl : {morph f^~ z : x y / x - y}.
Proof.
by move=> ??; rewrite -applyrE raddfB. Qed.
Lemma linearMnl n : {morph f^~ z : x / x *+ n}.
Proof.
by move=> ?; rewrite -applyrE raddfMn. Qed.
Lemma linearMNnl n : {morph f^~ z : x / x *- n}.
Proof.
by move=> ?; rewrite -applyrE raddfMNn. Qed.
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.
by move=> ??; rewrite -applyrE linearP. Qed.
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.
Canonical rev_mulmx (
R : ringType)
m n p := @RevOp _ _ _ (
@mulmxr R m n p)
(
@mulmx R m n p) (
fun _ _ => erefl).
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.
by rewrite /form !mul0mx mxE. Qed.
Lemma form0r u : '[u, 0] = 0.
Proof.
Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w].
Proof.
by rewrite /form !mulmxDl mxE. Qed.
Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w].
Proof.
by rewrite /form linearD !map_mxD !mulmxDr mxE. Qed.
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.
rewrite /form -rowE -map_trmx map_delta_mx -[M in LHS]trmxK.
by rewrite -tr_col -trmx_mul -rowE !mxE.
Qed.
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 []. Qed.
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.
gen have nC : p q A B / A _|_ B -> B _|_ A; last by apply/idP/idP; apply/nC.
move=> AnB; apply/normalP => u v ? ?; rewrite normalE.
rewrite formC mulf_eq0 ?fmorph_eq0 ?signr_eq0 /=.
by rewrite -normalE (
normalP _ _ AnB).
Qed.
Lemma normal_ortho_mx p (
A : 'M_(
p, n))
: ((
A^_|_)
_|_ A).
Proof.
by []. Qed.
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.