OAI/Analysis/BoundedHochschild/EncodedMapFamilies.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal isometry columns encode finitely many maps into a single map. Each map is recovered using only input and output left multiplication.

  1. def OAI.BoundedHochschild.KadisonRingrose.encodeMapFamily line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.extract_encodeMapFamily line 21
  3. lemma OAI.BoundedHochschild.KadisonRingrose.encodeMapFamily_completelyBounded line 37