FiniteFactorApplication.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform strong stability of separably acting II₁ factors

Boundary means, field projections and finite type stability combine with a common tracial position and uniform amplification to give a small spatial implementation.

structure OAI.KadisonKastler.FiniteFactorPublishedInputs line 35
Source documentation
The published specializations used for the finite-factor application. Each field refers to a separately documented published input.
```
structure FiniteFactorPublishedInputs : Prop where
…
```

theorem OAI.KadisonKastler.finiteFactor_spatial_of_published line 47

Source documentation

The neighbor need not be given as a finite factor, and the original representation need not have a tracial vector.

theorem finiteFactor_spatial_of_published (h : FiniteFactorPublishedInputs.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    {t : ℝ} (ht : 0 < t) (_htEmbed : t < 1 / 100)
    (htPosition : 302 * t < 174 / 1000000000000000)
    (hgap : kkDistance M N < t)
    (htStandard : 3 * 50948 * Real.sqrt (302 * t) < 1 / 100000)
    (htSpatial : commonPositionError (302 * t) < 1 / 4000000) :
    ∃ u : unitary (H →L[ℂ] H), Conjugates u M N ∧
      ‖(u : H →L[ℂ] H) - 1‖ ≤ constructedFiniteFactorError t := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.commonPositionError, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.constructedFiniteFactorError

theorem OAI.KadisonKastler.uniform_II1_strong_stability line 65

Source documentation

The tolerance is uniform in the factors, their representations and the separable ambient Hilbert space. This is the finite-factor part of the paper.

theorem uniform_II1_strong_stability (h : FiniteFactorPublishedInputs.{u})
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
      (M N : VonNeumannAlgebra H), Generator.IsII1Factor M.toStarSubalgebra →
      kkDistance M N < δ → NearConjugacy M N ε := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.NearConjugacy