OAI/Analysis/KadisonKastler/BicentralizerStrongContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the bicentralizer retraction on bounded nets

The reference-vector projection estimate and the dense commutant orbit extend convergence to every vector in the original representation.

  1. theorem OAI.KadisonKastler.bicentralizerProjection_strong_tendsto line 21