🌓
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 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 .