Theorems · Definition · functional analysis

InnerProductSpace.gramSchmidtOrthonormalBasis

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_3} →
            [inst_3 : LinearOrder ι] →
              [LocallyFiniteOrderBot ι] →
                [WellFoundedLT ι] →
                  [inst_6 : Fintype ι] →
                    [FiniteDimensional 𝕜 E] → Module.finrank 𝕜 E = Fintype.card ι → (ι → 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.

Defined in

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Cited by

11 results in Mathlib

Foundations

Depth 236 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceLinearOrderLocallyFiniteOrderBotWellFoundedLTFintypeFiniteDimensional