FiniteGroupAverage.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite averaging gives the equivariant bimodule mean needed by quadratic correction, for every C-star algebra of values.

def OAI.KadisonKastler.finiteGroupAverage line 20
Source documentation
Normalized counting average on bounded functions.
```
def finiteGroupAverage : (G →ᵇ B) →L[ℂ] B :=
…
```
theorem OAI.KadisonKastler.finiteGroupAverage_apply line 25
theorem OAI.KadisonKastler.finiteGroupAverage_norm_le line 30
theorem OAI.KadisonKastler.finiteGroupAverage_const line 44
theorem OAI.KadisonKastler.finiteGroupAverage_star line 53
theorem OAI.KadisonKastler.finiteGroupAverage_left line 59
theorem OAI.KadisonKastler.finiteGroupAverage_right line 65
theorem OAI.KadisonKastler.finiteGroupAverage_translate line 71
Source documentation
Normalized counting measure is invariant under left translation.
```
theorem finiteGroupAverage_translate (g : G) (f : G →ᵇ B) :
    finiteGroupAverage (boundaryTranslate (1 : G →* (B ≃⋆ₐ[ℂ] B)) g f) =
      finiteGroupAverage f := by
…
```
Mentions: OAI.KadisonKastler.finiteGroupAverage, OAI.KadisonKastler.boundaryTranslate
def OAI.KadisonKastler.finiteGroupBimoduleMean line 80
Source documentation
The finite-group mean, with both module identities.
```
def finiteGroupBimoduleMean : BimoduleMean (boundaryConstant (G := G) (B := B)) where
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant