OAI/Analysis/KadisonKastler/StandardTracialPosition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete standard tracial position

A faithful vector trace and cyclicity suffice to construct the standard tracial conjugation. Its isometry and involution are proved rather than included in the common-position input.

  1. structure OAI.KadisonKastler.StandardTracialPosition line 20

    Source documentation

    The minimal concrete data for a standard tracial representation.

    structure StandardTracialPosition (M : VonNeumannAlgebra H) where
…
  2. theorem OAI.KadisonKastler.StandardTracialPosition.vector_norm line 30
  3. theorem OAI.KadisonKastler.StandardTracialPosition.vectorMap_norm line 39
  4. theorem OAI.KadisonKastler.StandardTracialPosition.finiteVectorTrace line 48
  5. theorem OAI.KadisonKastler.StandardTracialPosition.separating line 53
  6. def OAI.KadisonKastler.StandardTracialPosition.conjugation line 57

    Source documentation

    The standard conjugation, constructed from the actual vector trace.

    def conjugation : H ≃ₗᵢ⋆[ℂ] H :=
…
  7. theorem OAI.KadisonKastler.StandardTracialPosition.conjugation_algebraVector line 61
  8. theorem OAI.KadisonKastler.StandardTracialPosition.conjugation_involutive line 66
  9. theorem OAI.KadisonKastler.StandardTracialPosition.conjugation_vector line 71