OAI/Analysis/Nuclearity/NuclearCommutingBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A direct finite tensor norm bound for commuting representations of a nuclear nonunital algebra. The proof uses only its matrix CP approximations.

  1. lemma OAI.WeakPureInfiniteness.nuclear_matrix_coordinates_norm_le line 18
  2. theorem OAI.WeakPureInfiniteness.nuclear_commuting_sum_norm_le line 31