OAI/Analysis/KadisonKastler/PrescribedMatrixState.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Faithful positive matrix states with a prescribed projection weight

Rational matrix ranks approximate any weight strictly between zero and one. This constructs the comparison state used in the local homogeneity step; proximity of the two whole states is a separate requirement.

  1. theorem OAI.KadisonKastler.exists_positive_rank_ratio_near line 21
  2. theorem OAI.KadisonKastler.matrixCentralVector_inner_entry line 56
  3. theorem OAI.KadisonKastler.TypeIIIFactor.exists_positive_matrix_state_near_projection_weight line 77