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

<p>In this article, we formalize the Gram-Schmidt process in the Mizar system [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_002">2</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_003">3</xref>] (compare another formalization using Isabelle/HOL proof assistant [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_001">1</xref>]). This process is one of the most famous methods for orthonormalizing a set of vectors. The method is named after Jørgen Pedersen Gram and Erhard Schmidt [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_004">4</xref>]. There are many applications of the Gram-Schmidt process in the field of computer science, e.g., error correcting codes or cryptology [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_008">8</xref>]. First, we prove some preliminary theorems about real unitary space. Next, we formalize the definition of the Gram-Schmidt process that finds orthonormal basis. We followed [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_005">5</xref>] in the formalization, continuing work developed in [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_007">7</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0005_ref_006">6</xref>].</p>
</abstract>

In this article, we formalize the Gram-Schmidt process in the Mizar system [2], [3] (compare another formalization using Isabelle/HOL proof assistant [1]). This process is one of the most famous methods for orthonormalizing a set of vectors. The method is named after Jørgen Pedersen Gram and Erhard Schmidt [4]. There are many applications of the Gram-Schmidt process in the field of computer science, e.g., error correcting codes or cryptology [8]. First, we prove some preliminary theorems about real unitary space. Next, we formalize the definition of the Gram-Schmidt process that finds orthonormal basis. We followed [5] in the formalization, continuing work developed in [7], [6].

On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors

Formalized Mathematics

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

In this article, we formalize the Gram-Schmidt process in the Mizar system [2], [3] (compare another formalization using Isabelle/HOL proof assistant [1])....

On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors

Data publikacji: 26 wrz 2023

Zakres stron: 53 - 57

Przyjęty: 31 mar 2023

DOI: https://doi.org/10.2478/forma-2023-0005

Słowa kluczowe
Gram-Schmidt process, orthonormal basis, linear algebra

© 2023 Hiroyuki Okazaki, published by Sciendo

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

On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors

Data publikacji: 26 wrz 2023

Zakres stron: 53 - 57

Przyjęty: 31 mar 2023

DOI: https://doi.org/10.2478/forma-2023-0005

Słowa kluczoweGram-Schmidt process, orthonormal basis, linear algebra

© 2023 Hiroyuki Okazaki, published by Sciendo

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

Słowa kluczowe
Gram-Schmidt process, orthonormal basis, linear algebra