OperatorMeanEquivariance.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The nonsingular action and equivariant operator mean

def OAI.KadisonKastler.NonsingularAction.operatorEquiv line 25
Source documentation
Inverse pullback gives the boundary action on actual operator classes.
```
def operatorEquiv (g : G) :
    WeakOperatorField (H := H) μ ≃⋆ₐ[ℂ] WeakOperatorField (H := H) μ where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.NonsingularAction.operatorEquiv_apply line 49
def OAI.KadisonKastler.NonsingularAction.operatorAction line 53
Source documentation
The inverse pullbacks form a group action.
```
def operatorAction : G →* (WeakOperatorField (H := H) μ ≃⋆ₐ[ℂ] WeakOperatorField (H := H) μ) where
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.NonsingularAction.operatorAction_coefficient line 75
theorem OAI.KadisonKastler.NonsingularAction.operatorAction_constant line 83
theorem OAI.KadisonKastler.WeakOperatorField.coefficientFamily_translate line 93
Source documentation
Scalar coefficients intertwine the two simultaneous translations.
```
theorem coefficientFamily_translate (α : NonsingularAction G D μ) (g : G)
    (F : G →ᵇ WeakOperatorField (H := H) μ) (ξ η : H) :
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorMean_equivariant line 110
Source documentation
Equivariance of the operator mean follows from its scalar coefficient identity.
```
theorem operatorMean_equivariant (m : ScalarBoundaryMean α) (g : G)
    (F : G →ᵇ WeakOperatorField (H := H) μ) :
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_operator_cocycle line 121
Source documentation
The constructed equivariant mean now feeds the complete cocycle iteration.
```
theorem exists_operator_cocycle (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama