OAI/Analysis/Nuclearity/NuclearCommutingRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The commuting representation of the minimal tensor product supplied by the nuclear matrix approximation. No tensor norm uniqueness is assumed.

  1. def OAI.WeakPureInfiniteness.commutingProductPolynomial line 17
  2. lemma OAI.WeakPureInfiniteness.commutingProductPolynomial_bound line 21
  3. def OAI.WeakPureInfiniteness.commutingMinimalLinear line 31
  4. lemma OAI.WeakPureInfiniteness.commutingMinimalLinear_polynomial line 35
  5. lemma OAI.WeakPureInfiniteness.commutingMinimalLinear_elementary line 42
  6. lemma OAI.WeakPureInfiniteness.commutingMinimalLinear_mul line 48
  7. lemma OAI.WeakPureInfiniteness.commutingMinimalLinear_star line 71
  8. def OAI.WeakPureInfiniteness.nuclearCommutingRepresentation line 98