Documentation

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

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 #

noncomputable def gramSchmidt (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (n : ฮน) :
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
Instances For
    theorem gramSchmidt_def (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (n : ฮน) :
    gramSchmidt ๐•œ f n = f n - Finset.sum (Finset.Iio n) fun (i : ฮน) => โ†‘((orthogonalProjection (Submodule.span ๐•œ {gramSchmidt ๐•œ f i})) (f n))

    This lemma uses โˆ‘ i in instead of โˆ‘ i :.

    theorem gramSchmidt_def' (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (n : ฮน) :
    f n = gramSchmidt ๐•œ f n + Finset.sum (Finset.Iio n) fun (i : ฮน) => โ†‘((orthogonalProjection (Submodule.span ๐•œ {gramSchmidt ๐•œ f i})) (f n))
    theorem gramSchmidt_def'' (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (n : ฮน) :
    f n = gramSchmidt ๐•œ f n + Finset.sum (Finset.Iio n) fun (i : ฮน) => (โŸชgramSchmidt ๐•œ f i, f nโŸซ_๐•œ / โ†‘โ€–gramSchmidt ๐•œ f iโ€– ^ 2) โ€ข gramSchmidt ๐•œ f i
    @[simp]
    theorem gramSchmidt_zero (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_4} [LinearOrder ฮน] [LocallyFiniteOrder ฮน] [OrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) :
    theorem gramSchmidt_orthogonal (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) {a : ฮน} {b : ฮน} (hโ‚€ : a โ‰  b) :
    โŸชgramSchmidt ๐•œ f a, gramSchmidt ๐•œ f bโŸซ_๐•œ = 0

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

    theorem gramSchmidt_pairwise_orthogonal (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) :
    Pairwise fun (a b : ฮน) => โŸชgramSchmidt ๐•œ f a, gramSchmidt ๐•œ f bโŸซ_๐•œ = 0

    This is another version of gramSchmidt_orthogonal using pairwise instead.

    theorem gramSchmidt_inv_triangular (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (v : ฮน โ†’ E) {i : ฮน} {j : ฮน} (hij : i < j) :
    โŸชgramSchmidt ๐•œ v j, v iโŸซ_๐•œ = 0
    theorem mem_span_gramSchmidt (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) {i : ฮน} {j : ฮน} (hij : i โ‰ค j) :
    f i โˆˆ Submodule.span ๐•œ (gramSchmidt ๐•œ f '' Set.Iic j)
    theorem gramSchmidt_mem_span (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) {j : ฮน} {i : ฮน} :
    i โ‰ค j โ†’ gramSchmidt ๐•œ f i โˆˆ Submodule.span ๐•œ (f '' Set.Iic j)
    theorem span_gramSchmidt_Iic (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (c : ฮน) :
    Submodule.span ๐•œ (gramSchmidt ๐•œ f '' Set.Iic c) = Submodule.span ๐•œ (f '' Set.Iic c)
    theorem span_gramSchmidt_Iio (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (c : ฮน) :
    Submodule.span ๐•œ (gramSchmidt ๐•œ f '' Set.Iio c) = Submodule.span ๐•œ (f '' Set.Iio c)
    theorem span_gramSchmidt (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) :
    Submodule.span ๐•œ (Set.range (gramSchmidt ๐•œ f)) = Submodule.span ๐•œ (Set.range f)

    gramSchmidt preserves span of vectors.

    theorem gramSchmidt_of_orthogonal (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (hf : Pairwise fun (i j : ฮน) => โŸชf i, f jโŸซ_๐•œ = 0) :
    gramSchmidt ๐•œ f = f
    theorem gramSchmidt_ne_zero_coe {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (n : ฮน) (hโ‚€ : LinearIndependent (ฮน := { x : ฮน // x โˆˆ Set.Iic n }) ๐•œ (f โˆ˜ Subtype.val)) :
    gramSchmidt ๐•œ f n โ‰  0
    theorem gramSchmidt_ne_zero {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (n : ฮน) (hโ‚€ : LinearIndependent ๐•œ f) :
    gramSchmidt ๐•œ f n โ‰  0

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

    theorem gramSchmidt_triangular {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {i : ฮน} {j : ฮน} (hij : i < j) (b : Basis ฮน ๐•œ E) :
    (b.repr (gramSchmidt ๐•œ (โ‡‘b) i)) j = 0

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

    theorem gramSchmidt_linearIndependent {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (hโ‚€ : LinearIndependent ๐•œ f) :
    LinearIndependent ๐•œ (gramSchmidt ๐•œ f)

    gramSchmidt produces linearly independent vectors when given linearly independent vectors.

    noncomputable def gramSchmidtBasis {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (b : Basis ฮน ๐•œ E) :
    Basis ฮน ๐•œ E

    When given a basis, gramSchmidt produces a basis.

    Equations
    Instances For
      theorem coe_gramSchmidtBasis {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (b : Basis ฮน ๐•œ E) :
      โ‡‘(gramSchmidtBasis b) = gramSchmidt ๐•œ โ‡‘b
      noncomputable def gramSchmidtNormed (๐•œ : Type u_1) {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (n : ฮน) :
      E

      the normalized gramSchmidt (i.e each vector in gramSchmidtNormed has unit length.)

      Equations
      Instances For
        theorem gramSchmidtNormed_unit_length_coe {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (n : ฮน) (hโ‚€ : LinearIndependent (ฮน := { x : ฮน // x โˆˆ Set.Iic n }) ๐•œ (f โˆ˜ Subtype.val)) :
        theorem gramSchmidtNormed_unit_length {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (n : ฮน) (hโ‚€ : LinearIndependent ๐•œ f) :
        theorem gramSchmidtNormed_unit_length' {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} {n : ฮน} (hn : gramSchmidtNormed ๐•œ f n โ‰  0) :
        theorem gramSchmidt_orthonormal {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] {f : ฮน โ†’ E} (hโ‚€ : LinearIndependent ๐•œ f) :
        Orthonormal ๐•œ (gramSchmidtNormed ๐•œ f)

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

        theorem gramSchmidt_orthonormal' {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) :
        Orthonormal ๐•œ fun (i : โ†‘{i : ฮน | gramSchmidtNormed ๐•œ f i โ‰  0}) => gramSchmidtNormed ๐•œ f โ†‘i

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

        theorem span_gramSchmidtNormed {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) (s : Set ฮน) :
        Submodule.span ๐•œ (gramSchmidtNormed ๐•œ f '' s) = Submodule.span ๐•œ (gramSchmidt ๐•œ f '' s)
        theorem span_gramSchmidtNormed_range {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] (f : ฮน โ†’ E) :
        Submodule.span ๐•œ (Set.range (gramSchmidtNormed ๐•œ f)) = Submodule.span ๐•œ (Set.range (gramSchmidt ๐•œ f))
        noncomputable def gramSchmidtOrthonormalBasis {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) (f : ฮน โ†’ E) :
        OrthonormalBasis ฮน ๐•œ 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
        Instances For
          theorem gramSchmidtOrthonormalBasis_apply {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) {f : ฮน โ†’ E} {i : ฮน} (hi : gramSchmidtNormed ๐•œ f i โ‰  0) :
          theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) {f : ฮน โ†’ E} (hf : Pairwise fun (i j : ฮน) => โŸชf i, f jโŸซ_๐•œ = 0) {i : ฮน} (hi : f i โ‰  0) :
          theorem inner_gramSchmidtOrthonormalBasis_eq_zero {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) {f : ฮน โ†’ E} {i : ฮน} (hi : gramSchmidtNormed ๐•œ f i = 0) (j : ฮน) :
          โŸช(gramSchmidtOrthonormalBasis h f) i, f jโŸซ_๐•œ = 0
          theorem gramSchmidtOrthonormalBasis_inv_triangular {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) (f : ฮน โ†’ E) {i : ฮน} {j : ฮน} (hij : i < j) :
          โŸช(gramSchmidtOrthonormalBasis h f) j, f iโŸซ_๐•œ = 0
          theorem gramSchmidtOrthonormalBasis_inv_triangular' {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) (f : ฮน โ†’ E) {i : ฮน} {j : ฮน} (hij : i < j) :
          (gramSchmidtOrthonormalBasis h f).repr (f i) j = 0
          theorem gramSchmidtOrthonormalBasis_inv_blockTriangular {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.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 gramSchmidtOrthonormalBasis constructed from f is upper-triangular.

          theorem gramSchmidtOrthonormalBasis_det {๐•œ : Type u_1} {E : Type u_2} [IsROrC ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] {ฮน : Type u_3} [LinearOrder ฮน] [LocallyFiniteOrderBot ฮน] [IsWellOrder ฮน fun (x x_1 : ฮน) => x < x_1] [Fintype ฮน] [FiniteDimensional ๐•œ E] (h : FiniteDimensional.finrank ๐•œ E = Fintype.card ฮน) (f : ฮน โ†’ E) [DecidableEq ฮน] :
          (Basis.det (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f))) f = Finset.prod Finset.univ fun (i : ฮน) => โŸช(gramSchmidtOrthonormalBasis h f) i, f iโŸซ_๐•œ