OAI/Analysis/KadisonKastler/TomitaVectorProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The state vector in the Tomita graph

Projection of (Ω,0) onto the unscaled graph is exactly half of (Ω,JΩ). This elementary identity identifies the state vector for the polar construction.

  1. theorem OAI.KadisonKastler.tomita_state_coefficient line 18
  2. theorem OAI.KadisonKastler.rescaledGraphProjection_state line 25
  3. theorem OAI.KadisonKastler.graphResolvent_state line 52