OAI/Analysis/KadisonKastler/RemoteScalingSequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strongly central sequences of scaling coisometries

The copies commute exactly with increasingly many sites. The state-scaling identity controls multiplication on the product vector, and its separating property extends convergence to every vector in the represented Hilbert space.

  1. theorem OAI.KadisonKastler.PointedMatrixSites.remoteCopy_commutator_tendsto line 29
  2. theorem OAI.KadisonKastler.PointedMatrixSites.exists_remote_scaling_sequence line 68