OAI/Analysis/KadisonKastler/TomitaRootDomain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The domain of the closed Tomita operator

The polar graph coordinates parametrize the full closed graph, not only its algebraic core. Thus the first coordinate has exactly the range of the positive graph square root as its domain.

  1. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_root_graph line 23
  2. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_graph_iff line 41
  3. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_domain_eq_range line 62
  4. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_root_mem line 76
  5. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_apply_root line 80