OAI/Analysis/KadisonKastler/FiniteMatrixUnitBasis.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A Hilbert basis adapted to a full matrix system

A basis of one diagonal corner is transported by the matrix columns. This gives an explicit tensor-shaped basis on which every matrix unit has its standard action, the bridge needed for compatible finite matrix groups.

  1. def OAI.Generator.MatrixUnitSystem.initialHilbertSpace line 25
  2. instance OAI.Generator.MatrixUnitSystem.initialHilbertSpace_complete line 27
  3. theorem OAI.Generator.MatrixUnitSystem.initialHilbertSpace_fixed line 33
  4. def OAI.Generator.MatrixUnitSystem.initialCoordinate line 40
  5. def OAI.Generator.MatrixUnitSystem.initialColumn line 45
  6. theorem OAI.Generator.MatrixUnitSystem.initialColumn_apply line 49
  7. theorem OAI.Generator.MatrixUnitSystem.inner_initialColumns line 52
  8. theorem OAI.Generator.MatrixUnitSystem.sum_initialColumn_coordinate line 64
  9. def OAI.Generator.MatrixUnitSystem.adaptedVector line 75
  10. theorem OAI.Generator.MatrixUnitSystem.adaptedVector_orthonormal line 77
  11. theorem OAI.Generator.MatrixUnitSystem.adaptedVector_span line 85
  12. def OAI.Generator.MatrixUnitSystem.adaptedBasis line 98

    Source documentation

    The explicit basis obtained by transporting the initial-corner basis.

    def adaptedBasis : OrthonormalBasis (ι × κ) ℂ H :=
…
  13. theorem OAI.Generator.MatrixUnitSystem.adaptedBasis_apply line 102
  14. theorem OAI.Generator.MatrixUnitSystem.entry_adaptedBasis line 108

    Source documentation

    On the adapted basis the original matrix units act on the first index.

    theorem entry_adaptedBasis (i j k : ι) (r : κ) :
    E.entry i j (E.adaptedBasis o b (k, r)) =
      if j = k then E.adaptedBasis o b (i, r) else 0 := by
…