OAI/Analysis/KadisonKastler/RelativeUnitaryStateDefect.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

State commutator bounds in a finite-matrix relative commutant

The relative Powers–Størmer estimate supplies the unitary defect bound on the central-vector space, without treating the relative algebra as cyclic on the full ambient Hilbert space.

  1. theorem OAI.KadisonKastler.relative_conjugation_mem_commutant line 27
  2. theorem OAI.KadisonKastler.relative_modularQuadratic_mem_central line 38
  3. theorem OAI.KadisonKastler.relative_centralVectorDefect_unitary_sq_le_stateCommutator line 49