MeasurableBoundaryIntertwiner.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable representatives of the averaged boundary intertwiner

The operator-field mean and polar normalization construct the intertwiner in the quotient algebra. The null ideal then gives the exact measurable operator identity needed by the finite-factor argument.

def OAI.KadisonKastler.constantFieldRepresentation line 26
Source documentation
A constant operator representation in the actual field quotient.
```
def constantFieldRepresentation (U : G →* unitary (H →L[ℂ] H)) :
    G →* unitary (WeakOperatorField (H := H) μ) :=
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.constantFieldRepresentation_coe line 33
theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_measurable_boundary_intertwiner line 41
Source documentation
The averaged polar intertwiner has measurable everywhere-unitary values, the same norm bound, and the exact covariance almost everywhere.
```
theorem exists_measurable_boundary_intertwiner
    {α : NonsingularAction G D μ} (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama