:: Hermitan Functionals. {C}anonical Construction of Scalar Product inQuotient Vector Space
:: by Jaros{\l}aw Kotowicz
::
:: Received November 12, 2002
:: Copyright (c) 2002 Association of Mizar Users
Lm1:
0 = 0 + (0 * <i> )
;
theorem Th1: :: HERMITAN:1
theorem Th2: :: HERMITAN:2
theorem :: HERMITAN:3
theorem Th4: :: HERMITAN:4
theorem :: HERMITAN:5
theorem :: HERMITAN:6
canceled;
theorem :: HERMITAN:7
theorem Th8: :: HERMITAN:8
theorem Th9: :: HERMITAN:9
theorem Th10: :: HERMITAN:10
theorem Th11: :: HERMITAN:11
theorem :: HERMITAN:12
theorem :: HERMITAN:13
canceled;
theorem Th14: :: HERMITAN:14
theorem :: HERMITAN:15
canceled;
theorem Th16: :: HERMITAN:16
theorem Th17: :: HERMITAN:17
theorem Th18: :: HERMITAN:18
:: deftheorem Def1 defines cmplxhomogeneous HERMITAN:def 1 :
:: deftheorem Def2 defines *' HERMITAN:def 2 :
theorem :: HERMITAN:19
theorem :: HERMITAN:20
theorem Th21: :: HERMITAN:21
theorem Th22: :: HERMITAN:22
theorem :: HERMITAN:23
theorem :: HERMITAN:24
theorem Th25: :: HERMITAN:25
theorem Th26: :: HERMITAN:26
theorem :: HERMITAN:27
theorem Th28: :: HERMITAN:28
:: deftheorem defines QcFunctional HERMITAN:def 3 :
theorem Th29: :: HERMITAN:29
:: deftheorem Def4 defines cmplxhomogeneousFAF HERMITAN:def 4 :
theorem Th30: :: HERMITAN:30
:: 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 ;
:: thesis: 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;
:: thesis: 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;
:: thesis: (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
;
:: thesis: 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:
:: HERMITAN:def 8
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: :: HERMITAN:31
theorem :: HERMITAN:32
theorem :: HERMITAN:33
theorem Th34: :: HERMITAN:34
theorem Th35: :: HERMITAN:35
theorem :: HERMITAN:36
theorem :: HERMITAN:37
theorem Th38: :: HERMITAN:38
theorem Th39: :: HERMITAN:39
theorem Th40: :: HERMITAN:40
for
V,
W being non
empty right_complementable add-associative right_zeroed VectSp-like 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: :: HERMITAN:41
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: :: HERMITAN:42
theorem :: HERMITAN:43
:: deftheorem defines signnorm HERMITAN:def 9 :
theorem Th44: :: HERMITAN:44
theorem Th45: :: HERMITAN:45
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 &
Re (a * (f . w,v)) = |.(f . w,v).| &
Im (a * (f . w,v)) = 0 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: :: HERMITAN:46
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).| &
Im (a * (f . w,v)) = 0 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: :: HERMITAN:47
theorem Th48: :: HERMITAN:48
theorem Th49: :: HERMITAN:49
theorem Th50: :: HERMITAN:50
theorem :: HERMITAN:51
theorem Th52: :: HERMITAN:52
theorem :: HERMITAN:53
:: deftheorem Def10 defines quasinorm HERMITAN:def 10 :
theorem :: HERMITAN:54
theorem Th55: :: HERMITAN:55
theorem Th56: :: HERMITAN:56
theorem :: HERMITAN:57
theorem Th58: :: HERMITAN:58
theorem Th59: :: HERMITAN:59
theorem Th60: :: HERMITAN:60
theorem Th61: :: HERMITAN:61
:: deftheorem defines RQ*Form HERMITAN:def 11 :
theorem Th62: :: HERMITAN:62
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:
:: HERMITAN:def 12
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: :: HERMITAN:63
theorem Th64: :: HERMITAN:64
theorem Th65: :: HERMITAN:65
theorem Th66: :: HERMITAN:66
theorem Th67: :: HERMITAN:67
:: deftheorem Def13 defines positivediagvalued HERMITAN:def 13 :
:: deftheorem defines ScalarForm HERMITAN:def 14 :
theorem :: HERMITAN:68
theorem Th69: :: HERMITAN:69
theorem :: HERMITAN:70