OAI/Analysis/KadisonKastler/ModularIsometryCorner.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Isometric coordinates in a two-sided modular corner

An algebra isometry induces an isometry on the Hilbert space by v J v J. Projection sandwiches intertwine both left and right actions, preserving the commutator norms used in projection refinement.

  1. def OAI.KadisonKastler.isometryProjectionImage line 25
  2. theorem OAI.KadisonKastler.isometryProjectionImage_nonzero line 35
  3. theorem OAI.KadisonKastler.isometryProjectionImage_le line 47
  4. theorem OAI.KadisonKastler.modularQuadratic_one line 57
  5. theorem OAI.KadisonKastler.modularQuadratic_isometry line 62
  6. theorem OAI.KadisonKastler.modularQuadratic_conjugation line 70
  7. theorem OAI.KadisonKastler.modularQuadratic_fixed line 78
  8. theorem OAI.KadisonKastler.isometry_sandwich_modular_left line 85
  9. theorem OAI.KadisonKastler.isometry_sandwich_modular_right line 98
  10. theorem OAI.KadisonKastler.isometry_sandwich_modular_defect line 105
  11. theorem OAI.KadisonKastler.isometry_sandwich_modular_defect_norm line 120
  12. theorem OAI.KadisonKastler.isometry_sandwich_modular_left_norm line 127