OAI/Analysis/KadisonKastler/ModularKMS.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The KMS condition for the constructed modular group

The graph coordinates give both boundary values of a bounded holomorphic strip. No normalization or commutant theorem is assumed here.

  1. theorem OAI.KadisonKastler.modularStrongGroup_kms line 22
  2. theorem OAI.KadisonKastler.modularStrongGroup_isModular line 40