OAI/Analysis/KadisonKastler/ModularPolarSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polar conjugation commutes with the constructed modular group

Conjugation exchanges R and 1-R. It therefore negates the real regularized logarithm, while also conjugating the imaginary scalar in its exponential. These two sign changes cancel.

  1. theorem OAI.KadisonKastler.regularizedModularLog_polar_conjugation line 23
  2. theorem OAI.KadisonKastler.regularizedModularGroup_polar_conjugation line 57
  3. theorem OAI.KadisonKastler.modularStrongGroup_polar_conjugation line 80