FiniteFactorStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

First move a constructed injective subfactor into the neighbor, then apply common-position stability, and compose the two actual ambient unitaries.

def OAI.KadisonKastler.finiteFactorError line 40
Source documentation
The total displacement, including the initial injective embedding.
```
def finiteFactorError (t : ℝ) : ℝ := 150 * t + 2400 * commonPositionError (302 * t)
```
Mentions: OAI.KadisonKastler.commonPositionError
theorem OAI.KadisonKastler.finiteFactor_spatial_of_injective_subfactor line 43
Source documentation
An irreducible injective subfactor need not already belong to the neighbor.
```
theorem finiteFactor_spatial_of_injective_subfactor
    (hEmbedding : PublishedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding
theorem OAI.KadisonKastler.finiteFactor_spatial_in_tracial_representation line 87
Source documentation
The matrix construction supplies the required subfactor in a tracial representation; its injectivity is the stated published AFD implication.
```
theorem finiteFactor_spatial_in_tracial_representation
    (hMatrix : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity