<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace <italic>S</italic> of a Hilbert space <italic>H</italic>, any vector can be represented by the sum of a vector in <italic>S</italic> and a vector orthogonal to <italic>S.</italic> The formalization of orthogonal complements of Hilbert spaces has been stored in the Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.</p>
</abstract>

In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. 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 Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.

Formalization of Orthogonal Decomposition for Hilbert Spaces

Formalized Mathematics

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

{"article-title":"Formalization of Orthogonal Decomposition for Hilbert Spaces"}

In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace S of a Hilbert...

Formalization of Orthogonal Decomposition for Hilbert Spaces

Pubblicato online: 18 feb 2023

Pagine: 295 - 299

Accettato: 27 dic 2022

DOI: https://doi.org/10.2478/forma-2022-0023

Parole chiave
Hilbert space, orthogonal decomposition, topological space

© 2022 Hiroyuki Okazaki, published by Sciendo

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

Formalization of Orthogonal Decomposition for Hilbert Spaces

Pubblicato online: 18 feb 2023

Pagine: 295 - 299

Accettato: 27 dic 2022

DOI: https://doi.org/10.2478/forma-2022-0023

Parole chiaveHilbert space, orthogonal decomposition, topological space

© 2022 Hiroyuki Okazaki, published by Sciendo

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

Parole chiave
Hilbert space, orthogonal decomposition, topological space