OAI/Analysis/KadisonKastler/PositiveConeProjectionSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projection supports of positive vectors

A projection kills a positive vector precisely when its matching left-right corner does. This proves that positive summands cannot cancel on a left support. No self-duality or state-representation theorem is assumed.

  1. theorem OAI.KadisonKastler.projection_pairing line 24
  2. theorem OAI.KadisonKastler.conjugation_projection line 33
  3. theorem OAI.KadisonKastler.positiveCone_projection_kills_of_corner_kills line 49
  4. theorem OAI.KadisonKastler.positiveCone_projection_kills_summands line 95