OAI/Analysis/KadisonKastler/ModularPositiveSymmetry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Inverse and group symmetries of the positive modular operator

All identities concern the full closed graph. The inverse is densely defined, and polar conjugation exchanges its two coordinates.

  1. theorem OAI.KadisonKastler.modularPositiveOperator_ker line 21
  2. theorem OAI.KadisonKastler.tomitaGraphComplementRoot_dense line 33
  3. theorem OAI.KadisonKastler.modularPositiveOperator_range line 45
  4. theorem OAI.KadisonKastler.modularPositiveOperator_denseRange line 59
  5. theorem OAI.KadisonKastler.modularPositiveOperator_inverse_graph_iff line 65
  6. theorem OAI.KadisonKastler.modularPositiveOperator_conjugate_inverse_graph line 73

    Source documentation

    The polar conjugation sends the positive graph to its inverse graph.

    theorem modularPositiveOperator_conjugate_inverse_graph (x y : H) :
    (tomitaPolarConjugation J Ω hsep hcyc x, tomitaPolarConjugation J Ω hsep hcyc y) ∈
      (modularPositiveOperator J Ω hsep hcyc).inverse.graph ↔
    (x, y) ∈ (modularPositiveOperator J Ω hsep hcyc).graph := by
…

    Mentions: OAI.KadisonKastler.tomitaPolarConjugation, OAI.KadisonKastler.modularPositiveOperator

  7. theorem OAI.KadisonKastler.tomitaGraphComplementRoot_group_apply line 93
  8. theorem OAI.KadisonKastler.modularPositiveOperator_group_graph line 106
  9. theorem OAI.KadisonKastler.modularPositiveOperator_group_domain line 116