begin
Lm1:
0 = 0 + (0 * <i> )
;
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem
theorem
canceled;
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
canceled;
theorem Th14:
theorem
canceled;
theorem Th16:
theorem Th17:
theorem Th18:
begin
:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def 1 :
:: deftheorem Def2 defines *' HERMITAN:def 2 :
theorem
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
:: deftheorem defines QcFunctional HERMITAN:def 3 :
theorem Th29:
begin
:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :
theorem Th30:
:: deftheorem Def5 defines hermitan HERMITAN:def 5 :
:: deftheorem Def6 defines diagRvalued HERMITAN:def 6 :
:: deftheorem Def7 defines diagReR+0valued HERMITAN:def 7 :
Lm2:
now
let V be non
empty VectSpStr of
F_Complex ;
for f being Functional of V
for v1, w being Vector of V holds (FormFunctional f,(0Functional V)) . v1,w = 0. F_Complex let f be
Functional of
V;
for v1, w being Vector of V holds (FormFunctional f,(0Functional V)) . v1,w = 0. F_Complex set 0F =
0Functional V;
let v1,
w be
Vector of
V;
(FormFunctional f,(0Functional V)) . v1,w = 0. F_Complex thus (FormFunctional f,(0Functional V)) . v1,
w =
(f . v1) * ((0Functional V) . w)
by BILINEAR:def 11
.=
(f . v1) * (0. F_Complex )
by HAHNBAN1:22
.=
0. F_Complex
by VECTSP_1:39
;
verum
end;
Lm3:
for V being non empty VectSpStr of F_Complex
for f being Functional of V holds FormFunctional f,(0Functional V) is hermitan
definition
let V,
W be non
empty VectSpStr of
F_Complex ;
let f be
Form of
V,
W;
func f *' -> Form of
V,
W means :
Def8:
for
v being
Vector of
V for
w being
Vector of
W holds
it . v,
w = (f . v,w) *' ;
existence
ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . v,w = (f . v,w) *'
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . v,w = (f . v,w) *' ) & ( for v being Vector of V
for w being Vector of W holds b2 . v,w = (f . v,w) *' ) holds
b1 = b2
end;
:: deftheorem Def8 defines *' HERMITAN:def 8 :
theorem Th31:
theorem
theorem
theorem Th34:
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
for
V,
W being non
empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of
F_Complex for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
F_Complex for
f being
sesquilinear-Form of
V,
W holds
f . (v + (a * u)),
(w + (b * t)) = ((f . v,w) + ((b *' ) * (f . v,t))) + ((a * (f . u,w)) + (a * ((b *' ) * (f . u,t))))
theorem Th41:
for
V,
W being
VectSp of
F_Complex for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
F_Complex for
f being
sesquilinear-Form of
V,
W holds
f . (v - (a * u)),
(w - (b * t)) = ((f . v,w) - ((b *' ) * (f . v,t))) - ((a * (f . u,w)) - (a * ((b *' ) * (f . u,t))))
theorem Th42:
theorem
:: deftheorem defines signnorm HERMITAN:def 9 :
theorem Th44:
theorem Th45:
for
V being
VectSp of
F_Complex for
v,
w being
Vector of
V for
f being
sesquilinear-Form of
V,
V for
r being
real number for
a being
Element of
F_Complex st
|.a.| = 1 holds
f . (v - (([**r,0 **] * a) * w)),
(v - (([**r,0 **] * a) * w)) = (((f . v,v) - ([**r,0 **] * (a * (f . w,v)))) - ([**r,0 **] * ((a *' ) * (f . v,w)))) + ([**(r ^2 ),0 **] * (f . w,w))
theorem Th46:
for
V being
VectSp of
F_Complex for
v,
w being
Vector of
V for
f being
diagReR+0valued hermitan-Form of
V for
r being
real number for
a being
Element of
F_Complex st
|.a.| = 1 &
Re (a * (f . w,v)) = |.(f . w,v).| holds
(
Re (f . (v - (([**r,0 **] * a) * w)),(v - (([**r,0 **] * a) * w))) = ((signnorm f,v) - ((2 * |.(f . w,v).|) * r)) + ((signnorm f,w) * (r ^2 )) &
0 <= ((signnorm f,v) - ((2 * |.(f . w,v).|) * r)) + ((signnorm f,w) * (r ^2 )) )
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem
:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :
begin
theorem
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
:: deftheorem defines RQ*Form HERMITAN:def 11 :
theorem Th62:
definition
let V,
W be
VectSp of
F_Complex ;
let f be
sesquilinear-Form of
V,
W;
func Q*Form f -> sesquilinear-Form of
(VectQuot V,(LKer f)),
(VectQuot W,(RKer (f *' ))) means :
Def12:
for
A being
Vector of
(VectQuot V,(LKer f)) for
B being
Vector of
(VectQuot W,(RKer (f *' ))) for
v being
Vector of
V for
w being
Vector of
W st
A = v + (LKer f) &
B = w + (RKer (f *' )) holds
it . A,
B = f . v,
w;
existence
ex b1 being sesquilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer (f *' ))) st
for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer (f *' )))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *' )) holds
b1 . A,B = f . v,w
uniqueness
for b1, b2 being sesquilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer (f *' ))) st ( for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer (f *' )))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *' )) holds
b1 . A,B = f . v,w ) & ( for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer (f *' )))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *' )) holds
b2 . A,B = f . v,w ) holds
b1 = b2
end;
:: deftheorem Def12 defines Q*Form HERMITAN:def 12 :
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
begin
:: deftheorem Def13 defines positivediagvalued HERMITAN:def 13 :
:: deftheorem defines ScalarForm HERMITAN:def 14 :
theorem
theorem Th69:
theorem