@MISC{RUSUB_6.MIZ,
  AUTHOR = {Okazaki, Hiroyuki},
  TITLE = {On the Formalization of {G}ram-{S}chmidt Process for Orthonormalizing a Set of Vectors},
  SECTION1 = {Preliminaries},
  SECTION2 = {Gram-Schmidt Process},
  DAY = {31},
  MONTH = {March},
  YEAR = {2023},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {65F25 94A11 97H60},
  KEYWORDS = {Gram-Schmidt process; Orthonormal Basis; Linear Algebra},
  SUMMARY = {In this article, we formalize the Gram-Schmidt process.
  The Gram-Schmidt process is one of the most famous method for orthonormalizing a set of   vectors. 
  The method is named after J{\o}rgen Pedersen Gram and Erhard Schmidt \cite{CheneyKincaid:2009}.
  There are many applications of the Gram-Schmidt process in the field of computer science, 
  e.g., error correcting codes, cryptology.
  First, we prove some theorems about real unitary space for preparation.
  Next, we formalize the definition of the Gram-Schmidt process that finds orthonormal basis.
  We referred to \cite{Luenberger:1969} in the formalization.},
  ACKNOWLEDGEMENT = {The author would like to express our gratitude to Prof. Yasunari Shidama for   his support and encouragement.}}

@BOOK{CheneyKincaid:2009,
 AUTHOR = {Cheney, Ward and Kincaid, David},
 TITLE = {Linear Algebra: Theory and Applications},
 YEAR = {2009},
 PUBLISHER = {Jones and Bartlett publishers}}

@BOOK{Luenberger:1969,
 AUTHOR = {David G., Luenberger},
 TITLE = {Optimization by Vector Space Methods},
 YEAR = {1969},
 PUBLISHER = {Jhon Wiley  & Sons}}
