mathlib3 documentation

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 #

noncomputable def gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (n : ι) :
gram_schmidt 𝕜 f n = f n - (finset.Iio n).sum (λ (i : ι), ((orthogonal_projection (submodule.span 𝕜 {gram_schmidt 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (n : ι) :
f n = gram_schmidt 𝕜 f n + (finset.Iio n).sum (λ (i : ι), ((orthogonal_projection (submodule.span 𝕜 {gram_schmidt 𝕜 f i})) (f n)))
theorem gram_schmidt_def'' (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (n : ι) :
f n = gram_schmidt 𝕜 f n + (finset.Iio n).sum (λ (i : ι), (has_inner.inner (gram_schmidt 𝕜 f i) (f n) / gram_schmidt 𝕜 f i ^ 2) gram_schmidt 𝕜 f i)
@[simp]
theorem gram_schmidt_zero (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order ι] [order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) :
theorem gram_schmidt_orthogonal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) {a b : ι} (h₀ : a b) :
has_inner.inner (gram_schmidt 𝕜 f a) (gram_schmidt 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) :
pairwise (λ (a b : ι), has_inner.inner (gram_schmidt 𝕜 f a) (gram_schmidt 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (v : ι E) {i j : ι} (hij : i < j) :
has_inner.inner (gram_schmidt 𝕜 v j) (v i) = 0
theorem mem_span_gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) {i j : ι} (hij : i j) :
theorem gram_schmidt_mem_span (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) {j i : ι} :
i j gram_schmidt 𝕜 f i submodule.span 𝕜 (f '' set.Iic j)
theorem span_gram_schmidt_Iic (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (c : ι) :
theorem span_gram_schmidt_Iio (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (c : ι) :
theorem span_gram_schmidt (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) :

gram_schmidt preserves span of vectors.

theorem gram_schmidt_of_orthogonal (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (hf : pairwise (λ (i j : ι), has_inner.inner (f i) (f j) = 0)) :
gram_schmidt 𝕜 f = f
theorem gram_schmidt_ne_zero_coe {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (n : ι) (h₀ : linear_independent 𝕜 (f coe)) :
gram_schmidt 𝕜 f n 0
theorem gram_schmidt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (n : ι) (h₀ : linear_independent 𝕜 f) :
gram_schmidt 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {i j : ι} (hij : i < j) (b : basis ι 𝕜 E) :
((b.repr) (gram_schmidt 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (h₀ : linear_independent 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (b : basis ι 𝕜 E) :
basis ι 𝕜 E

When given a basis, gram_schmidt produces a basis.

Equations
noncomputable def gram_schmidt_normed (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (n : ι) (h₀ : linear_independent 𝕜 (f coe)) :
theorem gram_schmidt_normed_unit_length {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (n : ι) (h₀ : linear_independent 𝕜 f) :
theorem gram_schmidt_normed_unit_length' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} {n : ι} (hn : gram_schmidt_normed 𝕜 f n 0) :
theorem gram_schmidt_orthonormal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] {f : ι E} (h₀ : linear_independent 𝕜 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) :
orthonormal 𝕜 (λ (i : {i : ι | gram_schmidt_normed 𝕜 f i 0}), gram_schmidt_normed 𝕜 f 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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] (f : ι E) (s : set ι) :
noncomputable def gram_schmidt_orthonormal_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] [fintype ι] [finite_dimensional 𝕜 E] (h : finite_dimensional.finrank 𝕜 E = fintype.card ι) (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.

Equations
theorem gram_schmidt_orthonormal_basis_apply_of_orthogonal {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] [fintype ι] [finite_dimensional 𝕜 E] (h : finite_dimensional.finrank 𝕜 E = fintype.card ι) {f : ι E} (hf : pairwise (λ (i j : ι), has_inner.inner (f i) (f j) = 0)) {i : ι} (hi : f i 0) :
theorem gram_schmidt_orthonormal_basis_inv_triangular' {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι : Type u_3} [linear_order ι] [locally_finite_order_bot ι] [is_well_order ι has_lt.lt] [fintype ι] [finite_dimensional 𝕜 E] (h : finite_dimensional.finrank 𝕜 E = fintype.card ι) (f : ι E) {i j : ι} (hij : i < j) :

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.