RestrictedOperatorMean.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Equivariant averaging within a von Neumann algebra

The constant-commutant description of the field algebra is invariant under boundary pullback. Restricting the constructed mean therefore keeps both the cocycle and its correction in the prescribed von Neumann algebra.

theorem OAI.KadisonKastler.NonsingularAction.operatorAction_mem line 32
Source documentation
Boundary pullback preserves the algebra of fields with values in M.
```
theorem operatorAction_mem (g : G) (q : WeakOperatorField (H := H) μ)
…
```
Mentions: OAI.KadisonKastler.WeakOperatorField
def OAI.KadisonKastler.NonsingularAction.restrictedOperatorEquiv line 42
Source documentation
The boundary automorphism restricted to the M-valued field algebra.
```
def restrictedOperatorEquiv (g : G) :
    operatorFieldAlgebra (μ := μ) M ≃⋆ₐ[ℂ] operatorFieldAlgebra (μ := μ) M where
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra
def OAI.KadisonKastler.NonsingularAction.restrictedOperatorAction line 61
Source documentation
The restricted automorphisms form a group action.
```
def restrictedOperatorAction :
    G →* (operatorFieldAlgebra (μ := μ) M ≃⋆ₐ[ℂ] operatorFieldAlgebra (μ := μ) M) where
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.NonsingularAction.restrictedOperatorAction_coe line 80
instance OAI.KadisonKastler.restrictedOperatorFamilyCStar line 88
def OAI.KadisonKastler.operatorFieldFamilyInclusion line 92
Source documentation
The inclusion of bounded M-valued field families into all field families.
```
def operatorFieldFamilyInclusion : (G →ᵇ operatorFieldAlgebra (μ := μ) M) →⋆ₐ[ℂ]
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.operatorFieldFamilyInclusion_apply line 105
theorem OAI.KadisonKastler.norm_operatorFieldFamilyInclusion_le line 109
theorem OAI.KadisonKastler.operatorFieldFamilyInclusion_constant line 114
def OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMeanValue line 126
Source documentation
The restricted mean value, with its range proof separated from linearity.
```
def restrictedOperatorMeanValue (M : VonNeumannAlgebra H)
    (F : G →ᵇ operatorFieldAlgebra (μ := μ) M) : operatorFieldAlgebra (μ := μ) M :=
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMeanValue_coe line 133
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMeanValue_add line 138
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMeanValue_smul line 154
theorem OAI.KadisonKastler.ScalarBoundaryMean.norm_restrictedOperatorMeanValue_le line 167
def OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean line 174
Source documentation
Restrict the scalar-coefficient operator mean to M-valued fields.
```
def restrictedOperatorMean (M : VonNeumannAlgebra H) :
    (G →ᵇ operatorFieldAlgebra (μ := μ) M) →L[ℂ] operatorFieldAlgebra (μ := μ) M :=
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_coe line 185
theorem OAI.KadisonKastler.ScalarBoundaryMean.norm_restrictedOperatorMean_le line 190
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_one line 195
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_star line 203
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_left line 214
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_right line 230
def OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorBimoduleMean line 247
Source documentation
The restricted mean retains the two module identities.
```
def restrictedOperatorBimoduleMean (M : VonNeumannAlgebra H) :
    BimoduleMean (boundaryConstant (G := G) (B := operatorFieldAlgebra (μ := μ) M)) where
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant, OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.ScalarBoundaryMean.operatorFieldFamilyInclusion_translate line 257
theorem OAI.KadisonKastler.ScalarBoundaryMean.restrictedOperatorMean_equivariant line 264
theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_restricted_operator_cocycle line 278
Source documentation
The exact cocycle correction remains in the prescribed field algebra.
```
theorem exists_restricted_operator_cocycle (M : VonNeumannAlgebra H)
    (V : unitary (G →ᵇ operatorFieldAlgebra (μ := μ) M))
…
```
Mentions: OAI.KadisonKastler.operatorFieldAlgebra