@MISC{RUSUB_7.MIZ,
  AUTHOR = {Okazaki, Hiroyuki},
  TITLE = {Formalization of Orthogonal Decomposition for Hilbert Spaces},
  SECTION1 = {Preliminaries},
  SECTION2 = {Topological Space generated from Real Unitary Space},
  DAY = {27},
  MONTH = {December},
  YEAR = {2022},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  MSC = {46C05 46C07 46M35},
  KEYWORDS = {Hilbert Space; Orthogonal Decomposition; Topological Space},
  SUMMARY = {In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces.
  For any subspace $S$ of a Hilbert space $H$, any vector can be represented by the sum of 
  a vector in $S$ and a vector orthogonal to $S.$  
  The formalization of orthogonal complements of Hilbert spaces has been stored in the MML \cite{RUSUB_5.ABS}.
   We referred to \cite{Luenberger} and \cite{YOSIDA} in the formalization.},
ACKNOWLEDGEMENT = {The authors would also like to express our gratitude to Prof. Yasunari Shidama 
   for his support and encouragement.}}

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

@BOOK{YOSIDA,
 AUTHOR = {Yosida, Kosaku},
 TITLE = {Functional Analysis},
 YEAR = {1980},
 PUBLISHER = {Springer}}

