OAI/Analysis/KadisonSimilarity/Tracial/NormalTracialGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A tracial Hilbert geometry with faithful normal left range supplies the concrete vector-trace model used in the discharged tracial inputs.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_eq_vectorTrace line 21
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_identityVector line 25
  3. def OAI.KadisonSimilarity.TracialCornerGeometry.normalTracialRepresentation line 33
  4. theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalTracialRepresentation_vector line 58
  5. theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalTracialRepresentation_trace line 63