OAI/Analysis/KadisonKastler/TwoStateMatrixRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The two-state matrix representation

The first matrix column acts on the cyclic vector for the first state; the second column acts on the cyclic vector for the second state. Their direct sum represents the diagonal state on the two-by-two matrix algebra.

  1. abbrev OAI.KadisonKastler.TwoStateMatrixHilbert line 24
  2. def OAI.KadisonKastler.twoStateMatrixRepresentation line 28
  3. def OAI.KadisonKastler.twoStateMatrixVector line 34
  4. theorem OAI.KadisonKastler.twoStateMatrixVector_norm_sq line 38
  5. theorem OAI.KadisonKastler.twoStateMatrixRepresentation_vector_fst line 45
  6. theorem OAI.KadisonKastler.twoStateMatrixRepresentation_vector_snd line 52
  7. theorem OAI.KadisonKastler.twoStateMatrixRepresentation_separating line 59