OAI/Analysis/KadisonKastler/RelativeRankMatrixState.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Prescribed-rank positive states inside a matrix relative commutant

The comparison matrix stays in the relative algebra. Averaging over its product with the initial matrix algebra produces a faithful positive vector central for both algebras on the original Hilbert space.

  1. theorem OAI.KadisonKastler.rank_projection_weight line 24
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_positive_matrix_state_near_weight line 57