SeparableModelConstruction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The separable central model is constructed from the represented algebra. All norm, density and factor-fiber properties are proved.

theorem OAI.KadisonSimilarity.exists_publishedSeparableModel line 23
Source documentation
Construct the central factor decomposition needed by the manuscript's separable estimate, including possible zero fibers.
```
theorem exists_publishedSeparableModel (P : VonNeumannAlgebra H) :
    Nonempty (PublishedSeparableModel P) := by
…
```
Mentions: OAI.KadisonSimilarity.PublishedSeparableModel
theorem OAI.KadisonSimilarity.publishedUniformInputs line 80
Source documentation
Every separable represented von Neumann algebra admits the central factor decomposition used in the uniform commutator estimate.
```
theorem publishedUniformInputs : PublishedUniformInputs.{u} :=
…
```