OAI/Analysis/OperatorAlgebra/IntertwinerTensorCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Tensoring the actual commuting compression with the standard left action. The bound is uniform in the finite tensor being tested.

  1. def OAI.WeakPureInfiniteness.standardLeftFactor line 18
  2. def OAI.WeakPureInfiniteness.intertwinerOppositeCP line 29
  3. lemma OAI.WeakPureInfiniteness.intertwinerOppositeCP_cp line 38
  4. lemma OAI.WeakPureInfiniteness.intertwinerOppositeCP_norm_le line 48
  5. lemma OAI.WeakPureInfiniteness.intertwinerOppositeCP_evaluate line 61