OAI/Analysis/KadisonKastler/DiagonalPairAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The diagonal algebra on two Hilbert copies

Weak compactness shows that duplicating a represented von Neumann algebra already has weakly closed range. This is the ambient algebra for two vector states of the same represented algebra.

  1. def OAI.KadisonKastler.diagonalPairHom line 23
  2. theorem OAI.KadisonKastler.diagonalPairHom_injective line 27
  3. theorem OAI.KadisonKastler.diagonalPairHom_norm line 36
  4. theorem OAI.KadisonKastler.diagonalPairHom_tendsto_weak line 40
  5. def OAI.KadisonKastler.diagonalPairAlgebra line 51
  6. theorem OAI.KadisonKastler.diagonalPairHom_surjective_unitBall line 54
  7. theorem OAI.KadisonKastler.diagonalPairHom_surjective line 88
  8. def OAI.KadisonKastler.diagonalPairEquiv line 102
  9. theorem OAI.KadisonKastler.diagonalPairEquiv_coe line 114