OAI/Analysis/BoundedHochschild/CompletelyPositiveNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The norm bound supplied by the constructed Stinespring factorization.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringEmbedding_norm_le line 16
  2. theorem OAI.BoundedHochschild.KadisonRingrose.completelyPositive_norm_apply_le line 21
  3. def OAI.BoundedHochschild.KadisonRingrose.completelyPositiveContinuous line 41
  4. lemma OAI.BoundedHochschild.KadisonRingrose.completelyPositiveContinuous_apply line 45
  5. lemma OAI.BoundedHochschild.KadisonRingrose.completelyPositiveContinuous_norm_le line 49