SubalgebraInvariantMean.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Restricting an invariant operator mean to a von Neumann algebra

The coefficient construction preserves every von Neumann algebra. Restricting its domain and codomain therefore gives the exact mean for internal unitary correction, without a normality or injectivity assumption on the target.

def OAI.KadisonKastler.ambientAlgebraFamily line 26
Source documentation
Pointwise inclusion of bounded algebra-valued families.
```
def ambientAlgebraFamily (N : VonNeumannAlgebra H) :
    (G →ᵇ Algebra N) →⋆ₐ[ℂ] (G →ᵇ (H →L[ℂ] H)) where
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.ambientAlgebraFamily_apply line 39
theorem OAI.KadisonKastler.norm_ambientAlgebraFamily_le line 43
def OAI.KadisonKastler.ScalarInvariantMean.algebraMean line 52
Source documentation
The actual algebra-valued mean.
```
def algebraMean : (G →ᵇ Algebra N) →L[ℂ] Algebra N :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_coe line 72
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_norm_le line 75
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_const line 78
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_star line 83
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_left line 91
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_right line 96
def OAI.KadisonKastler.ScalarInvariantMean.algebraBimoduleMean line 102
Source documentation
The algebra-valued mean satisfies the two module identities.
```
def algebraBimoduleMean : BimoduleMean (boundaryConstant (G := G) (B := Algebra N)) where
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.ScalarInvariantMean.algebraMean_translate line 111
Source documentation
Translation invariance survives restriction to the algebra.
```
theorem algebraMean_translate (g : G) (F : G →ᵇ Algebra N) :
    m.algebraMean N (boundaryTranslate (1 : G →* (Algebra N ≃⋆ₐ[ℂ] Algebra N)) g F) =
      m.algebraMean N F := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.boundaryTranslate