OAI/Analysis/KadisonKastler/ModularGraphInvariance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Invariance of the full closed Tomita graph

Commutation with the graph square root and polar conjugation gives domain invariance for the constructed group on the full closed operator domain.

  1. theorem OAI.KadisonKastler.tomitaPolarConjugation_group_apply line 22
  2. theorem OAI.KadisonKastler.tomitaGraphRoot_group_apply line 35
  3. theorem OAI.KadisonKastler.modularStrongGroup_preserves_tomita_graph line 43
  4. theorem OAI.KadisonKastler.modularStrongGroup_preserves_tomita_domain line 55
  5. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_group_apply line 63