<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. </p><p>Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.</p></abstract>

In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.

The Orthogonal Projection and the Riesz Representation Theorem

Gifu National College of Technology Gifu, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"The Orthogonal Projection and the Riesz Representation Theorem"}

In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on...

The Orthogonal Projection and the Riesz Representation Theorem

Published Online: Sep 30, 2015

Page range: 243 - 252

Received: Jul 01, 2015

DOI: https://doi.org/10.1515/forma-2015-0020

Keywords
normed linear spaces, Banach spaces, duality, orthogonal projection, Riesz representation

© by Keiko Narita

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

The Orthogonal Projection and the Riesz Representation Theorem

Published Online: Sep 30, 2015

Page range: 243 - 252

Received: Jul 01, 2015

DOI: https://doi.org/10.1515/forma-2015-0020

Keywordsnormed linear spaces, Banach spaces, duality, orthogonal projection, Riesz representation

© by Keiko Narita

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Keywords
normed linear spaces, Banach spaces, duality, orthogonal projection, Riesz representation