mathlib documentation

analysis.inner_product_space.gram_schmidt_ortho

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 #

TODO #

Construct a version with an orthonormal basis from Gram-Schmidt process.

noncomputable def gram_schmidt (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [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)))
@[simp]
theorem gram_schmidt_zero (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [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 mem_span_gram_schmidt (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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_ne_zero_coe (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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
theorem coe_gram_schmidt_basis (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] {ΞΉ : Type u_3} [linear_order ΞΉ] [locally_finite_order_bot ΞΉ] [is_well_order ΞΉ has_lt.lt] (b : basis ΞΉ π•œ E) :
noncomputable def gram_schmidt_normed (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [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_orthonormal (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 produces an orthornormal system of vectors.

theorem span_gram_schmidt_normed (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [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 π•œ] [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 π•œ] [inner_product_space π•œ E] {ΞΉ : Type u_3} [linear_order ΞΉ] [locally_finite_order_bot ΞΉ] [is_well_order ΞΉ has_lt.lt] [fintype ΞΉ] (b : basis ΞΉ π•œ E) :
orthonormal_basis ΞΉ π•œ E

When given a basis, gram_schmidt_normed produces an orthonormal basis.

Equations