OAI/Analysis/BoundedHochschild/PaulsenEntries.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Recover the original linear map from the off-diagonal corner of its positive two-by-two extension.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.paulsen_single_mem line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenLinear_single line 26
  3. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenExtension_entry line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.single_offDiagonal_factor line 48
  5. lemma OAI.BoundedHochschild.KadisonRingrose.single_offDiagonal_norm_le_one line 55