OAI/Analysis/KadisonKastler/ProductBoundaryIntertwiner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The measurable product intertwiner in common tracial position

  1. theorem OAI.KadisonKastler.exists_product_boundary_intertwiner line 22

    Source documentation

    The two commuting boundary actions have a measurable unitary intertwiner close to the identity, using the actual product mean.

    theorem exists_product_boundary_intertwiner
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (α : NonsingularAction G D μ) (m₂ : ScalarBoundaryMean α.prod)
    (hTom : PublishedFieldTomiyama (G := G × G) (H := H) (μ := μ.prod μ))
…

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