OAI/Analysis/KadisonKastler/ModularPairingOperator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded operator equation for modular averaging

This is the application-sized form of Rieffel--Van Daele, Lemma 4.5. All operators and algebra representatives are constructed in the original representation. Our graph resolvent is one half of their operator R.

  1. theorem OAI.KadisonKastler.modular_pairing_operator line 23