OAI/Analysis/BoundedHochschild/CompletelyPositiveCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space compression preserves complete positivity.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.operatorMatrix_nonneg_of_quadratic line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.compressCompletelyPositive line 35
  3. lemma OAI.BoundedHochschild.KadisonRingrose.compressCompletelyPositive_apply line 48