OAI/Analysis/OperatorAlgebra/TracialMinimalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite tracial multiplication representation satisfies the actual minimal tensor norm bound. This uses its concrete spatial norm and the preceding cyclic-state argument, without assuming nuclearity of the algebra.

  1. lemma OAI.WeakPureInfiniteness.tracialSpatialTensor_completed_tmul line 18
  2. lemma OAI.WeakPureInfiniteness.tracialSpatialTensor_sum_norm_le_minimal line 29
  3. lemma OAI.WeakPureInfiniteness.tracialSpatialTensor_norm_le_minimal line 40