OAI/Analysis/KadisonKastler/TomitaCoreCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded graph coordinates for algebraic Tomita vectors

Every algebra vector is the image of a concrete vector under the square root of the graph resolvent. Its adjoint vector uses the polar conjugate of the same coordinate. These are the two boundary data for the KMS strip.

  1. def OAI.KadisonKastler.tomitaCoreCoordinate line 21
  2. theorem OAI.KadisonKastler.tomitaCoreCoordinate_graph line 25
  3. theorem OAI.KadisonKastler.tomitaCoreCoordinate_first line 31
  4. theorem OAI.KadisonKastler.tomitaCoreCoordinate_adjoint line 38
  5. theorem OAI.KadisonKastler.tomitaCoreCoordinate_star line 48