Gram-Schmidt Orthogonalization and Orthonormalization #
In this file we introduce Gram-Schmidt Orthogonalization and Orthonormalization.
The Gram-Schmidt process takes a set of vectors as input and outputs a set of orthogonal vectors which have the same span.
Main results #
gramSchmidt
: the Gram-Schmidt processgramSchmidt_orthogonal
:gramSchmidt
produces an orthogonal system of vectors.span_gramSchmidt
:gramSchmidt
preserves span of vectors.gramSchmidt_ne_zero
: If the input vectors ofgramSchmidt
are linearly independent, then the output vectors are non-zero.gramSchmidt_basis
: The basis produced by the Gram-Schmidt process when given a basis as input.gramSchmidtNormed
: the normalizedgramSchmidt
(i.e each vector ingramSchmidtNormed
has unit length.)gramSchmidt_orthonormal
:gramSchmidtNormed
produces an orthornormal system of vectors.gramSchmidtOrthonormalBasis
: orthonormal basis constructed by the Gram-Schmidt process from an indexed set of vectors of the right size
The Gram-Schmidt process takes a set of vectors as input and outputs a set of orthogonal vectors which have the same span.
Equations
- gramSchmidt ๐ f n = f n - โ i : { x : ฮน // x โ Finset.Iio n }, โ((orthogonalProjection (Submodule.span ๐ {gramSchmidt ๐ f โi})) (f n))
Instances For
This lemma uses โ i in
instead of โ i :
.
Gram-Schmidt Orthogonalisation:
gramSchmidt
produces an orthogonal system of vectors.
This is another version of gramSchmidt_orthogonal
using Pairwise
instead.
gramSchmidt
preserves span of vectors.
If the input vectors of gramSchmidt
are linearly independent,
then the output vectors are non-zero.
gramSchmidt
produces a triangular matrix of vectors when given a basis.
gramSchmidt
produces linearly independent vectors when given linearly independent vectors.
When given a basis, gramSchmidt
produces a basis.
Equations
- gramSchmidtBasis b = Basis.mk โฏ โฏ
Instances For
the normalized gramSchmidt
(i.e each vector in gramSchmidtNormed
has unit length.)
Equations
- gramSchmidtNormed ๐ f n = (โโgramSchmidt ๐ f nโ)โปยน โข gramSchmidt ๐ f n
Instances For
Gram-Schmidt Orthonormalization:
gramSchmidtNormed
applied to a linearly independent set of vectors produces an orthornormal
system of vectors.
Gram-Schmidt Orthonormalization:
gramSchmidtNormed
produces an orthornormal system of vectors after removing the vectors which
become zero in the process.
Given an indexed family f : ฮน โ E
of vectors in an inner product space E
, for which the
size of the index set is the dimension of E
, produce an orthonormal basis for E
which agrees
with the orthonormal set produced by the Gram-Schmidt orthonormalization process on the elements of
ฮน
for which this process gives a nonzero number.
Equations
- gramSchmidtOrthonormalBasis h f = โฏ.choose
Instances For
Given an indexed family f : ฮน โ E
of vectors in an inner product space E
, for which the
size of the index set is the dimension of E
, the matrix of coefficients of f
with respect to the
orthonormal basis gramSchmidtOrthonormalBasis
constructed from f
is upper-triangular.