PublishedStandardIsomorphism.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Common-position isomorphism from the published scalar inputs

The countable group is constructed from trace-dense unitaries. The boundary, both scalar means, and double ergodicity are then supplied by PublishedBoundary. The only additional input is the family of constant- field specializations of Tomiyama's Theorem 1(2), Proceedings of the Japan Academy 33 (1957), 608--612, pp. 608--609.

def OAI.KadisonKastler.PublishedFieldTomiyamaFamily line 29
Source documentation
Tomiyama's same published theorem, specialized to every scalar field base and group used on the fixed represented Hilbert space.
```
def PublishedFieldTomiyamaFamily : Prop :=
…
```

theorem OAI.KadisonKastler.exists_standard_finiteFactor_isomorphism_of_published line 38

Source documentation

Published scalar hypotheses determine the group and boundary data for the standard-position theorem.

theorem exists_standard_finiteFactor_isomorphism_of_published
    (hBoundary : PublishedBoundary.{u}) (hTom : PublishedFieldTomiyamaFamily H)
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (hΩ : pM.vector = pN.vector)
    {b : ℝ} (hb : b < 1 / 100000) (hgap : kkDistance M N < b)
    (hJ : ‖(pM.conjugation : H →L⋆[ℂ] H) -
      (pN.conjugation : H →L⋆[ℂ] H)‖ ≤ 768 * b) :
    ∃ θ : Algebra M ≃⋆ₐ[ℂ] Algebra N,
      ∀ x, ‖(θ x : H →L[ℂ] H) - (x : H →L[ℂ] H)‖ ≤ 378 * b * ‖x‖ := by
…

Mentions: OAI.KadisonKastler.PublishedFieldTomiyamaFamily, OAI.Generator.IsII1Factor, OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra