OAI/Analysis/KadisonKastler/TomitaMiddleCore.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded middle operator on the algebra and commutant cores

The product of the complementary graph roots replaces the unbounded modular square root in the operator identities used below.

  1. def OAI.KadisonKastler.tomitaMiddleOperator line 20
  2. theorem OAI.KadisonKastler.tomitaMiddleOperator_selfAdjoint line 23
  3. theorem OAI.KadisonKastler.tomitaMiddleOperator_polar line 30
  4. theorem OAI.KadisonKastler.tomitaMiddleOperator_algebra line 40
  5. theorem OAI.KadisonKastler.tomitaMiddleOperator_commutant line 65