OAI/Analysis/KadisonKastler/PositiveVectorPinching.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pinching positive vectors directly in the original representation

The matching two-sided cut preserves the positive cone and faithfulness, centralizes the chosen projection, and has exactly the original left-right projection gap as its displacement.

  1. theorem OAI.KadisonKastler.pairedProjectionCut_intertwines line 24
  2. def OAI.KadisonKastler.positiveVectorPinch line 37
  3. theorem OAI.KadisonKastler.positiveVectorPinch_eq line 44
  4. theorem OAI.KadisonKastler.positiveVectorPinch_norm_sub line 57
  5. theorem OAI.KadisonKastler.positiveVectorPinch_centralizes_projection line 72
  6. theorem OAI.KadisonKastler.positiveVectorPinch_mem_cone line 85
  7. theorem OAI.KadisonKastler.positiveVectorPinch_separating line 94