OAI/Analysis/KadisonKastler/ExpectedFromRefinement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The expected-subfactor construction from one-vector refinement

This is the closing construction in Haagerup's Lemma 3.8: finite tests, a summable increasing sequence, the central line, and the support corner. The local one-vector refinement hypothesis is kept explicit here; proving it from the absorbing type III₁ hypotheses remains a separate step.

  1. theorem OAI.KadisonKastler.scalarStage_centralProjection line 24
  2. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_local_refinement line 34