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_linearIndependent: if the input vectors of gramSchmidt are linearly independent, then so are the output vectors.
• gramSchmidt_ne_zero: if the input vectors of gramSchmidt are linearly independent, then the output vectors are non-zero.
• gramSchmidtBasis: the basis produced by the Gram-Schmidt process when given a basis as input
• gramSchmidtNormed: the normalized gramSchmidt process, 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 InnerProductSpace.gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (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.

theorem InnerProductSpace.gramSchmidt_def (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) (n : ι) : gramSchmidt 𝕜 f n = f n - ∑ i ∈ Finset.Iio n, (Submodule.span 𝕜 {gramSchmidt 𝕜 f i}).starProjection (f n)

This lemma uses ∑ i in instead of ∑ i :.

theorem InnerProductSpace.gramSchmidt_def' (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) (n : ι) : f n = gramSchmidt 𝕜 f n + ∑ i ∈ Finset.Iio n, (Submodule.span 𝕜 {gramSchmidt 𝕜 f i}).starProjection (f n)

theorem InnerProductSpace.gramSchmidt_def'' (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (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 InnerProductSpace.gramSchmidt_bot (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [WellFoundedLT ι] (f : ι → E) : gramSchmidt 𝕜 f ⊥ = f ⊥

@[simp]

theorem InnerProductSpace.gramSchmidt_zero (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (n : ι) : gramSchmidt 𝕜 0 n = 0

theorem InnerProductSpace.gramSchmidt_orthogonal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (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 InnerProductSpace.gramSchmidt_pairwise_orthogonal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (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 InnerProductSpace.gramSchmidt_inv_triangular (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (v : ι → E) {i j : ι} (hij : i < j) : inner 𝕜 (gramSchmidt 𝕜 v j) (v i) = 0

theorem InnerProductSpace.mem_span_gramSchmidt (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) {i j : ι} (hij : i ≤ j) : f i ∈ Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

@[irreducible]

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

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

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

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

gramSchmidt preserves span of vectors.

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

If given an orthogonal set of vectors, gramSchmidt fixes its input.

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

theorem InnerProductSpace.gramSchmidt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {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 InnerProductSpace.gramSchmidt_triangular {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {i j : ι} (hij : i < j) (b : Module.Basis ι 𝕜 E) : (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0

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

theorem InnerProductSpace.gramSchmidt_linearIndependent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {f : ι → E} (h₀ : LinearIndependent 𝕜 f) : LinearIndependent 𝕜 (gramSchmidt 𝕜 f)

gramSchmidt produces linearly independent vectors when given linearly independent vectors.

noncomputable def InnerProductSpace.gramSchmidtBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (b : Module.Basis ι 𝕜 E) : Module.Basis ι 𝕜 E

When given a basis, gramSchmidt produces a basis.

theorem InnerProductSpace.coe_gramSchmidtBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (b : Module.Basis ι 𝕜 E) : ⇑(gramSchmidtBasis b) = gramSchmidt 𝕜 ⇑b

noncomputable def InnerProductSpace.gramSchmidtNormed (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) (n : ι) : E

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

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

theorem InnerProductSpace.gramSchmidtNormed_unit_length {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 f) : ‖gramSchmidtNormed 𝕜 f n‖ = 1

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

theorem InnerProductSpace.gramSchmidtNormed_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {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.

@[deprecated InnerProductSpace.gramSchmidtNormed_orthonormal (since := "2025-07-10")]

theorem InnerProductSpace.gramSchmidt_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {f : ι → E} (h₀ : LinearIndependent 𝕜 f) : Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f)

Alias of InnerProductSpace.gramSchmidtNormed_orthonormal.

---

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

theorem InnerProductSpace.gramSchmidtNormed_orthonormal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (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.

@[deprecated InnerProductSpace.gramSchmidtNormed_orthonormal' (since := "2025-07-10")]

theorem InnerProductSpace.gramSchmidt_orthonormal' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) : Orthonormal 𝕜 fun (i : ↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0}) => gramSchmidtNormed 𝕜 f ↑i

Alias of InnerProductSpace.gramSchmidtNormed_orthonormal'.

---

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

theorem InnerProductSpace.span_gramSchmidtNormed {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) (s : Set ι) : Submodule.span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = Submodule.span 𝕜 (gramSchmidt 𝕜 f '' s)

theorem InnerProductSpace.span_gramSchmidtNormed_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] (f : ι → E) : Submodule.span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = Submodule.span 𝕜 (Set.range (gramSchmidt 𝕜 f))

theorem InnerProductSpace.gramSchmidtNormed_linearIndependent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {f : ι → E} (h₀ : LinearIndependent 𝕜 f) : LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f)

gramSchmidtNormed produces linearly independent vectors when given linearly independent vectors.

noncomputable def InnerProductSpace.gramSchmidtOrthonormalBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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.

theorem InnerProductSpace.gramSchmidtOrthonormalBasis_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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 InnerProductSpace.gramSchmidtOrthonormalBasis_det {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] [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)