OAI/Analysis/KadisonKastler/RestrictedMeasurableCocycle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable cocycle correction with values in a von Neumann algebra

  1. theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_measurable_correction_in line 26

    Source documentation

    The scalar boundary mean corrects an M-valued approximate cocycle to an actual measurable unitary cocycle whose values remain in M.

    theorem exists_measurable_correction_in (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…

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