OAI/Analysis/KadisonKastler/MatrixStatePreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

State approximation by a finite matrix centralizer

Two-sided vector pinching centralizes an almost-central projection. The constructed matrix state then differs from the original vector state by at most the requested error plus four times the projection gap. Connes--Størmer homogeneity is retained as its exact explicit input.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrix_state_of_projection_gap line 25