OAI/Analysis/KadisonKastler/ExpectedFromCentralTests.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From finite central-vector tests to the expected subfactor

Uniform displacement below one keeps the strong-limit vector nonzero. Vanishing errors on a dense sequence force the central line. Normalization and the support transfer then give all expected-subfactor data.

  1. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_central_tests line 24