gramSchmidt_triangular
theorem gramSchmidt_triangular :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] {i j : ΞΉ},
i < j β β (b : Basis ΞΉ π E), (b.repr (gramSchmidt π (βb) i)) j = 0
This theorem, `gramSchmidt_triangular`, states that for any types `π` and `E`, where `π` is a ring-conjugate-like structure and `E` is a normed add commutative group with an inner product space over `π`, and any type `ΞΉ` with linear order and locally finite order bot, and which is well ordered, if `i` and `j` are elements of `ΞΉ` such that `i < j`, then for any basis `b` of type `Basis ΞΉ π E`, the `j`-th component of the representation of the `i`-th vector in the Gram-Schmidt process applied to the function from `ΞΉ` to `π` induced by the basis `b` is zero. In other words, the theorem asserts that the Gram-Schmidt process produces a triangular matrix of vectors when given a basis.
More concisely: Given a ring-conjugate-like structure `π`, a normed add commutative group `E` with an inner product over `π`, and a well-ordered, locally finite type `ΞΉ` with basis `b`, the Gram-Schmidt process applied to the function induced by `b` results in a triangular matrix.
|
span_gramSchmidt
theorem span_gramSchmidt :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E),
Submodule.span π (Set.range (gramSchmidt π f)) = Submodule.span π (Set.range f)
The theorem `span_gramSchmidt` states that for any scalar field `π`, a type `E` that is a normed additive commutative group and an inner product space over `π`, a type `ΞΉ` that is a linear order, a locally finite order with a least element, and a well order, and a function `f` from `ΞΉ` to `E`, the span of the set of vectors produced by the Gram-Schmidt process applied to `f` (denoted as `gramSchmidt π f`) is equal to the span of the set of vectors produced by `f`. In other words, the Gram-Schmidt process preserves the span of a set of vectors.
More concisely: Given a scalar field `π`, a normed additive commutative group and inner product space `E` over `π`, a locally finite order `ΞΉ` with a least element and well order, and a function `f` from `ΞΉ` to `E`, the span of `gramSchmidt π f` equals the span of `{f i | i β ΞΉ}`.
|
gramSchmidt_orthonormal'
theorem gramSchmidt_orthonormal' :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E), Orthonormal π fun i => gramSchmidtNormed π f βi
The theorem named "Gram-Schmidt Orthonormalization" states that for any field `π` and vector spaces `E` over `π`, given a function `f` mapping from an index set `ΞΉ` to `E` which respects a linear order and local finiteness condition, the function `gramSchmidtNormed` produces an orthonormal set of vectors when applied to `f`. Here, orthonormal means that each vector has unit length and any pair of distinct vectors are orthogonal. The vectors that become zero during the Gram-Schmidt process are removed from this set.
More concisely: Given a function mapping an ordered index set to a vector space over a field, under certain conditions, the Gram-Schmidt process produces an orthonormal set of non-zero vectors.
|
gramSchmidtOrthonormalBasis_inv_blockTriangular
theorem gramSchmidtOrthonormalBasis_inv_blockTriangular :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] [inst_6 : Fintype ΞΉ] [inst_7 : FiniteDimensional π E]
(h : FiniteDimensional.finrank π E = Fintype.card ΞΉ) (f : ΞΉ β E),
((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id
The theorem `gramSchmidtOrthonormalBasis_inv_blockTriangular` states that for a given indexed family of vectors `f : ΞΉ β E` in an inner product space `E`, where the size of the index set is the same as the dimension of `E`, the matrix of coefficients of `f` with respect to the orthonormal basis constructed from `f` using the Gram-Schmidt process is an upper-triangular matrix. The index set `ΞΉ` is assumed to have a finite number of elements and a linear order that is locally finite at the bottom, well-ordered by the strict less-than relation, and the inner product space `E` is finite-dimensional over the scalar field `π`.
More concisely: Given an indexed family `f : ΞΉ β E` of vectors in a finite-dimensional inner product space `E` over a scalar field `π`, the matrix of coefficients of `f` with respect to the orthonormal basis obtained by Gram-Schmidt process is upper-triangular.
|
gramSchmidt_orthogonal
theorem gramSchmidt_orthogonal :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E) {a b : ΞΉ},
a β b β βͺgramSchmidt π f a, gramSchmidt π f bβ«_π = 0
The **Gram-Schmidt Orthogonalisation** theorem states that for any type π, a given type E that is a NormedAddCommGroup and an InnerProductSpace over π, and any type ΞΉ that is a linearly ordered and locally finite ordered set with a well-defined ordering function, the `gramSchmidt` function produces an orthogonal system of vectors for any function f from ΞΉ to E. In other words, for any two different elements a and b in ΞΉ, the inner product of the vectors produced by applying `gramSchmidt` to a and b is equal to zero, indicating that these vectors are orthogonal.
More concisely: For any normed vector space E over a normed field π and any linearly ordered and locally finite index set ΞΉ, the Gram-Schmidt process constructs an orthogonal system of vectors in E from the given set.
|
gramSchmidt_def
theorem gramSchmidt_def :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E) (n : ΞΉ),
gramSchmidt π f n =
f n - (Finset.Iio n).sum fun i => β((orthogonalProjection (Submodule.span π {gramSchmidt π f i})) (f n))
This theorem, named `gramSchmidt_def`, defines the Gram-Schmidt process in the context of an inner product space over a field `π` and a normed add commutative group `E`. The Gram-Schmidt process forms an orthonormal basis from a basis of the space. Given a linearly ordered, well-ordered set of indices `ΞΉ`, a function `f` from `ΞΉ` to `E`, and an index `n` from `ΞΉ`, the lemma states that the `n`-th step of the Gram-Schmidt process applied to `f` gives `f n` minus the sum (over all indices less than `n`) of the orthogonal projection of `f n` onto the subspace spanned by the `i`-th step of the Gram-Schmidt process applied to `f`. The sum uses the "β i in" notation rather than "β i :", indicating summation over a finite set of indices rather than all indices.
More concisely: Given a linearly ordered, well-ordered set of indices `ΞΉ`, a function `f` from `ΞΉ` to an inner product space over a field `π` and a normed add commutative group `E`, the `n`-th step of the Gram-Schmidt process applied to `f` is `f n` minus the sum (over indices `i` less than `n`) of the orthogonal projection of `f n` onto the subspace spanned by the previous Gram-Schmidt steps.
|
gramSchmidt_mem_span
theorem gramSchmidt_mem_span :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E) {j i : ΞΉ},
i β€ j β gramSchmidt π f i β Submodule.span π (f '' Set.Iic j)
The theorem `gramSchmidt_mem_span` states that for any type `π` which behaves like a real closed field, `E` which forms a normed additive commutative group and an inner product space over `π`, and an index type `ΞΉ` that has a linear order, a locally finite order at bottom and a well order, given a function `f` from `ΞΉ` to `E` and two indices `i` and `j` from `ΞΉ`, if `i` is less than or equal to `j`, then the result of applying the Gram-Schmidt process to the function `f` at index `i` is an element of the smallest submodule of `E` over `π` that contains the image of the function `f` over the interval from negative infinity to `j` (inclusive). In other words, each vector obtained from the Gram-Schmidt process is in the linear span of the set of function outputs indexed by values less than or equal to `j`.
More concisely: For any real closed field `π`, normed additive commutative group and inner product space `E` over `π`, and orderable index type `ΞΉ`, if `f` is a function from `ΞΉ` to `E`, then for all `i β€ j` in `ΞΉ`, the vector obtained from the Gram-Schmidt process of `f` at index `i` is in the span of the first `j+1` function outputs.
|
gramSchmidt_linearIndependent
theorem gramSchmidt_linearIndependent :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] {f : ΞΉ β E},
LinearIndependent π f β LinearIndependent π (gramSchmidt π f)
The theorem `gramSchmidt_linearIndependent` states that for any type π, if π behaves like a field and has a defined concept of an inner product, and for any type E, if E is a normed additive commutative group and forms an inner product space over π, then the Gram-Schmidt process, when applied to a linearly independent family of vectors `f : ΞΉ β E`, will produce a new family of vectors that are also linearly independent over π. This holds for any type ΞΉ, if ΞΉ has a linear order, a locally finite order at the bottom, and a well-order where one element is less than the other.
More concisely: If π is a field with an inner product, E is a normed additive commutative group over π forming an inner product space, and `f : ΞΉ β E` is a linearly independent family of vectors in E where ΞΉ is a type with a linear order, a locally finite order at the bottom, and a well-order, then the Gram-Schmidt process applied to `f` produces a linearly independent family of vectors over π.
|
gramSchmidt_orthonormal
theorem gramSchmidt_orthonormal :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] {f : ΞΉ β E},
LinearIndependent π f β Orthonormal π (gramSchmidtNormed π f)
The Gram-Schmidt Orthonormalization theorem states that for any type π with real or complex-like properties and any normed additive commutative group E with an inner product space structure over π, given a linearly independent set of vectors (defined by a function `f` mapping from type ΞΉ to E), the normalized version of the Gram-Schmidt process (`gramSchmidtNormed`) when applied to `f`, results in an orthonormal system of vectors. Here, an orthonormal system of vectors in an inner product space is defined as a set of vectors where each vector has a norm of 1, and the inner product of any two distinct vectors is zero.
More concisely: For any real or complex normed additive commutative group with an inner product structure and a linearly independent set of vectors, the Gram-Schmidt process produces an orthonormal set of vectors with equal norm 1.
|
gramSchmidt_ne_zero
theorem gramSchmidt_ne_zero :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] {f : ΞΉ β E} (n : ΞΉ),
LinearIndependent π f β gramSchmidt π f n β 0
The theorem `gramSchmidt_ne_zero` asserts that given a family of vectors `f` indexed by `ΞΉ` in an inner product space `E` over a field `π`, if `f` is linearly independent, then the vectors produced by the Gram-Schmidt process (as denoted by `gramSchmidt π f n`) are nonzero. The inner product space, the field, and the index set `ΞΉ` are abstract and can be any types that meet the requirements (normed add commutative group, RC-like structure, linear order, locally finite order bot, and well-order respectively). The Gram-Schmidt process is a method for orthonormalizing a set of vectors in an inner product space.
More concisely: Given a linearly independent family of vectors `f` in an inner product space over a field, the Gram-Schmidt process produces a set of nonzero vectors.
|
gramSchmidt_pairwise_orthogonal
theorem gramSchmidt_pairwise_orthogonal :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E),
Pairwise fun a b => βͺgramSchmidt π f a, gramSchmidt π f bβ«_π = 0
The theorem `gramSchmidt_pairwise_orthogonal` states that for any type `π`, given certain conditions on `π` and the type `E` (namely, `π` must be a ring-like structure, `E` must be a normed additive commutative group, and `E` must have an inner product space structure over `π`), and any type `ΞΉ` (which must be a linearly ordered, locally finite ordered set with a well-ordering), if `f` is a function from `ΞΉ` to `E`, then the Gram-Schmidt process applied to `f` yields a family of elements in `E` such that any two different elements in the family are orthogonal. It means, the inner product of any two different elements from this sequence is zero. The inner product is taken with respect to `π`.
More concisely: Given a ring-like structure `π`, a normed additive commutative group `E` with an inner product space structure over `π`, and a linearly ordered, locally finite set `ΞΉ` with a well-order, the Gram-Schmidt process applied to a function `f` from `ΞΉ` to `E` yields a family of orthogonal elements.
|
mem_span_gramSchmidt
theorem mem_span_gramSchmidt :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
{ΞΉ : Type u_3} [inst_3 : LinearOrder ΞΉ] [inst_4 : LocallyFiniteOrderBot ΞΉ]
[inst_5 : IsWellOrder ΞΉ fun x x_1 => x < x_1] (f : ΞΉ β E) {i j : ΞΉ},
i β€ j β f i β Submodule.span π (gramSchmidt π f '' Set.Iic j)
The theorem `mem_span_gramSchmidt` states that for any type `π` that behaves like the real numbers, a normed additively commutative group `E` equipped with an inner product space over `π`, and an ordered type `ΞΉ` that has a lower bound and is well-ordered, given a function `f : ΞΉ β E` and two elements `i` and `j` of type `ΞΉ` such that `i` is less than or equal to `j`, then the value of the function `f` at `i` is in the span of the set of vectors obtained by applying the Gram-Schmidt orthogonalization process to the image of the function `f` over the interval of `ΞΉ` that includes all elements less than or equal to `j`. In simple terms, this theorem states that the `i`th vector (for `i` less than or equal to `j`) belongs to the linear space spanned by the Gram-Schmidt orthogonalization of all vectors up to the `j`th vector.
More concisely: For any type `π` behaving like the real numbers, any normed additively commutative group `E` with an inner product over `π`, and any well-ordered type `ΞΉ` with a lower bound, if `f : ΞΉ β E` is a function and `i β€ j` are elements of `ΞΉ`, then the `i`th vector `f i` is in the span of the Gram-Schmidt orthogonalization of `{f k | k β€ j}`.
|