OAI/Analysis/BoundedHochschild/PositiveUnitBlocks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary two-by-two positivity test for a contraction.

  1. def OAI.BoundedHochschild.KadisonRingrose.positiveUnitBlock line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.positiveUnitBlock_nonneg line 19
  3. lemma OAI.BoundedHochschild.KadisonRingrose.norm_le_one_of_positiveUnitBlock line 43
  4. theorem OAI.BoundedHochschild.KadisonRingrose.positiveUnitBlock_nonneg_iff line 57