OAI/Analysis/KadisonKastler/CountableOperatorEntries.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Entries of operators on a countable Hilbert sum

Entrywise identities detect equality and diagonal commutation. Under the countable tensor unitary, tensoring an operator on the sum tensors each of its entries. No summability of the operator's matrix is assumed.

  1. def OAI.KadisonKastler.countableOperatorEntry line 21
  2. theorem OAI.KadisonKastler.countableOperatorEntry_apply line 25
  3. theorem OAI.KadisonKastler.countableOperator_ext line 29
  4. theorem OAI.KadisonKastler.countableOperatorEntry_diagonal_mul line 50
  5. theorem OAI.KadisonKastler.countableOperatorEntry_mul_diagonal line 56
  6. theorem OAI.KadisonKastler.countableOperator_commutes_diagonal_iff line 62
  7. theorem OAI.KadisonKastler.countableTensorVector_single line 78
  8. theorem OAI.KadisonKastler.countableTensorEquiv_symm_single line 87
  9. theorem OAI.KadisonKastler.countableOperatorEntry_spatialLeft line 97