OAI/Analysis/KadisonKastler/SpatialLocalScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Remote scaling in an arbitrary spatial product

Finite matrix stages are used only in the second leg. The first algebra is arbitrary and retains its original cyclic separating representation.

  1. def OAI.KadisonKastler.spatialRightAlgebraHom line 25
  2. theorem OAI.KadisonKastler.spatialMatrix_commutes_right line 30
  3. theorem OAI.KadisonKastler.PointedMatrixSites.spatialMatrix_reference_approximation line 53
  4. theorem OAI.KadisonKastler.PointedMatrixSites.spatial_remote_commutator_tendsto line 76
  5. theorem OAI.KadisonKastler.PointedMatrixSites.spatial_remote_adjoint_commutator_tendsto line 102