OAI/Analysis/KadisonKastler/RelativeBicentralizerGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bicentralizer projection gaps in the matrix relative algebra

The residual vector is approximated only in the central-vector space. The original positive cone supplies the relative state-to-vector bound.

  1. theorem OAI.KadisonKastler.exists_relative_unitary_residual_gap line 25
  2. theorem OAI.KadisonKastler.exists_relative_projection_residual_gap line 55