OAI/Analysis/KadisonKastler/ModularCoreFiniteWindow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite frequency windows for every KMS implementation

Uniqueness of the modular implementation transfers the constructed finite projection to any strongly continuous normalizing KMS group of the given cyclic separating vector.

  1. theorem OAI.KadisonKastler.modularCore_unitWindow_finite line 30
  2. theorem OAI.KadisonKastler.modularFactorialCore_projectionSemifinite line 38