OAI/Analysis/KadisonKastler/CyclicSpatialDerivation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial implementation in the initial irreducible representation

The proved cyclic column estimate and completely bounded factorization implement a bounded derivation in a cyclic representation. Taking the real part gives the self-adjoint implementer used in Sakai's quotient argument.

  1. theorem OAI.KadisonKastler.cyclic_spatial_derivation line 23
  2. theorem OAI.KadisonKastler.selfAdjoint_spatial_implementer line 47
  3. theorem OAI.KadisonKastler.exists_simple_spatial_derivation line 76