Hermitan Functionals. Canonical Construction of Scalar Product in Quotient Vector Space

Jaroslaw Kotowicz

University of Bialystok

Summary.

In the article we present antilinear functionals, sesquilinear and hermitan forms. We prove Schwarz and Minkowski inequalities, and Parallelogram Law for non negative hermitan form. The proof of Schwarz inequality is based on [16]. The incorrect proof of this fact can be found in [13]. The construction of scalar product in quotient vector space from non negative hermitan functions is the main result of the article.

This work has been partially supported by TRIAL-SOLUTION grant IST-2001-35447 and SPUB-M grant of KBN.

MML Identifier: HERMITAN

Contents (PDF format)

1. Auxiliary Facts about Complex Numbers
2. Antilinear Functionals in Complex Vector Spaces
3. Sesquilinear Forms in Complex Vector Spaces
4. Kernel of Hermitan Forms and Hermitan Forms in Quotient Vector Spaces
5. Scalar Product in Quotient Vector Space Generated by Nonnegative Hermitan Form

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. The complex numbers. Journal of Formalized Mathematics, 2, 1990.

[7] Library Committee. Introduction to arithmetic. Journal of Formalized Mathematics, Addenda, 2003.

[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[9] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.

[10] Jaroslaw Kotowicz. Bilinear functionals in vector spaces. Journal of Formalized Mathematics, 14, 2002.

[11] Jaroslaw Kotowicz. Quotient vector spaces and functionals. Journal of Formalized Mathematics, 14, 2002.

[12] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.

[13] Krzysztof Maurin. \em Analiza, II, volume 70 of \em Biblioteka Matematyczna. PWN - Warszawa, 1991.

[14] Anna Justyna Milewska. The field of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[15] Anna Justyna Milewska. The Hahn Banach theorem in the vector space over the field of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[16] Walter Rudin. \em Real and Complex Analysis. Mc Graw-Hill, Inc., 1974.

[17] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[18] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[19] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[20] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[21] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[22] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Journal of Formalized Mathematics, 2, 1990.

[23] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[24] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.