OAI/Analysis/KadisonKastler/StandardBoundaryIsomorphism.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the boundary variables in common standard position

The product intertwiner, trace-diagonal comparison and double ergodicity give an actual near-identity star isomorphism. The scalar invariant-vector condition and the right-action identities are proved from standard position.

  1. theorem OAI.KadisonKastler.exists_standard_starEquiv_of_boundary_cocycle line 30

    Source documentation

    A close algebra-valued measurable cocycle yields a nearby star isomorphism, with constant 18δ.

    theorem exists_standard_starEquiv_of_boundary_cocycle
    (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 α.prod)
    (hTom : PublishedFieldTomiyama (G := G × G) (H := H) (μ := μ.prod μ))
…

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