OAI/Analysis/KadisonKastler/LocalScalingCentrality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong centrality from local commutation and state scaling

The local algebras may contain an arbitrary first tensor factor; only their density on the reference vector is used.

  1. theorem OAI.KadisonKastler.local_scaling_commutator_tendsto line 21
  2. theorem OAI.KadisonKastler.local_scaling_adjoint_commutator_tendsto line 54