CommonPositionSpatial.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial stability after a common injective subfactor is fixed

The published change of representation, the constructed boundary isomorphism and the actual paired-factor amplification are joined here. The unitary acts on the original Hilbert space.

def OAI.KadisonKastler.commonPositionError line 40
Source documentation
Explicit common-position error after returning to the original space.
```
def commonPositionError (g : ℝ) : ℝ := 1135 * 50948 * Real.sqrt g + 2 * g
```

theorem OAI.KadisonKastler.common_subfactor_spatial_stability line 44

Source documentation

Nearby II₁ factors with a common irreducible injective subalgebra are conjugate on the original space, with an explicit square-root bound.

theorem common_subfactor_spatial_stability
    (hPosition : PublishedCommonTracialPosition.{u})
    (hBoundary : PublishedBoundary.{u})
    (hTom : ∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K] [TopologicalSpace.SeparableSpace K], PublishedFieldTomiyamaFamily K)
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hFock : PublishedDiagonalFockRepresentation.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (hCyclic : ∀ θ : Algebra M ≃⋆ₐ[ℂ] Algebra N,
…

Mentions: OAI.KadisonKastler.PublishedFieldTomiyamaFamily, OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra