OAI/Analysis/KadisonKastler/ModularSpatialTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial transport of the constructed modular group

Intertwining the bounded graph resolvent suffices: its continuous phase approximations intertwine, and so do their strong limits.

  1. theorem OAI.KadisonKastler.modularApproximation_spatial line 33
  2. theorem OAI.KadisonKastler.modularStrongGroup_spatial line 56