OAI/Analysis/KadisonKastler/StateScalingGraph.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

State scaling in the closed Tomita graph

A state-scaling operator gives an exact eigenvector of the bounded graph resolvent. This identifies its modular square-root ratio without any unbounded-operator domain convention.

  1. theorem OAI.KadisonKastler.StateScales.tomita_coefficient line 22
  2. theorem OAI.KadisonKastler.StateScales.graphProjection line 40
  3. theorem OAI.KadisonKastler.StateScales.graphResolvent line 72
  4. theorem OAI.KadisonKastler.StateScales.polarCoordinates line 77