OAI/Analysis/KadisonKastler/BicentralizerProjectionGap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Projection residual gaps from a trivial bicentralizer

The weak hull, unitary gap and spectral projection cut are all constructed. The only hypothesis in this step is the scalar bicentralizer itself.

  1. theorem OAI.KadisonKastler.exists_projection_residual_gap_of_bicentralizer line 25