OAI/Analysis/KadisonKastler/StandardFiniteIsomorphism.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-factor isomorphism in common tracial position

All boundary fields are constructed from the actual Kadison--Kastler approximants. Only the scalar boundary means and their double-ergodicity property, together with the precisely stated Tomiyama input, are supplied.

  1. theorem OAI.KadisonKastler.exists_standard_finiteFactor_isomorphism line 30

    Source documentation

    Common standard position and the 768b conjugation estimate produce an actual star isomorphism with displacement at most 378b.

    theorem exists_standard_finiteFactor_isomorphism
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (hΩ : pM.vector = pN.vector)
    (α : NonsingularAction G D μ) (m : ScalarBoundaryMean α) (m₂ : ScalarBoundaryMean α.prod)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama