OAI/Analysis/KadisonKastler/MatrixStateHomogeneity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nearby matrix-central states from the exact homogeneity input

This constructs the state approximation in Haagerup's Lemma3.6 from Connes--Størmer homogeneity. The finite matrix algebra and its positive vector are constructed. The homogeneity input remains explicit and is not discharged by this adapter.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_nearby_positive_matrix_central_state line 28