RootBoundaryMeanConstruction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar boundary mean from rooted shift averages

Selection at the root is equivariant because the root translates by left multiplication. The positive invariant projection then descends the averages to the invariant boundary, with the exact module and action identities required by ScalarBoundaryMean.

theorem OAI.KadisonKastler.scalarBoundaryRootL_module line 27
theorem OAI.KadisonKastler.scalarBoundaryRootL_translate line 42
def OAI.KadisonKastler.rootedScalarBoundaryMean line 59
def OAI.KadisonKastler.randomWalkScalarBoundaryMean line 100
Source documentation
The original action of the countable group on its random-walk boundary has the exact scalar mean needed by the stability argument.
```
def randomWalkScalarBoundaryMean : ScalarBoundaryMean (randomWalkBoundaryAction G) :=
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.randomWalkBoundaryAction