# mathlib3documentation

analysis.inner_product_space.gram_schmidt_ortho

# Gram-Schmidt Orthogonalization and Orthonormalization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• gram_schmidt : the Gram-Schmidt process
• gram_schmidt_orthogonal : gram_schmidt produces an orthogonal system of vectors.
• span_gram_schmidt : gram_schmidt preserves span of vectors.
• gram_schmidt_ne_zero : If the input vectors of gram_schmidt are linearly independent, then the output vectors are non-zero.
• gram_schmidt_basis : The basis produced by the Gram-Schmidt process when given a basis as input.
• gram_schmidt_normed : the normalized gram_schmidt (i.e each vector in gram_schmidt_normed has unit length.)
• gram_schmidt_orthornormal : gram_schmidt_normed produces an orthornormal system of vectors.
• gram_schmidt_orthonormal_basis: orthonormal basis constructed by the Gram-Schmidt process from an indexed set of vectors of the right size
noncomputable def gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) :
ι 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
theorem gram_schmidt_def (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (n : ι) :
f n = f n - (finset.Iio n).sum (λ (i : ι), ((orthogonal_projection f i})) (f n)))

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

theorem gram_schmidt_def' (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (n : ι) :
f n = f n + (finset.Iio n).sum (λ (i : ι), ((orthogonal_projection f i})) (f n)))
theorem gram_schmidt_def'' (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (n : ι) :
f n = f n + (finset.Iio n).sum (λ (i : ι), (has_inner.inner f i) (f n) / f i ^ 2) f i)
@[simp]
theorem gram_schmidt_zero (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [order_bot ι] (f : ι E) :
f = f
theorem gram_schmidt_orthogonal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) {a b : ι} (h₀ : a b) :
has_inner.inner f a) f b) = 0

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

theorem gram_schmidt_pairwise_orthogonal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) :
pairwise (λ (a b : ι), has_inner.inner f a) f b) = 0)

This is another version of gram_schmidt_orthogonal using pairwise instead.

theorem gram_schmidt_inv_triangular (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (v : ι E) {i j : ι} (hij : i < j) :
has_inner.inner v j) (v i) = 0
theorem mem_span_gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) {i j : ι} (hij : i j) :
f i f '' set.Iic j)
theorem gram_schmidt_mem_span (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) {j i : ι} :
i j f i (f '' set.Iic j)
theorem span_gram_schmidt_Iic (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (c : ι) :
f '' set.Iic c) = (f '' set.Iic c)
theorem span_gram_schmidt_Iio (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (c : ι) :
f '' set.Iio c) = (f '' set.Iio c)
theorem span_gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) :

gram_schmidt preserves span of vectors.

theorem gram_schmidt_of_orthogonal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (hf : pairwise (λ (i j : ι), has_inner.inner (f i) (f j) = 0)) :
f = f
theorem gram_schmidt_ne_zero_coe {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (n : ι) (h₀ : (f coe)) :
f n 0
theorem gram_schmidt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (n : ι) (h₀ : f) :
f n 0

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

theorem gram_schmidt_triangular {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {i j : ι} (hij : i < j) (b : 𝕜 E) :
((b.repr) b i)) j = 0

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

theorem gram_schmidt_linear_independent {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (h₀ : f) :
f)

gram_schmidt produces linearly independent vectors when given linearly independent vectors.

noncomputable def gram_schmidt_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (b : 𝕜 E) :
𝕜 E

When given a basis, gram_schmidt produces a basis.

Equations
theorem coe_gram_schmidt_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (b : 𝕜 E) :
noncomputable def gram_schmidt_normed (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (n : ι) :
E

the normalized gram_schmidt (i.e each vector in gram_schmidt_normed has unit length.)

Equations
theorem gram_schmidt_normed_unit_length_coe {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (n : ι) (h₀ : (f coe)) :
n = 1
theorem gram_schmidt_normed_unit_length {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (n : ι) (h₀ : f) :
n = 1
theorem gram_schmidt_normed_unit_length' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} {n : ι} (hn : n 0) :
n = 1
theorem gram_schmidt_orthonormal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] {f : ι E} (h₀ : f) :
f)

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

theorem gram_schmidt_orthonormal' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) :
(λ (i : {i : ι | i 0}), i)

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

theorem span_gram_schmidt_normed {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) (s : set ι) :
'' s) = f '' s)
theorem span_gram_schmidt_normed_range {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] (f : ι E) :
(set.range f)) = (set.range f))
noncomputable def gram_schmidt_orthonormal_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) (f : ι E) :
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
theorem gram_schmidt_orthonormal_basis_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) {f : ι E} {i : ι} (hi : i 0) :
= i
theorem gram_schmidt_orthonormal_basis_apply_of_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) {f : ι E} (hf : pairwise (λ (i j : ι), has_inner.inner (f i) (f j) = 0)) {i : ι} (hi : f i 0) :
= (f i)⁻¹ f i
theorem inner_gram_schmidt_orthonormal_basis_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) {f : ι E} {i : ι} (hi : i = 0) (j : ι) :
(f j) = 0
theorem gram_schmidt_orthonormal_basis_inv_triangular {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) (f : ι E) {i j : ι} (hij : i < j) :
(f i) = 0
theorem gram_schmidt_orthonormal_basis_inv_triangular' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) (f : ι E) {i j : ι} (hij : i < j) :
.repr) (f i) j = 0
theorem gram_schmidt_orthonormal_basis_inv_block_triangular {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ 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 gram_schmidt_orthonormal_basis constructed from f is upper-triangular.

theorem gram_schmidt_orthonormal_basis_det {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {ι : Type u_3} [linear_order ι] [fintype ι] [ E] (h : = ) (f : ι E) :
f = finset.univ.prod (λ (i : ι), (f i))