OAI/Analysis/BoundedHochschild/CompletelyBoundedFactorization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Factor a completely contractive map through an actual star representation.

  1. structure OAI.BoundedHochschild.KadisonRingrose.OperatorFactorization line 20
  2. theorem OAI.BoundedHochschild.KadisonRingrose.factorization_of_complete_contraction line 36
  3. theorem OAI.BoundedHochschild.KadisonRingrose.factorization_of_complete_bound line 80