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 processgram_schmidt_orthogonal:gram_schmidtproduces an orthogonal system of vectors.span_gram_schmidt:gram_schmidtpreserves span of vectors.gram_schmidt_ne_zero: If the input vectors ofgram_schmidtare 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 normalizedgram_schmidt(i.e each vector ingram_schmidt_normedhas unit length.)gram_schmidt_orthornormal:gram_schmidt_normedproduces 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 𝕜]
[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
- gram_schmidt 𝕜 f n = f n - finset.univ.sum (λ (i : ↥(finset.Iio n)), ↑(⇑(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 : ι) :
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) :
gram_schmidt 𝕜 f ⊥ = f ⊥
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) :
f i ∈ submodule.span 𝕜 (gram_schmidt 𝕜 f '' set.Iic 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 : ι) :
submodule.span 𝕜 (gram_schmidt 𝕜 f '' set.Iic c) = submodule.span 𝕜 (f '' set.Iic 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 : ι) :
submodule.span 𝕜 (gram_schmidt 𝕜 f '' set.Iio c) = submodule.span 𝕜 (f '' set.Iio 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) :
submodule.span 𝕜 (set.range (gram_schmidt 𝕜 f)) = submodule.span 𝕜 (set.range f)
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) :
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) :
linear_independent 𝕜 (gram_schmidt 𝕜 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
- gram_schmidt_basis b = basis.mk _ _
theorem
coe_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) :
⇑(gram_schmidt_basis b) = gram_schmidt 𝕜 ⇑b
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
- gram_schmidt_normed 𝕜 f n = (↑‖gram_schmidt 𝕜 f n‖)⁻¹ • gram_schmidt 𝕜 f n
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)) :
‖gram_schmidt_normed 𝕜 f n‖ = 1
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) :
‖gram_schmidt_normed 𝕜 f n‖ = 1
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) :
‖gram_schmidt_normed 𝕜 f n‖ = 1
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) :
orthonormal 𝕜 (gram_schmidt_normed 𝕜 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 ι) :
submodule.span 𝕜 (gram_schmidt_normed 𝕜 f '' s) = submodule.span 𝕜 (gram_schmidt 𝕜 f '' s)
theorem
span_gram_schmidt_normed_range
{𝕜 : 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) :
submodule.span 𝕜 (set.range (gram_schmidt_normed 𝕜 f)) = submodule.span 𝕜 (set.range (gram_schmidt 𝕜 f))
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) :
orthonormal_basis ι 𝕜 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 𝕜]
[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 : ι}
(hi : gram_schmidt_normed 𝕜 f i ≠ 0) :
⇑(gram_schmidt_orthonormal_basis h f) i = gram_schmidt_normed 𝕜 f i
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
inner_gram_schmidt_orthonormal_basis_eq_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]
[fintype ι]
[finite_dimensional 𝕜 E]
(h : finite_dimensional.finrank 𝕜 E = fintype.card ι)
{f : ι → E}
{i : ι}
(hi : gram_schmidt_normed 𝕜 f i = 0)
(j : ι) :
has_inner.inner (⇑(gram_schmidt_orthonormal_basis h f) i) (f j) = 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) :
has_inner.inner (⇑(gram_schmidt_orthonormal_basis h f) j) (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) :
⇑((gram_schmidt_orthonormal_basis h f).repr) (f i) j = 0
theorem
gram_schmidt_orthonormal_basis_inv_block_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) :
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 𝕜]
[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) :
⇑((gram_schmidt_orthonormal_basis h f).to_basis.det) f = finset.univ.prod (λ (i : ι), has_inner.inner (⇑(gram_schmidt_orthonormal_basis h f) i) (f i))