OAI/Analysis/BoundedHochschild/CompletelyBoundedArithmetic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite linear combinations and left multiplication in the input and output preserve the complete bounds needed to combine finitely many maps.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_add line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_sum line 22
  3. def OAI.BoundedHochschild.KadisonRingrose.leftSandwichMap line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.leftSandwichMap_apply line 38
  5. lemma OAI.BoundedHochschild.KadisonRingrose.matrix_scalar_mul_apply line 42
  6. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_leftSandwich line 47