OAI/Analysis/KadisonKastler/OrthonormalMatrixUnits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Full matrix units from a finite orthonormal basis

  1. def OAI.Generator.orthonormalMatrixUnits line 17

    Source documentation

    The rank-one matrix units associated with an orthonormal basis.

    def orthonormalMatrixUnits (b : OrthonormalBasis ι ℂ H) : MatrixUnitSystem ι (H →L[ℂ] H) where
…

    Mentions: OAI.Generator.MatrixUnitSystem

  2. theorem OAI.Generator.orthonormalMatrixUnits_entry_apply line 29
  3. theorem OAI.Generator.orthonormalMatrixUnits_surjective line 34

    Source documentation

    These matrix units span all bounded operators on the finite Hilbert space.

    theorem orthonormalMatrixUnits_surjective (b : OrthonormalBasis ι ℂ H) :
    Function.Surjective (orthonormalMatrixUnits b).hom := by
…

    Mentions: OAI.Generator.orthonormalMatrixUnits