OAI/Analysis/KadisonKastler/RelativeMatrixStateHomogeneity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Faithful matrix-state approximation in a relative algebra

The matrix comparison is performed in the relative algebra, while positivity, faithfulness and the central-vector conditions stay on the original space. Connes–Størmer homogeneity remains an explicit input.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_nearby_positive_matrix_central_state line 26