@MISC{DUALSP06.MIZ,
  AUTHOR = {Okazaki, Hiroyuki},
  TITLE = {Formalization of Orthogonal Complements of Normed Spaces},
  SECTION1 = {Orthogonal Complements of Normed Spaces},
  SECTION2 = {Minimum Norm Problems},
  DAY = {28},
  MONTH = {November},
  YEAR = {2024},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {13P25 46N10 74P20},
  KEYWORDS = {dual space; orthonormal complements; minimum norm problem},
  SUMMARY = {In this study we are formalizing the optimization theory in Mizar.
  It is well known that geometric principles of linear vector space theory play fundamental roles
  in optimization \cite{NirL}.
  This article focuses on formalization of definitions and some theorems about dual spaces.
  First, we formalize orthogonal complements of real normed spaces. Next, we
  formalize minimum norm problems. We referred to \cite{Luenberger} and \cite{NirL}
  in the formalization.},
  ACKNOWLEDGEMENT = {The author would like to express our gratitude to Prof. Yasunari Shidama
   for his support and encouragement.}}

@BOOK{NirL,
 AUTHOR = {Nirenberg, Louis},
 TITLE = {Functional Analysis: Lectures Given in 1960--61. Notes by Lesley Sibner},
 YEAR = {1961},
 PUBLISHER = {New York University}}

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