OAI/Analysis/KadisonKastler/FullCopyHilbertSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Full projection copies identify the countable Hilbert amplification

  1. def OAI.KadisonKastler.CountableProjectionCopies.fullCopyIsometry line 22
  2. theorem OAI.KadisonKastler.CountableProjectionCopies.fullCopyIsometry_orthogonal line 27
  3. theorem OAI.KadisonKastler.CountableProjectionCopies.fullCopyIsometry_total line 49
  4. theorem OAI.KadisonKastler.CountableProjectionCopies.fullCopyHilbertSum line 63
  5. def OAI.KadisonKastler.CountableProjectionCopies.fullCopyUnitary line 66
  6. theorem OAI.KadisonKastler.CountableProjectionCopies.fullCopyUnitary_single line 69
  7. theorem OAI.KadisonKastler.CountableProjectionCopies.fullCopyUnitary_intertwines line 73