OAI/Analysis/KadisonKastler/ProjectionPinchedStateProperties.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positivity and faithfulness of the pinched vector state

  1. theorem OAI.KadisonKastler.projectionPinchedState_star_mul_self line 16
  2. theorem OAI.KadisonKastler.projectionPinchedState_positive line 23
  3. theorem OAI.KadisonKastler.projectionPinchedState_one line 28
  4. theorem OAI.KadisonKastler.projectionPinchedState_faithful line 35
  5. theorem OAI.KadisonKastler.projectionPinchedState_centralizes line 49
  6. theorem OAI.KadisonKastler.projectionPinchedState_norm_le line 62