OAI/Analysis/KadisonKastler/TomitaCentralizerGraph.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.vectorState_star line 14
2. theorem OAI.KadisonKastler.vectorState_centralizer_star line 20
3. theorem OAI.KadisonKastler.tomita_centralizer_coefficient line 32
4. theorem OAI.KadisonKastler.rescaledGraphProjection_centralizer line 50

   Source documentation

   The graph resolvent acts as one half on every vector-state centralizer vector.

   theorem rescaledGraphProjection_centralizer (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (r : Algebra M)
       (hr : ∀ a : Algebra M,
         inner ℂ Ω ((r.val * a.val) Ω) = inner ℂ Ω ((a.val * r.val) Ω)) :
       rescaledGraphProjection M J Ω 1 (Generator.tupleSingle 0 (r.val Ω)) =
         (1 / 2 : ℂ) • rescaledGraphVector J Ω 1 r.val := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphProjection, OAI.Generator.tupleSingle, OAI.KadisonKastler.rescaledGraphVector

5. theorem OAI.KadisonKastler.graphResolvent_centralizer line 78