OAI/Analysis/KadisonKastler/RowOperatorFactorization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Operator factorizations and their exact behavior under finite row averages. The representation is supplied by the proved Paulsen--Stinespring construction.

  1. theorem OAI.KadisonKastler.exists_row_operator_factorization line 30
  2. def OAI.KadisonKastler.representationRowAverage line 46
  3. theorem OAI.KadisonKastler.finiteRightAverage_operator_factorization line 51
  4. theorem OAI.KadisonKastler.representationRowAverage_comp line 68