# Documentation

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

# 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} [] [] {ι : 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} [] [] {ι : 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} [] [] {ι : 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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) (n : ι) :
f n = gramSchmidt 𝕜 f n + Finset.sum () fun i => (inner (gramSchmidt 𝕜 f i) (f n) / gramSchmidt 𝕜 f i ^ 2) gramSchmidt 𝕜 f i
@[simp]
theorem gramSchmidt_zero (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_4} [] [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) :
= f
theorem gramSchmidt_orthogonal (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) {a : ι} {b : ι} (h₀ : a b) :
inner (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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) :
Pairwise fun a b => inner (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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (v : ιE) {i : ι} {j : ι} (hij : i < j) :
inner (gramSchmidt 𝕜 v j) (v i) = 0
theorem mem_span_gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) {i : ι} {j : ι} (hij : i j) :
f i Submodule.span 𝕜 ( '' )
theorem gramSchmidt_mem_span (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) {j : ι} {i : ι} :
i jgramSchmidt 𝕜 f i Submodule.span 𝕜 (f '' )
theorem span_gramSchmidt_Iic (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) (c : ι) :
Submodule.span 𝕜 ( '' ) = Submodule.span 𝕜 (f '' )
theorem span_gramSchmidt_Iio (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) (c : ι) :
Submodule.span 𝕜 ( '' ) = Submodule.span 𝕜 (f '' )
theorem span_gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) :

gramSchmidt preserves span of vectors.

theorem gramSchmidt_of_orthogonal (𝕜 : Type u_1) {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (hf : Pairwise fun i j => inner (f i) (f j) = 0) :
= f
theorem gramSchmidt_ne_zero_coe {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (n : ι) (h₀ : LinearIndependent 𝕜 (f Subtype.val)) :
gramSchmidt 𝕜 f n 0
theorem gramSchmidt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (n : ι) (h₀ : ) :
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} [] [] {ι : 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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (h₀ : ) :

gramSchmidt produces linearly independent vectors when given linearly independent vectors.

noncomputable def gramSchmidtBasis {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (b : Basis ι 𝕜 E) :
Basis ι 𝕜 E

When given a basis, gramSchmidt produces a basis.

Instances For
theorem coe_gramSchmidtBasis {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : 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} [] [] {ι : 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.)

Instances For
theorem gramSchmidtNormed_unit_length_coe {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (n : ι) (h₀ : LinearIndependent 𝕜 (f Subtype.val)) :
theorem gramSchmidtNormed_unit_length {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (n : ι) (h₀ : ) :
theorem gramSchmidtNormed_unit_length' {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} {n : ι} (hn : 0) :
theorem gramSchmidt_orthonormal {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] {f : ιE} (h₀ : ) :
Orthonormal 𝕜 ()

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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) :
Orthonormal 𝕜 fun 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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) (s : Set ι) :
Submodule.span 𝕜 ( '' s) = Submodule.span 𝕜 ( '' s)
theorem span_gramSchmidtNormed_range {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] (f : ιE) :
noncomputable def gramSchmidtOrthonormalBasis {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (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, 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.

Instances For
theorem gramSchmidtOrthonormalBasis_apply {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) {f : ιE} {i : ι} (hi : 0) :
↑() i =
theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) {f : ιE} (hf : Pairwise fun i j => inner (f i) (f j) = 0) {i : ι} (hi : f i 0) :
↑() i = (f i)⁻¹ f i
theorem inner_gramSchmidtOrthonormalBasis_eq_zero {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) {f : ιE} {i : ι} (hi : = 0) (j : ι) :
inner (↑() i) (f j) = 0
theorem gramSchmidtOrthonormalBasis_inv_triangular {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) (f : ιE) {i : ι} {j : ι} (hij : i < j) :
inner (↑() j) (f i) = 0
theorem gramSchmidtOrthonormalBasis_inv_triangular' {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) (f : ιE) {i : ι} {j : ι} (hij : i < j) :
().repr (f i) j = 0
theorem gramSchmidtOrthonormalBasis_inv_blockTriangular {𝕜 : Type u_1} {E : Type u_2} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (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} [] [] {ι : Type u_3} [] [IsWellOrder ι fun x x_1 => x < x_1] [] [] (h : ) (f : ιE) [] :
= Finset.prod Finset.univ fun i => inner (↑() i) (f i)