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 :
for V being non empty VectSpStr of F_Complex
for f being Functional of V holds
( f is cmplxhomogeneous iff for v being Vector of V
for a being Scalar of holds f . (a * v) = (a *') * (f . v) );
:: deftheorem Def2 defines *' HERMITAN:def 2 :
for V being non empty VectSpStr of F_Complex
for f, b3 being Functional of V holds
( b3 = f *' iff for v being Vector of V holds b3 . v = (f . v) *' );
theorem
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
:: deftheorem defines QcFunctional HERMITAN:def 3 :
for V being VectSp of F_Complex
for f being antilinear-Functional of V holds QcFunctional f = QFunctional (f,(Ker (f *')));
theorem Th29:
begin
:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :
for V, W being non empty VectSpStr of F_Complex
for f being Form of V,W holds
( f is cmplxhomogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is cmplxhomogeneous );
theorem Th30:
:: deftheorem Def5 defines hermitan HERMITAN:def 5 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V holds
( f is hermitan iff for v, u being Vector of V holds f . (v,u) = (f . (u,v)) *' );
:: deftheorem Def6 defines diagRvalued HERMITAN:def 6 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V holds
( f is diagRvalued iff for v being Vector of V holds Im (f . (v,v)) = 0 );
:: deftheorem Def7 defines diagReR+0valued HERMITAN:def 7 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V holds
( f is diagReR+0valued iff for v being Vector of V holds 0 <= Re (f . (v,v)) );
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_Complexlet f be
Functional of
V;
for v1, w being Vector of V holds (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complexset 0F =
0Functional V;
let v1,
w be
Vector of
V;
(FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complexthus (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 :
for V, W being non empty VectSpStr of F_Complex
for f, b4 being Form of V,W holds
( b4 = f *' iff for v being Vector of V
for w being Vector of W holds b4 . (v,w) = (f . (v,w)) *' );
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 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V
for v being Vector of V holds signnorm (f,v) = Re (f . (v,v));
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 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V
for b3 being RFunctional of V holds
( b3 = quasinorm f iff for v being Element of V holds b3 . v = sqrt (signnorm (f,v)) );
begin
theorem
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
:: deftheorem defines RQ*Form HERMITAN:def 11 :
for V being non empty VectSpStr of F_Complex
for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W holds RQ*Form f = (RQForm (f *')) *' ;
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 :
for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W
for b4 being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) holds
( b4 = Q*Form f iff 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
b4 . (A,B) = f . (v,w) );
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
begin
:: deftheorem Def13 defines positivediagvalued HERMITAN:def 13 :
for V being non empty VectSpStr of F_Complex
for f being Form of V,V holds
( f is positivediagvalued iff for v being Vector of V st v <> 0. V holds
0 < Re (f . (v,v)) );
:: deftheorem defines ScalarForm HERMITAN:def 14 :
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds ScalarForm f = Q*Form f;
theorem
theorem Th69:
theorem