OAI/Analysis/KadisonKastler/ModularOrbitCommutant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Modular orbits of polar-conjugated commutant elements

The bounded equation and strip-average separation give the inclusion on every orbit. The reverse inclusion is the previously proved polar duality.

  1. theorem OAI.KadisonKastler.modularOrbit_polar_commutant_selfAdjoint_mem line 23
  2. theorem OAI.KadisonKastler.modularOrbit_polar_commutant_mem line 54
  3. theorem OAI.KadisonKastler.tomitaPolarConjugation_commutant_eq line 72