OAI/Analysis/KadisonKastler/PointedLocalMatrix.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The four-dimensional pointed matrix state

Left and right matrix multiplication act on the Hilbert space of two by two matrices. The square root of the diagonal density is cyclic for both actions. An orthonormal basis beginning at that vector makes the reference vector the zero-coordinate vacuum used by the infinite product.

  1. abbrev OAI.KadisonKastler.PointedLocalHilbert line 19
  2. def OAI.KadisonKastler.pointedLocalVacuum line 21
  3. structure OAI.KadisonKastler.PointedLocalMatrixData line 23
  4. abbrev OAI.KadisonKastler.PointedRawHilbert line 34
  5. def OAI.KadisonKastler.pointedRawLeft line 36
  6. theorem OAI.KadisonKastler.pointedRawLeft_apply line 42
  7. def OAI.KadisonKastler.pointedRawRight line 45
  8. theorem OAI.KadisonKastler.pointedRawRight_apply line 51
  9. theorem OAI.KadisonKastler.pointedRawLeft_star line 54
  10. theorem OAI.KadisonKastler.pointedRawRight_star line 63
  11. def OAI.KadisonKastler.pointedRawLeftUnits line 72
  12. def OAI.KadisonKastler.pointedRawRightUnits line 87
  13. theorem OAI.KadisonKastler.pointedRawUnits_commute line 102
  14. def OAI.KadisonKastler.pointedRawVacuum line 108
  15. theorem OAI.KadisonKastler.pointedRawVacuum_apply line 111
  16. theorem OAI.KadisonKastler.twoSiteWeight_pos line 115
  17. theorem OAI.KadisonKastler.twoSiteWeight_sum line 120
  18. theorem OAI.KadisonKastler.pointedRawLeft_vacuum line 125
  19. theorem OAI.KadisonKastler.pointedRawRight_vacuum line 134
  20. theorem OAI.KadisonKastler.pointedRawLeft_moment line 143
  21. theorem OAI.KadisonKastler.pointedRawVacuum_norm line 155
  22. theorem OAI.KadisonKastler.span_of_basis_mem line 164
  23. theorem OAI.KadisonKastler.pointedRawLeft_spans line 171
  24. theorem OAI.KadisonKastler.pointedRawRight_spans line 186
  25. theorem OAI.KadisonKastler.exists_pointedRaw_basis line 201
  26. theorem OAI.KadisonKastler.span_linearEquiv_image line 212
  27. theorem OAI.KadisonKastler.exists_pointedLocalMatrixData line 228

    Source documentation

    The two faithful matrix actions with the designated vacuum vector.

    theorem exists_pointedLocalMatrixData {ν : ℝ} (hν : 0 < ν) :
    Nonempty (PointedLocalMatrixData ν) := by
…

    Mentions: OAI.KadisonKastler.PointedLocalMatrixData