OAI/Analysis/KadisonKastler/RowPinching.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Projection rows give completely contractive idempotent averages.

  1. def OAI.KadisonKastler.projectionRow line 13
  2. theorem OAI.KadisonKastler.projectionRow_normalized line 15
  3. def OAI.KadisonKastler.projectionAverage line 20
  4. theorem OAI.KadisonKastler.projectionAverage_apply line 23
  5. theorem OAI.KadisonKastler.projectionAverage_module line 29
  6. theorem OAI.KadisonKastler.projectionAverage_fixed_iff line 36
  7. theorem OAI.KadisonKastler.projectionAverage_idempotent line 53
  8. theorem OAI.KadisonKastler.projectionAverage_fixed_one_sub line 57
  9. theorem OAI.KadisonKastler.finiteRightAverage_commute line 64
  10. theorem OAI.KadisonKastler.CompletelyBoundedBy.projectionAverage line 83