OAI/Analysis/KadisonKastler/BicentralizerHilbertProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The bicentralizer retraction on the faithful Hilbert-space vector

It agrees with the orthogonal projection onto the bicentralizer orbit. In particular it is contractive for the reference-vector norm as well as the operator norm.

  1. theorem OAI.KadisonKastler.bicentralizerProjection_vector_eq line 21
  2. theorem OAI.KadisonKastler.bicentralizerProjection_vector_norm_le line 50