OAI/Analysis/KadisonKastler/TomitaVectorFixed.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The polar conjugation fixes the cyclic separating vector

  1. theorem OAI.KadisonKastler.positive_square_eigenvector line 15
  2. theorem OAI.KadisonKastler.tomitaGraphRoot_eigen line 41

    Source documentation

    Positive eigenvalues of the graph resolvent pass to its positive square root.

    theorem tomitaGraphRoot_eigen (J : H ≃ₗᵢ⋆[ℂ] H) (Ω x : H)
    {t : ℝ} (ht : 0 < t)
    (hx : graphResolvent M J Ω 1 x = (t : ℂ) • x) :
    tomitaGraphRoot (M := M) J Ω x = (Real.sqrt t : ℂ) • x := by
…

    Mentions: OAI.KadisonKastler.graphResolvent, OAI.KadisonKastler.tomitaGraphRoot

  3. theorem OAI.KadisonKastler.tomitaGraphRoot_half_eigen line 56
  4. theorem OAI.KadisonKastler.tomitaGraphRoot_state line 75
  5. theorem OAI.KadisonKastler.tomitaPolarConjugation_fixes_vector line 79