# 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 process
• gramSchmidt_orthogonal : gramSchmidt produces an orthogonal system of vectors.
• span_gramSchmidt : gramSchmidt preserves span of vectors.
• gramSchmidt_ne_zero : If the input vectors of gramSchmidt 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 normalized gramSchmidt (i.e each vector in gramSchmidtNormed 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
noncomputable def gramSchmidt (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (n : ฮน) :
E

The Gram-Schmidt process takes a set of vectors as input and outputs a set of orthogonal vectors which have the same span.

Equations
Instances For
theorem gramSchmidt_def (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (n : ฮน) :
gramSchmidt ๐ f n = f n - Finset.sum () fun (i : ฮน) => โ((orthogonalProjection (Submodule.span ๐ {gramSchmidt ๐ f i})) (f n))

This lemma uses โ i in instead of โ i :.

theorem gramSchmidt_def' (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (n : ฮน) :
f n = gramSchmidt ๐ f n + Finset.sum () fun (i : ฮน) => โ((orthogonalProjection (Submodule.span ๐ {gramSchmidt ๐ f i})) (f n))
theorem gramSchmidt_def'' (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (n : ฮน) :
f n = gramSchmidt ๐ f n + Finset.sum () fun (i : ฮน) => (โชgramSchmidt ๐ f i, f nโซ_๐ / โโgramSchmidt ๐ f iโ ^ 2) โข gramSchmidt ๐ f i
@[simp]
theorem gramSchmidt_zero (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_4} [] [] [OrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) :
theorem gramSchmidt_orthogonal (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) {a : ฮน} {b : ฮน} (hโ : a โ  b) :
โชgramSchmidt ๐ f a, gramSchmidt ๐ f bโซ_๐ = 0

Gram-Schmidt Orthogonalisation: gramSchmidt produces an orthogonal system of vectors.

theorem gramSchmidt_pairwise_orthogonal (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) :
Pairwise fun (a b : ฮน) => โชgramSchmidt ๐ f a, gramSchmidt ๐ f bโซ_๐ = 0

This is another version of gramSchmidt_orthogonal using Pairwise instead.

theorem gramSchmidt_inv_triangular (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (v : ฮน โ E) {i : ฮน} {j : ฮน} (hij : i < j) :
โชgramSchmidt ๐ v j, v iโซ_๐ = 0
theorem mem_span_gramSchmidt (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) {i : ฮน} {j : ฮน} (hij : i โค j) :
f i โ Submodule.span ๐ (gramSchmidt ๐ f '' )
theorem gramSchmidt_mem_span (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) {j : ฮน} {i : ฮน} :
i โค j โ gramSchmidt ๐ f i โ Submodule.span ๐ (f '' )
theorem span_gramSchmidt_Iic (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (c : ฮน) :
Submodule.span ๐ (gramSchmidt ๐ f '' ) = Submodule.span ๐ (f '' )
theorem span_gramSchmidt_Iio (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (c : ฮน) :
Submodule.span ๐ (gramSchmidt ๐ f '' ) = Submodule.span ๐ (f '' )
theorem span_gramSchmidt (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) :
Submodule.span ๐ (Set.range (gramSchmidt ๐ f)) = Submodule.span ๐ ()

gramSchmidt preserves span of vectors.

theorem gramSchmidt_of_orthogonal (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (hf : Pairwise fun (i j : ฮน) => โชf i, f jโซ_๐ = 0) :
gramSchmidt ๐ f = f
theorem gramSchmidt_ne_zero_coe {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (n : ฮน) (hโ : LinearIndependent (ฮน := { x : ฮน // x โ }) ๐ (f โ Subtype.val)) :
gramSchmidt ๐ f n โ  0
theorem gramSchmidt_ne_zero {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (n : ฮน) (hโ : LinearIndependent ๐ f) :
gramSchmidt ๐ f n โ  0

If the input vectors of gramSchmidt are linearly independent, then the output vectors are non-zero.

theorem gramSchmidt_triangular {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {i : ฮน} {j : ฮน} (hij : i < j) (b : Basis ฮน ๐ E) :
(b.repr (gramSchmidt ๐ (โb) i)) j = 0

gramSchmidt produces a triangular matrix of vectors when given a basis.

theorem gramSchmidt_linearIndependent {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (hโ : LinearIndependent ๐ f) :
LinearIndependent ๐ (gramSchmidt ๐ f)

gramSchmidt produces linearly independent vectors when given linearly independent vectors.

noncomputable def gramSchmidtBasis {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (b : Basis ฮน ๐ E) :
Basis ฮน ๐ E

When given a basis, gramSchmidt produces a basis.

Equations
Instances For
theorem coe_gramSchmidtBasis {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (b : Basis ฮน ๐ E) :
โ() = gramSchmidt ๐ โb
noncomputable def gramSchmidtNormed (๐ : Type u_1) {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (n : ฮน) :
E

the normalized gramSchmidt (i.e each vector in gramSchmidtNormed has unit length.)

Equations
Instances For
theorem gramSchmidtNormed_unit_length_coe {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (n : ฮน) (hโ : LinearIndependent (ฮน := { x : ฮน // x โ }) ๐ (f โ Subtype.val)) :
theorem gramSchmidtNormed_unit_length {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (n : ฮน) (hโ : LinearIndependent ๐ f) :
theorem gramSchmidtNormed_unit_length' {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} {n : ฮน} (hn : gramSchmidtNormed ๐ f n โ  0) :
theorem gramSchmidt_orthonormal {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ E} (hโ : LinearIndependent ๐ f) :
Orthonormal ๐ (gramSchmidtNormed ๐ f)

Gram-Schmidt Orthonormalization: gramSchmidtNormed applied to a linearly independent set of vectors produces an orthornormal system of vectors.

theorem gramSchmidt_orthonormal' {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) :
Orthonormal ๐ fun (i : โ{i : ฮน | gramSchmidtNormed ๐ f i โ  0}) => gramSchmidtNormed ๐ f โi

Gram-Schmidt Orthonormalization: gramSchmidtNormed produces an orthornormal system of vectors after removing the vectors which become zero in the process.

theorem span_gramSchmidtNormed {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) (s : Set ฮน) :
Submodule.span ๐ (gramSchmidtNormed ๐ f '' s) = Submodule.span ๐ (gramSchmidt ๐ f '' s)
theorem span_gramSchmidtNormed_range {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ E) :
Submodule.span ๐ (Set.range (gramSchmidtNormed ๐ f)) = Submodule.span ๐ (Set.range (gramSchmidt ๐ f))
noncomputable def gramSchmidtOrthonormalBasis {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) (f : ฮน โ E) :
OrthonormalBasis ฮน ๐ E

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
Instances For
theorem gramSchmidtOrthonormalBasis_apply {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) {f : ฮน โ E} {i : ฮน} (hi : gramSchmidtNormed ๐ f i โ  0) :
i = gramSchmidtNormed ๐ f i
theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) {f : ฮน โ E} (hf : Pairwise fun (i j : ฮน) => โชf i, f jโซ_๐ = 0) {i : ฮน} (hi : f i โ  0) :
theorem inner_gramSchmidtOrthonormalBasis_eq_zero {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) {f : ฮน โ E} {i : ฮน} (hi : gramSchmidtNormed ๐ f i = 0) (j : ฮน) :
โช i, f jโซ_๐ = 0
theorem gramSchmidtOrthonormalBasis_inv_triangular {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) (f : ฮน โ E) {i : ฮน} {j : ฮน} (hij : i < j) :
โช j, f iโซ_๐ = 0
theorem gramSchmidtOrthonormalBasis_inv_triangular' {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) (f : ฮน โ E) {i : ฮน} {j : ฮน} (hij : i < j) :
.repr (f i) j = 0
theorem gramSchmidtOrthonormalBasis_inv_blockTriangular {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) (f : ฮน โ E) :

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.

theorem gramSchmidtOrthonormalBasis_det {๐ : Type u_1} {E : Type u_2} [RCLike ๐] [InnerProductSpace ๐ E] {ฮน : Type u_3} [] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐ E] (h : = ) (f : ฮน โ E) [] :
= Finset.prod Finset.univ fun (i : ฮน) => โช i, f iโซ_๐