(Joint Center)Library forms

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
Require Import finfun tuple ssralg matrix zmodp vector.

Set Implicit Arguments.
Open Local Scope ring_scope.

Import GRing.Theory.

Section RingLmodule.

Variable (R : fieldType).

Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x .

Lemma r2rv_morph_p : linear r2rv.

Canonical Structure r2rv_morph := Linear r2rv_morph_p.

Definition rv2r (A: 'rV[R]_1): R^o := A 0 0.

Lemma r2rv_bij : bijective r2rv.

Canonical Structure RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij.
Canonical Structure RVVectType := VectType R RVMixin.

Lemma dimR : vdim RVVectType = 1%nat.

End RingLmodule.

BiLinear & Sesquilinear & Quadratic Forms over a vectType
Section LinearForm.

Variable (F : fieldType) (V : vectType F).

Section SesquiLinearFormDef.

Structure fautomorphism:= FautoMorph {fval :> FF;
                                      _ : rmorphism fval;
                                      _ : bijective fval}.
Variable theta: fautomorphism.

Lemma fval_rmorph : rmorphism theta.

Canonical Structure fautomorh_additive := Additive fval_rmorph.
Canonical Structure fautomorph_rmorphism := RMorphism fval_rmorph.

Local Notation vvf:= (VVF).

Structure sesquilinear_form :=
              SesqlinearForm {formv :> vvf;
                 _ : x, {morph formv x : y z / y + z};
                 _ : x, {morph formv ^~ x : y z / y + z};
                 _ : a x y, formv (a *: x) y = a × formv x y;
                 _ : a x y , formv x (a *: y) = (theta a) × (formv x y)}.

Variable f : sesquilinear_form.

Lemma bilin1 : x, {morph f x : y z / y + z}.
Lemma bilin2 : x, {morph f ^~ x : y z / y + z}.
Lemma bilina1 : a x y, f (a *: x) y = a × f x y.
Lemma bilina2 : a x y, f x (a *: y) = (theta a) × (f x y).

End SesquiLinearFormDef.

Section SesquiLinearFormTheory.

Variable theta: fautomorphism.
Local Notation sqlf := (sesquilinear_form theta).

Definition symmetric (f : sqlf):= ( a, (theta a = a)) ∧
                                   x y, (f x y = f y x).
Definition skewsymmetric (f : sqlf) := ( a , theta a = a) ∧
                                       x y, f x y = -(f y x).

Definition hermitian_sym (f : sqlf) := ( x y, f x y = (theta (f y x))).

Inductive symmetricf (f : sqlf): Prop :=
  Symmetric : symmetric fsymmetricf f
| Skewsymmetric: skewsymmetric fsymmetricf f
| Hermitian_sym : hermitian_sym fsymmetricf f .

Lemma fsym_f0: (f: sqlf) x y, (symmetricf f) →
                                        (f x y = 0 ↔ f y x = 0).

End SesquiLinearFormTheory.

Variable theta: fautomorphism.
Variable f: (sesquilinear_form theta).
Hypothesis fsym: symmetricf f.

Section orthogonal.

Definition orthogonal x y := f x y = 0.

Lemma ortho_sym: x y, orthogonal x yorthogonal y x.

Theorem Pythagore: u v, orthogonal u vf (u+v) (u+v) = f u u + f v v.

Lemma orthoD : u v w , orthogonal u vorthogonal u worthogonal u (v + w).

Lemma orthoZ: u v a, orthogonal u vorthogonal (a *: u) v.

Variable x:V.

Definition alpha : V→ (RVVectType F) := fun yf y x.

Definition alpha_lfun := (lfun_of_fun alpha).

Definition xbar := lker alpha_lfun .

Lemma alpha_lin: linear alpha.

Lemma xbarP: e1, reflect (orthogonal e1 x ) (e1 \in xbar).

Lemma dim_xbar : vs,(\dim vs ) - 1 ≤ \dim (vs :&: xbar).

to be improved
Lemma xbar_eqvs: vs, ( v , v \in vsorthogonal v x )-> \dim (vs :&: xbar)= (\dim vs ).

End orthogonal.

Definition quadraticf (Q: VF) :=
     ( x a, Q (a *: x) = a ^+ 2 × (Q x))%R ×
     ( x y, Q (x + y) = Q x + Q y + f x y)%R : Prop.
Variable Q : VF.
Hypothesis quadQ : quadraticf Q.
Import GRing.Theory.

Lemma f2Q: x, Q x + Q x = f x x.

End LinearForm.