OAI/Analysis/KadisonKastler/ScaledCentralProjectionCut.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Projection cuts for unnormalized central vectors

The reference vector may be a finite-matrix central projection of a unit vector, and the test vector may be any nonzero residual. The fixed gap therefore scales with the squared norm of the residual.

  1. theorem OAI.KadisonKastler.exists_scaled_projection_gap_of_central_defect line 21