OAI/Analysis/KadisonKastler/MatrixProjectionCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A spectral cut supplies the matrix central-vector contraction

A matrix subalgebra containing the cut lies inside its diagonal central-vector space. The exact discarded-energy identity therefore gives the contraction estimate used in Haagerup's Lemma 3.6.

  1. theorem OAI.KadisonKastler.matrixStageCentralProjection_contraction line 23
  2. theorem OAI.KadisonKastler.centralProjection_displacement_le_of_central_vector line 43