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

@[irreducible]

noncomputable def gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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

• gramSchmidt 𝕜 f n = f n - ∑ i : { x : ι // x ∈ Finset.Iio n }, ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 f ↑i})) (f n))

theorem gramSchmidt_def (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (n : ι) : gramSchmidt 𝕜 f n = f n - ∑ i ∈ Finset.Iio n, ↑((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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (n : ι) : f n = gramSchmidt 𝕜 f n + ∑ i ∈ Finset.Iio n, ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 f i})) (f n))

theorem gramSchmidt_def'' (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (n : ι) : f n = gramSchmidt 𝕜 f n + ∑ i ∈ Finset.Iio n, (inner (gramSchmidt 𝕜 f i) (f n) / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i

@[simp]

theorem gramSchmidt_zero (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) : gramSchmidt 𝕜 f ⊥ = f ⊥

theorem gramSchmidt_orthogonal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) {i : ι} {j : ι} (hij : i ≤ j) : f i ∈ Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

@[irreducible]

theorem gramSchmidt_mem_span (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) {j : ι} {i : ι} : i ≤ j → gramSchmidt 𝕜 f i ∈ Submodule.span 𝕜 (f '' Set.Iic j)

theorem span_gramSchmidt_Iic (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (c : ι) : Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic c) = Submodule.span 𝕜 (f '' Set.Iic c)

theorem span_gramSchmidt_Iio (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (c : ι) : Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio c) = Submodule.span 𝕜 (f '' Set.Iio c)

theorem span_gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) : Submodule.span 𝕜 (Set.range (gramSchmidt 𝕜 f)) = Submodule.span 𝕜 (Set.range f)

gramSchmidt preserves span of vectors.

theorem gramSchmidt_of_orthogonal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {f : ι → E} (hf : Pairwise fun (i j : ι) => inner (f i) (f j) = 0) : gramSchmidt 𝕜 f = f

theorem gramSchmidt_ne_zero_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)) : gramSchmidt 𝕜 f n ≠ 0

theorem gramSchmidt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (b : Basis ι 𝕜 E) : Basis ι 𝕜 E

When given a basis, gramSchmidt produces a basis.

Equations

• gramSchmidtBasis b = Basis.mk ⋯ ⋯

theorem coe_gramSchmidtBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (b : Basis ι 𝕜 E) : ⇑(gramSchmidtBasis b) = gramSchmidt 𝕜 ⇑b

noncomputable def gramSchmidtNormed (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (f : ι → E) (n : ι) : E

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

Equations

• gramSchmidtNormed 𝕜 f n = (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n

theorem gramSchmidtNormed_unit_length_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)) : ‖gramSchmidtNormed 𝕜 f n‖ = 1

theorem gramSchmidtNormed_unit_length {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 f) : ‖gramSchmidtNormed 𝕜 f n‖ = 1

theorem gramSchmidtNormed_unit_length' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {f : ι → E} {n : ι} (hn : gramSchmidtNormed 𝕜 f n ≠ 0) : ‖gramSchmidtNormed 𝕜 f n‖ = 1

theorem gramSchmidt_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] (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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (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

• gramSchmidtOrthonormalBasis h f = ⋯.choose

theorem gramSchmidtOrthonormalBasis_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E} {i : ι} (hi : gramSchmidtNormed 𝕜 f i ≠ 0) : (gramSchmidtOrthonormalBasis h f) i = gramSchmidtNormed 𝕜 f i

theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E} (hf : Pairwise fun (i j : ι) => inner (f i) (f j) = 0) {i : ι} (hi : f i ≠ 0) : (gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i

theorem inner_gramSchmidtOrthonormalBasis_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E} {i : ι} (hi : gramSchmidtNormed 𝕜 f i = 0) (j : ι) : inner ((gramSchmidtOrthonormalBasis h f) i) (f j) = 0

theorem gramSchmidtOrthonormalBasis_inv_triangular {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) {i : ι} {j : ι} (hij : i < j) : inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

theorem gramSchmidtOrthonormalBasis_inv_triangular' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) {i : ι} {j : ι} (hij : i < j) : (gramSchmidtOrthonormalBasis h f).repr (f i) j = 0

theorem gramSchmidtOrthonormalBasis_inv_blockTriangular {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) : ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id

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 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Fintype ι] [FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) [DecidableEq ι] : (gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i : ι, inner ((gramSchmidtOrthonormalBasis h f) i) (f i)