OAI/Analysis/KadisonKastler/TomitaLinearPolarCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Linear polar coordinates for the closed Tomita graph

  1. def OAI.KadisonKastler.tomitaLinearPolarUnitary line 18

    Source documentation

    The linear unitary part of the Tomita operator in the chosen conjugate coordinates.

    def tomitaLinearPolarUnitary : H ≃ₗᵢ[ℂ] H where
…
  2. theorem OAI.KadisonKastler.tomitaLinearPolarUnitary_apply line 29
  3. theorem OAI.KadisonKastler.tomitaLinearPolarUnitary_symm_apply line 32
  4. theorem OAI.KadisonKastler.tomitaGraphRoot_polar_symm line 36
  5. theorem OAI.KadisonKastler.tomitaGraphRoots_commute line 47

    Source documentation

    Both positive coordinates are functions of the same positive contraction.

    theorem tomitaGraphRoots_commute :
    Commute (tomitaGraphRoot (M := M) J Ω) (tomitaGraphComplementRoot (M := M) J Ω) := by
…

    Mentions: OAI.KadisonKastler.tomitaGraphRoot, OAI.KadisonKastler.tomitaGraphComplementRoot

  6. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_positive_graph_iff line 54