OAI/Analysis/KadisonKastler/NormalTwoStateSupports.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The right supports of the two summands in the two-state representation

  1. def OAI.KadisonKastler.twoStateSummandProjection line 24

    Source documentation

    The projection onto one of the two original representation summands.

    def twoStateSummandProjection (i : Fin 2) :
    TwoStateMatrixHilbert H K →L[ℂ] TwoStateMatrixHilbert H K :=
…

    Mentions: OAI.KadisonKastler.TwoStateMatrixHilbert

  2. theorem OAI.KadisonKastler.twoStateSummandProjection_mem_commutant line 29
  3. theorem OAI.KadisonKastler.twoStateSummandProjection_vector line 42
  4. theorem OAI.KadisonKastler.normalTwoStateProjection_star line 61
  5. theorem OAI.KadisonKastler.normalTwoStateProjection_conjugation line 69