Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/15404
Tytuł: | On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors |
Autorzy: | Okazaki, Hiroyuki |
Słowa kluczowe: | Gram-Schmidt process orthonormal basis linear algebra |
Data wydania: | 2023 |
Data dodania: | 9-paź-2023 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 31, Issue 1, Pages 53-57 |
Abstrakt: | 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]. |
Afiliacja: | Shinshu University, Nagano, Japan |
URI: | http://hdl.handle.net/11320/15404 |
DOI: | 10.2478/forma-2023-0005 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2023 The Author(s) CC BY-SA 3.0 license |
Występuje w kolekcji(ach): | Formalized Mathematics, 2023, Volume 31, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2023-0005.pdf | 256,86 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL